ami_wstd.miz



    begin

    reserve x for set,

D for non empty set,

k,n for Element of 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 Element of NAT ,

s for State of S;

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

    begin

    definition

      let N, S;

      let l1,l2 be Nat;

      :: AMI_WSTD:def1

      pred l1 <= l2,S means ex f be non empty FinSequence of NAT st (f /. 1) = l1 & (f /. ( len f)) = l2 & for n st 1 <= n & n < ( len f) holds (f /. (n + 1)) in ( SUCC ((f /. n),S));

    end

    theorem :: AMI_WSTD:1

    for N, S holds for l1,l2 be Nat holds l1 <= (l2,S) & l2 <= (l3,S) implies l1 <= (l3,S)

    proof

      let N, S;

      let l1,l2 be Nat;

      given f1 be non empty FinSequence of NAT such that

       A1: (f1 /. 1) = l1 and

       A2: (f1 /. ( len f1)) = l2 and

       A3: for n st 1 <= n & n < ( len f1) holds (f1 /. (n + 1)) in ( SUCC ((f1 /. n),S));

      given f2 be non empty FinSequence of NAT such that

       A4: (f2 /. 1) = l2 and

       A5: (f2 /. ( len f2)) = l3 and

       A6: for n st 1 <= n & n < ( len f2) holds (f2 /. (n + 1)) in ( SUCC ((f2 /. n),S));

      take (f1 ^' f2);

      thus ((f1 ^' f2) /. 1) = l1 by A1, FINSEQ_6: 155;

      now

        per cases ;

          suppose f2 is trivial;

          then

           A7: ex x be Element of NAT st f2 = <*x*> by FINSEQ_6: 107;

          then (f1 ^' f2) = f1 by FINSEQ_6: 158;

          hence ((f1 ^' f2) /. ( len (f1 ^' f2))) = l3 by A2, A4, A5, A7, FINSEQ_1: 39;

        end;

          suppose not f2 is trivial;

          hence ((f1 ^' f2) /. ( len (f1 ^' f2))) = l3 by A5, FINSEQ_6: 156;

        end;

      end;

      hence ((f1 ^' f2) /. ( len (f1 ^' f2))) = l3;

      let n such that

       A8: 1 <= n and

       A9: n < ( len (f1 ^' f2));

      

       A10: (( len (f1 ^' f2)) + 1) = (( len f1) + ( len f2)) by FINSEQ_6: 139;

      per cases by XXREAL_0: 1;

        suppose

         A11: n < ( len f1);

        then (n + 1) <= ( len f1) by NAT_1: 13;

        then

         A12: ((f1 ^' f2) /. (n + 1)) = (f1 /. (n + 1)) by FINSEQ_6: 159, NAT_1: 11;

        ((f1 ^' f2) /. n) = (f1 /. n) by A8, A11, FINSEQ_6: 159;

        hence thesis by A3, A8, A11, A12;

      end;

        suppose

         A13: n = ( len f1);

        then

         A14: ((f1 ^' f2) /. n) = (f2 /. 1) by A2, A4, A8, FINSEQ_6: 159;

        (n + 1) < (( len (f1 ^' f2)) + 1) by A9, XREAL_1: 6;

        then

         A15: 1 < ( len f2) by A10, A13, XREAL_1: 6;

        then ((f1 ^' f2) /. (n + 1)) = (f2 /. (1 + 1)) by A13, FINSEQ_6: 160;

        hence thesis by A6, A14, A15;

      end;

        suppose

         A16: n > ( len f1);

        then

        consider m be Nat such that

         A17: (( len f1) + m) = n by NAT_1: 10;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        

         A18: (( len f1) + m) > (( len f1) + 0 ) by A16, A17;

        ((( len f1) + m) + 1) < (( len f1) + ( len f2)) by A9, A10, A17, XREAL_1: 6;

        then (( len f1) + (m + 1)) < (( len f1) + ( len f2));

        then

         A19: (m + 1) < ( len f2) by XREAL_1: 6;

        

         A20: ((f1 ^' f2) /. (n + 1)) = ((f1 ^' f2) /. (( len f1) + (m + 1))) by A17

        .= (f2 /. ((m + 1) + 1)) by A19, FINSEQ_6: 160, NAT_1: 11;

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

        then m < ( len f2) by A19, XXREAL_0: 2;

        then ((f1 ^' f2) /. n) = (f2 /. (m + 1)) by A17, A18, FINSEQ_6: 160, NAT_1: 14;

        hence thesis by A6, A19, A20, NAT_1: 11;

      end;

    end;

    definition

      let N, S;

      :: AMI_WSTD:def2

      attr S is InsLoc-antisymmetric means for l1, l2 st l1 <= (l2,S) & l2 <= (l1,S) holds l1 = l2;

    end

    definition

      let N, S;

      :: AMI_WSTD:def3

      attr S is weakly_standard means

      : Def3: ex f be sequence of NAT st f is bijective & for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S);

    end

    theorem :: AMI_WSTD:2

    

     Th2: for f1,f2 be sequence of NAT st f1 is bijective & (for m,n be Element of NAT holds m <= n iff (f1 . m) <= ((f1 . n),S)) & f2 is bijective & (for m,n be Element of NAT holds m <= n iff (f2 . m) <= ((f2 . n),S)) holds f1 = f2

    proof

      let f1,f2 be sequence of NAT such that

       A1: f1 is bijective and

       A2: for m,n be Element of NAT holds m <= n iff (f1 . m) <= ((f1 . n),S) and

       A3: f2 is bijective and

       A4: for m,n be Element of NAT holds m <= n iff (f2 . m) <= ((f2 . n),S);

      

       A5: ( dom f1) = NAT by FUNCT_2:def 1;

      

       A6: ( dom f2) = NAT by FUNCT_2:def 1;

      defpred P[ Nat] means (f1 . $1) <> (f2 . $1);

      assume f1 <> f2;

      then ex c be Element of NAT st P[c] by FUNCT_2: 63;

      then

       A7: ex c be Nat st P[c];

      consider d be Nat such that

       A8: P[d] and

       A9: for n be Nat st P[n] holds d <= n from NAT_1:sch 5( A7);

      reconsider d as Element of NAT by ORDINAL1:def 12;

      

       A10: ( rng f1) = NAT by A1, FUNCT_2:def 3;

      

       A11: ( rng f2) = NAT by A3, FUNCT_2:def 3;

      consider d1 be object such that

       A12: d1 in ( dom f1) and

       A13: (f2 . d) = (f1 . d1) by A10, FUNCT_1:def 3;

      reconsider d1 as Element of NAT by A12;

      consider d2 be object such that

       A14: d2 in ( dom f2) and

       A15: (f1 . d) = (f2 . d2) by A11, FUNCT_1:def 3;

      reconsider d2 as Element of NAT by A14;

      per cases ;

        suppose

         A16: d1 <= d & d2 <= d;

        then (f2 . d2) <= ((f2 . d),S) by A4;

        then d <= d1 by A2, A15, A13;

        hence contradiction by A8, A13, A16, XXREAL_0: 1;

      end;

        suppose

         A17: d <= d1 & d2 <= d;

        (f2 . d2) = (f1 . d2)

        proof

          assume not thesis;

          then d <= d2 by A9;

          hence contradiction by A8, A15, A17, XXREAL_0: 1;

        end;

        hence contradiction by A1, A8, A15, A5, FUNCT_1:def 4;

      end;

        suppose

         A18: d1 <= d & d <= d2;

        (f1 . d1) = (f2 . d1)

        proof

          assume not thesis;

          then d <= d1 by A9;

          hence contradiction by A8, A13, A18, XXREAL_0: 1;

        end;

        hence contradiction by A3, A8, A13, A6, FUNCT_1:def 4;

      end;

        suppose

         A19: d <= d1 & d <= d2;

        then (f2 . d) <= ((f2 . d2),S) by A4;

        then d1 <= d by A2, A15, A13;

        hence contradiction by A8, A13, A19, XXREAL_0: 1;

      end;

    end;

    

     Lm1: k <= (k,S)

    proof

      reconsider l = k as Element of NAT ;

      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 :: AMI_WSTD:3

    

     Th3: for f be sequence of NAT st f is bijective holds (for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S)) iff for k be Element of NAT holds (f . (k + 1)) in ( SUCC ((f . k),S)) & for j be Element of NAT st (f . j) in ( SUCC ((f . k),S)) holds k <= j

    proof

      let f be sequence of NAT ;

      assume

       A1: f is bijective;

      hereby

        assume

         A2: for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S);

        let k be Element of NAT ;

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

        then (f . k) <= ((f . (k + 1)),S) by A2;

        then

        consider F be non empty FinSequence of NAT such that

         A3: (F /. 1) = (f . k) and

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

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

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

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

        

         A6: (f . (k + 1)) in ( rng F) by A4, FINSEQ_6: 168;

        then

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

        then

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

        

         A9: x in ( dom F) by A6, FINSEQ_4: 20;

        

        then

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

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

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

        then

         A11: ( len F1) < ( len F) by A8, NAT_1: 13;

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

        then

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

        then

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

        

         A14: (F . x) = (f . (k + 1)) by A6, FINSEQ_4: 19;

        

         A15: ( dom f) = NAT by FUNCT_2:def 1;

        

         A16: (f . k) <> (f . (k + 1))

        proof

          assume not thesis;

          then ( 0 + k) = (k + 1) by A1, A15, FUNCT_1:def 4;

          hence contradiction;

        end;

        then

         A17: ( len F1) <> 0 by A3, A14, A12, A7, PARTFUN1:def 6;

        1 <= x by A9, FINSEQ_3: 25;

        then 1 < x by A3, A16, A14, A13, XXREAL_0: 1;

        then

         A18: 1 <= ( len F1) by A8, NAT_1: 13;

        reconsider F1 as non empty FinSequence of NAT by A17, A6, FINSEQ_4: 41;

        ( rng f) = NAT by A1, FUNCT_2:def 3;

        then

        consider m be object such that

         A19: m in ( dom f) and

         A20: (f . m) = (F /. ( len F1)) by FUNCT_1:def 3;

        reconsider m as Element of NAT by A19;

        

         A21: ( len F1) in ( dom F) by A18, A11, FINSEQ_3: 25;

        

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

        

        then

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

        .= (F . ( len F1)) by A6, A22, FINSEQ_4: 36

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

         A24:

        now

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

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

          then

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

          assume

           A26: m = (k + 1);

          

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

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

          hence contradiction by A20, A23, A26, A25, A27, FUNCT_1:def 3, TARSKI:def 1;

        end;

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

        

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

        then

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

        

        then

         A30: (F2 /. ( len F2)) = (F2 . 2) by A28, PARTFUN1:def 6

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

        .= (f . (k + 1)) by A14, A9, PARTFUN1:def 6;

        

         A31: 1 in ( dom F2) by A28, FINSEQ_3: 25;

         A32:

        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

           A33: n = 1 by NAT_1: 25;

          

          then

           A34: (F2 /. n) = (F2 . 1) by A31, PARTFUN1:def 6

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

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

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

          hence (F2 /. (n + 1)) in ( SUCC ((F2 /. n),S)) by A5, A18, A11, A34;

        end;

         A35:

        now

          let n;

          assume that

           A36: 1 <= n and

           A37: n < ( len F1);

          

           A38: 1 <= (n + 1) by A36, NAT_1: 13;

          

           A39: (n + 1) <= ( len F1) by A37, NAT_1: 13;

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

          then

           A40: (n + 1) in ( dom F) by A38, FINSEQ_3: 25;

          n <= ( len F) by A11, A37, XXREAL_0: 2;

          then

           A41: n in ( dom F) by A36, FINSEQ_3: 25;

          

           A42: n in ( dom F1) by A36, A37, FINSEQ_3: 25;

          

          then

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

          .= (F . n) by A6, A42, FINSEQ_4: 36

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

          

           A44: n < ( len F) by A11, A37, XXREAL_0: 2;

          

           A45: (n + 1) in ( dom F1) by A38, A39, FINSEQ_3: 25;

          

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

          .= (F . (n + 1)) by A6, A45, FINSEQ_4: 36

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

          hence (F1 /. (n + 1)) in ( SUCC ((F1 /. n),S)) by A5, A36, A43, A44;

        end;

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

        .= (f . m) by A20, FINSEQ_1: 44;

        then (f . m) <= ((f . (k + 1)),S) by A30, A32;

        then

         A46: m <= (k + 1) by A2;

        

         A47: 1 in ( dom F1) by A18, FINSEQ_3: 25;

        

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

        .= (F . 1) by A6, A47, FINSEQ_4: 36

        .= (f . k) by A3, A12, PARTFUN1:def 6;

        then (f . k) <= ((f . m),S) by A20, A23, A35;

        then k <= m by A2;

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

        hence (f . (k + 1)) in ( SUCC ((f . k),S)) by A5, A18, A11, A10, A20, A24;

        let j be Element of NAT ;

        reconsider fk = (f . k), fj = (f . j) as Element of NAT ;

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

        

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

        then

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

        

         A50: 1 in ( dom F) by A48, FINSEQ_3: 25;

        

        then

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

        .= (f . k) by FINSEQ_1: 44;

        assume

         A52: (f . j) in ( SUCC ((f . k),S));

         A53:

        now

          let n be Element of 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

           A54: n = 1 by NAT_1: 25;

          

          then

           A55: (F /. n) = (F . 1) by A50, PARTFUN1:def 6

          .= (f . k) by FINSEQ_1: 44;

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

          .= (f . j) by FINSEQ_1: 44;

          hence (F /. (n + 1)) in ( SUCC ((F /. n),S)) by A52, A55;

        end;

        (F /. ( len F)) = (F . 2) by A48, A49, PARTFUN1:def 6

        .= (f . j) by FINSEQ_1: 44;

        then (f . k) <= ((f . j),S) by A51, A53;

        hence k <= j by A2;

      end;

      assume

       A56: for k be Element of NAT holds (f . (k + 1)) in ( SUCC ((f . k),S)) & for j be Element of NAT st (f . j) in ( SUCC ((f . k),S)) holds k <= j;

      let m,n be Element of NAT ;

      hereby

        assume

         A57: m <= n;

        per cases by A57, XXREAL_0: 1;

          suppose m = n;

          hence (f . m) <= ((f . n),S) by Lm1;

        end;

          suppose

           A58: m < n;

          thus (f . m) <= ((f . n),S)

          proof

            reconsider f9 = f as sequence of NAT ;

            set mn = (n -' m);

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

            consider F be FinSequence of NAT such that

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

             A60: 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 A59;

            take F;

            

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

            then

             A62: 1 in ( dom F) by A59, FINSEQ_3: 25;

            

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

            .= (f . ((m + 1) -' 1)) by A60, A62

            .= (f . m) by NAT_D: 34;

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

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

            then 0 <= (n - m);

            then

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

            

             A64: ( len F) in ( dom F) by A59, A61, FINSEQ_3: 25;

            

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

            .= (f . ((m + (mn + 1)) -' 1)) by A59, A60, A64

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

            .= (f . n) by A63, NAT_D: 34;

            let p be Element of NAT ;

            assume that

             A65: 1 <= p and

             A66: p < ( len F);

            

             A67: p in ( dom F) by A65, A66, FINSEQ_3: 25;

            

            then

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

            .= (f . ((m + p) -' 1)) by A60, A67;

            

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

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

            then

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

            

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

            .= (f . ((m + (p + 1)) -' 1)) by A60, A70

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

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

            hence thesis by A56, A68;

          end;

        end;

      end;

      assume (f . m) <= ((f . n),S);

      then

      consider F be non empty FinSequence of NAT such that

       A71: (F /. 1) = (f . m) and

       A72: (F /. ( len F)) = (f . n) and

       A73: for n be Element of 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 Element of NAT st (F /. $1) = (f . l) & m <= l;

       A74:

      now

        let k be Nat such that

         A75: P[k];

        now

          assume that 1 <= (k + 1) and

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

          per cases ;

            suppose k = 0 ;

            hence ex l be Element of NAT st (F /. (k + 1)) = (f . l) & m <= l by A71;

          end;

            suppose

             A77: k > 0 ;

            ( rng f) = NAT by A1, FUNCT_2:def 3;

            then

            consider l1 be object such that

             A78: l1 in ( dom f) and

             A79: (f . l1) = (F /. (k + 1)) by FUNCT_1:def 3;

            consider l be Element of NAT such that

             A80: (F /. k) = (f . l) and

             A81: m <= l by A75, A76, A77, NAT_1: 13, NAT_1: 14;

            reconsider l1 as Element of NAT by A78;

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

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

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

            then l <= l1 by A56, A80, A79;

            hence ex l be Element of NAT st (F /. (k + 1)) = (f . l) & m <= l by A81, A79, XXREAL_0: 2;

          end;

        end;

        hence P[(k + 1)];

      end;

      

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

      

       A83: P[ 0 ];

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

      then ( dom f) = NAT & ex l be Element of NAT st (F /. ( len F)) = (f . l) & m <= l by A82, FUNCT_2:def 1;

      hence thesis by A1, A72, FUNCT_1:def 4;

    end;

    theorem :: AMI_WSTD:4

    

     Th4: S is weakly_standard iff ex f be sequence of NAT st f is bijective & for k be Element of NAT holds (f . (k + 1)) in ( SUCC ((f . k),S)) & for j be Element of NAT st (f . j) in ( SUCC ((f . k),S)) holds k <= j

    proof

      hereby

        assume S is weakly_standard;

        then

        consider f be sequence of NAT such that

         A1: f is bijective and

         A2: for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S);

        thus ex f be sequence of NAT st f is bijective & for k be Element of NAT holds (f . (k + 1)) in ( SUCC ((f . k),S)) & for j be Element of NAT st (f . j) in ( SUCC ((f . k),S)) holds k <= j

        proof

          take f;

          thus f is bijective by A1;

          thus thesis by A1, A2, Th3;

        end;

      end;

      given f be sequence of NAT such that

       A3: f is bijective and

       A4: for k be Element of NAT holds (f . (k + 1)) in ( SUCC ((f . k),S)) & for j be Element of NAT st (f . j) in ( SUCC ((f . k),S)) holds k <= j;

      take f;

      thus f is bijective by A3;

      thus thesis by A3, A4, Th3;

    end;

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

    begin

    

     Lm2: for i be Instruction of ( STC N), s be State of ( STC N) st ( InsCode i) = 1 holds ( IC ( Exec (i,s))) = (( 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 AMISTD_1:def 7;

      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 AMISTD_1:def 7;

      

       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 AMISTD_1:def 7;

      

       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 AMISTD_1:def 7;

      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 ( IC ( Exec (i,s))) = ((s +* ( 0 .--> (( In ((s . 0 ), NAT )) + 1))) . 0 ) by A9, A8

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

      .= (( IC s) + 1) by A9, A4, FUNCOP_1: 7;

    end;

    

     Lm3: for l be Element of 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 Element of 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

        reconsider f = ( NAT --> i) as Instruction-Sequence of M;

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

        reconsider w = the l -started State of M as Element of ( product ( the_Values_of M)) by CARD_3: 107;

        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, Lm2;

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

        end;

        assume y in {(z + 1)};

        then

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

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

        

        then

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

        .= z by A1, FUNCOP_1: 72;

        then ( IC ( Exec (i,t))) = (z + 1) by A2, Lm2;

        hence y in F by A1, A4, A5;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let N be with_zero set;

      cluster ( STC N) -> weakly_standard;

      coherence

      proof

        reconsider f = ( id NAT ) as sequence of NAT ;

        set M = ( STC N);

        now

          let k be Element of NAT ;

          reconsider fk = (f . k) as Element of NAT ;

          

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

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

          let j be Element of NAT ;

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

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

          then j = (k + 1) or j = k;

          hence k <= j by NAT_1: 11;

        end;

        hence thesis by Th4;

      end;

    end

    registration

      let N be with_zero set;

      cluster weakly_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 weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

    definition

      let N be with_zero set, S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, k be natural Number;

      :: AMI_WSTD:def4

      func il. (S,k) -> Element of NAT means

      : Def4: ex f be sequence of NAT st f is bijective & (for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S)) & it = (f . k);

      existence

      proof

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

        consider f be sequence of NAT such that

         A1: f is bijective & for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),S) by Def3;

        reconsider fk = (f . k) as Element of NAT ;

        take fk;

        take f;

        thus thesis by A1;

      end;

      uniqueness by Th2;

    end

    theorem :: AMI_WSTD:5

    

     Th5: for N, T holds for k1,k2 be Nat st ( il. (T,k1)) = ( il. (T,k2)) holds k1 = k2

    proof

      let N, T;

      let k1,k2 be Nat;

      assume

       A1: ( il. (T,k1)) = ( il. (T,k2));

      

       A2: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;

      consider f2 be sequence of NAT such that

       A3: f2 is bijective & for m,n be Element of NAT holds m <= n iff (f2 . m) <= ((f2 . n),T) and

       A4: ( il. (T,k2)) = (f2 . k2) by Def4;

      consider f1 be sequence of NAT such that

       A5: f1 is bijective and

       A6: for m,n be Element of NAT holds m <= n iff (f1 . m) <= ((f1 . n),T) and

       A7: ( il. (T,k1)) = (f1 . k1) by Def4;

      

       A8: ( dom f1) = NAT by FUNCT_2:def 1;

      f1 = f2 by A5, A6, A3, Th2;

      hence thesis by A1, A2, A5, A7, A4, A8, FUNCT_1:def 4;

    end;

    theorem :: AMI_WSTD:6

    

     Th6: for l be Nat holds ex k be Nat st l = ( il. (T,k))

    proof

      let l be Nat;

      consider f1 be sequence of NAT such that

       A1: f1 is bijective and

       A2: for m,n be Element of NAT holds m <= n iff (f1 . m) <= ((f1 . n),T) and ( il. (T, 0 )) = (f1 . 0 ) by Def4;

      l in NAT & ( rng f1) = NAT by A1, FUNCT_2:def 3, ORDINAL1:def 12;

      then

      consider k be object such that

       A3: k in ( dom f1) and

       A4: (f1 . k) = l by FUNCT_1:def 3;

      reconsider k as Nat by A3;

      take k;

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

      l = ( il. (T,k)) by A1, A2, A4, Def4;

      hence thesis;

    end;

    definition

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

      :: AMI_WSTD:def5

      func locnum (l,S) -> Nat means

      : Def5: ( il. (S,it )) = l;

      existence by Th6;

      uniqueness by Th5;

    end

    definition

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

      :: original: locnum

      redefine

      func locnum (l,S) -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: AMI_WSTD:7

    

     Th7: for l1,l2 be Element of NAT holds ( locnum (l1,T)) = ( locnum (l2,T)) implies l1 = l2

    proof

      let l1,l2 be Element of NAT ;

      assume

       A1: ( locnum (l1,T)) = ( locnum (l2,T));

      ( il. (T,( locnum (l1,T)))) = l1 by Def5;

      hence thesis by A1, Def5;

    end;

    theorem :: AMI_WSTD:8

    

     Th8: for N, T holds for k1,k2 be natural Number holds ( il. (T,k1)) <= (( il. (T,k2)),T) iff k1 <= k2

    proof

      let N, T;

      let k1,k2 be natural Number;

      

       A1: k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12;

      consider f2 be sequence of NAT such that

       A2: f2 is bijective & for m,n be Element of NAT holds m <= n iff (f2 . m) <= ((f2 . n),T) and

       A3: ( il. (T,k2)) = (f2 . k2) by Def4;

      consider f1 be sequence of NAT such that

       A4: f1 is bijective and

       A5: for m,n be Element of NAT holds m <= n iff (f1 . m) <= ((f1 . n),T) and

       A6: ( il. (T,k1)) = (f1 . k1) by Def4;

      f1 = f2 by A4, A5, A2, Th2;

      hence thesis by A1, A5, A6, A3;

    end;

    theorem :: AMI_WSTD:9

    

     Th9: for N, T holds for l1,l2 be Element of NAT holds ( locnum (l1,T)) <= ( locnum (l2,T)) iff l1 <= (l2,T)

    proof

      let N, T;

      let l1,l2 be Element of NAT ;

      ( il. (T,( locnum (l1,T)))) = l1 & ( il. (T,( locnum (l2,T)))) = l2 by Def5;

      hence thesis by Th8;

    end;

    theorem :: AMI_WSTD:10

    

     Th10: for N, T holds T is InsLoc-antisymmetric

    proof

      let N, T;

      let l1,l2 be Element of NAT ;

      assume

       A1: l1 <= (l2,T) & l2 <= (l1,T);

      reconsider T as weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      reconsider l1, l2 as Element of NAT ;

      ( locnum (l1,T)) <= ( locnum (l2,T)) & ( locnum (l2,T)) <= ( locnum (l1,T)) by A1, Th9;

      hence thesis by Th7, XXREAL_0: 1;

    end;

    registration

      let N;

      cluster weakly_standard -> InsLoc-antisymmetric for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      coherence by Th10;

    end

    definition

      let N be with_zero set, S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, f be Element of NAT , k be Nat;

      :: AMI_WSTD:def6

      func f + (k,S) -> Element of NAT equals ( il. (S,(( locnum (f,S)) + k)));

      coherence ;

    end

    theorem :: AMI_WSTD:11

    for f be Element of NAT holds (f + ( 0 ,T)) = f by Def5;

    theorem :: AMI_WSTD:12

    for f,g be Element of NAT st (f + (z,T)) = (g + (z,T)) holds f = g

    proof

      let f,g be Element of NAT ;

      assume (f + (z,T)) = (g + (z,T));

      then (( locnum (f,T)) + z) = (( locnum (g,T)) + z) by Th5;

      hence thesis by Th7;

    end;

    theorem :: AMI_WSTD:13

    for f be Element of NAT holds (( locnum (f,T)) + z) = ( locnum ((f + (z,T)),T)) by Def5;

    definition

      let N be with_zero set, S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, f be Element of NAT ;

      :: AMI_WSTD:def7

      func NextLoc (f,S) -> Element of NAT equals (f + (1,S));

      coherence ;

    end

    theorem :: AMI_WSTD:14

    for f be Element of NAT holds ( NextLoc (f,T)) = ( il. (T,(( locnum (f,T)) + 1)));

    theorem :: AMI_WSTD:15

    

     Th15: for f be Element of NAT holds f <> ( NextLoc (f,T))

    proof

      let f be Element of NAT ;

      assume f = ( NextLoc (f,T));

      then ( locnum (f,T)) = (( locnum (f,T)) + 1) by Def5;

      hence thesis;

    end;

    theorem :: AMI_WSTD:16

    for f,g be Element of NAT st ( NextLoc (f,T)) = ( NextLoc (g,T)) holds f = g

    proof

      let f,g be Element of NAT such that

       A1: ( NextLoc (f,T)) = ( NextLoc (g,T));

      set m = ( locnum (g,T));

      set k = ( locnum (f,T));

      (k + 0 ) = ((k + 1) - 1)

      .= ((m + 1) - 1) by A1, Th5

      .= (m + 0 );

      hence thesis by Th7;

    end;

    theorem :: AMI_WSTD:17

    

     Th17: ( il. (( STC N),z)) = z

    proof

      set M = ( STC N);

      reconsider f2 = ( id NAT ) as sequence of NAT ;

      consider f be sequence of NAT such that

       A1: f is bijective & for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),( STC N)) and

       A2: ( il. (M,z)) = (f . z) by Def4;

      now

        let k be Element of NAT ;

        reconsider fk = (f2 . k) as Element of NAT ;

        

         A3: ( SUCC (fk,( STC N))) = {k, (k + 1)} by AMISTD_1: 8;

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

        let j be Element of NAT ;

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

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

        hence k <= j by NAT_1: 11;

      end;

      then for m,n be Element of NAT holds m <= n iff (f2 . m) <= ((f2 . n),M) by Th3;

      then z is Element of NAT & f = f2 by A1, Th2, ORDINAL1:def 12;

      hence thesis by A2;

    end;

    theorem :: AMI_WSTD:18

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

    proof

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

      set M = ( STC N);

      set k = ( locnum (( IC s),( STC N)));

      reconsider K = ( IC s) as Element of NAT ;

      assume ( InsCode i) = 1;

      

      then

       A1: ( IC ( Exec (i,s))) = (( IC s) + 1) by Lm2

      .= (K + 1);

      ( il. (M,k)) = k & ( il. (M,(k + 1))) = (k + 1) by Th17;

      hence thesis by A1, Def5;

    end;

    theorem :: AMI_WSTD:19

    for l be Element of NAT , i be Element of the InstructionsF of ( STC N) st ( InsCode i) = 1 holds ( NIC (i,l)) = {( NextLoc (l,( STC N)))}

    proof

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

      assume

       A1: ( InsCode i) = 1;

      set M = ( STC N);

      consider k be Nat such that

       A2: l = ( il. (M,k)) by Th6;

      k = ( locnum (l,M)) by A2, Def5;

      then ( NextLoc (l,( STC N))) = (k + 1) by Th17;

      hence thesis by A1, A2, Lm3, Th17;

    end;

    theorem :: AMI_WSTD:20

    for l be Element of NAT holds ( SUCC (l,( STC N))) = {l, ( NextLoc (l,( STC N)))}

    proof

      let l be Element of NAT ;

      set M = ( STC N);

      consider k be Nat such that

       A1: l = ( il. (M,k)) by Th6;

      

       A2: k = ( locnum (l,M)) by A1, Def5;

      

      thus ( SUCC (l,( STC N))) = {k, (k + 1)} by A1, Th17, AMISTD_1: 8

      .= {k, ( il. (M,(k + 1)))} by Th17

      .= {l, ( NextLoc (l,( STC N)))} by A1, A2, Th17;

    end;

    definition

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

      :: AMI_WSTD:def8

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

    end

    theorem :: AMI_WSTD:21

    

     Th21: for S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il be Element of NAT , i be Instruction of S st i is sequential holds ( NIC (i,il)) = {( NextLoc (il,S))}

    proof

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

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

      now

        let x be object;

         A2:

        now

          reconsider il1 = il 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 = ( NextLoc (il,S));

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

          il in NAT ;

          then

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

          

           A5: ((P +* (il,i)) /. il) = ((P +* (il,i)) . il) 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))) = ( NextLoc (il,S)) 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 = ( NextLoc (il,S)) by A1;

        end;

        hence x in {( NextLoc (il,S))} 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;

    theorem :: AMI_WSTD:22

    

     Th22: for S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Instruction of S st i is sequential holds i is non halting

    proof

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

       A1: i is sequential;

      set s = the State of S;

      ( NIC (i,( IC s))) = {( NextLoc (( IC s),S))} by A1, Th21;

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

      hence thesis by AMISTD_1: 2;

    end;

    registration

      let N;

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

      cluster sequential -> non halting for Instruction of S;

      coherence by Th22;

      cluster halting -> non sequential for Instruction of S;

      coherence ;

    end

    begin

    definition

      let N be with_zero set;

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

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

      :: AMI_WSTD:def9

      attr F is para-closed means for s be State of S st ( IC s) = ( il. (S, 0 )) holds for k be Element of NAT holds ( IC ( Comput (F,s,k))) in ( dom F);

    end

    theorem :: AMI_WSTD:23

    

     Th23: for S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F be NAT -definedthe InstructionsF of S -valued finite Function st F is really-closed & ( il. (S, 0 )) in ( dom F) holds F is para-closed by AMISTD_1: 14;

    theorem :: AMI_WSTD:24

    

     Th24: for S be weakly_standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds (( il. (S, 0 )) .--> ( halt S)) qua NAT -definedthe InstructionsF of S -valued finite Function is really-closed

    proof

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

      reconsider F = (( il. (S, 0 )) .--> ( halt S)) as NAT -definedthe InstructionsF of S -valued finite Function;

      let l be Nat;

      assume

       A1: l in ( dom (( il. (S, 0 )) .--> ( halt S)));

      

       A3: l = ( il. (S, 0 )) by A1, TARSKI:def 1;

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

      .= ( halt S) by A3, FUNCOP_1: 72;

      hence thesis by A3, AMISTD_1: 2;

    end;

    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 the InstructionsF of S -valued NAT -defined finite Function;

      :: AMI_WSTD:def10

      attr F is lower means

      : Def10: for l be Element of NAT st l in ( dom F) holds for m be Element of NAT st m <= (l,S) holds m in ( dom F);

    end

    registration

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

      cluster empty -> lower for finitethe InstructionsF of S -valued NAT -defined Function;

      coherence ;

    end

    theorem :: AMI_WSTD:25

    

     Th25: for i be Element of the InstructionsF of T holds (( il. (T, 0 )) .--> i) is lower

    proof

      let i be Element of the InstructionsF of T;

      set F = (( il. (T, 0 )) .--> i);

      let l be Element of NAT such that

       A1: l in ( dom F);

      let m be Element of NAT such that

       A2: m <= (l,T);

      consider k be Nat such that

       A3: m = ( il. (T,k)) by Th6;

      

       A4: l = ( il. (T, 0 )) by A1, TARSKI:def 1;

      then 0 <= k & k <= 0 by A2, A3, Th8;

      hence thesis by A1, A4, A3, XXREAL_0: 1;

    end;

    registration

      let N be with_zero set;

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

      cluster lower1 -element for NAT -definedthe InstructionsF of S -valued finite Function;

      existence

      proof

        set i = the Instruction of S;

        take (( il. (S, 0 )) .--> i);

        thus thesis by Th25;

      end;

    end

    theorem :: AMI_WSTD:26

    

     Th26: for F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function holds ( il. (T, 0 )) in ( dom F)

    proof

      let F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function;

      consider l be object such that

       A1: l in ( dom F) by XBOOLE_0:def 1;

      reconsider l as Element of NAT by A1;

      consider f be sequence of NAT such that

       A2: f is bijective and

       A3: for m,n be Element of NAT holds m <= n iff (f . m) <= ((f . n),T) and

       A4: ( il. (T, 0 )) = (f . 0 ) by Def4;

      ( rng f) = NAT by A2, FUNCT_2:def 3;

      then

      consider x be object such that

       A5: x in ( dom f) and

       A6: l = (f . x) by FUNCT_1:def 3;

      reconsider x as Element of NAT by A5;

      (f . 0 ) <= ((f . x),T) by A3;

      hence thesis by A1, A4, A6, Def10;

    end;

    theorem :: AMI_WSTD:27

    

     Th27: for P be lower NAT -definedthe InstructionsF of T -valued finite Function holds z < ( card P) iff ( il. (T,z)) in ( dom P)

    proof

      let P be lower NAT -definedthe InstructionsF of T -valued finite Function;

      deffunc F( Element of NAT ) = ( il. (T,$1));

      defpred P[ Element of NAT ] means F($1) in ( dom P);

      set A = { k : P[k] };

      

       A1: A is Subset of NAT from DOMAIN_1:sch 7;

       A2:

      now

        let a,b be Nat;

        assume a in A;

        then

         A3: ex l be Element of NAT st l = a & ( il. (T,l)) in ( dom P);

        

         A4: b in NAT by ORDINAL1:def 12;

        assume b < a;

        then ( il. (T,b)) <= (( il. (T,a)),T) by Th8;

        then ( il. (T,b)) in ( dom P) by A3, Def10;

        hence b in A by A4;

      end;

       A5:

      now

        let x be set;

        assume x in ( dom P);

        then

        reconsider l = x as Element of NAT ;

        consider n be Nat such that

         A6: l = ( il. (T,n)) by Th6;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        take n;

        thus x = F(n) by A6;

      end;

      reconsider A as Cardinal by A1, A2, FUNCT_7: 20;

      set A1 = { k : F(k) in ( dom P) };

      

       A7: z is Element of NAT by ORDINAL1:def 12;

      

       A8: for k1,k2 be Element of NAT st F(k1) = F(k2) holds k1 = k2 by Th5;

      

       A9: (( dom P),A1) are_equipotent from FUNCT_7:sch 3( A5, A8);

      hereby

        assume z < ( card P);

        then ( card ( Segm z)) in ( card ( Segm ( card P))) by NAT_1: 41;

        then z in ( card ( dom P)) by CARD_1: 62;

        then z in ( card A) by A9, CARD_1: 5;

        then ex d be Element of NAT st d = z & ( il. (T,d)) in ( dom P);

        hence ( il. (T,z)) in ( dom P);

      end;

      assume ( il. (T,z)) in ( dom P);

      then z in ( card A) by A7;

      then z in ( card ( dom P)) by A9, CARD_1: 5;

      then ( card ( Segm z)) in ( card ( Segm ( card P))) by CARD_1: 62;

      hence thesis by NAT_1: 41;

    end;

    definition

      let N be with_zero set;

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

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

      :: AMI_WSTD:def11

      func LastLoc F -> Element of NAT means

      : Def11: ex M be finite non empty natural-membered set st M = { ( locnum (l,S)) where l be Element of NAT : l in ( dom F) } & it = ( il. (S,( max M)));

      existence

      proof

        deffunc F( Element of NAT ) = ( locnum ($1,S));

        set M = { F(l) where l be Element of NAT : l in ( dom F) };

        set l = the Element of ( dom F);

        reconsider l as Element of NAT ;

        

         A1: ( locnum (l,S)) in M;

        

         A2: M c= NAT

        proof

          let k be object;

          assume k in M;

          then ex l be Element of NAT st k = ( locnum (l,S)) & l in ( dom F);

          hence thesis;

        end;

        

         A3: ( dom F) is finite;

        M is finite from FRAENKEL:sch 21( A3);

        then

        reconsider M as finite non empty Subset of NAT by A1, A2;

        take ( il. (S,( max M))), M;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: AMI_WSTD:28

    

     Th28: for F be non empty NAT -definedthe InstructionsF of T -valued finite Function holds ( LastLoc F) in ( dom F)

    proof

      let F be non empty NAT -definedthe InstructionsF of T -valued finite Function;

      consider M be finite non empty natural-membered set such that

       A1: M = { ( locnum (l,T)) where l be Element of NAT : l in ( dom F) } and

       A2: ( LastLoc F) = ( il. (T,( max M))) by Def11;

      ( max M) in M by XXREAL_2:def 8;

      then ex l be Element of NAT st ( max M) = ( locnum (l,T)) & l in ( dom F) by A1;

      hence thesis by A2, Def5;

    end;

    theorem :: AMI_WSTD:29

    for F,G be non empty NAT -definedthe InstructionsF of T -valued finite Function st F c= G holds ( LastLoc F) <= (( LastLoc G),T)

    proof

      let F,G be non empty NAT -definedthe InstructionsF of T -valued finite Function such that

       A1: F c= G;

      consider N be finite non empty natural-membered set such that

       A2: N = { ( locnum (l,T)) where l be Element of NAT : l in ( dom G) } and

       A3: ( LastLoc G) = ( il. (T,( max N))) by Def11;

      consider M be finite non empty natural-membered set such that

       A4: M = { ( locnum (l,T)) where l be Element of NAT : l in ( dom F) } and

       A5: ( LastLoc F) = ( il. (T,( max M))) by Def11;

      reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED: 3;

      M c= N

      proof

        let a be object;

        assume a in M;

        then

         A6: ex l be Element of NAT st a = ( locnum (l,T)) & l in ( dom F) by A4;

        ( dom F) c= ( dom G) by A1, GRFUNC_1: 2;

        hence thesis by A2, A6;

      end;

      then ( max MM) <= ( max NN) by XXREAL_2: 59;

      hence thesis by A5, A3, Th8;

    end;

    theorem :: AMI_WSTD:30

    

     Th30: for F be non empty NAT -definedthe InstructionsF of T -valued finite Function, l be Element of NAT st l in ( dom F) holds l <= (( LastLoc F),T)

    proof

      let F be non empty NAT -definedthe InstructionsF of T -valued finite Function, l be Element of NAT such that

       A1: l in ( dom F);

      consider M be finite non empty natural-membered set such that

       A2: M = { ( locnum (w,T)) where w be Element of NAT : w in ( dom F) } and

       A3: ( LastLoc F) = ( il. (T,( max M))) by Def11;

      ( locnum (l,T)) in M by A1, A2;

      then

       A4: ( locnum (l,T)) <= ( max M) by XXREAL_2:def 8;

      ( max M) is Nat by TARSKI: 1;

      then ( locnum (( LastLoc F),T)) = ( max M) by A3, Def5;

      hence thesis by A4, Th9;

    end;

    theorem :: AMI_WSTD:31

    for F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function, G be non empty NAT -defined NAT -definedthe InstructionsF of T -valued finite Function holds F c= G & ( LastLoc F) = ( LastLoc G) implies F = G

    proof

      let F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function, G be non empty NAT -definedthe InstructionsF of T -valued finite Function such that

       A1: F c= G and

       A2: ( LastLoc F) = ( LastLoc G);

      ( dom F) = ( dom G)

      proof

        thus ( dom F) c= ( dom G) by A1, GRFUNC_1: 2;

        let x be object;

        assume

         A3: x in ( dom G);

        reconsider x as Element of NAT by A3;

        

         A4: ( LastLoc F) in ( dom F) by Th28;

        x <= (( LastLoc F),T) by A2, A3, Th30;

        hence thesis by A4, Def10;

      end;

      hence thesis by A1, GRFUNC_1: 3;

    end;

    theorem :: AMI_WSTD:32

    

     Th32: for F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function holds ( LastLoc F) = ( il. (T,(( card F) -' 1)))

    proof

      let F be lower non empty NAT -definedthe InstructionsF of T -valued finite Function;

      consider k be Nat such that

       A1: ( LastLoc F) = ( il. (T,k)) by Th6;

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

      ( LastLoc F) in ( dom F) by Th28;

      then k < ( card F) by A1, Th27;

      then

       A2: k <= (( card F) -' 1) by NAT_D: 49;

      per cases by A2, XXREAL_0: 1;

        suppose k < (( card F) -' 1);

        then (k + 1) < ((( card F) -' 1) + 1) by XREAL_1: 6;

        then (k + 1) < ( card F) by NAT_1: 14, XREAL_1: 235;

        then ( il. (T,(k + 1))) in ( dom F) by Th27;

        then ( il. (T,(k + 1))) <= (( LastLoc F),T) by Th30;

        then

         A3: (k + 1) <= k by A1, Th8;

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

        then (k + 0 ) = (k + 1) by A3, XXREAL_0: 1;

        hence thesis;

      end;

        suppose k = (( card F) -' 1);

        hence thesis by A1;

      end;

    end;

    registration

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

      cluster really-closed lower non empty -> para-closed for NAT -definedthe InstructionsF of S -valued finite Function;

      coherence by Th26, Th23;

    end

     Lm4:

    now

      let N;

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

      set F = (( il. (S, 0 )) .--> ( halt S));

      

       A1: ( card ( dom F)) = 1 by CARD_1: 30;

      F is lower NAT -definedthe InstructionsF of S -valued finite Function by Th25;

      

      then

       A2: ( LastLoc F) = ( il. (S,(( card F) -' 1))) by Th32

      .= ( il. (S,(( card ( dom F)) -' 1))) by CARD_1: 62

      .= ( il. (S, 0 )) by A1, XREAL_1: 232;

      hence (F . ( LastLoc F)) = ( halt S) by FUNCOP_1: 72;

      let l be Element of NAT such that (F . l) = ( halt S);

      assume l in ( dom F);

      hence l = ( LastLoc F) by A2, TARSKI:def 1;

    end;

    definition

      let N be with_zero set, S be weakly_standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F be non empty NAT -definedthe InstructionsF of S -valued finite Function;

      :: AMI_WSTD:def12

      attr F is halt-ending means

      : Def12: (F . ( LastLoc F)) = ( halt S);

      :: AMI_WSTD:def13

      attr F is unique-halt means

      : Def13: for f be Element of NAT st (F . f) = ( halt S) & f in ( dom F) holds f = ( LastLoc F);

    end

    registration

      let N be with_zero set;

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

      cluster halt-ending unique-halt trivial for lower non empty NAT -definedthe InstructionsF of S -valued finite Function;

      existence

      proof

        reconsider F = (( il. (S, 0 )) .--> ( halt S)) as lower non empty NAT -definedthe InstructionsF of S -valued finite Function by Th25;

        take F;

        thus (F . ( LastLoc F)) = ( halt S) by Lm4;

        thus for f be Element of NAT st (F . f) = ( halt S) & f in ( dom F) holds f = ( LastLoc F) by Lm4;

        thus thesis;

      end;

    end

    registration

      let N be with_zero set;

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

      cluster trivial really-closed lower non empty for NAT -definedthe InstructionsF of S -valued finite Function;

      existence

      proof

        reconsider F = (( il. (S, 0 )) .--> ( halt S)) as lower non empty NAT -definedthe InstructionsF of S -valued finite Function by Th25;

        take F;

        thus thesis by Th24;

      end;

    end

    registration

      let N be with_zero set;

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

      cluster halt-ending unique-halt trivial really-closed for lower non empty NAT -definedthe InstructionsF of S -valued finite Function;

      existence

      proof

        reconsider F = (( il. (S, 0 )) .--> ( halt S)) as lower non empty NAT -definedthe InstructionsF of S -valued finite Function by Th25;

        take F;

        thus (F . ( LastLoc F)) = ( halt S) by Lm4;

        thus for f be Element of NAT st (F . f) = ( halt S) & f in ( dom F) holds f = ( LastLoc F) by Lm4;

        thus thesis by Th24;

      end;

    end

    definition

      let N be with_zero set;

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

      mode pre-Macro of S is halt-ending unique-halt lower non empty NAT -definedthe InstructionsF of S -valued finite Function;

    end

    registration

      let N be with_zero set;

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

      cluster really-closed for pre-Macro of S;

      existence

      proof

        reconsider F = (( il. (S, 0 )) .--> ( halt S)) as lower non empty NAT -definedthe InstructionsF of S -valued finite Function by Th25;

        (F . ( LastLoc F)) = ( halt S) & for l be Element of NAT st (F . l) = ( halt S) & l in ( dom F) holds l = ( LastLoc F) by Lm4;

        then

        reconsider F as pre-Macro of S by Def12, Def13;

        take F;

        thus thesis by Th24;

      end;

    end

    theorem :: AMI_WSTD:33

    for N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, l1,l2 be Element of NAT st ( SUCC (l1,S)) = NAT holds l1 <= (l2,S)

    proof

      let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, l1,l2 be Element of NAT such that

       A1: ( SUCC (l1,S)) = NAT ;

      defpred P[ set, set] means ($1 = 1 implies $2 = l1) & ($1 = 2 implies $2 = l2);

      

       A2: for n be Nat st n in ( Seg 2) holds ex d be Element of NAT st P[n, d]

      proof

        let n be Nat;

        assume

         A3: n in ( Seg 2);

        per cases by A3, FINSEQ_1: 2, TARSKI:def 2;

          suppose

           A4: n = 1;

          reconsider l1 as Element of NAT ;

          take l1;

          thus thesis by A4;

        end;

          suppose

           A5: n = 2;

          reconsider l2 as Element of NAT ;

          take l2;

          thus thesis by A5;

        end;

      end;

      consider f be FinSequence of NAT such that

       A6: ( len f) = 2 and

       A7: for n be Nat st n in ( Seg 2) holds P[n, (f /. n)] from FINSEQ_4:sch 1( A2);

      

       A8: 1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

      then

       A9: (f /. 1) = l1 by A7;

      reconsider f as non empty FinSequence of NAT by A6;

      take f;

      2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

      hence (f /. 1) = l1 & (f /. ( len f)) = l2 by A6, A7, A8;

      let n be Element of NAT ;

      assume

       A10: 1 <= n;

      assume n < ( len f);

      then n < (1 + 1) by A6;

      then n <= 1 by NAT_1: 13;

      then n = 1 by A10, XXREAL_0: 1;

      hence thesis by A1, A9;

    end;

    reserve i,j,k for Nat,

n for Element of NAT ,

N for with_zero set,

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

l for Element of NAT ,

f for FinPartState of S;

    definition

      let N be with_zero set, S be weakly_standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, loc be Element of NAT , k be Nat;

      :: AMI_WSTD:def14

      func loc -' (k,S) -> Element of NAT equals ( il. (S,(( locnum (loc,S)) -' k)));

      coherence ;

    end

    theorem :: AMI_WSTD:34

    (l -' ( 0 ,S)) = l by NAT_D: 40, Def5;

    theorem :: AMI_WSTD:35

    ((l + (k,S)) -' (k,S)) = l

    proof

      

      thus ((l + (k,S)) -' (k,S)) = ( il. (S,((( locnum (l,S)) + k) -' k))) by Def5

      .= ( il. (S,( locnum (l,S)))) by NAT_D: 34

      .= l by Def5;

    end;