amistd_1.miz



    begin

    reserve x for set,

D for non empty set,

k,n for Nat,

z for Nat;

    reserve N for with_zero set,

S for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,

i for Element of the InstructionsF of S,

l,l1,l2,l3 for Nat,

s for State of S;

    registration

      let N be with_zero set, S be with_non-empty_values AMI-Struct over N, i be Element of the InstructionsF of S, s be State of S;

      cluster ((the Execution of S . i) . s) -> Function-like Relation-like;

      coherence

      proof

        reconsider A = (the Execution of S . i) as Function of ( product ( the_Values_of S)), ( product ( the_Values_of S)) by FUNCT_2: 66;

        reconsider s as Element of ( product ( the_Values_of S)) by CARD_3: 107;

        (A . s) in ( product ( the_Values_of S));

        hence thesis;

      end;

    end

    registration

      let N;

      cluster non empty with_non-empty_values for AMI-Struct over N;

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    definition

      let N be with_zero set;

      let S be non empty with_non-empty_values AMI-Struct over N;

      let T be InsType of the InstructionsF of S;

      :: AMISTD_1:def1

      attr T is jump-only means for s be State of S, o be Object of S, I be Instruction of S st ( InsCode I) = T & o in ( Data-Locations S) holds (( Exec (I,s)) . o) = (s . o);

    end

    definition

      let N be with_zero set;

      let S be non empty with_non-empty_values AMI-Struct over N;

      let I be Instruction of S;

      :: AMISTD_1:def2

      attr I is jump-only means ( InsCode I) is jump-only;

    end

    reserve ss for Element of ( product ( the_Values_of S));

    definition

      let N, S;

      let l be Nat;

      let i be Element of the InstructionsF of S;

      :: AMISTD_1:def3

      func NIC (i,l) -> Subset of NAT equals { ( IC ( Exec (i,ss))) : ( IC ss) = l };

      coherence

      proof

        { ( IC ( Exec (i,ss))) : ( IC ss) = l } c= NAT

        proof

          let e be object;

          assume e in { ( IC ( Exec (i,ss))) : ( IC ss) = l };

          then ex ss st e = ( IC ( Exec (i,ss))) & ( IC ss) = l;

          hence thesis;

        end;

        hence thesis;

      end;

    end

     Lm1:

    now

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Element of the InstructionsF of S, l be Nat, s be State of S, P be Instruction-Sequence of S;

      reconsider t = (s +* (( IC S),l)) as Element of ( product ( the_Values_of S)) by CARD_3: 107;

      l in NAT by ORDINAL1:def 12;

      then

       A1: l in ( dom P) by PARTFUN1:def 2;

      ( IC S) in ( dom s) by MEMSTR_0: 2;

      then

       A2: ( IC t) = l by FUNCT_7: 31;

      

      then ( CurInstr ((P +* (l,i)),t)) = ((P +* (l,i)) . l) by PBOOLE: 143

      .= i by A1, FUNCT_7: 31;

      hence ( IC ( Following ((P +* (l,i)),(s +* (( IC S),l))))) in ( NIC (i,l)) by A2;

    end;

    registration

      let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Element of the InstructionsF of S, l be Nat;

      cluster ( NIC (i,l)) -> non empty;

      coherence by Lm1;

    end

    definition

      let N, S, i;

      :: AMISTD_1:def4

      func JUMP i -> Subset of NAT equals ( meet the set of all ( NIC (i,l)));

      coherence

      proof

        set X = the set of all ( NIC (i,l));

        X c= ( bool NAT )

        proof

          let x be object;

          assume x in X;

          then ex l st x = ( NIC (i,l));

          hence thesis;

        end;

        then

        reconsider X as Subset-Family of NAT ;

        ( meet X) c= NAT ;

        hence thesis;

      end;

    end

    definition

      let N, S;

      let l be Nat;

      :: AMISTD_1:def5

      func SUCC (l,S) -> Subset of NAT equals ( union the set of all (( NIC (i,l)) \ ( JUMP i)));

      coherence

      proof

        set X = the set of all (( NIC (i,l)) \ ( JUMP i));

        X c= ( bool NAT )

        proof

          let x be object;

          assume x in X;

          then ex i st x = (( NIC (i,l)) \ ( JUMP i));

          hence thesis;

        end;

        then

        reconsider X as Subset-Family of NAT ;

        ( union X) c= NAT ;

        hence thesis;

      end;

    end

    theorem :: AMISTD_1:1

    

     Th1: for i be Element of the InstructionsF of S st for l be Nat holds ( NIC (i,l)) = {l} holds ( JUMP i) is empty

    proof

      let i be Element of the InstructionsF of S;

      set p = 0 , q = 1;

      set X = the set of all ( NIC (i,l)) where l be Nat;

      reconsider p, q as Nat;

      assume

       A1: for l be Nat holds ( NIC (i,l)) = {l};

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);

      ( NIC (i,p)) = {p} by A1;

      then {p} in X;

      then

       A3: x in {p} by A2, SETFAM_1:def 1;

      ( NIC (i,q)) = {q} by A1;

      then {q} in X;

      then x in {q} by A2, SETFAM_1:def 1;

      hence contradiction by A3, TARSKI:def 1;

    end;

    theorem :: AMISTD_1:2

    

     Th2: for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il be Nat, i be Instruction of S st i is halting holds ( NIC (i,il)) = {il}

    proof

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il be Nat, i be Instruction of S such that

       A1: for s be State of S holds ( Exec (i,s)) = s;

      hereby

        let n be object;

        assume n in ( NIC (i,il));

        then ex s be Element of ( product ( the_Values_of S)) st n = ( IC ( Exec (i,s))) & ( IC s) = il;

        then n = il by A1;

        hence n in {il} by TARSKI:def 1;

      end;

      set s = the State of S, P = the Instruction-Sequence of S;

      let n be object;

      assume n in {il};

      then

       A2: n = il by TARSKI:def 1;

      il in NAT by ORDINAL1:def 12;

      then

       A3: il in ( dom P) by PARTFUN1:def 2;

      

       A4: ( IC S) in ( dom s) by MEMSTR_0: 2;

      then ( IC (s +* (( IC S),il))) = il by FUNCT_7: 31;

      

      then ( CurInstr ((P +* (il,i)),(s +* (( IC S),il)))) = ((P +* (il,i)) . il) by PBOOLE: 143

      .= i by A3, FUNCT_7: 31;

      

      then ( IC ( Following ((P +* (il,i)),(s +* (( IC S),il))))) = ( IC (s +* (( IC S),il))) by A1

      .= n by A2, A4, FUNCT_7: 31;

      hence n in ( NIC (i,il)) by Lm1;

    end;

    begin

    definition

      let N, S;

      :: AMISTD_1:def6

      attr S is standard means for m,n be Nat holds m <= n iff ex f be non empty FinSequence of NAT st (f /. 1) = m & (f /. ( len f)) = n & for n st 1 <= n & n < ( len f) holds (f /. (n + 1)) in ( SUCC ((f /. n),S));

    end

    

     Lm2: ex f be non empty FinSequence of NAT st (f /. 1) = k & (f /. ( len f)) = k & for n st 1 <= n & n < ( len f) holds (f /. (n + 1)) in ( SUCC ((f /. n),S))

    proof

      reconsider l = k as Element of NAT by ORDINAL1:def 12;

      reconsider f = <*l*> as non empty FinSequence of NAT ;

      take f;

      thus (f /. 1) = k by FINSEQ_4: 16;

      hence thesis by FINSEQ_1: 39;

    end;

    theorem :: AMISTD_1:3

    

     Th3: S is standard iff for k be Nat holds (k + 1) in ( SUCC (k,S)) & for j be Nat st j in ( SUCC (k,S)) holds k <= j

    proof

      hereby

        assume

         A1: S is standard;

        let k be Nat;

        k <= (k + 1) by NAT_1: 11;

        then

        consider F be non empty FinSequence of NAT such that

         A2: (F /. 1) = k and

         A3: (F /. ( len F)) = (k + 1) and

         A4: for n st 1 <= n & n < ( len F) holds (F /. (n + 1)) in ( SUCC ((F /. n),S)) by A1;

        set F1 = (F -| (k + 1));

        set x = ((k + 1) .. F);

        

         A5: (k + 1) in ( rng F) by A3, FINSEQ_6: 168;

        then

         A6: ( len F1) = (x - 1) by FINSEQ_4: 34;

        then

         A7: (( len F1) + 1) = x;

        

         A8: x in ( dom F) by A5, FINSEQ_4: 20;

        

        then

         A9: (F /. (( len F1) + 1)) = (F . x) by A6, PARTFUN1:def 6

        .= (k + 1) by A5, FINSEQ_4: 19;

        x <= ( len F) by A8, FINSEQ_3: 25;

        then

         A10: ( len F1) < ( len F) by A7, NAT_1: 13;

        1 <= ( len F) by NAT_1: 14;

        then

         A11: 1 in ( dom F) by FINSEQ_3: 25;

        then

         A12: (F /. 1) = (F . 1) by PARTFUN1:def 6;

        

         A13: (F . x) = (k + 1) by A5, FINSEQ_4: 19;

        

         A14: k <> (k + 1);

        then

         A15: ( len F1) <> 0 by A2, A13, A11, A6, PARTFUN1:def 6;

        1 <= x by A8, FINSEQ_3: 25;

        then 1 < x by A2, A14, A13, A12, XXREAL_0: 1;

        then

         A16: 1 <= ( len F1) by A7, NAT_1: 13;

        reconsider F1 as non empty FinSequence of NAT by A15, A5, FINSEQ_4: 41;

        set m = (F /. ( len F1));

        reconsider m as Nat;

        

         A17: ( len F1) in ( dom F) by A16, A10, FINSEQ_3: 25;

        

         A18: ( len F1) in ( dom F1) by A16, FINSEQ_3: 25;

        

        then

         A19: (F1 /. ( len F1)) = (F1 . ( len F1)) by PARTFUN1:def 6

        .= (F . ( len F1)) by A5, A18, FINSEQ_4: 36

        .= (F /. ( len F1)) by A17, PARTFUN1:def 6;

         A20:

        now

          ( rng F1) misses {(k + 1)} by A5, FINSEQ_4: 38;

          then (( rng F1) /\ {(k + 1)}) = {} ;

          then

           A21: not (k + 1) in ( rng F1) or not (k + 1) in {(k + 1)} by XBOOLE_0:def 4;

          assume

           A22: m = (k + 1);

          

           A23: ( len F1) in ( dom F1) by A16, FINSEQ_3: 25;

          then (F1 /. ( len F1)) = (F1 . ( len F1)) by PARTFUN1:def 6;

          hence contradiction by A19, A22, A21, A23, FUNCT_1:def 3, TARSKI:def 1;

        end;

        reconsider F2 = <*(F /. ( len F1)), (F /. x)*> as non empty FinSequence of NAT ;

        

         A24: ( len F2) = 2 by FINSEQ_1: 44;

        then

         A25: 2 in ( dom F2) by FINSEQ_3: 25;

        

        then

         A26: (F2 /. ( len F2)) = (F2 . 2) by A24, PARTFUN1:def 6

        .= (F /. x) by FINSEQ_1: 44

        .= (k + 1) by A13, A8, PARTFUN1:def 6;

        

         A27: 1 in ( dom F2) by A24, FINSEQ_3: 25;

         A28:

        now

          let n;

          assume 1 <= n & n < ( len F2);

          then n <> 0 & n < (1 + 1) by FINSEQ_1: 44;

          then n <> 0 & n <= 1 by NAT_1: 13;

          then

           A29: n = 1 by NAT_1: 25;

          

          then

           A30: (F2 /. n) = (F2 . 1) by A27, PARTFUN1:def 6

          .= (F /. ( len F1)) by FINSEQ_1: 44;

          (F2 /. (n + 1)) = (F2 . 2) by A25, A29, PARTFUN1:def 6

          .= (F /. (( len F1) + 1)) by A6, FINSEQ_1: 44;

          hence (F2 /. (n + 1)) in ( SUCC ((F2 /. n),S)) by A4, A16, A10, A30;

        end;

         A31:

        now

          let n;

          assume that

           A32: 1 <= n and

           A33: n < ( len F1);

          

           A34: 1 <= (n + 1) by A32, NAT_1: 13;

          

           A35: (n + 1) <= ( len F1) by A33, NAT_1: 13;

          then (n + 1) <= ( len F) by A10, XXREAL_0: 2;

          then

           A36: (n + 1) in ( dom F) by A34, FINSEQ_3: 25;

          n <= ( len F) by A10, A33, XXREAL_0: 2;

          then

           A37: n in ( dom F) by A32, FINSEQ_3: 25;

          

           A38: n in ( dom F1) by A32, A33, FINSEQ_3: 25;

          

          then

           A39: (F1 /. n) = (F1 . n) by PARTFUN1:def 6

          .= (F . n) by A5, A38, FINSEQ_4: 36

          .= (F /. n) by A37, PARTFUN1:def 6;

          

           A40: n < ( len F) by A10, A33, XXREAL_0: 2;

          

           A41: (n + 1) in ( dom F1) by A34, A35, FINSEQ_3: 25;

          

          then (F1 /. (n + 1)) = (F1 . (n + 1)) by PARTFUN1:def 6

          .= (F . (n + 1)) by A5, A41, FINSEQ_4: 36

          .= (F /. (n + 1)) by A36, PARTFUN1:def 6;

          hence (F1 /. (n + 1)) in ( SUCC ((F1 /. n),S)) by A4, A32, A39, A40;

        end;

        (F2 /. 1) = (F2 . 1) by A27, PARTFUN1:def 6

        .= m by FINSEQ_1: 44;

        then

         A42: m <= (k + 1) by A1, A26, A28;

        

         A43: 1 in ( dom F1) by A16, FINSEQ_3: 25;

        

        then (F1 /. 1) = (F1 . 1) by PARTFUN1:def 6

        .= (F . 1) by A5, A43, FINSEQ_4: 36

        .= k by A2, A11, PARTFUN1:def 6;

        then k <= m by A1, A19, A31;

        then m = k or m = (k + 1) by A42, NAT_1: 9;

        hence (k + 1) in ( SUCC (k,S)) by A4, A16, A10, A9, A20;

        let j be Nat;

        reconsider fk = k, fj = j as Element of NAT by ORDINAL1:def 12;

        reconsider F = <*fk, fj*> as non empty FinSequence of NAT ;

        

         A44: ( len F) = 2 by FINSEQ_1: 44;

        then

         A45: 2 in ( dom F) by FINSEQ_3: 25;

        

         A46: 1 in ( dom F) by A44, FINSEQ_3: 25;

        

        then

         A47: (F /. 1) = (F . 1) by PARTFUN1:def 6

        .= k by FINSEQ_1: 44;

        assume

         A48: j in ( SUCC (k,S));

         A49:

        now

          let n be Nat;

          assume 1 <= n & n < ( len F);

          then n <> 0 & n < (1 + 1) by FINSEQ_1: 44;

          then n <> 0 & n <= 1 by NAT_1: 13;

          then

           A50: n = 1 by NAT_1: 25;

          

          then

           A51: (F /. n) = (F . 1) by A46, PARTFUN1:def 6

          .= k by FINSEQ_1: 44;

          (F /. (n + 1)) = (F . 2) by A45, A50, PARTFUN1:def 6

          .= j by FINSEQ_1: 44;

          hence (F /. (n + 1)) in ( SUCC ((F /. n),S)) by A48, A51;

        end;

        (F /. ( len F)) = (F . 2) by A44, A45, PARTFUN1:def 6

        .= j by FINSEQ_1: 44;

        hence k <= j by A1, A47, A49;

      end;

      assume

       A52: for k be Nat holds (k + 1) in ( SUCC (k,S)) & for j be Nat st j in ( SUCC (k,S)) holds k <= j;

      thus S is standard

      proof

        let m,n be Nat;

        thus m <= n implies ex f be non empty FinSequence of NAT st (f /. 1) = m & (f /. ( len f)) = n & for k st 1 <= k & k < ( len f) holds (f /. (k + 1)) in ( SUCC ((f /. k),S))

        proof

          assume

           A53: m <= n;

          per cases by A53, XXREAL_0: 1;

            suppose m = n;

            hence ex f be non empty FinSequence of NAT st (f /. 1) = m & (f /. ( len f)) = n & for n st 1 <= n & n < ( len f) holds (f /. (n + 1)) in ( SUCC ((f /. n),S)) by Lm2;

          end;

            suppose

             A54: m < n;

            thus ex f be non empty FinSequence of NAT st (f /. 1) = m & (f /. ( len f)) = n & for n st 1 <= n & n < ( len f) holds (f /. (n + 1)) in ( SUCC ((f /. n),S))

            proof

              set mn = (n -' m);

              deffunc F( Nat) = ((m + $1) -' 1);

              consider F be FinSequence of NAT such that

               A55: ( len F) = (mn + 1) and

               A56: for j be Nat st j in ( dom F) holds (F . j) = F(j) from FINSEQ_2:sch 1;

              reconsider F as non empty FinSequence of NAT by A55;

              take F;

              

               A57: 1 <= (mn + 1) by NAT_1: 11;

              then

               A58: 1 in ( dom F) by A55, FINSEQ_3: 25;

              

              hence (F /. 1) = (F . 1) by PARTFUN1:def 6

              .= ((m + 1) -' 1) by A56, A58

              .= m by NAT_D: 34;

              (m + 1) <= n by A54, INT_1: 7;

              then 1 <= (n - m) by XREAL_1: 19;

              then 0 <= (n - m);

              then

               A59: mn = (n - m) by XREAL_0:def 2;

              

               A60: ( len F) in ( dom F) by A55, A57, FINSEQ_3: 25;

              

              hence (F /. ( len F)) = (F . ( len F)) by PARTFUN1:def 6

              .= ((m + (mn + 1)) -' 1) by A55, A56, A60

              .= (((m + mn) + 1) -' 1)

              .= n by A59, NAT_D: 34;

              let p be Nat;

              assume that

               A61: 1 <= p and

               A62: p < ( len F);

              

               A63: p in ( dom F) by A61, A62, FINSEQ_3: 25;

              

              then

               A64: (F /. p) = (F . p) by PARTFUN1:def 6

              .= ((m + p) -' 1) by A56, A63;

              

               A65: p <= (m + p) by NAT_1: 11;

              1 <= (p + 1) & (p + 1) <= ( len F) by A61, A62, NAT_1: 13;

              then

               A66: (p + 1) in ( dom F) by FINSEQ_3: 25;

              

              then (F /. (p + 1)) = (F . (p + 1)) by PARTFUN1:def 6

              .= ((m + (p + 1)) -' 1) by A56, A66

              .= (((m + p) + 1) -' 1)

              .= (((m + p) -' 1) + 1) by A61, A65, NAT_D: 38, XXREAL_0: 2;

              hence thesis by A52, A64;

            end;

          end;

        end;

        given F be non empty FinSequence of NAT such that

         A67: (F /. 1) = m and

         A68: (F /. ( len F)) = n and

         A69: for n be Nat st 1 <= n & n < ( len F) holds (F /. (n + 1)) in ( SUCC ((F /. n),S));

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len F) implies ex l be Nat st (F /. $1) = l & m <= l;

         A70:

        now

          let k be Nat such that

           A71: P[k];

          now

            assume that 1 <= (k + 1) and

             A72: (k + 1) <= ( len F);

            per cases ;

              suppose k = 0 ;

              hence ex l be Nat st (F /. (k + 1)) = l & m <= l by A67;

            end;

              suppose

               A73: k > 0 ;

              set l1 = (F /. (k + 1));

              consider l be Nat such that

               A74: (F /. k) = l and

               A75: m <= l by A71, A72, A73, NAT_1: 13, NAT_1: 14;

              reconsider l1 as Nat;

              k < ( len F) by A72, NAT_1: 13;

              then (F /. (k + 1)) in ( SUCC ((F /. k),S)) by A69, A73, NAT_1: 14;

              then l <= l1 by A52, A74;

              hence ex l be Nat st (F /. (k + 1)) = l & m <= l by A75, XXREAL_0: 2;

            end;

          end;

          hence P[(k + 1)];

        end;

        

         A76: 1 <= ( len F) by NAT_1: 14;

        

         A77: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A77, A70);

        then ex l be Nat st (F /. ( len F)) = l & m <= l by A76;

        hence thesis by A68;

      end;

    end;

    set III = { [1, {} , {} ], [ 0 , {} , {} ]};

    begin

    definition

      let N be with_zero set;

      :: AMISTD_1:def7

      func STC N -> strict AMI-Struct over N means

      : Def7: the carrier of it = { 0 } & ( IC it ) = 0 & the InstructionsF of it = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} & the Object-Kind of it = ( 0 .--> 0 ) & the ValuesF of it = (N --> NAT ) & ex f be Function of ( product ( the_Values_of it )), ( product ( the_Values_of it )) st (for s be Element of ( product ( the_Values_of it )) holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))) & the Execution of it = (( [1, 0 , 0 ] .--> f) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of it )))));

      existence

      proof

        set O = { 0 };

        set V = (N --> NAT );

        reconsider IC1 = 0 as Element of O by TARSKI:def 1;

        reconsider i = [ 0 , 0 , 0 ] as Element of III by TARSKI:def 2;

        

         A1: 0 in N by MEASURE6:def 2;

        then

         A2: (V * ( 0 .--> 0 )) = ( 0 .--> NAT ) by FUNCOP_1: 89;

        then

         A3: ( dom (V * ( 0 .--> 0 ))) = O;

        

         A4: ( dom ( 0 .--> 0 )) = O;

        ( rng ( 0 .--> 0 )) = { 0 } by FUNCOP_1: 88;

        then ( rng ( 0 .--> 0 )) c= N by A1, ZFMISC_1: 31;

        then

        reconsider Ok = ( 0 .--> 0 ) as Function of O, N by A4, RELSET_1: 4;

        deffunc F( Element of ( product (V * Ok))) = ($1 +* ( 0 .--> (( In (($1 . 0 ), NAT )) + 1)));

         A5:

        now

          let s be Element of ( product (V * Ok));

          now

            

            thus ( dom (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))) = (( dom s) \/ ( dom ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))) by FUNCT_4:def 1

            .= (( dom s) \/ { 0 })

            .= ( { 0 } \/ { 0 }) by PARTFUN1:def 2

            .= ( dom (V * Ok)) by A3;

            let o be object;

            

             A6: ( dom ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) = { 0 };

            assume

             A7: o in ( dom (V * Ok));

            

             A8: ((V * Ok) . o) = NAT by A7, A2, FUNCOP_1: 7;

            ((s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) . o) = (( 0 .--> (( In ((s . 0 ), NAT )) + 1)) . o) by A6, A7, FUNCT_4: 13

            .= (( In ((s . 0 ), NAT )) + 1) by A7, FUNCOP_1: 7;

            hence ((s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) . o) in ((V * Ok) . o) by A8;

          end;

          hence F(s) in ( product (V * Ok)) by CARD_3: 9;

        end;

        consider f be Function of ( product (V * Ok)), ( product (V * Ok)) such that

         A9: for s be Element of ( product (V * Ok)) holds (f . s) = F(s) from FUNCT_2:sch 8( A5);

        set E = (( [1, 0 , 0 ] .--> f) +* ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok)))));

        

         A10: ( dom E) = (( dom ( [1, 0 , 0 ] .--> f)) \/ ( dom ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok)))))) by FUNCT_4:def 1

        .= ( { [1, 0 , 0 ]} \/ ( dom ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok))))))

        .= ( { [1, 0 , 0 ]} \/ { [ 0 , 0 , 0 ]})

        .= III by ENUMSET1: 1;

        

         A11: ( rng ( [1, 0 , 0 ] .--> f)) c= {f} & ( rng ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok))))) c= {( id ( product (V * Ok)))} by FUNCOP_1: 13;

        

         A12: ( rng E) c= (( rng ( [1, 0 , 0 ] .--> f)) \/ ( rng ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok)))))) by FUNCT_4: 17;

        ( rng E) c= ( Funcs (( product (V * Ok)),( product (V * Ok))))

        proof

          let e be object;

          assume e in ( rng E);

          then e in ( rng ( [1, 0 , 0 ] .--> f)) or e in ( rng ( [ 0 , 0 , 0 ] .--> ( id ( product (V * Ok))))) by A12, XBOOLE_0:def 3;

          then e = f or e = ( id ( product (V * Ok))) by A11, TARSKI:def 1;

          hence thesis by FUNCT_2: 9;

        end;

        then

        reconsider E as Function of III, ( Funcs (( product (V * Ok)),( product (V * Ok)))) by A10, FUNCT_2:def 1, RELSET_1: 4;

        set V = (N --> NAT );

        set M = AMI-Struct (# O, IC1, III, Ok, V, E #);

        take M qua strict AMI-Struct over N;

        thus the carrier of M = { 0 };

        thus ( IC M) = 0 ;

        thus the InstructionsF of M = { [ 0 , 0 , 0 ], [1, 0 , 0 ]};

        thus the Object-Kind of M = ( 0 .--> 0 );

        thus the ValuesF of M = (N --> NAT );

        reconsider f as Function of ( product ( the_Values_of M)), ( product ( the_Values_of M));

        take f;

        thus for s be Element of ( product ( the_Values_of M)) holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) by A9;

        thus thesis;

      end;

      uniqueness

      proof

        let it1,it2 be strict AMI-Struct over N such that

         A13: the carrier of it1 = { 0 } & ( IC it1) = 0 & the InstructionsF of it1 = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} and

         A14: the Object-Kind of it1 = ( 0 .--> 0 ) and

         A15: the ValuesF of it1 = (N --> NAT );

        given f1 be Function of ( product ( the_Values_of it1)), ( product ( the_Values_of it1)) such that

         A16: for s be Element of ( product ( the_Values_of it1)) holds (f1 . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) and

         A17: the Execution of it1 = (( [1, 0 , 0 ] .--> f1) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of it1)))));

        assume that

         A18: the carrier of it2 = { 0 } & ( IC it2) = 0 & the InstructionsF of it2 = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} and

         A19: the Object-Kind of it2 = ( 0 .--> 0 ) and

         A20: the ValuesF of it2 = (N --> NAT );

        given f2 be Function of ( product ( the_Values_of it2)), ( product ( the_Values_of it2)) such that

         A21: for s be Element of ( product ( the_Values_of it2)) holds (f2 . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) and

         A22: the Execution of it2 = (( [1, 0 , 0 ] .--> f2) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of it2)))));

        

         A23: ( the_Values_of it1) = ( the_Values_of it2) by A14, A15, A19, A20;

        now

          let c be Element of ( product ( the_Values_of it1));

          

          thus (f1 . c) = (c +* ( 0 .--> (( In ((c . 0 ), NAT )) + 1))) by A16

          .= (f2 . c) by A21, A23;

        end;

        hence thesis by A13, A14, A17, A18, A19, A22, A15, A20, FUNCT_2: 63;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> finite non empty;

      coherence by Def7;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> with_non-empty_values;

      coherence

      proof

        let n be object;

        set S = ( STC N), F = ( the_Values_of S);

        assume

         A1: n in ( dom F);

        then

         A2: (the Object-Kind of S . n) in ( dom the ValuesF of S) by FUNCT_1: 11;

        

         A3: the ValuesF of S = (N --> NAT ) by Def7;

        

         A4: (the Object-Kind of S . n) in N by A2;

        (F . n) = (the ValuesF of S . (the Object-Kind of S . n)) by A1, FUNCT_1: 12

        .= NAT by A4, A3, FUNCOP_1: 7;

        hence (F . n) is non empty;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> IC-Ins-separated;

      coherence

      proof

        set IT = ( STC N);

        set Ok = ( the_Values_of IT);

        

         A1: 0 in { 0 } by TARSKI:def 1;

        

         A2: ( the_Values_of IT) = (the ValuesF of IT * the Object-Kind of IT)

        .= (the ValuesF of IT * ( 0 .--> 0 )) by Def7

        .= ((N --> NAT ) * ( 0 .--> 0 )) by Def7;

         0 in N by MEASURE6:def 2;

        

        then (Ok . 0 ) = (( 0 .--> NAT ) . 0 ) by A2, FUNCOP_1: 89

        .= NAT by A1, FUNCOP_1: 7;

        then ( Values ( IC IT)) = NAT by Def7;

        hence ( STC N) is IC-Ins-separated;

      end;

    end

    

     Lm3: for i be Instruction of ( STC N), s be State of ( STC N) st ( InsCode i) = 1 holds (( Exec (i,s)) . ( IC ( STC N))) = (( IC s) + 1)

    proof

      let i be Instruction of ( STC N), s be State of ( STC N);

      set M = ( STC N);

      assume

       A1: ( InsCode i) = 1;

       A2:

      now

        assume i in { [ 0 , 0 , 0 ]};

        then i = [ 0 , 0 , 0 ] by TARSKI:def 1;

        hence contradiction by A1;

      end;

      the InstructionsF of M = III by Def7;

      then i = [1, 0 , 0 ] or i = [ 0 , 0 , 0 ] by TARSKI:def 2;

      then

       A3: i in { [1, 0 , 0 ]} by A1, TARSKI:def 1;

      

       A4: 0 in { 0 } by TARSKI:def 1;

      then

       A5: 0 in ( dom ( 0 .--> (( In ((s . 0 ), NAT )) + 1)));

      consider f be Function of ( product ( the_Values_of M)), ( product ( the_Values_of M)) such that

       A6: for s be Element of ( product ( the_Values_of M)) holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) and

       A7: the Execution of M = (( [1, 0 , 0 ] .--> f) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M))))) by Def7;

      

       A8: for s be State of M holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))

      proof

        let s be State of M;

        reconsider s as Element of ( product ( the_Values_of M)) by CARD_3: 107;

        (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) by A6;

        hence thesis;

      end;

      

       A9: ( IC M) = 0 by Def7;

      

       A10: s in ( product ( the_Values_of M)) by CARD_3: 107;

      ( dom ( the_Values_of M)) = the carrier of M by PARTFUN1:def 2

      .= { 0 } by Def7;

      then

       A11: 0 in ( dom ( the_Values_of M)) by TARSKI:def 1;

      ( Values ( IC M)) = NAT by MEMSTR_0:def 6;

      then

      reconsider k = (s . 0 ) as Element of NAT by A10, A11, CARD_3: 9, A9;

      ( dom ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M))))) = { [ 0 , 0 , 0 ]};

      

      then (the Execution of M . i) = (( [1, 0 , 0 ] .--> f) . i) by A7, A2, FUNCT_4: 11

      .= f by A3, FUNCOP_1: 7;

      

      hence (( Exec (i,s)) . ( IC ( STC N))) = ((s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) . 0 ) by A9, A8

      .= (( 0 .--> (( In ((s . 0 ), NAT )) + 1)) . 0 ) by A5, FUNCT_4: 13

      .= (( In (k, NAT )) + 1) by A4, FUNCOP_1: 7

      .= (( IC s) + 1) by A9;

    end;

    theorem :: AMISTD_1:4

    

     Th4: for i be Instruction of ( STC N) st ( InsCode i) = 0 holds i is halting

    proof

      let i be Instruction of ( STC N);

      set M = ( STC N);

      the InstructionsF of M = III by Def7;

      then

       A1: i = [1, 0 , 0 ] or i = [ 0 , 0 , 0 ] by TARSKI:def 2;

      assume ( InsCode i) = 0 ;

      then

       A2: i in { [ 0 , 0 , 0 ]} by A1, TARSKI:def 1;

      let s be State of M;

      reconsider s as Element of ( product ( the_Values_of M)) by CARD_3: 107;

      (ex f be Function of ( product ( the_Values_of M)), ( product ( the_Values_of M)) st (for s be Element of ( product ( the_Values_of M)) holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))) & the Execution of M = (( [1, 0 , 0 ] .--> f) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M)))))) & ( dom ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M))))) = { [ 0 , 0 , 0 ]} by Def7;

      

      then (the Execution of M . i) = (( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M)))) . i) by A2, FUNCT_4: 13

      .= ( id ( product ( the_Values_of M))) by A2, FUNCOP_1: 7;

      then ((the Execution of M . i) . s) = s;

      hence thesis;

    end;

    theorem :: AMISTD_1:5

    for i be Instruction of ( STC N) st ( InsCode i) = 1 holds i is non halting

    proof

      let i be Instruction of ( STC N);

      set M = ( STC N);

      set s = the State of M;

      assume ( InsCode i) = 1;

      then

       A1: (( Exec (i,s)) . ( IC M)) = (( IC s) + 1) by Lm3;

      assume for s be State of M holds ( Exec (i,s)) = s;

      then (( Exec (i,s)) . ( IC M)) = ( IC s);

      hence thesis by A1;

    end;

    theorem :: AMISTD_1:6

    

     Th6: for i be Element of the InstructionsF of ( STC N) holds ( InsCode i) = 1 or ( InsCode i) = 0

    proof

      let i be Element of the InstructionsF of ( STC N);

      the InstructionsF of ( STC N) = III by Def7;

      then i = [1, 0 , 0 ] or i = [ 0 , 0 , 0 ] by TARSKI:def 2;

      hence thesis;

    end;

    theorem :: AMISTD_1:7

    for i be Instruction of ( STC N) holds i is jump-only

    proof

      let i be Instruction of ( STC N);

      set M = ( STC N);

      let s be State of M, o be Object of M, I be Instruction of M such that ( InsCode I) = ( InsCode i) and

       A1: o in ( Data-Locations M);

      

       A2: ( IC M) = 0 by Def7;

      ( Data-Locations M) = ( { 0 } \ { 0 }) by A2, Def7

      .= {} by XBOOLE_1: 37;

      hence thesis by A1;

    end;

    registration

      let N;

      cluster -> ins-loc-free for Instruction of ( STC N);

      coherence

      proof

        let I be Instruction of ( STC N);

        I in the InstructionsF of ( STC N);

        then I in { [ 0 , 0 , 0 ], [1, 0 , 0 ]} by Def7;

        then I = [ 0 , 0 , 0 ] or I = [1, 0 , 0 ] by TARSKI:def 2;

        hence ( JumpPart I) is empty;

      end;

    end

    

     Lm4: for l be Nat, i be Element of the InstructionsF of ( STC N) st l = z & ( InsCode i) = 1 holds ( NIC (i,l)) = {(z + 1)}

    proof

      let l be Nat, i be Element of the InstructionsF of ( STC N);

      assume that

       A1: l = z and

       A2: ( InsCode i) = 1;

      set M = ( STC N);

      set F = { ( IC ( Exec (i,ss))) where ss be Element of ( product ( the_Values_of ( STC N))) : ( IC ss) = l };

      now

        set f = ( NAT --> i);

        set w = the State of M;

        reconsider ll = l as Element of NAT by ORDINAL1:def 12;

        reconsider l9 = ll as Element of ( Values ( IC M)) by MEMSTR_0:def 6;

        set u = (( IC M) .--> l9);

        let y be object;

        reconsider t = (w +* u) as Element of ( product ( the_Values_of ( STC N))) by CARD_3: 107;

        hereby

          assume y in F;

          then ex s be Element of ( product ( the_Values_of ( STC N))) st y = ( IC ( Exec (i,s))) & ( IC s) = l;

          then y = (z + 1) by A1, A2, Lm3;

          hence y in {(z + 1)} by TARSKI:def 1;

        end;

        assume y in {(z + 1)};

        then

         A5: y = (z + 1) by TARSKI:def 1;

        ( IC M) in ( dom u) by TARSKI:def 1;

        

        then

         A6: ( IC t) = (u . ( IC M)) by FUNCT_4: 13

        .= z by A1, FUNCOP_1: 72;

        then ( IC ( Following (f,t))) = (z + 1) by A2, Lm3;

        hence y in F by A1, A5, A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm5: for i be Element of the InstructionsF of ( STC N) holds ( JUMP i) is empty

    proof

      let i be Element of the InstructionsF of ( STC N);

      per cases by Th6;

        suppose

         A1: ( InsCode i) = 1;

        reconsider l1 = 0 , l2 = 1 as Nat;

        set X = the set of all ( NIC (i,l)) where l be Nat;

        assume not thesis;

        then

        consider x be object such that

         A2: x in ( meet X);

        ( NIC (i,l1)) in X;

        then {( 0 + 1)} in X by A1, Lm4;

        then x in {1} by A2, SETFAM_1:def 1;

        then

         A3: x = 1 by TARSKI:def 1;

        ( NIC (i,l2)) in X;

        then {(1 + 1)} in X by A1, Lm4;

        then x in {2} by A2, SETFAM_1:def 1;

        hence contradiction by A3, TARSKI:def 1;

      end;

        suppose

         A4: ( InsCode i) = 0 ;

        reconsider i as Instruction of ( STC N);

        for l be Nat holds ( NIC (i,l)) = {l} by A4, Th2, Th4;

        hence thesis by Th1;

      end;

    end;

    theorem :: AMISTD_1:8

    

     Th8: for l be Nat st l = z holds ( SUCC (l,( STC N))) = {z, (z + 1)}

    proof

      let l be Nat such that

       A1: l = z;

      set M = ( STC N);

      set K = the set of all (( NIC (i,l)) \ ( JUMP i)) where i be Element of the InstructionsF of ( STC N);

      now

        let y be object;

        hereby

          assume y in K;

          then

          consider ii be Element of the InstructionsF of ( STC N) such that

           A2: y = (( NIC (ii,l)) \ ( JUMP ii)) and not contradiction;

          reconsider ii as Instruction of ( STC N);

          now

            per cases by Th6;

              suppose

               A3: ( InsCode ii) = 1;

              ( JUMP ii) = {} by Lm5;

              then y = {(z + 1)} by A1, A2, A3, Lm4;

              hence y in { {z}, {(z + 1)}} by TARSKI:def 2;

            end;

              suppose

               A4: ( InsCode ii) = 0 ;

              ( JUMP ii) = {} by Lm5;

              then y = {z} by A1, A2, A4, Th2, Th4;

              hence y in { {z}, {(z + 1)}} by TARSKI:def 2;

            end;

          end;

          hence y in { {z}, {(z + 1)}};

        end;

        assume

         A5: y in { {z}, {(z + 1)}};

        per cases by A5, TARSKI:def 2;

          suppose

           A6: y = {z};

          ( halt M) = [ 0 , {} , {} ];

          then

          reconsider i = [ 0 , 0 , 0 ] as Instruction of M;

          ( JUMP i) = {} & ( InsCode i) = 0 by Lm5;

          then (( NIC (i,l)) \ ( JUMP i)) = y by A1, A6, Th2, Th4;

          hence y in K;

        end;

          suppose

           A7: y = {(z + 1)};

          set i = [1, 0 , 0 ];

          i in III by TARSKI:def 2;

          then

          reconsider i as Instruction of M by Def7;

          ( JUMP i) = {} & ( InsCode i) = 1 by Lm5;

          then (( NIC (i,l)) \ ( JUMP i)) = y by A1, A7, Lm4;

          hence y in K;

        end;

      end;

      then K = { {z}, {(z + 1)}} by TARSKI: 2;

      hence thesis by ZFMISC_1: 26;

    end;

    registration

      let N be with_zero set;

      cluster ( STC N) -> standard;

      coherence

      proof

        set M = ( STC N);

        now

          let k be Nat;

          

           A1: ( SUCC (k,( STC N))) = {k, (k + 1)} by Th8;

          thus (k + 1) in ( SUCC (k,( STC N))) by A1, TARSKI:def 2;

          let j be Nat;

          assume j in ( SUCC (k,( STC N)));

          then j = k or j = (k + 1) by A1, TARSKI:def 2;

          hence k <= j by NAT_1: 11;

        end;

        hence thesis by Th3;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> halting;

      coherence

      proof

        set I = ( halt ( STC N));

        ( InsCode I) = 0 ;

        hence I is halting by Th4;

      end;

    end

    registration

      let N be with_zero set;

      cluster standard halting for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    reserve T for standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

    theorem :: AMISTD_1:9

    for i be Instruction of ( STC N), s be State of ( STC N) st ( InsCode i) = 1 holds (( Exec (i,s)) . ( IC ( STC N))) = (( IC s) + 1) by Lm3;

    theorem :: AMISTD_1:10

    for l be Nat, i be Element of the InstructionsF of ( STC N) st ( InsCode i) = 1 holds ( NIC (i,l)) = {(l + 1)} by Lm4;

    theorem :: AMISTD_1:11

    for l be Nat holds ( SUCC (l,( STC N))) = {l, (l + 1)} by Th8;

    definition

      let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Instruction of S;

      :: AMISTD_1:def8

      attr i is sequential means for s be State of S holds (( Exec (i,s)) . ( IC S)) = (( IC s) + 1);

    end

    theorem :: AMISTD_1:12

    

     Th12: for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il be Nat, i be Instruction of S st i is sequential holds ( NIC (i,il)) = {(il + 1)}

    proof

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il be Nat, i be Instruction of S such that

       A1: for s be State of S holds (( Exec (i,s)) . ( IC S)) = (( IC s) + 1);

      now

        let x be object;

         A2:

        now

          reconsider ll = il as Element of NAT by ORDINAL1:def 12;

          reconsider il1 = ll as Element of ( Values ( IC S)) by MEMSTR_0:def 6;

          set I = i;

          set t = the State of S, P = the Instruction-Sequence of S;

          assume

           A3: x = (il + 1);

          reconsider u = (t +* (( IC S),il1)) as Element of ( product ( the_Values_of S)) by CARD_3: 107;

          ll in NAT ;

          then

           A4: il in ( dom P) by PARTFUN1:def 2;

          

           A5: ((P +* (il,i)) /. ll) = ((P +* (il,i)) . ll) by PBOOLE: 143

          .= i by A4, FUNCT_7: 31;

          ( IC S) in ( dom t) by MEMSTR_0: 2;

          then

           A6: ( IC u) = il by FUNCT_7: 31;

          then ( IC ( Following ((P +* (il,i)),u))) = (il + 1) by A1, A5;

          hence x in { ( IC ( Exec (i,ss))) where ss be Element of ( product ( the_Values_of S)) : ( IC ss) = il } by A3, A6, A5;

        end;

        now

          assume x in { ( IC ( Exec (i,ss))) where ss be Element of ( product ( the_Values_of S)) : ( IC ss) = il };

          then ex s be Element of ( product ( the_Values_of S)) st x = ( IC ( Exec (i,s))) & ( IC s) = il;

          hence x = (il + 1) by A1;

        end;

        hence x in {(il + 1)} iff x in { ( IC ( Exec (i,ss))) where ss be Element of ( product ( the_Values_of S)) : ( IC ss) = il } by A2, TARSKI:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      cluster sequential -> non halting for Instruction of S;

      coherence

      proof

        let i be Instruction of S such that

         A1: i is sequential;

        set s = the State of S;

        

         A2: (( IC s) + 1) <> (( IC s) + 0 );

        ( NIC (i,( IC s))) = {(( IC s) + 1)} by A1, Th12;

        then ( NIC (i,( IC s))) <> {( IC s)} by ZFMISC_1: 3, A2;

        hence thesis by Th2;

      end;

      cluster halting -> non sequential for Instruction of S;

      coherence ;

    end

    theorem :: AMISTD_1:13

    for T be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for i be Instruction of T st ( JUMP i) is non empty holds i is non sequential

    proof

      let T be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      let i be Instruction of T;

      set X = the set of all ( NIC (i,l1)) where l1 be Nat;

      assume ( JUMP i) is non empty;

      then

      consider l be object such that

       A1: l in ( JUMP i);

      reconsider l as Nat by A1;

      ( NIC (i,l)) in X;

      then l in ( NIC (i,l)) by A1, SETFAM_1:def 1;

      then

      consider s be Element of ( product ( the_Values_of T)) such that

       A2: l = ( IC ( Exec (i,s))) & ( IC s) = l;

      take s;

      thus thesis by A2;

    end;

    begin

    definition

      let N be with_zero set;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      let F be finite preProgram of S;

      :: AMISTD_1:def9

      attr F is really-closed means for l be Nat st l in ( dom F) holds ( NIC ((F /. l),l)) c= ( dom F);

    end

    ::$Canceled

    definition

      let N be with_zero set;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      let F be NAT -definedthe InstructionsF of S -valued Function;

      :: AMISTD_1:def10

      attr F is parahalting means for s be 0 -started State of S holds for P be Instruction-Sequence of S st F c= P holds P halts_on s;

    end

    theorem :: AMISTD_1:14

    

     Th14: for N be with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for F be finite preProgram of S holds F is really-closed iff for s be State of S st ( IC s) in ( dom F) holds for k be Nat holds ( IC ( Comput (F,s,k))) in ( dom F)

    proof

      let N be with_zero set;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      let F be finite preProgram of S;

      thus F is really-closed implies for s be State of S st ( IC s) in ( dom F) holds for k be Nat holds ( IC ( Comput (F,s,k))) in ( dom F)

      proof

        assume

         A1: F is really-closed;

        let s be State of S such that

         A2: ( IC s) in ( dom F);

        defpred P[ Nat] means ( IC ( Comput (F,s,$1))) in ( dom F);

         A3:

        now

          let k be Nat such that

           A4: P[k];

          reconsider t = ( Comput (F,s,k)) as Element of ( product ( the_Values_of S)) by CARD_3: 107;

          set l = ( IC ( Comput (F,s,k)));

          

           A5: ( IC ( Following (F,t))) in ( NIC ((F /. l),l));

          

           A6: ( Comput (F,s,(k + 1))) = ( Following (F,t)) by EXTPRO_1: 3;

          ( NIC ((F /. l),l)) c= ( dom F) by A1, A4;

          hence P[(k + 1)] by A5, A6;

        end;

        

         A7: P[ 0 ] by A2;

        thus for k be Nat holds P[k] from NAT_1:sch 2( A7, A3);

      end;

      assume

       A8: for s be State of S st ( IC s) in ( dom F) holds for k be Nat holds ( IC ( Comput (F,s,k))) in ( dom F);

      let l be Nat such that

       A9: l in ( dom F);

      let x be object;

      assume x in ( NIC ((F /. l),l));

      then

      consider ss be Element of ( product ( the_Values_of S)) such that

       A10: x = ( IC ( Exec ((F /. l),ss))) and

       A11: ( IC ss) = l;

      reconsider ss as State of S;

      ( IC ( Comput (F,ss,( 0 + 1)))) = ( IC ( Following (F,( Comput (F,ss, 0 ))))) by EXTPRO_1: 3

      .= ( IC ( Following (F,ss)))

      .= ( IC ( Exec ((F /. ( IC ss)),ss)));

      hence x in ( dom F) by A10, A11, A8, A9;

    end;

    

     Lm6: for N be with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for F be finite preProgram of S holds F is really-closed iff for s be State of S st ( IC s) in ( dom F) holds for P be Instruction-Sequence of S st F c= P holds for k be Nat holds ( IC ( Comput (P,s,k))) in ( dom F)

    proof

      let N be with_zero set;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      let F be finite preProgram of S;

      thus F is really-closed implies for s be State of S st ( IC s) in ( dom F) holds for P be Instruction-Sequence of S st F c= P holds for k be Nat holds ( IC ( Comput (P,s,k))) in ( dom F)

      proof

        assume

         A1: F is really-closed;

        let s be State of S such that

         A2: ( IC s) in ( dom F);

        let P be Instruction-Sequence of S such that

         A3: F c= P;

        defpred P[ Nat] means ( IC ( Comput (P,s,$1))) in ( dom F);

         A4:

        now

          let k be Nat such that

           A5: P[k];

          reconsider t = ( Comput (P,s,k)) as Element of ( product ( the_Values_of S)) by CARD_3: 107;

          set l = ( IC ( Comput (P,s,k)));

          

           A6: ( IC ( Following (P,t))) in ( NIC ((P /. l),l));

          

           A7: ( Comput (P,s,(k + 1))) = ( Following (P,t)) by EXTPRO_1: 3;

          (P /. l) = (F /. l) by A5, A3, PARTFUN2: 61;

          then ( NIC ((P /. l),l)) c= ( dom F) by A1, A5;

          hence P[(k + 1)] by A6, A7;

        end;

        

         A8: P[ 0 ] by A2;

        thus for k be Nat holds P[k] from NAT_1:sch 2( A8, A4);

      end;

      assume

       A9: for s be State of S st ( IC s) in ( dom F) holds for P be Instruction-Sequence of S st F c= P holds for k be Nat holds ( IC ( Comput (P,s,k))) in ( dom F);

      for s be State of S st ( IC s) in ( dom F) holds for k be Nat holds ( IC ( Comput (F,s,k))) in ( dom F)

      proof

        let s be State of S such that

         A10: ( IC s) in ( dom F);

        consider P be Instruction-Sequence of S such that

         A11: F c= P by PBOOLE: 145;

        let k be Nat;

        

         A12: ( IC ( Comput (P,s,k))) in ( dom F) by A9, A10, A11;

        defpred P[ Nat] means ( Comput (P,s,$1)) = ( Comput (F,s,$1));

        

         A13: P[ 0 ];

        

         A14: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A15: P[k];

          reconsider kk = k as Nat;

          

           A16: ( IC ( Comput (P,s,kk))) in ( dom F) by A9, A10, A11;

          ( Comput (P,s,(k + 1))) = ( Following (P,( Comput (F,s,k)))) by A15, EXTPRO_1: 3

          .= ( Following (F,( Comput (F,s,k)))) by A16, A11, A15, PARTFUN2: 61

          .= ( Comput (F,s,(k + 1))) by EXTPRO_1: 3;

          hence P[(k + 1)];

        end;

        for k be Nat holds P[k] from NAT_1:sch 2( A13, A14);

        hence ( IC ( Comput (F,s,k))) in ( dom F) by A12;

      end;

      hence thesis by Th14;

    end;

    registration

      let N;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      cluster ( Stop S) -> really-closed;

      coherence

      proof

        set F = ( Stop S);

        let l be Nat;

        assume

         A1: l in ( dom F);

        

         A3: l = 0 by A1, TARSKI:def 1;

        (F /. l) = (F . l) by A1, PARTFUN1:def 6

        .= ( halt S) by A3;

        hence thesis by A3, Th2;

      end;

    end

    ::$Canceled

    registration

      let N be with_zero set;

      let S be standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      cluster really-closed trivial for MacroInstruction of S;

      existence

      proof

        take F = ( Stop S);

        thus thesis;

      end;

    end

    theorem :: AMISTD_1:17

    for i be Instruction of ( Trivial-AMI N) holds i is halting

    proof

      let i be Instruction of ( Trivial-AMI N);

      set M = ( Trivial-AMI N);

      

       A1: the InstructionsF of M = { [ 0 , {} , {} ]} by EXTPRO_1:def 1;

      let s be State of M;

      reconsider s as Element of ( product ( the_Values_of M)) by CARD_3: 107;

      

       A2: the Object-Kind of M = ( 0 .--> 0 ) & the ValuesF of M = (N --> NAT ) by EXTPRO_1:def 1;

      (the Execution of M . i) = (( [ 0 , {} , {} ] .--> ( id ( product ( the_Values_of M)))) . i) by A2, EXTPRO_1:def 1

      .= ( id ( product ( the_Values_of M))) by A1;

      then ((the Execution of M . i) . s) = s;

      hence thesis;

    end;

    theorem :: AMISTD_1:18

    for i be Element of the InstructionsF of ( Trivial-AMI N) holds ( InsCode i) = 0

    proof

      let i be Element of the InstructionsF of ( Trivial-AMI N);

      the InstructionsF of ( Trivial-AMI N) = { [ 0 , {} , {} ]} by EXTPRO_1:def 1;

      then i = [ 0 , {} , {} ] by TARSKI:def 1;

      hence thesis;

    end;

    begin

    theorem :: AMISTD_1:19

    for N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Instruction of S, l be Nat holds ( JUMP i) c= ( NIC (i,l))

    proof

      let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Instruction of S, l be Nat;

      set X = the set of all ( NIC (i,k)) where k be Nat;

      let x be object;

      

       A1: ( NIC (i,l)) in X;

      assume x in ( JUMP i);

      hence thesis by A1, SETFAM_1:def 1;

    end;

    theorem :: AMISTD_1:20

    for i be Instruction of ( STC N), s be State of ( STC N) st ( InsCode i) = 1 holds ( Exec (i,s)) = ( IncIC (s,1))

    proof

      let i be Instruction of ( STC N), s be State of ( STC N);

      set M = ( STC N);

      assume

       A1: ( InsCode i) = 1;

       A2:

      now

        assume i in { [ 0 , 0 , 0 ]};

        then i = [ 0 , 0 , 0 ] by TARSKI:def 1;

        hence contradiction by A1;

      end;

      the InstructionsF of M = III by Def7;

      then i = [1, 0 , 0 ] or i = [ 0 , 0 , 0 ] by TARSKI:def 2;

      then

       A3: i in { [1, 0 , 0 ]} by A1, TARSKI:def 1;

      consider f be Function of ( product ( the_Values_of M)), ( product ( the_Values_of M)) such that

       A4: for s be Element of ( product ( the_Values_of M)) holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) and

       A5: the Execution of M = (( [1, 0 , 0 ] .--> f) +* ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M))))) by Def7;

      

       A6: for s be State of M holds (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1)))

      proof

        let s be State of M;

        reconsider s as Element of ( product ( the_Values_of M)) by CARD_3: 107;

        (f . s) = (s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) by A4;

        hence thesis;

      end;

      

       A7: ( IC M) = 0 by Def7;

      

       A8: s in ( product ( the_Values_of M)) by CARD_3: 107;

      ( dom ( the_Values_of M)) = the carrier of M by PARTFUN1:def 2

      .= { 0 } by Def7;

      then

       A9: 0 in ( dom ( the_Values_of M)) by TARSKI:def 1;

      ( Values ( IC M)) = NAT by MEMSTR_0:def 6;

      then

      reconsider k = (s . 0 ) as Element of NAT by A8, A9, CARD_3: 9, A7;

      

       A10: ( Start-At ((( IC s) + 1),M)) = ( 0 .--> (( In (k, NAT )) + 1)) by A7;

      ( dom ( [ 0 , 0 , 0 ] .--> ( id ( product ( the_Values_of M))))) = { [ 0 , 0 , 0 ]};

      

      then (the Execution of M . i) = (( [1, 0 , 0 ] .--> f) . i) by A5, A2, FUNCT_4: 11

      .= f by A3, FUNCOP_1: 7;

      hence ( Exec (i,s)) = ( IncIC (s,1)) by A10, A6;

    end;

    registration

      let N;

      let p be PartState of ( STC N);

      cluster ( DataPart p) -> empty;

      coherence

      proof

        ( Data-Locations ( STC N)) = (the carrier of ( STC N) \ { 0 }) by Def7

        .= ( { 0 } \ { 0 }) by Def7

        .= {} by XBOOLE_1: 37;

        hence thesis;

      end;

    end

    theorem :: AMISTD_1:21

    for N be with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for F be finite preProgram of S holds F is really-closed iff for s be State of S st ( IC s) in ( dom F) holds for P be Instruction-Sequence of S st F c= P holds for k be Nat holds ( IC ( Comput (P,s,k))) in ( dom F) by Lm6;

    registration

      let N be with_zero set;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      cluster parahalting for finite non halt-free non empty NAT -definedthe InstructionsF of S -valued Function;

      existence

      proof

        take ( Stop S);

        let s be 0 -started State of S;

        let P be Instruction-Sequence of S such that

         A1: ( Stop S) c= P;

        take 0 ;

        

         A2: 0 in ( dom ( Stop S)) by COMPOS_1: 3;

        ( dom ( Stop S)) c= ( dom P) by A1, RELAT_1: 11;

        then

         A3: 0 in ( dom P) by A2;

        

         A4: ( IC s) = 0 by MEMSTR_0:def 11;

        hence ( IC ( Comput (P,s, 0 ))) in ( dom P) by A3;

        

        thus ( CurInstr (P,( Comput (P,s, 0 )))) = (P /. 0 ) by A4

        .= (P . 0 ) by A3, PARTFUN1:def 6

        .= (( Stop S) . 0 ) by A1, A2, GRFUNC_1: 2

        .= ( halt S);

      end;

    end