extpro_1.miz



    begin

    definition

      let N be set;

      struct ( Mem-Struct over N, COM-Struct) AMI-Struct over N (# the carrier -> set,

the ZeroF -> Element of the carrier,

the InstructionsF -> Instructions,

the Object-Kind -> Function of the carrier, N,

the ValuesF -> ManySortedSet of N,

the Execution -> Action of the InstructionsF, ( product ( the ValuesF * the Object-Kind)) #)

       attr strict strict;

    end

    reserve N for with_zero set;

    definition

      let N;

      :: EXTPRO_1:def1

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

      : Def1: the carrier of it = { 0 } & the ZeroF of it = 0 & the InstructionsF of it = { [ 0 , {} , {} ]} & the Object-Kind of it = ( 0 .--> 0 ) & the ValuesF of it = (N --> NAT ) & the Execution of it = ( [ 0 , {} , {} ] .--> ( id ( product ((N --> NAT ) * ( 0 .--> 0 )))));

      existence

      proof

        set I = { [ 0 , {} , {} ]};

        reconsider i = [ 0 , {} , {} ] as Element of I by TARSKI:def 1;

        set f = ( 0 .--> 0 );

        

         A1: ( dom f) = ( dom ( 0 .--> 0 ))

        .= { 0 };

        

         A2: ( rng f) c= { 0 } by FUNCOP_1: 13;

         0 in N by MEASURE6:def 2;

        then { 0 } c= N by ZFMISC_1: 31;

        then ( rng f) c= N by A2, XBOOLE_1: 1;

        then

        reconsider f as Function of { 0 }, N by A1, RELSET_1: 4;

        reconsider y = 0 as Element of { 0 } by TARSKI:def 1;

        set E = ( id ( product ((N --> NAT ) * f)));

        E in ( Funcs (( product ((N --> NAT ) * f)),( product ((N --> NAT ) * f)))) by FUNCT_2: 9;

        then

        reconsider F = (I --> E) as Action of I, ( product ((N --> NAT ) * f)) by FUNCOP_1: 45;

        take AMI-Struct (# { 0 }, y, I, f, (N --> NAT ), F #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let N;

      cluster ( Trivial-AMI N) -> 1 -element;

      coherence by Def1;

    end

    registration

      let N;

      cluster non empty for AMI-Struct over N;

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    registration

      let N;

      cluster ( Trivial-AMI N) -> with_non-empty_values;

      coherence

      proof

        let n be object;

        set S = ( Trivial-AMI 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 Def1;

        then

         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;

      cluster with_non-empty_values1 -element for AMI-Struct over N;

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    definition

      let N;

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

      let I be Instruction of S, s be State of S;

      :: EXTPRO_1:def2

      func Exec (I,s) -> State of S equals ((the Execution of S . I) . s);

      coherence

      proof

        consider f be Function such that

         A1: (the Execution of S . I) = f & ( dom f) = ( product ( the_Values_of S)) and

         A2: ( rng f) c= ( product ( the_Values_of S)) by FUNCT_2:def 2;

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

        ((the Execution of S . I) . s) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A2;

      end;

    end

    reserve N for with_zero set;

    definition

      let N;

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

      let I be Instruction of S;

      :: EXTPRO_1:def3

      attr I is halting means

      : Def3: for s be State of S holds ( Exec (I,s)) = s;

    end

    definition

      let N;

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

      :: EXTPRO_1:def4

      attr S is halting means

      : Def4: ( halt S) is halting;

    end

    registration

      let N;

      cluster ( Trivial-AMI N) -> halting;

      coherence

      proof

        set T = ( Trivial-AMI N);

        set f = ((N --> NAT ) * ( 0 .--> 0 ));

        

         A1: the Object-Kind of T = ( 0 .--> 0 ) & the ValuesF of T = (N --> NAT ) by Def1;

        set I = ( halt T);

        let s be State of T;

        reconsider ss = s as Element of ( product ( the_Values_of T)) by CARD_3: 107;

        ((I .--> ( id ( product f))) . I) = ( id ( product f)) by FUNCOP_1: 72;

        

        hence ( Exec (I,s)) = (( id ( product f)) . ss) by Def1

        .= s by A1;

      end;

    end

    registration

      let N;

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

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    registration

      let N;

      let S be halting with_non-empty_values AMI-Struct over N;

      cluster ( halt S) -> halting;

      coherence by Def4;

    end

    registration

      let N;

      let S be halting with_non-empty_values AMI-Struct over N;

      cluster halting for Instruction of S;

      existence

      proof

        take ( halt S);

        thus thesis;

      end;

    end

    theorem :: EXTPRO_1:1

    for s be State of ( Trivial-AMI N), i be Instruction of ( Trivial-AMI N) holds ( Exec (i,s)) = s

    proof

      set T = ( Trivial-AMI N);

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

      set f = ((N --> NAT ) * ( 0 .--> 0 ));

      

       A1: the Object-Kind of T = ( 0 .--> 0 ) & the ValuesF of T = (N --> NAT ) by Def1;

      reconsider ss = s as Element of ( product ( the_Values_of T)) by CARD_3: 107;

      the InstructionsF of T = { [ 0 , {} , {} ]} by Def1;

      then ((i .--> ( id ( product f))) . i) = ( id ( product f)) & i = [ 0 , {} , {} ] by FUNCOP_1: 72, TARSKI:def 1;

      

      hence ( Exec (i,s)) = (( id ( product f)) . ss) by Def1

      .= s by A1;

    end;

    registration

      let E be with_zero set;

      cluster ( Trivial-AMI E) -> IC-Ins-separated;

      coherence

      proof

        set S = ( Trivial-AMI E);

        

         A1: the Object-Kind of ( Trivial-AMI E) = ( 0 .--> 0 ) & the ValuesF of ( Trivial-AMI E) = (E --> NAT ) by Def1;

        

         A2: 0 in E by MEASURE6:def 2;

        

         A3: 0 in ( dom ( 0 .--> 0 )) by FUNCOP_1: 73;

        

        thus ( Values ( IC ( Trivial-AMI E))) = (( the_Values_of ( Trivial-AMI E)) . 0 ) by Def1

        .= (((E --> NAT ) * ( 0 .--> 0 )) . 0 ) by A1

        .= ((E --> NAT ) . (( 0 .--> 0 ) . 0 )) by A3, FUNCT_1: 13

        .= ((E --> NAT ) . 0 ) by FUNCOP_1: 72

        .= NAT by A2, FUNCOP_1: 7;

      end;

    end

    registration

      let M be with_zero set;

      cluster IC-Ins-separated strict trivial for non empty with_non-empty_values AMI-Struct over M;

      existence

      proof

        take ( Trivial-AMI M);

        thus thesis;

      end;

    end

    registration

      let N;

      cluster IC-Ins-separated halting strict for 1 -element with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    begin

    reserve x,y,z,A,B for set,

f,g,h for Function,

i,j,k for Nat;

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

s for State of S;

    definition

      let N, S;

      let p be the InstructionsF of S -valued Function;

      let s be State of S;

      :: EXTPRO_1:def5

      func CurInstr (p,s) -> Instruction of S equals (p /. ( IC s));

      coherence ;

    end

    definition

      let N, S;

      let s be State of S;

      let p be the InstructionsF of S -valued Function;

      :: EXTPRO_1:def6

      func Following (p,s) -> State of S equals ( Exec (( CurInstr (p,s)),s));

      correctness ;

    end

    definition

      let N, S;

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

      deffunc F( set, State of S) = ( down ( Following (p,$2)));

      let s be State of S, k be Nat;

      :: EXTPRO_1:def7

      func Comput (p,s,k) -> State of S means

      : Def7: ex f be sequence of ( product ( the_Values_of S)) st it = (f . k) & (f . 0 ) = s & for i be Nat holds (f . (i + 1)) = ( Following (p,(f . i)));

      existence

      proof

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

        consider f be sequence of ( product ( the_Values_of S)) such that

         A1: (f . 0 ) = ss and

         A2: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 12;

        take (f . k), f;

        thus (f . k) = (f . k);

        thus (f . 0 ) = s by A1;

        let i be Nat;

        

        thus (f . (i + 1)) = F(i,.) by A2

        .= ( Following (p,(f . i)));

      end;

      uniqueness

      proof

        let s1,s2 be State of S;

        given f1 be sequence of ( product ( the_Values_of S)) such that

         A3: s1 = (f1 . k) and

         A4: (f1 . 0 ) = s and

         A5: for i be Nat holds (f1 . (i + 1)) = ( Following (p,(f1 . i)));

        given f2 be sequence of ( product ( the_Values_of S)) such that

         A6: s2 = (f2 . k) and

         A7: (f2 . 0 ) = s and

         A8: for i be Nat holds (f2 . (i + 1)) = ( Following (p,(f2 . i)));

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

        

         A9: (f1 . 0 ) = s by A4;

        

         A10: for i be Nat holds (f1 . (i + 1)) = F(i,.) by A5;

        

         A11: (f2 . 0 ) = s by A7;

        

         A12: for i be Nat holds (f2 . (i + 1)) = F(i,.) by A8;

        f1 = f2 from NAT_1:sch 16( A9, A10, A11, A12);

        hence thesis by A3, A6;

      end;

    end

    definition

      let N;

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

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

      let s be State of S;

      :: EXTPRO_1:def8

      pred p halts_on s means ex k be Nat st ( IC ( Comput (p,s,k))) in ( dom p) & ( CurInstr (p,( Comput (p,s,k)))) = ( halt S);

    end

    registration

      let N be non empty with_zero set;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S;

      reduce ( Comput (p,s, 0 )) to s;

      reducibility

      proof

        ex f be sequence of ( product ( the_Values_of S)) st ( Comput (p,s, 0 )) = (f . 0 ) & (f . 0 ) = s & for i be Nat holds (f . (i + 1)) = ( Following (p,(f . i))) by Def7;

        hence thesis;

      end;

    end

    theorem :: EXTPRO_1:2

    for N be non empty with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S holds ( Comput (p,s, 0 )) = s;

    theorem :: EXTPRO_1:3

    

     Th3: for N be non empty with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S, k be Nat holds ( Comput (p,s,(k + 1))) = ( Following (p,( Comput (p,s,k))))

    proof

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S, k be Nat;

      deffunc F( set, State of S) = ( down ( Following (p,$2)));

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

      consider f be sequence of ( product ( the_Values_of S)) such that

       A1: ( Comput (p,s,(k + 1))) = (f . (k + 1)) and

       A2: (f . 0 ) = s and

       A3: for i be Nat holds (f . (i + 1)) = ( Following (p,(f . i))) by Def7;

      consider g be sequence of ( product ( the_Values_of S)) such that

       A4: ( Comput (p,s,k)) = (g . k) and

       A5: (g . 0 ) = s and

       A6: for i be Nat holds (g . (i + 1)) = ( Following (p,(g . i))) by Def7;

      

       A7: for i be Nat holds (f . (i + 1)) = F(i,.) by A3;

      

       A8: for i be Nat holds (g . (i + 1)) = F(i,.) by A6;

      f = g from NAT_1:sch 16( A2, A7, A5, A8);

      hence thesis by A1, A4, A6;

    end;

    reserve N for non empty with_zero set,

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

s for State of S;

    theorem :: EXTPRO_1:4

    

     Th4: for p be NAT -definedthe InstructionsF of S -valued Function holds for k holds ( Comput (p,s,(i + k))) = ( Comput (p,( Comput (p,s,i)),k))

    proof

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

      defpred P[ Nat] means ( Comput (p,s,(i + $1))) = ( Comput (p,( Comput (p,s,i)),$1));

       A1:

      now

        let k;

        assume

         A2: P[k];

        ( Comput (p,s,(i + (k + 1)))) = ( Comput (p,s,((i + k) + 1)))

        .= ( Following (p,( Comput (p,s,(i + k))))) by Th3

        .= ( Comput (p,( Comput (p,s,i)),(k + 1))) by A2, Th3;

        hence P[(k + 1)];

      end;

      

       A3: P[ 0 ];

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

    end;

    theorem :: EXTPRO_1:5

    

     Th5: i <= j implies for N holds for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for p be NAT -definedthe InstructionsF of S -valued Function holds for s be State of S st ( CurInstr (p,( Comput (p,s,i)))) = ( halt S) holds ( Comput (p,s,j)) = ( Comput (p,s,i))

    proof

      assume i <= j;

      then

      consider k be Nat such that

       A1: j = (i + k) by NAT_1: 10;

      reconsider k as Nat;

      

       A2: j = (i + k) by A1;

      let N;

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

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

      let s be State of S such that

       A3: ( CurInstr (p,( Comput (p,s,i)))) = ( halt S);

      defpred P[ Nat] means ( Comput (p,s,(i + $1))) = ( Comput (p,s,i));

       A4:

      now

        let k;

        assume

         A5: P[k];

        ( Comput (p,s,(i + (k + 1)))) = ( Comput (p,s,((i + k) + 1)))

        .= ( Following (p,( Comput (p,s,(i + k))))) by Th3

        .= ( Comput (p,s,i)) by A3, A5, Def3;

        hence P[(k + 1)];

      end;

      

       A6: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A6, A4);

      hence thesis by A2;

    end;

    reserve n for Nat;

    definition

      let N;

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

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

      let s be State of S;

      :: EXTPRO_1:def9

      func Result (p,s) -> State of S means

      : Def9: ex k st it = ( Comput (p,s,k)) & ( CurInstr (p,it )) = ( halt S);

      uniqueness

      proof

        let s1,s2 be State of S;

        given k1 be Nat such that

         A2: s1 = ( Comput (p,s,k1)) & ( CurInstr (p,s1)) = ( halt S);

        given k2 be Nat such that

         A3: s2 = ( Comput (p,s,k2)) & ( CurInstr (p,s2)) = ( halt S);

        k1 <= k2 or k2 <= k1;

        hence thesis by A2, A3, Th5;

      end;

      correctness by A1;

    end

    theorem :: EXTPRO_1:6

    for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for P be Instruction-Sequence of S holds for s be State of S holds ( Comput (P,s,(k + 1))) = ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k))))

    proof

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

      let P be Instruction-Sequence of S;

      let s be State of S;

      

       A1: ( dom P) = NAT by PARTFUN1:def 2;

      

      thus ( Comput (P,s,(k + 1))) = ( Following (P,( Comput (P,s,k)))) by Th3

      .= ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k)))) by A1, PARTFUN1:def 6;

    end;

    theorem :: EXTPRO_1:7

    

     Th7: for S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N holds for P be Instruction-Sequence of S holds for s be State of S, k st (P . ( IC ( Comput (P,s,k)))) = ( halt S) holds ( Result (P,s)) = ( Comput (P,s,k))

    proof

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

      let P be Instruction-Sequence of S;

      let s be State of S, k;

      

       A1: ( dom P) = NAT by PARTFUN1:def 2;

      assume (P . ( IC ( Comput (P,s,k)))) = ( halt S);

      then

       A2: ( CurInstr (P,( Comput (P,s,k)))) = ( halt S) by A1, PARTFUN1:def 6;

      then P halts_on s by A1;

      hence thesis by A2, Def9;

    end;

    theorem :: EXTPRO_1:8

    

     Th8: for S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N holds for P be Instruction-Sequence of S holds for s be State of S st ex k st (P . ( IC ( Comput (P,s,k)))) = ( halt S) holds for i holds ( Result (P,s)) = ( Result (P,( Comput (P,s,i))))

    proof

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

      let P be Instruction-Sequence of S;

      let s be State of S;

      given k such that

       A1: (P . ( IC ( Comput (P,s,k)))) = ( halt S);

      let i;

      

       A2: ( dom P) = NAT by PARTFUN1:def 2;

      set s9 = ( Comput (P,s,k));

      

       A3: ( CurInstr (P,s9)) = ( halt S) by A1, A2, PARTFUN1:def 6;

      now

        per cases ;

          suppose i <= k;

          then

          consider j be Nat such that

           A4: k = (i + j) by NAT_1: 10;

          reconsider j as Nat;

          

           A5: ( Comput (P,s,k)) = ( Comput (P,( Comput (P,s,i)),j)) by A4, Th4;

          

           A6: P halts_on ( Comput (P,s,i)) by A3, A5, A2;

          

          thus ( Result (P,s)) = s9 by A1, Th7

          .= ( Result (P,( Comput (P,s,i)))) by A3, A5, A6, Def9;

        end;

          suppose

           A7: i >= k;

          

           A8: ( Comput (P,( Comput (P,s,k)), 0 )) = ( Comput (P,s,k));

          

           A9: ( Comput (P,s,i)) = s9 by A3, A7, Th5;

          

           A10: P halts_on ( Comput (P,s,i)) by A2, A9, A3, A8;

          

          thus ( Result (P,s)) = s9 by A1, Th7

          .= ( Result (P,( Comput (P,s,i)))) by A3, A9, A8, A10, Def9;

        end;

      end;

      hence thesis;

    end;

    definition

      let N;

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

      let p be the InstructionsF of S -valued NAT -defined Function;

      let IT be PartState of S;

      :: EXTPRO_1:def10

      attr IT is p -autonomic means for P,Q be Instruction-Sequence of S st p c= P & p c= Q holds for s1,s2 be State of S st IT c= s1 & IT c= s2 holds for i holds (( Comput (P,s1,i)) | ( dom IT)) = (( Comput (Q,s2,i)) | ( dom IT));

    end

    definition

      let N;

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

      let p be the InstructionsF of S -valued NAT -defined Function;

      let IT be PartState of S;

      :: EXTPRO_1:def11

      attr IT is p -halted means for s be State of S st IT c= s holds for P be Instruction-Sequence of S st p c= P holds P halts_on s;

    end

    registration

      let N;

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

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    begin

    theorem :: EXTPRO_1:9

    

     Th9: for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for l be Nat, I be Instruction of S holds for P be NAT -definedthe InstructionsF of S -valued Function st (l .--> I) c= P holds for s be State of S st (( IC S) .--> l) c= s holds ( CurInstr (P,s)) = I

    proof

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

      let l be Nat, I be Instruction of S;

      let P be NAT -definedthe InstructionsF of S -valued Function such that

       A1: (l .--> I) c= P;

      let s be State of S such that

       A2: (( IC S) .--> l) c= s;

      ( IC S) in ( dom (( IC S) .--> l)) by TARSKI:def 1;

      

      then

       A3: ( IC s) = ((( IC S) .--> l) . ( IC S)) by A2, GRFUNC_1: 2

      .= l by FUNCOP_1: 72;

      

       A4: ( IC s) in ( dom (l .--> I)) by A3, TARSKI:def 1;

      ( dom (l .--> I)) c= ( dom P) by A1, RELAT_1: 11;

      

      hence ( CurInstr (P,s)) = (P . ( IC s)) by A4, PARTFUN1:def 6

      .= ((l .--> I) . ( IC s)) by A4, A1, GRFUNC_1: 2

      .= I by A3, FUNCOP_1: 72;

    end;

    theorem :: EXTPRO_1:10

    

     Th10: for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for l be Nat holds for P be NAT -definedthe InstructionsF of S -valued Function st (l .--> ( halt S)) c= P holds for p be l -started PartState of S holds p is P -halted

    proof

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

      let l be Nat;

      let P be NAT -definedthe InstructionsF of S -valued Function such that

       A1: (l .--> ( halt S)) c= P;

      let p be l -started PartState of S;

      set h = ( halt S);

      set I = (p +* P);

      let s be State of S such that

       A2: p c= s;

      let Q be Instruction-Sequence of S such that

       A3: P c= Q;

      take 0 ;

      ( dom Q) = NAT by PARTFUN1:def 2;

      hence ( IC ( Comput (Q,s, 0 ))) in ( dom Q);

      ( Start-At (l,S)) c= p by MEMSTR_0: 29;

      then

       A4: ( Start-At (l,S)) c= s by A2, XBOOLE_1: 1;

      

       A5: (l .--> h) c= Q by A1, A3, XBOOLE_1: 1;

      ( IC S) in ( dom ( Start-At (l,S))) by MEMSTR_0: 15;

      

      then

       A7: ( IC s) = ( IC ( Start-At (l,S))) by A4, GRFUNC_1: 2

      .= l by FUNCOP_1: 72;

      

       A8: ( IC s) in ( dom (l .--> h)) by A7, TARSKI:def 1;

      

       A9: ( dom (l .--> h)) c= ( dom Q) by A5, RELAT_1: 11;

      

      thus ( CurInstr (Q,( Comput (Q,s, 0 )))) = ( CurInstr (Q,s))

      .= (Q . ( IC s)) by A9, A8, PARTFUN1:def 6

      .= ((l .--> h) . ( IC s)) by A8, A5, GRFUNC_1: 2

      .= ( CurInstr ((l .--> h),s)) by A8, PARTFUN1:def 6

      .= ( halt S) by A4, A5, Th9;

    end;

    theorem :: EXTPRO_1:11

    

     Th11: for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for l be Nat holds for P be NAT -definedthe InstructionsF of S -valued Function st (l .--> ( halt S)) c= P holds for p be l -started PartState of S holds for s be State of S st p c= s holds for i holds ( Comput (P,s,i)) = s

    proof

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

      let l be Nat;

      let P be NAT -definedthe InstructionsF of S -valued Function such that

       A1: (l .--> ( halt S)) c= P;

      let p be l -started PartState of S;

      set h = ( halt S);

      let s be State of S such that

       A2: p c= s;

      

       A3: ( Start-At (l,S)) c= p by MEMSTR_0: 29;

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

      

       A4: ( Start-At (l,S)) c= s by A3, A2, XBOOLE_1: 1;

       A5:

      now

        let i;

        assume

         A6: P[i];

        ( Comput (P,s,(i + 1))) = ( Following (P,s)) by A6, Th3

        .= ( Exec (( halt S),s)) by A4, A1, Th9

        .= s by Def3;

        hence P[(i + 1)];

      end;

      

       A7: P[ 0 ];

      thus for i holds P[i] from NAT_1:sch 2( A7, A5);

    end;

    theorem :: EXTPRO_1:12

    

     Th12: for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for l be Nat holds for P be NAT -definedthe InstructionsF of S -valued Function st (l .--> ( halt S)) c= P holds for p be l -started PartState of S holds p is P -autonomic

    proof

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

      let l be Nat;

      set h = ( halt S);

      set p = ( Start-At (l,S));

      let P be NAT -definedthe InstructionsF of S -valued Function such that

       A1: (l .--> ( halt S)) c= P;

      let p be l -started PartState of S;

      set I = (p +* P);

      let Q1,Q2 be Instruction-Sequence of S such that

       A2: P c= Q1 & P c= Q2;

      let s1,s2 be State of S;

      assume that

       A3: p c= s1 and

       A4: p c= s2;

      let i;

      

       A5: (l .--> ( halt S)) c= Q1 & (l .--> ( halt S)) c= Q2 by A1, A2, XBOOLE_1: 1;

      

      hence (( Comput (Q1,s1,i)) | ( dom p)) = (s1 | ( dom p)) by A3, Th11

      .= p by A3, GRFUNC_1: 23

      .= (s2 | ( dom p)) by A4, GRFUNC_1: 23

      .= (( Comput (Q2,s2,i)) | ( dom p)) by A4, Th11, A5;

    end;

    registration

      let N;

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

      let P be non halt-freethe InstructionsF of S -valued NAT -defined Function;

      cluster P -autonomicP -halted non empty for FinPartState of S;

      existence

      proof

        ( halt S) in ( rng P) by COMPOS_1:def 11;

        then

        consider i be object such that

         A1: i in ( dom P) and

         A2: (P . i) = ( halt S) by FUNCT_1:def 3;

        ( dom P) c= NAT by RELAT_1:def 18;

        then

        reconsider i as Nat by A1;

        take p = ( Start-At (i,S));

        (i .--> ( halt S)) c= P by A1, A2, FUNCT_4: 85;

        hence thesis by Th10, Th12;

      end;

    end

    definition

      let N;

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

      let P be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      :: EXTPRO_1:def12

      mode Autonomy of P -> FinPartState of S means

      : Def12: it is P -autonomicP -halted;

      existence

      proof

        ( halt S) in ( rng P) by COMPOS_1:def 11;

        then

        consider x be object such that

         A1: x in ( dom P) and

         A2: (P . x) = ( halt S) by FUNCT_1:def 3;

        ( dom P) c= NAT by RELAT_1:def 18;

        then

        reconsider m = x as Nat by A1;

         [m, ( halt S)] in P by A1, A2, FUNCT_1:def 2;

        then { [m, ( halt S)]} c= P by ZFMISC_1: 31;

        then

         A3: (m .--> ( halt S)) c= P by FUNCT_4: 82;

        take d = ( Start-At (m,S));

        thus d is P -autonomic by A3, Th12;

        thus d is P -halted by A3, Th10;

      end;

    end

    definition

      let N;

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

      let p be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      let d be FinPartState of S;

      assume

       A1: d is Autonomy of p;

      :: EXTPRO_1:def13

      func Result (p,d) -> FinPartState of S means for P be Instruction-Sequence of S st p c= P holds for s be State of S st d c= s holds it = (( Result (P,s)) | ( dom d));

      existence

      proof

        consider h be State of S such that

         A2: d c= h by PBOOLE: 141;

        consider H be Instruction-Sequence of S such that

         A3: p c= H by PBOOLE: 145;

        

         A4: d is p -haltedp -autonomic by A1, Def12;

        then H halts_on h by A2, A3;

        then

        consider k1 be Nat such that

         A5: ( Result (H,h)) = ( Comput (H,h,k1)) and

         A6: ( CurInstr (H,( Result (H,h)))) = ( halt S) by Def9;

        reconsider R = (( Result (H,h)) | ( dom d)) as FinPartState of S;

        take R;

        let P be Instruction-Sequence of S such that

         A7: p c= P;

        let s be State of S;

        assume

         A8: d c= s;

        then P halts_on s by A4, A7;

        then

        consider k2 be Nat such that

         A9: ( Result (P,s)) = ( Comput (P,s,k2)) and

         A10: ( CurInstr (P,( Result (P,s)))) = ( halt S) by Def9;

        per cases ;

          suppose k1 <= k2;

          then ( Result (H,h)) = ( Comput (H,h,k2)) by A5, A6, Th5;

          hence R = (( Result (P,s)) | ( dom d)) by A9, A4, A3, A7, A8, A2;

        end;

          suppose k1 >= k2;

          then ( Result (P,s)) = ( Comput (P,s,k1)) by A9, A10, Th5;

          hence thesis by A5, A4, A3, A7, A8, A2;

        end;

      end;

      correctness

      proof

        consider h be State of S such that

         A11: d c= h by PBOOLE: 141;

        consider H be Instruction-Sequence of S such that

         A12: p c= H by PBOOLE: 145;

        let p1,p2 be FinPartState of S such that

         A13: for P be Instruction-Sequence of S st p c= P holds for s be State of S st d c= s holds p1 = (( Result (P,s)) | ( dom d)) and

         A14: for P be Instruction-Sequence of S st p c= P holds for s be State of S st d c= s holds p2 = (( Result (P,s)) | ( dom d));

        

        thus p1 = (( Result (H,h)) | ( dom d)) by A13, A11, A12

        .= p2 by A14, A11, A12;

      end;

    end

    begin

    definition

      let N;

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

      let p be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      let d be FinPartState of S, F be Function;

      :: EXTPRO_1:def14

      pred p,d computes F means for x be set st x in ( dom F) holds ex s be FinPartState of S st x = s & (d +* s) is Autonomy of p & (F . s) c= ( Result (p,(d +* s)));

    end

    theorem :: EXTPRO_1:13

    for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for p be non halt-free NAT -definedthe InstructionsF of S -valued Function holds for d be FinPartState of S holds (p,d) computes {} ;

    theorem :: EXTPRO_1:14

    for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for p be non halt-free NAT -definedthe InstructionsF of S -valued Function holds for d be FinPartState of S holds d is Autonomy of p iff (p,d) computes ( {} .--> ( Result (p,d)))

    proof

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

      let p be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      let d be FinPartState of S;

      thus d is Autonomy of p implies (p,d) computes ( {} .--> ( Result (p,d)))

      proof

        assume

         A2: d is Autonomy of p;

        let x be set;

        assume

         A3: x in ( dom ( {} .--> ( Result (p,d))));

        then

         A4: x = {} by TARSKI:def 1;

        then

        reconsider s = x as FinPartState of S by FUNCT_1: 104, RELAT_1: 171;

        take s;

        thus x = s;

        (d +* {} ) = d;

        hence (d +* s) is Autonomy of p by A2, A3, TARSKI:def 1;

        thus thesis by A4, FUNCOP_1: 72;

      end;

      

       A5: {} in ( dom ( {} .--> ( Result (p,d)))) by TARSKI:def 1;

      assume (p,d) computes ( {} .--> ( Result (p,d)));

      then ex s be FinPartState of S st {} = s & (d +* s) is Autonomy of p & (( {} .--> ( Result (p,d))) . s) c= ( Result (p,(d +* s))) by A5;

      hence thesis;

    end;

    theorem :: EXTPRO_1:15

    for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for p be non halt-free NAT -definedthe InstructionsF of S -valued Function holds for d be FinPartState of S holds d is Autonomy of p iff (p,d) computes ( {} .--> {} )

    proof

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

      let p be non halt-free NAT -definedthe InstructionsF of S -valued Function;

      let d be FinPartState of S;

      thus d is Autonomy of p implies (p,d) computes ( {} .--> {} )

      proof

        assume

         A2: d is Autonomy of p;

        let x be set;

        assume

         A3: x in ( dom ( {} .--> {} ));

        then x = {} by TARSKI:def 1;

        then

        reconsider s = x as FinPartState of S by FUNCT_1: 104, RELAT_1: 171;

        take s;

        

         A5: (d +* {} ) = d;

        thus x = s;

        thus (d +* s) is Autonomy of p by A2, A3, A5, TARSKI:def 1;

        (( {} .--> {} ) . s) = {} ;

        hence thesis by XBOOLE_1: 2;

      end;

      

       A6: {} in ( dom ( {} .--> {} )) by TARSKI:def 1;

      assume (p,d) computes ( {} .--> {} );

      then ex s be FinPartState of S st {} = s & (d +* s) is Autonomy of p & (( {} .--> {} ) . s) c= ( Result (p,(d +* s))) by A6;

      hence thesis;

    end;

    begin

    registration

      let N;

      cluster IC-Ins-separated for non empty AMI-Struct over N;

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    begin

    reserve N for with_zero non empty set;

    theorem :: EXTPRO_1:16

    

     Th16: for S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S holds p halts_on s iff ex i st p halts_at ( IC ( Comput (p,s,i)))

    proof

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

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

      let s be State of S;

      hereby

        assume p halts_on s;

        then

        consider i be Nat such that

         A1: ( IC ( Comput (p,s,i))) in ( dom p) and

         A2: ( CurInstr (p,( Comput (p,s,i)))) = ( halt S);

        reconsider i as Nat;

        take i;

        (p . ( IC ( Comput (p,s,i)))) = ( halt S) by A1, A2, PARTFUN1:def 6;

        hence p halts_at ( IC ( Comput (p,s,i))) by A1;

      end;

      given i be Nat such that

       A3: p halts_at ( IC ( Comput (p,s,i)));

      

       A4: ( IC ( Comput (p,s,i))) in ( dom p) by A3;

      

       A5: (p . ( IC ( Comput (p,s,i)))) = ( halt S) by A3;

      take i;

      thus ( IC ( Comput (p,s,i))) in ( dom p) by A3;

      thus ( CurInstr (p,( Comput (p,s,i)))) = ( halt S) by A4, A5, PARTFUN1:def 6;

    end;

    theorem :: EXTPRO_1:17

    

     Th17: for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S, k be Nat st p halts_on s holds ( Result (p,s)) = ( Comput (p,s,k)) iff p halts_at ( IC ( Comput (p,s,k)))

    proof

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

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

      let s be State of S, k be Nat;

      assume

       A1: p halts_on s;

      then

      consider n be Nat such that

       A2: ( IC ( Comput (p,s,n))) in ( dom p) and

       A3: ( CurInstr (p,( Comput (p,s,n)))) = ( halt S);

      hereby

        assume

         A4: ( Result (p,s)) = ( Comput (p,s,k));

        consider i be Nat such that

         A5: ( Result (p,s)) = ( Comput (p,s,i)) and

         A6: ( CurInstr (p,( Result (p,s)))) = ( halt S) by A1, Def9;

        reconsider i, n as Nat;

         A7:

        now

          per cases ;

            suppose i <= n;

            hence ( Comput (p,s,i)) = ( Comput (p,s,n)) by A5, A6, Th5;

          end;

            suppose n <= i;

            hence ( Comput (p,s,i)) = ( Comput (p,s,n)) by A3, Th5;

          end;

        end;

        (p . ( IC ( Comput (p,s,k)))) = ( halt S) by A7, A6, A4, A2, A5, PARTFUN1:def 6;

        hence p halts_at ( IC ( Comput (p,s,k))) by A7, A2, A5, A4;

      end;

      assume that

       A8: ( IC ( Comput (p,s,k))) in ( dom p) and

       A9: (p . ( IC ( Comput (p,s,k)))) = ( halt S);

      

       A10: ( CurInstr (p,( Comput (p,s,k)))) = ( halt S) by A8, A9, PARTFUN1:def 6;

      reconsider k, n as Nat;

      now

        per cases ;

          suppose n <= k;

          hence ( Comput (p,s,k)) = ( Comput (p,s,n)) by A3, Th5;

        end;

          suppose k <= n;

          hence ( Comput (p,s,k)) = ( Comput (p,s,n)) by A10, Th5;

        end;

      end;

      hence thesis by A3, Def9, A1;

    end;

    theorem :: EXTPRO_1:18

    

     Th18: for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for P be the InstructionsF of S -valued NAT -defined Function, s be State of S, k st P halts_at ( IC ( Comput (P,s,k))) holds ( Result (P,s)) = ( Comput (P,s,k))

    proof

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be the InstructionsF of S -valued NAT -defined Function, s be State of S, k;

      assume

       A1: P halts_at ( IC ( Comput (P,s,k)));

      then P halts_on s by Th16;

      hence thesis by A1, Th17;

    end;

    theorem :: EXTPRO_1:19

    

     Th19: i <= j implies for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for P be the InstructionsF of S -valued NAT -defined Function holds for s be State of S st P halts_at ( IC ( Comput (P,s,i))) holds P halts_at ( IC ( Comput (P,s,j)))

    proof

      assume

       A1: i <= j;

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

      let s be State of S;

      assume that

       A2: ( IC ( Comput (p,s,i))) in ( dom p) and

       A3: (p . ( IC ( Comput (p,s,i)))) = ( halt S);

      

       A4: ( CurInstr (p,( Comput (p,s,i)))) = ( halt S) by A2, A3, PARTFUN1:def 6;

      hence ( IC ( Comput (p,s,j))) in ( dom p) by A2, A1, Th5;

      thus (p . ( IC ( Comput (p,s,j)))) = ( halt S) by A1, A3, A4, Th5;

    end;

    theorem :: EXTPRO_1:20

    i <= j implies for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for P be the InstructionsF of S -valued NAT -defined Function holds for s be State of S st P halts_at ( IC ( Comput (P,s,i))) holds ( Comput (P,s,j)) = ( Comput (P,s,i))

    proof

      assume

       A1: i <= j;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be the InstructionsF of S -valued NAT -defined Function, s be State of S;

      assume

       A2: P halts_at ( IC ( Comput (P,s,i)));

      then P halts_at ( IC ( Comput (P,s,j))) by A1, Th19;

      

      hence ( Comput (P,s,j)) = ( Result (P,s)) by Th18

      .= ( Comput (P,s,i)) by A2, Th18;

    end;

    theorem :: EXTPRO_1:21

    for S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N holds for P be Instruction-Sequence of S holds for s be State of S st ex k st P halts_at ( IC ( Comput (P,s,k))) holds for i holds ( Result (P,s)) = ( Result (P,( Comput (P,s,i)))) by Th8;

    definition

      let N;

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

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

      let s be State of S;

      :: EXTPRO_1:def15

      func LifeSpan (p,s) -> Nat means

      : Def15: ( CurInstr (p,( Comput (p,s,it )))) = ( halt S) & for k be Nat st ( CurInstr (p,( Comput (p,s,k)))) = ( halt S) holds it <= k;

      existence

      proof

        defpred X[ Nat] means ( CurInstr (p,( Comput (p,s,$1)))) = ( halt S);

        consider k be Nat such that ( IC ( Comput (p,s,k))) in ( dom p) and

         A2: ( CurInstr (p,( Comput (p,s,k)))) = ( halt S) by A1;

        

         A3: ex k be Nat st X[k] by A2;

        consider k be Nat such that

         A4: X[k] & for n be Nat st X[n] holds k <= n from NAT_1:sch 5( A3);

        reconsider k as Nat;

        take k;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let it1,it2 be Nat;

        assume

         A5: not thesis;

        then it1 <= it2 & it2 <= it1;

        hence contradiction by A5, XXREAL_0: 1;

      end;

    end

    theorem :: EXTPRO_1:22

    

     Th22: for N be non empty with_zero set, S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S, m be Nat holds p halts_on s iff p halts_on ( Comput (p,s,m))

    proof

      let N;

      let S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S, m be Nat;

      hereby

        assume p halts_on s;

        then

        consider n be Nat such that

         A1: ( IC ( Comput (p,s,n))) in ( dom p) and

         A2: ( CurInstr (p,( Comput (p,s,n)))) = ( halt S);

        reconsider n as Nat;

        per cases ;

          suppose n <= m;

          

          then ( Comput (p,s,n)) = ( Comput (p,s,(m + 0 ))) by A2, Th5

          .= ( Comput (p,( Comput (p,s,m)), 0 ));

          hence p halts_on ( Comput (p,s,m)) by A2, A1;

        end;

          suppose n >= m;

          then

          reconsider k = (n - m) as Element of NAT by INT_1: 5;

          ( Comput (p,( Comput (p,s,m)),k)) = ( Comput (p,s,(m + k))) by Th4

          .= ( Comput (p,s,n));

          hence p halts_on ( Comput (p,s,m)) by A1, A2;

        end;

      end;

      given n be Nat such that

       A3: ( IC ( Comput (p,( Comput (p,s,m)),n))) in ( dom p) and

       A4: ( CurInstr (p,( Comput (p,( Comput (p,s,m)),n)))) = ( halt S);

      reconsider nn = n as Nat;

      take (m + nn);

      thus ( IC ( Comput (p,s,(m + nn)))) in ( dom p) & ( CurInstr (p,( Comput (p,s,(m + nn))))) = ( halt S) by A3, A4, Th4;

    end;

    reserve N for with_zero non empty set,

S for IC-Ins-separated non empty AMI-Struct over N;

    reserve m,n for Nat;

    theorem :: EXTPRO_1:23

    for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S st p halts_on s holds ( Result (p,s)) = ( Comput (p,s,( LifeSpan (p,s))))

    proof

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

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

      let s be State of S;

      assume

       A1: p halts_on s;

      then

       A2: ( CurInstr (p,( Comput (p,s,( LifeSpan (p,s)))))) = ( halt S) by Def15;

      consider m such that

       A3: ( Result (p,s)) = ( Comput (p,s,m)) and

       A4: ( CurInstr (p,( Result (p,s)))) = ( halt S) by A1, Def9;

      ( LifeSpan (p,s)) <= m by A1, A3, A4, Def15;

      hence thesis by A2, A3, Th5;

    end;

    theorem :: EXTPRO_1:24

    for N be non empty with_zero set, S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be Instruction-Sequence of S, s be State of S, k be Nat st ( CurInstr (P,( Comput (P,s,k)))) = ( halt S) holds ( Comput (P,s,( LifeSpan (P,s)))) = ( Comput (P,s,k))

    proof

      let N;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be Instruction-Sequence of S, s be State of S, k be Nat such that

       A1: ( CurInstr (P,( Comput (P,s,k)))) = ( halt S);

      

       A2: ( dom P) = NAT by PARTFUN1:def 2;

      

       A3: P halts_on s by A2, A1;

      set Ls = ( LifeSpan (P,s));

      

       A4: ( CurInstr (P,( Comput (P,s,Ls)))) = ( halt S) by A3, Def15;

      Ls <= k by A1, A3, Def15;

      hence thesis by A4, Th5;

    end;

    theorem :: EXTPRO_1:25

    for N be non empty with_zero set holds for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for p be NAT -definedthe InstructionsF of S -valued Function holds for s be State of S st ( LifeSpan (p,s)) <= j & p halts_on s holds ( Comput (p,s,j)) = ( Comput (p,s,( LifeSpan (p,s))))

    proof

      let N;

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT -definedthe InstructionsF of S -valued Function, s be State of S;

      assume that

       A1: ( LifeSpan (p,s)) <= j and

       A2: p halts_on s;

      ( CurInstr (p,( Comput (p,s,( LifeSpan (p,s)))))) = ( halt S) by A2, Def15;

      hence thesis by A1, Th5;

    end;

    theorem :: EXTPRO_1:26

    for N be with_zero non empty set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, e be Nat, I be Instruction of S, t be e -started State of S, u be Instruction-Sequence of S st (e .--> I) c= u holds ( Following (u,t)) = ( Exec (I,t))

    proof

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, e be Nat, I be Instruction of S, t be e -started State of S, u be Instruction-Sequence of S such that

       A1: (e .--> I) c= u;

      

       A2: e in ( dom (e .--> I)) by TARSKI:def 1;

      ( IC t) = e by MEMSTR_0:def 11;

      

      then ( CurInstr (u,t)) = (u . e) by PBOOLE: 143

      .= ((e .--> I) . e) by A1, A2, GRFUNC_1: 2

      .= I by FUNCOP_1: 72;

      hence thesis;

    end;

    theorem :: EXTPRO_1:27

    for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be Instruction-Sequence of S, s be State of S st s = ( Following (P,s)) holds for n holds ( Comput (P,s,n)) = s

    proof

      let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be Instruction-Sequence of S, s be State of S;

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

      assume s = ( Following (P,s));

      then

       A1: for n st X[n] holds X[(n + 1)] by Th3;

      

       A2: X[ 0 ];

      thus for n holds X[n] from NAT_1:sch 2( A2, A1);

    end;

    theorem :: EXTPRO_1:28

    for N be with_zero non empty set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P be Instruction-Sequence of S, s be State of S, i be Instruction of S holds (( Exec ((P . ( IC s)),s)) . ( IC S)) = ( IC ( Following (P,s)))

    proof

      let N;

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

       NAT = ( dom P) by PARTFUN1:def 2;

      hence (( Exec ((P . ( IC s)),s)) . ( IC S)) = ( IC ( Following (P,s))) by PARTFUN1:def 6;

    end;

    theorem :: EXTPRO_1:29

    for S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N holds for P be Instruction-Sequence of S holds for s be State of S holds P halts_on s iff ex k st ( CurInstr (P,( Comput (P,s,k)))) = ( halt S)

    proof

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

      let P be Instruction-Sequence of S;

      let s be State of S;

      thus P halts_on s implies ex k st ( CurInstr (P,( Comput (P,s,k)))) = ( halt S);

      given k such that

       A1: ( CurInstr (P,( Comput (P,s,k)))) = ( halt S);

      take k;

      ( IC ( Comput (P,s,k))) in NAT ;

      hence ( IC ( Comput (P,s,k))) in ( dom P) by PARTFUN1:def 2;

      thus ( CurInstr (P,( Comput (P,s,k)))) = ( halt S) by A1;

    end;

    reserve S for IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N;

    theorem :: EXTPRO_1:30

    

     Th30: for F be Instruction-Sequence of S holds for s be State of S st ex k be Nat st (F . ( IC ( Comput (F,s,k)))) = ( halt S) holds F halts_on s

    proof

      let F be Instruction-Sequence of S;

      let s be State of S;

      given k be Nat such that

       A1: (F . ( IC ( Comput (F,s,k)))) = ( halt S);

      take k;

      

       A2: ( dom F) = NAT by PARTFUN1:def 2;

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

      thus ( CurInstr (F,( Comput (F,s,k)))) = ( halt S) by A1, A2, PARTFUN1:def 6;

    end;

    ::$Canceled

    theorem :: EXTPRO_1:32

    

     Th31: for F be Instruction-Sequence of S holds for s be State of S, k be Nat holds (F . ( IC ( Comput (F,s,k)))) <> ( halt S) & (F . ( IC ( Comput (F,s,(k + 1))))) = ( halt S) iff ( LifeSpan (F,s)) = (k + 1) & F halts_on s

    proof

      let F be Instruction-Sequence of S;

      let s be State of S, k be Nat;

      

       A1: ( dom F) = NAT by PARTFUN1:def 2;

      hereby

        assume that

         A2: (F . ( IC ( Comput (F,s,k)))) <> ( halt S) and

         A3: (F . ( IC ( Comput (F,s,(k + 1))))) = ( halt S);

        

         A4: ( CurInstr (F,( Comput (F,s,k)))) <> ( halt S) by A2, A1, PARTFUN1:def 6;

         A5:

        now

          let i be Nat;

          assume that

           A6: ( CurInstr (F,( Comput (F,s,i)))) = ( halt S) and

           A7: (k + 1) > i;

          i <= k by A7, NAT_1: 13;

          hence contradiction by A4, A6, Th5;

        end;

        

         A8: F halts_on s by A3, Th30;

        ( CurInstr (F,( Comput (F,s,(k + 1))))) = ( halt S) by A3, A1, PARTFUN1:def 6;

        hence ( LifeSpan (F,s)) = (k + 1) & F halts_on s by A5, Def15, A8;

      end;

      assume

       A9: ( LifeSpan (F,s)) = (k + 1) & F halts_on s;

       A10:

      now

        assume ( CurInstr (F,( Comput (F,s,k)))) = ( halt S);

        then (k + 1) <= k by A9, Def15;

        hence contradiction by NAT_1: 13;

      end;

      ( CurInstr (F,( Comput (F,s,(k + 1))))) = ( halt S) by A9, Def15;

      hence thesis by A10, A1, PARTFUN1:def 6;

    end;

    theorem :: EXTPRO_1:33

    for F be Instruction-Sequence of S holds for s be State of S, k be Nat st ( IC ( Comput (F,s,k))) <> ( IC ( Comput (F,s,(k + 1)))) & (F . ( IC ( Comput (F,s,(k + 1))))) = ( halt S) holds ( LifeSpan (F,s)) = (k + 1)

    proof

      let F be Instruction-Sequence of S;

      let s be State of S, k be Nat;

      assume that

       A1: ( IC ( Comput (F,s,k))) <> ( IC ( Comput (F,s,(k + 1)))) and

       A2: (F . ( IC ( Comput (F,s,(k + 1))))) = ( halt S);

      

       A3: ( dom F) = NAT by PARTFUN1:def 2;

      now

        assume (F . ( IC ( Comput (F,s,k)))) = ( halt S);

        then ( CurInstr (F,( Comput (F,s,k)))) = ( halt S) by A3, PARTFUN1:def 6;

        hence contradiction by A1, Th5, NAT_1: 11;

      end;

      hence thesis by A2, Th31;

    end;

    theorem :: EXTPRO_1:34

    for F be Instruction-Sequence of S holds for s be State of S, k be Nat st F halts_on ( Comput (F,s,k)) & 0 < ( LifeSpan (F,( Comput (F,s,k)))) holds ( LifeSpan (F,s)) = (k + ( LifeSpan (F,( Comput (F,s,k)))))

    proof

      let F be Instruction-Sequence of S;

      let s be State of S, k be Nat;

      set s2 = ( Comput (F,s,k)), c = ( LifeSpan (F,( Comput (F,s,k))));

      assume that

       A1: F halts_on s2 and

       A2: 0 < c;

      consider l be Nat such that

       A3: c = (l + 1) by A2, NAT_1: 6;

      reconsider l as Nat;

      (F . ( IC ( Comput (F,s2,(l + 1))))) = ( halt S) by A1, A3, Th31;

      then

       A4: (F . ( IC ( Comput (F,s,(k + (l + 1)))))) = ( halt S) by Th4;

      (F . ( IC ( Comput (F,s2,l)))) <> ( halt S) by A1, A3, Th31;

      then (F . ( IC ( Comput (F,s,(k + l))))) <> ( halt S) by Th4;

      

      hence ( LifeSpan (F,s)) = ((k + l) + 1) by A4, Th31

      .= (k + c) by A3;

    end;

    theorem :: EXTPRO_1:35

    for F be Instruction-Sequence of S holds for s be State of S, k be Nat st F halts_on ( Comput (F,s,k)) holds ( Result (F,( Comput (F,s,k)))) = ( Result (F,s))

    proof

      let F be Instruction-Sequence of S;

      let s be State of S, k be Nat;

      set s2 = ( Comput (F,s,k));

      assume

       A1: F halts_on s2;

      then

      consider l be Nat such that

       A2: ( Result (F,s2)) = ( Comput (F,s2,l)) & ( CurInstr (F,( Result (F,s2)))) = ( halt S) by Def9;

      

       A3: F halts_on s by A1, Th22;

      ( Comput (F,( Comput (F,s,k)),l)) = ( Comput (F,s,(k + l))) by Th4;

      hence thesis by A3, A2, Def9;

    end;

    reserve S for halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

    reserve P for Instruction-Sequence of S;

    theorem :: EXTPRO_1:36

    for s be State of S st P halts_on s holds for k be Nat st ( LifeSpan (P,s)) <= k holds ( CurInstr (P,( Comput (P,s,k)))) = ( halt S)

    proof

      let s be State of S;

      assume P halts_on s;

      then

       A1: ( CurInstr (P,( Comput (P,s,( LifeSpan (P,s)))))) = ( halt S) by Def15;

      let k be Nat;

      assume ( LifeSpan (P,s)) <= k;

      hence thesis by A1, Th5;

    end;