amistd_5.miz



    begin

    theorem :: AMISTD_5:1

    for N be with_zero set holds for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for I be Instruction of S st I is jump-only holds for k be Nat holds ( IncAddr (I,k)) is jump-only by COMPOS_0:def 9;

    registration

      let N be with_zero set, S be with_explicit_jumps IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, I be IC-relocable Instruction of S, k be Nat;

      cluster ( IncAddr (I,k)) -> IC-relocable;

      coherence

      proof

        let j,i be Nat, s be State of S;

        

        thus (( IC ( Exec (( IncAddr (( IncAddr (I,k)),j)),s))) + i) = (( IC ( Exec (( IncAddr (I,(k + j))),s))) + i) by COMPOS_0: 7

        .= ( IC ( Exec (( IncAddr (I,((k + j) + i))),( IncIC (s,i))))) by AMISTD_2:def 3

        .= ( IC ( Exec (( IncAddr (I,(k + (j + i)))),( IncIC (s,i)))))

        .= ( IC ( Exec (( IncAddr (( IncAddr (I,k)),(j + i))),( IncIC (s,i))))) by COMPOS_0: 7;

      end;

    end

    definition

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

      :: AMISTD_5:def1

      attr I is relocable means

      : Def1: for j,k be Nat, s be State of S holds ( Exec (( IncAddr (I,(j + k))),( IncIC (s,k)))) = ( IncIC (( Exec (( IncAddr (I,j)),s)),k));

    end

    registration

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

      cluster relocable -> IC-relocable for Instruction of S;

      coherence

      proof

        let I be Instruction of S such that

         A1: I is relocable;

        let j,k be Nat, s be State of S;

        reconsider kk = k as Nat;

        

        thus (( IC ( Exec (( IncAddr (I,j)),s))) + k) = ( IC ( IncIC (( Exec (( IncAddr (I,j)),s)),kk))) by MEMSTR_0: 53

        .= ( IC ( Exec (( IncAddr (I,(j + k))),( IncIC (s,k))))) by A1;

      end;

    end

    definition

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

      :: AMISTD_5:def2

      attr S is relocable means

      : Def2: for I be Instruction of S holds I is relocable;

    end

    theorem :: AMISTD_5:2

    

     Th2: for N be with_zero set, I be Instruction of ( STC N), s be State of ( STC N), k be Nat holds ( Exec (I,( IncIC (s,k)))) = ( IncIC (( Exec (I,s)),k))

    proof

      let N be with_zero set, I be Instruction of ( STC N), s be State of ( STC N), k be Nat;

      per cases by AMISTD_1: 6;

        suppose

         A1: ( InsCode I) = 1;

        

        hence ( Exec (I,( IncIC (s,k)))) = ( IncIC (( IncIC (s,k)),1)) by AMISTD_1: 20

        .= ( IncIC (s,(1 + k))) by MEMSTR_0: 57

        .= ( IncIC (( IncIC (s,1)),k)) by MEMSTR_0: 57

        .= ( IncIC (( Exec (I,s)),k)) by A1, AMISTD_1: 20;

      end;

        suppose ( InsCode I) = 0 ;

        then

         A2: I is halting by AMISTD_1: 4;

        

        hence ( Exec (I,( IncIC (s,k)))) = ( IncIC (s,k))

        .= ( IncIC (( Exec (I,s)),k)) by A2;

      end;

    end;

    definition

      let N be with_zero set;

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

      :: AMISTD_5:def3

      attr S is IC-recognized means for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st p is non empty holds ( IC S) in ( dom p);

    end

    theorem :: AMISTD_5:3

    

     Th3: for N be with_zero set holds for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds S is IC-recognized iff for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( DataPart p) <> {} holds ( IC S) in ( dom p)

    proof

      let N be with_zero set;

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

      thus S is IC-recognized implies for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( DataPart p) <> {} holds ( IC S) in ( dom p)

      proof

        assume

         A1: S is IC-recognized;

        let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

        let p be q -autonomic FinPartState of S;

        assume ( DataPart p) <> {} ;

        then p is non empty;

        hence thesis by A1;

      end;

      assume

       A2: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( DataPart p) <> {} holds ( IC S) in ( dom p);

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic FinPartState of S;

      

       A3: ( dom p) c= ( {( IC S)} \/ ( dom ( DataPart p))) by MEMSTR_0: 32;

      assume

       A4: p is non empty;

      per cases ;

        suppose

         A5: ( IC S) in ( dom p);

        thus ( IC S) in ( dom p) by A5;

      end;

        suppose not ( IC S) in ( dom p);

        then {( IC S)} misses ( dom p) by ZFMISC_1: 50;

        then ( dom ( DataPart p)) is non empty by A4, A3, XBOOLE_1: 3, XBOOLE_1: 73;

        then ( DataPart p) is non empty;

        hence ( IC S) in ( dom p) by A2;

      end;

    end;

    registration

      let N be with_zero set;

      cluster ( Data-Locations ( STC N)) -> empty;

      coherence

      proof

        the carrier of ( STC N) = { 0 } by AMISTD_1:def 7

        .= {( IC ( STC N))} by AMISTD_1:def 7;

        hence thesis by XBOOLE_1: 37;

      end;

    end

    registration

      let N be with_zero set;

      let p be PartState of ( STC N);

      cluster ( DataPart p) -> empty;

      coherence ;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> IC-recognized relocable;

      coherence

      proof

        for q be non halt-free finitethe InstructionsF of ( STC N) -valued NAT -defined Function holds for p be q -autonomic FinPartState of ( STC N) st ( DataPart p) <> {} holds ( IC ( STC N)) in ( dom p);

        hence ( STC N) is IC-recognized by Th3;

        let I be Instruction of ( STC N);

        let j,k be Nat, s be State of ( STC N);

        

        thus ( Exec (( IncAddr (I,(j + k))),( IncIC (s,k)))) = ( Exec (I,( IncIC (s,k)))) by COMPOS_0: 4

        .= ( IncIC (( Exec (I,s)),k)) by Th2

        .= ( IncIC (( Exec (( IncAddr (I,j)),s)),k)) by COMPOS_0: 4;

      end;

    end

    registration

      let N be with_zero set;

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

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    registration

      let N be with_zero set;

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

      cluster -> relocable for Instruction of S;

      coherence by Def2;

    end

    reserve k for Nat;

    theorem :: AMISTD_5:4

    

     Th4: for N be with_zero set holds for S be relocable halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for INS be Instruction of S, s be State of S holds ( Exec (( IncAddr (INS,k)),( IncIC (s,k)))) = ( IncIC (( Exec (INS,s)),k))

    proof

      let N be with_zero set;

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

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

      

      thus ( Exec (( IncAddr (INS,k)),( IncIC (s,k)))) = ( Exec (( IncAddr (INS,( 0 qua Nat + k))),( IncIC (s,k))))

      .= ( IncIC (( Exec (( IncAddr (INS, 0 )),s)),k)) by Def1

      .= ( IncIC (( Exec (INS,s)),k)) by COMPOS_0: 3;

    end;

    theorem :: AMISTD_5:5

    

     Th5: for N be with_zero set holds for S be relocable halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for INS be Instruction of S, s be State of S, j,k be Nat st ( IC s) = (j + k) holds ( Exec (INS,( DecIC (s,k)))) = ( DecIC (( Exec (( IncAddr (INS,k)),s)),k))

    proof

      let N be with_zero set;

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

      let INS be Instruction of S, s be State of S, j,k be Nat such that

       A1: ( IC s) = (j + k);

      set s1 = (s +* ( Start-At (j,S)));

      

       A2: ( IncIC (s1,k)) = (s +* ( Start-At (( IC s),S))) by A1, MEMSTR_0: 58

      .= s by MEMSTR_0: 31;

      

      thus ( Exec (INS,( DecIC (s,k)))) = ( Exec (INS,s1)) by A1, NAT_D: 34

      .= (( Exec (INS,s1)) +* ( Start-At (( IC ( Exec (INS,s1))),S))) by MEMSTR_0: 31

      .= (( IncIC (( Exec (INS,s1)),k)) +* ( Start-At (( IC ( Exec (INS,s1))),S))) by FUNCT_4: 114

      .= ( DecIC (( IncIC (( Exec (INS,s1)),k)),k)) by MEMSTR_0: 59

      .= ( DecIC (( Exec (( IncAddr (INS,k)),s)),k)) by A2, Th4;

    end;

    registration

      let N be with_zero set;

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

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    reserve N for with_zero set,

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

    theorem :: AMISTD_5:6

    

     Th6: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S holds ( IC S) in ( dom p)

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of S;

      

       A1: ( dom p) meets ( {( IC S)} \/ ( Data-Locations S)) by MEMSTR_0: 41;

      per cases by A1, XBOOLE_1: 70;

        suppose ( dom p) meets {( IC S)};

        hence thesis by ZFMISC_1: 50;

      end;

        suppose ( dom p) meets ( Data-Locations S);

        then (( dom p) /\ ( Data-Locations S)) <> {} by XBOOLE_0:def 7;

        then ( DataPart p) <> {} by RELAT_1: 38, RELAT_1: 61;

        hence thesis by Th3;

      end;

    end;

    definition

      let N;

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

      :: AMISTD_5:def4

      attr S is CurIns-recognized means

      : Def4: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S holds for s be State of S st p c= s holds for P be Instruction-Sequence of S st q c= P holds for i be Nat holds ( IC ( Comput (P,s,i))) in ( dom q);

    end

    registration

      let N;

      cluster ( STC N) -> CurIns-recognized;

      coherence

      proof

        let q be non halt-free finitethe InstructionsF of ( STC N) -valued NAT -defined Function;

        let p be q -autonomic non empty FinPartState of ( STC N), s be State of ( STC N) such that

         A1: p c= s;

        let P be Instruction-Sequence of ( STC N) such that

         A2: q c= P;

        let i be Nat;

        set Csi = ( Comput (P,s,i));

        set loc = ( IC Csi);

        set loc1 = (loc + 1);

        assume

         A3: not ( IC ( Comput (P,s,i))) in ( dom q);

        the InstructionsF of ( STC N) = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} by AMISTD_1:def 7;

        then

        reconsider I = [1, 0 , 0 ] as Instruction of ( STC N) by TARSKI:def 2;

        set p1 = (q +* (loc .--> I));

        set p2 = (q +* (loc .--> ( halt ( STC N))));

        reconsider P1 = (P +* (loc .--> I)) as Instruction-Sequence of ( STC N);

        reconsider P2 = (P +* (loc .--> ( halt ( STC N)))) as Instruction-Sequence of ( STC N);

        

         A5: loc in ( dom (loc .--> ( halt ( STC N)))) by TARSKI:def 1;

        

         A7: loc in ( dom (loc .--> I)) by TARSKI:def 1;

        

         A8: ( dom q) misses ( dom (loc .--> ( halt ( STC N)))) by A3, ZFMISC_1: 50;

        

         A9: ( dom q) misses ( dom (loc .--> I)) by A3, ZFMISC_1: 50;

        

         A10: p1 c= P1 by A2, FUNCT_4: 123;

        

         A11: p2 c= P2 by A2, FUNCT_4: 123;

        set Cs2i = ( Comput (P2,s,i)), Cs1i = ( Comput (P1,s,i));

         not p is q -autonomic

        proof

          ((loc .--> ( halt ( STC N))) . loc) = ( halt ( STC N)) by FUNCOP_1: 72;

          then

           A12: (P2 . loc) = ( halt ( STC N)) by A5, FUNCT_4: 13;

          ((loc .--> I) . loc) = I by FUNCOP_1: 72;

          then

           A13: (P1 . loc) = I by A7, FUNCT_4: 13;

          take P1, P2;

          q c= p1 by A9, FUNCT_4: 32;

          hence

           A14: q c= P1 by A10, XBOOLE_1: 1;

          q c= p2 by A8, FUNCT_4: 32;

          hence

           A15: q c= P2 by A11, XBOOLE_1: 1;

          take s, s;

          thus p c= s by A1;

          

           A16: (Cs1i | ( dom p)) = (Csi | ( dom p)) by A14, A2, A1, EXTPRO_1:def 10;

          thus p c= s by A1;

          

           A17: (Cs1i | ( dom p)) = (Cs2i | ( dom p)) by A14, A15, A1, EXTPRO_1:def 10;

          take k = (i + 1);

          set Cs1k = ( Comput (P1,s,k));

          

           A18: Cs1k = ( Following (P1,Cs1i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

          ( InsCode I) = 1;

          then

           A19: ( IC ( Exec (I,Cs1i))) = (( IC Cs1i) + 1) by AMISTD_1: 9;

          

           A20: ( IC Csi) = ( IC (Csi | ( dom p))) by Th6, FUNCT_1: 49;

          then ( IC Cs1i) = loc by A16, Th6, FUNCT_1: 49;

          then

           A21: ( IC Cs1k) = loc1 by A19, A18, A13, PBOOLE: 143;

          set Cs2k = ( Comput (P2,s,k));

          

           A22: Cs2k = ( Following (P2,Cs2i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

          

           A23: (P2 /. ( IC Cs2i)) = (P2 . ( IC Cs2i)) by PBOOLE: 143;

          ( IC Cs2i) = loc by A16, A20, A17, Th6, FUNCT_1: 49;

          then

           A24: ( IC Cs2k) = loc by A22, A12, A23, EXTPRO_1:def 3;

          ( IC (Cs1k | ( dom p))) = ( IC Cs1k) & ( IC (Cs2k | ( dom p))) = ( IC Cs2k) by Th6, FUNCT_1: 49;

          hence thesis by A21, A24;

        end;

        hence contradiction;

      end;

    end

    registration

      let N be with_zero set;

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

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

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

    theorem :: AMISTD_5:7

    for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S, s1,s2 be State of S st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of S st q c= P1 & q c= P2 holds for i be Nat holds ( IC ( Comput (P1,s1,i))) = ( IC ( Comput (P2,s2,i))) & ( CurInstr (P1,( Comput (P1,s1,i)))) = ( CurInstr (P2,( Comput (P2,s2,i))))

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of S, s1,s2 be State of S such that

       A1: p c= s1 and

       A2: p c= s2;

      let P1,P2 be Instruction-Sequence of S such that

       A3: q c= P1 and

       A4: q c= P2;

      

       A5: ( dom q) c= ( dom P1) by A3, RELAT_1: 11;

      

       A6: ( dom q) c= ( dom P2) by A4, RELAT_1: 11;

      let i be Nat;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      

       A7: ( IC Cs1i) in ( dom q) by A3, Def4, A1;

      

       A8: ( IC Cs2i) in ( dom q) by A4, Def4, A2;

      thus

       A9: ( IC Cs1i) = ( IC Cs2i)

      proof

        assume

         A10: ( IC ( Comput (P1,s1,i))) <> ( IC ( Comput (P2,s2,i)));

        ((Cs1i | ( dom p)) . ( IC S)) = (Cs1i . ( IC S)) & ((Cs2i | ( dom p)) . ( IC S)) = (Cs2i . ( IC S)) by Th6, FUNCT_1: 49;

        hence contradiction by A10, A3, A4, A1, A2, EXTPRO_1:def 10;

      end;

      

      thus ( CurInstr (P1,( Comput (P1,s1,i)))) = (P1 . ( IC Cs1i)) by A7, A5, PARTFUN1:def 6

      .= (q . ( IC Cs1i)) by A7, A3, GRFUNC_1: 2

      .= (P2 . ( IC Cs2i)) by A8, A4, A9, GRFUNC_1: 2

      .= ( CurInstr (P2,( Comput (P2,s2,i)))) by A8, A6, PARTFUN1:def 6;

    end;

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

    theorem :: AMISTD_5:8

    for k be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( IC S) in ( dom p) holds for s be State of S st p c= s holds for P be Instruction-Sequence of S st q c= P holds for i be Nat holds ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)) = ( IncIC (( Comput (P,s,i)),k))

    proof

      let k be Nat;

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic FinPartState of S such that

       A1: ( IC S) in ( dom p);

      let s be State of S such that

       A2: p c= s;

      let P be Instruction-Sequence of S;

      assume

       A3: q c= P;

      defpred P[ Nat] means ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),$1)) = ( IncIC (( Comput (P,s,$1)),k));

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A5: ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)) = ( IncIC (( Comput (P,s,i)),k));

        reconsider kk = ( IC ( Comput (P,s,i))) as Nat;

        

         A6: ( IC S) in ( dom ( Start-At ((( IC ( Comput (P,s,i))) + k),S))) by TARSKI:def 1;

        

         A7: ( IC ( IncIC (( Comput (P,s,i)),k))) = ( IC ( Start-At ((( IC ( Comput (P,s,i))) + k),S))) by A6, FUNCT_4: 13

        .= (( IC ( Comput (P,s,i))) + k) by FUNCOP_1: 72;

         not p is empty by A1;

        then

         A8: ( IC ( Comput (P,s,i))) in ( dom q) by A3, Def4, A2;

        then

         A9: ( IC ( Comput (P,s,i))) in ( dom ( IncAddr (q,k))) by COMPOS_1:def 21;

        

         A10: (q /. kk) = (q . ( IC ( Comput (P,s,i)))) by A8, PARTFUN1:def 6

        .= (P . ( IC ( Comput (P,s,i)))) by A8, A3, GRFUNC_1: 2;

        reconsider kk = ( IC ( Comput (P,s,i))) as Nat;

        

         A11: (( IC ( Comput (P,s,i))) + k) in ( dom ( Reloc (q,k))) by A8, COMPOS_1: 46;

        

         A12: ( CurInstr ((P +* ( Reloc (q,k))),( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) = ((P +* ( Reloc (q,k))) . ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by PBOOLE: 143

        .= (( Reloc (q,k)) . (( IC ( Comput (P,s,i))) + k)) by A5, A7, A11, FUNCT_4: 13

        .= (( IncAddr (q,k)) . kk) by A9, VALUED_1:def 12

        .= ( IncAddr ((q /. kk),k)) by A8, COMPOS_1:def 21

        .= ( IncAddr (( CurInstr (P,( Comput (P,s,i)))),k)) by A10, PBOOLE: 143;

        

        thus ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),(i + 1))) = ( Following ((P +* ( Reloc (q,k))),( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by EXTPRO_1: 3

        .= ( IncIC (( Following (P,( Comput (P,s,i)))),k)) by A5, A12, Th4

        .= ( IncIC (( Comput (P,s,(i + 1))),k)) by EXTPRO_1: 3;

      end;

      

       A13: ( IC p) = ( IC s) by A2, A1, GRFUNC_1: 2;

      

       A14: ( DataPart p) c= p by MEMSTR_0: 12;

      ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))), 0 )) = (s +* (( DataPart p) +* ( Start-At ((( IC p) + k),S)))) by A1, MEMSTR_0: 56

      .= ((s +* ( DataPart p)) +* ( Start-At ((( IC p) + k),S))) by FUNCT_4: 14

      .= ( IncIC (( Comput (P,s, 0 )),k)) by A13, A14, A2, FUNCT_4: 98, XBOOLE_1: 1;

      then

       A15: P[ 0 ];

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

    end;

    theorem :: AMISTD_5:9

    

     Th9: for k be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( IC S) in ( dom p) holds for s be State of S st ( IncIC (p,k)) c= s holds for P be Instruction-Sequence of S st ( Reloc (q,k)) c= P holds for i be Nat holds ( Comput (P,s,i)) = ( IncIC (( Comput ((P +* q),(s +* p),i)),k))

    proof

      let k be Nat;

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic FinPartState of S such that

       A1: ( IC S) in ( dom p);

      let s be State of S such that

       A2: ( IncIC (p,k)) c= s;

      let P be Instruction-Sequence of S such that

       A3: ( Reloc (q,k)) c= P;

      defpred Z[ Nat] means ( Comput (P,s,$1)) = ( IncIC (( Comput ((P +* q),(s +* p),$1)),k));

      

       A4: for i be Nat st Z[i] holds Z[(i + 1)]

      proof

        let i be Nat such that

         A5: ( Comput (P,s,i)) = ( IncIC (( Comput ((P +* q),(s +* p),i)),k));

        reconsider kk = ( IC ( Comput ((P +* q),(s +* p),i))) as Nat;

        

         A6: ( IC S) in ( dom ( Start-At ((( IC ( Comput ((P +* q),(s +* p),i))) + k),S))) by TARSKI:def 1;

        

         A7: p c= (s +* p) by FUNCT_4: 25;

        

         A8: q c= (P +* q) by FUNCT_4: 25;

         not p is empty by A1;

        then

         A9: ( IC ( Comput ((P +* q),(s +* p),i))) in ( dom q) by Def4, A7, A8;

        then

         A10: ( IC ( Comput ((P +* q),(s +* p),i))) in ( dom ( IncAddr (q,k))) by COMPOS_1:def 21;

        

         A11: (( IC ( Comput ((P +* q),(s +* p),i))) + k) in ( dom ( Reloc (q,k))) by A9, COMPOS_1: 46;

        reconsider kk = ( IC ( Comput ((P +* q),(s +* p),i))) as Nat;

        

         A12: ( IC ( Comput (P,s,i))) = ( IC ( Start-At ((( IC ( Comput ((P +* q),(s +* p),i))) + k),S))) by A5, A6, FUNCT_4: 13

        .= (( IC ( Comput ((P +* q),(s +* p),i))) + k) by FUNCOP_1: 72;

        

         A13: q c= (P +* q) by FUNCT_4: 25;

        

         A14: (q /. kk) = (q . kk) by A9, PARTFUN1:def 6;

        

         A15: ( dom (P +* q)) = NAT by PARTFUN1:def 2;

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

        

        then

         A16: ( CurInstr (P,( Comput (P,s,i)))) = (P . ( IC ( Comput (P,s,i)))) by PARTFUN1:def 6

        .= (( Reloc (q,k)) . ( IC ( Comput (P,s,i)))) by A3, A11, A12, GRFUNC_1: 2

        .= (( IncAddr (q,k)) . kk) by A10, A12, VALUED_1:def 12

        .= ( IncAddr ((q /. kk),k)) by A9, COMPOS_1:def 21

        .= ( IncAddr (((P +* q) . ( IC ( Comput ((P +* q),(s +* p),i)))),k)) by A9, A14, A13, GRFUNC_1: 2

        .= ( IncAddr (( CurInstr ((P +* q),( Comput ((P +* q),(s +* p),i)))),k)) by A15, PARTFUN1:def 6;

        

        thus ( Comput (P,s,(i + 1))) = ( Following (P,( Comput (P,s,i)))) by EXTPRO_1: 3

        .= ( IncIC (( Following ((P +* q),( Comput ((P +* q),(s +* p),i)))),k)) by A5, A16, Th4

        .= ( IncIC (( Comput ((P +* q),(s +* p),(i + 1))),k)) by EXTPRO_1: 3;

      end;

      set IP = ( Start-At (( IC p),S));

      

       A17: ( dom ( Start-At (( IC p),S))) = {( IC S)};

      

       A18: ( Start-At ((( IC p) + k),S)) c= ( IncIC (p,k)) by MEMSTR_0: 55;

      

       A19: ( IC ( Comput ((P +* q),(s +* p), 0 ))) = ( IC p) by A1, FUNCT_4: 13;

      set DP = ( DataPart p);

      ( DataPart ( IncIC (p,k))) c= ( IncIC (p,k)) by RELAT_1: 59;

      then ( DataPart ( IncIC (p,k))) c= s by A2, XBOOLE_1: 1;

      then

       A20: ( DataPart p) c= s by MEMSTR_0: 51;

      set PR = ( Reloc (q,k));

      set IS = ( Start-At ((( IC ( Comput ((P +* q),(s +* p), 0 ))) + k),S));

      

       A21: ( dom ( Start-At ((( IC ( Comput ((P +* q),(s +* p), 0 ))) + k),S))) = {( IC S)};

      ( Comput (P,s, 0 )) = (s +* IS) by A19, A2, A18, FUNCT_4: 98, XBOOLE_1: 1

      .= ((s +* DP) +* IS) by A20, FUNCT_4: 98

      .= (((s +* DP) +* IP) +* IS) by A21, A17, FUNCT_4: 74

      .= ((s +* (DP +* IP)) +* IS) by FUNCT_4: 14

      .= ( IncIC (( Comput ((P +* q),(s +* p), 0 )),k)) by A1, MEMSTR_0: 26;

      then

       A22: Z[ 0 ];

      thus for i be Nat holds Z[i] from NAT_1:sch 2( A22, A4);

    end;

    reserve m,j for Nat;

    theorem :: AMISTD_5:10

    

     Th10: for k be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be non empty FinPartState of S st ( IC S) in ( dom p) holds for s be State of S st p c= s & ( IncIC (p,k)) is ( Reloc (q,k)) -autonomic holds for P be Instruction-Sequence of S st q c= P holds for i be Nat holds ( Comput (P,s,i)) = ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)),k))

    proof

      let k be Nat;

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be non empty FinPartState of S;

      assume

       A1: ( IC S) in ( dom p);

      then

       A2: ( Start-At (( IC p),S)) c= p by FUNCOP_1: 84;

      let s be State of S such that

       A3: p c= s and

       A4: ( IncIC (p,k)) is ( Reloc (q,k)) -autonomic;

      let P be Instruction-Sequence of S such that

       A5: q c= P;

      defpred Z[ Nat] means ( Comput (P,s,$1)) = ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),$1)),k));

      

       A6: for i be Nat st Z[i] holds Z[(i + 1)]

      proof

        reconsider pp = q as preProgram of S;

        let i be Nat such that

         A7: ( Comput (P,s,i)) = ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)),k));

        reconsider kk = ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) as Nat;

        reconsider jk = ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) as Nat;

        

         A8: ( IncIC (p,k)) c= (s +* ( IncIC (p,k))) by FUNCT_4: 25;

        

         A9: ( Reloc (q,k)) c= (P +* ( Reloc (q,k))) by FUNCT_4: 25;

        

         A10: ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) in ( dom ( Reloc (q,k))) by A4, Def4, A8, A9;

        then

         A11: jk in { (j + k) where j be Nat : j in ( dom q) } by COMPOS_1: 33;

        

         A12: ( IC S) in ( dom ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) -' k),S))) by TARSKI:def 1;

        consider j be Nat such that

         A13: jk = (j + k) and

         A14: j in ( dom q) by A11;

        

         A15: ( dom (P +* ( Reloc (q,k)))) = NAT by PARTFUN1:def 2;

        

         A16: ( Reloc (q,k)) c= (P +* ( Reloc (q,k))) by FUNCT_4: 25;

        

         A17: ( Reloc (q,k)) = ( IncAddr (( Shift (q,k)),k)) by COMPOS_1: 34;

        ( dom ( Shift (pp,k))) = { (m + k) where m be Nat : m in ( dom pp) } by VALUED_1:def 12;

        then

         A18: (j + k) in ( dom ( Shift (q,k))) by A14;

        

        then

         A19: ( IncAddr ((( Shift (q,k)) /. kk),k)) = (( Reloc (q,k)) . ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by A13, A17, COMPOS_1:def 21

        .= ((P +* ( Reloc (q,k))) . ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by A10, A16, GRFUNC_1: 2

        .= ( CurInstr ((P +* ( Reloc (q,k))),( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by A15, PARTFUN1:def 6;

        

         A20: ((j + k) -' k) = j by NAT_D: 34;

        

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

        

         A22: ( IC ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)),k))) = (( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) -' k),S)) . ( IC S)) by A12, FUNCT_4: 13

        .= (( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i))) -' k) by FUNCOP_1: 72;

        ( CurInstr (P,( Comput (P,s,i)))) = (P . ( IC ( Comput (P,s,i)))) by A21, PARTFUN1:def 6

        .= (q . ( IC ( Comput (P,s,i)))) by A7, A13, A14, A20, A5, A22, GRFUNC_1: 2

        .= (( Shift (q,k)) . ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) by A13, A14, A20, A7, A22, VALUED_1:def 12

        .= (( Shift (q,k)) /. kk) by A13, A18, PARTFUN1:def 6;

        then

         A23: ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),(i + 1))) = ( Following ((P +* ( Reloc (q,k))),( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))) & ( Exec (( CurInstr (P,( Comput (P,s,i)))),( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)),k)))) = ( DecIC (( Following ((P +* ( Reloc (q,k))),( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),i)))),k)) by A13, A19, Th5, EXTPRO_1: 3;

        

        thus ( Comput (P,s,(i + 1))) = ( Following (P,( Comput (P,s,i)))) by EXTPRO_1: 3

        .= ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))),(i + 1))),k)) by A7, A23;

      end;

      

       A24: ( IC S) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

      

       A25: ( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))), 0 ))) = ( IC ( IncIC (p,k))) by A24, FUNCT_4: 13;

      

       A26: ( DataPart p) c= p by RELAT_1: 59;

      set DP = ( DataPart p);

      set IP = ( Start-At ((( IC p) + k),S));

      set PP = q;

      set IS = ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))), 0 ))) -' k),S));

      

       A27: ( dom ( Start-At ((( IC p) + k),S))) = {( IC S)};

      set PR = ( Reloc (q,k));

      set SD = (s | ( dom ( Reloc (q,k))));

      

       A28: {( IC S)} misses ( dom ( DataPart p)) by MEMSTR_0: 4;

      

       A29: ( dom ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))), 0 ))) -' k),S))) = {( IC S)};

      

       A30: ( dom IP) misses ( dom DP) by A28;

      

       A31: (IP +* DP) = (DP +* IP) by A30, FUNCT_4: 35

      .= ( IncIC (p,k)) by A1, MEMSTR_0: 56;

      ( Comput (P,s, 0 )) = (s +* ( Start-At (( IC p),S))) by A3, A2, FUNCT_4: 98, XBOOLE_1: 1

      .= (s +* ( Start-At (((( IC p) + k) -' k),S))) by NAT_D: 34

      .= (s +* IS) by A25, MEMSTR_0: 53

      .= ((s +* DP) +* IS) by A26, A3, FUNCT_4: 98, XBOOLE_1: 1

      .= (((s +* DP) +* IP) +* IS) by A29, A27, FUNCT_4: 74

      .= ((s +* (DP +* IP)) +* IS) by FUNCT_4: 14

      .= ( DecIC (( Comput ((P +* ( Reloc (q,k))),(s +* ( IncIC (p,k))), 0 )),k)) by A31, A27, A28, FUNCT_4: 35;

      then

       A32: Z[ 0 ];

      thus for i be Nat holds Z[i] from NAT_1:sch 2( A32, A6);

    end;

    theorem :: AMISTD_5:11

    

     Th11: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be non empty FinPartState of S st ( IC S) in ( dom p) holds for k be Nat holds p is q -autonomic iff ( IncIC (p,k)) is ( Reloc (q,k)) -autonomic

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be non empty FinPartState of S such that

       A1: ( IC S) in ( dom p);

      let k be Nat;

      hereby

        assume

         A2: p is q -autonomic;

        thus ( IncIC (p,k)) is ( Reloc (q,k)) -autonomic

        proof

          let P,Q be Instruction-Sequence of S such that

           A3: ( Reloc (q,k)) c= P and

           A4: ( Reloc (q,k)) c= Q;

          let s1,s2 be State of S such that

           A5: ( IncIC (p,k)) c= s1 and

           A6: ( IncIC (p,k)) c= s2;

          let i be Nat;

          

           A7: ( dom ( Start-At ((( IC ( Comput ((Q +* q),(s2 +* p),i))) + k),S))) = {( IC S)};

          

           A8: ( dom ( DataPart p)) misses ( dom ( Start-At ((( IC ( Comput ((Q +* q),(s2 +* p),i))) + k),S))) by MEMSTR_0: 4;

          

           A9: ( dom ( Start-At ((( IC ( Comput ((P +* q),(s1 +* p),i))) + k),S))) = {( IC S)};

          

           A10: ( dom ( DataPart p)) misses ( dom ( Start-At ((( IC ( Comput ((P +* q),(s1 +* p),i))) + k),S))) by MEMSTR_0: 4;

          

           A11: q c= (P +* q) & q c= (Q +* q) by FUNCT_4: 25;

          p c= (s1 +* p) & p c= (s2 +* p) by FUNCT_4: 25;

          then

           A12: (( Comput ((P +* q),(s1 +* p),i)) | ( dom p)) = (( Comput ((Q +* q),(s2 +* p),i)) | ( dom p)) by A2, A11;

          

           A13: ( DataPart p) c= p by MEMSTR_0: 12;

          

           A14: (( Comput (P,s1,i)) | ( dom ( DataPart p))) = (( IncIC (( Comput ((P +* q),(s1 +* p),i)),k)) | ( dom ( DataPart p))) by A1, A2, A5, Th9, A3

          .= (( Comput ((P +* q),(s1 +* p),i)) | ( dom ( DataPart p))) by A10, FUNCT_4: 72

          .= (( Comput ((Q +* q),(s2 +* p),i)) | ( dom ( DataPart p))) by A12, A13, RELAT_1: 11, RELAT_1: 153

          .= (( IncIC (( Comput ((Q +* q),(s2 +* p),i)),k)) | ( dom ( DataPart p))) by A8, FUNCT_4: 72

          .= (( Comput (Q,s2,i)) | ( dom ( DataPart p))) by A1, A2, A6, Th9, A4;

          

           A15: {( IC S)} c= ( dom p) by A1, ZFMISC_1: 31;

          

           A16: ( Start-At (( IC ( Comput ((P +* q),(s1 +* p),i))),S)) = (( Comput ((P +* q),(s1 +* p),i)) | {( IC S)}) by MEMSTR_0: 18

          .= (( Comput ((Q +* q),(s2 +* p),i)) | {( IC S)}) by A12, A15, RELAT_1: 153

          .= ( Start-At (( IC ( Comput ((Q +* q),(s2 +* p),i))),S)) by MEMSTR_0: 18;

          

           A18: (( Comput (P,s1,i)) | ( dom ( Start-At ((( IC p) + k),S)))) = (( IncIC (( Comput ((P +* q),(s1 +* p),i)),k)) | ( dom ( Start-At ((( IC p) + k),S)))) by A1, A2, A5, Th9, A3

          .= ( Start-At ((( IC ( Comput ((P +* q),(s1 +* p),i))) + k),S)) by A9

          .= ( Start-At ((( IC ( Comput ((Q +* q),(s2 +* p),i))) + k),S)) by A16, MEMSTR_0: 21

          .= (( IncIC (( Comput ((Q +* q),(s2 +* p),i)),k)) | ( dom ( Start-At ((( IC p) + k),S)))) by A7

          .= (( Comput (Q,s2,i)) | ( dom ( Start-At ((( IC p) + k),S)))) by A1, A2, A6, Th9, A4;

          

           A20: ( dom p) = ( {( IC S)} \/ ( dom ( DataPart p))) by A1, MEMSTR_0: 24;

          

           A21: (( Comput (P,s1,i)) | ( dom p)) = ((( Comput (P,s1,i)) | {( IC S)}) \/ (( Comput (P,s1,i)) | ( dom ( DataPart p)))) by A20, RELAT_1: 78

          .= (( Comput (Q,s2,i)) | ( dom p)) by A20, A14, A18, RELAT_1: 78;

          

           A22: ( dom ( IncIC (p,k))) = (( dom p) \/ ( dom ( Start-At ((( IC p) + k),S)))) by FUNCT_4:def 1;

          

           A23: (( Comput (P,s1,i)) | ( dom ( IncIC (p,k)))) = ((( Comput (P,s1,i)) | ( dom p)) \/ (( Comput (P,s1,i)) | ( dom ( Start-At ((( IC p) + k),S))))) by A22, RELAT_1: 78

          .= (( Comput (Q,s2,i)) | ( dom ( IncIC (p,k)))) by A22, A18, A21, RELAT_1: 78;

          thus (( Comput (P,s1,i)) | ( dom ( IncIC (p,k)))) = (( Comput (Q,s2,i)) | ( dom ( IncIC (p,k)))) by A23;

        end;

      end;

      assume

       A24: ( IncIC (p,k)) is ( Reloc (q,k)) -autonomic;

      

       A25: ( DataPart p) c= ( IncIC (p,k)) by MEMSTR_0: 62;

      let P,Q be Instruction-Sequence of S such that

       A26: q c= P and

       A27: q c= Q;

      

       A28: ( Reloc (q,k)) c= (P +* ( Reloc (q,k))) & ( Reloc (q,k)) c= (Q +* ( Reloc (q,k))) by FUNCT_4: 25;

      let s1,s2 be State of S such that

       A29: p c= s1 and

       A30: p c= s2;

      let i be Nat;

      ( IncIC (p,k)) c= (s1 +* ( IncIC (p,k))) & ( IncIC (p,k)) c= (s2 +* ( IncIC (p,k))) by FUNCT_4: 25;

      then

       A31: (( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i)) | ( dom ( IncIC (p,k)))) = (( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i)) | ( dom ( IncIC (p,k)))) by A24, A28;

      

       A32: ( dom ( Start-At ((( IC ( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i))) -' k),S))) = {( IC S)};

      

       A33: ( dom ( DataPart p)) misses ( dom ( Start-At ((( IC ( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i))) -' k),S))) by MEMSTR_0: 4;

      

       A34: ( dom ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i))) -' k),S))) = {( IC S)};

      

       A35: ( dom ( DataPart p)) misses ( dom ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i))) -' k),S))) by MEMSTR_0: 4;

      

       A36: (( Comput (P,s1,i)) | ( dom ( DataPart p))) = (( DecIC (( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i)),k)) | ( dom ( DataPart p))) by A1, A24, A29, Th10, A26

      .= (( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i)) | ( dom ( DataPart p))) by A35, FUNCT_4: 72

      .= (( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i)) | ( dom ( DataPart p))) by A31, A25, RELAT_1: 11, RELAT_1: 153

      .= (( DecIC (( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i)),k)) | ( dom ( DataPart p))) by A33, FUNCT_4: 72

      .= (( Comput (Q,s2,i)) | ( dom ( DataPart p))) by A1, A24, A30, Th10, A27;

      ( IC S) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

      then

       A37: {( IC S)} c= ( dom ( IncIC (p,k))) by ZFMISC_1: 31;

      

       A38: ( Start-At (( IC ( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i))),S)) = (( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i)) | {( IC S)}) by MEMSTR_0: 18

      .= (( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i)) | {( IC S)}) by A31, A37, RELAT_1: 153

      .= ( Start-At (( IC ( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i))),S)) by MEMSTR_0: 18;

      

       A40: (( Comput (P,s1,i)) | ( dom ( Start-At (( IC p),S)))) = (( DecIC (( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i)),k)) | ( dom ( Start-At (( IC p),S)))) by A1, A24, A29, Th10, A26

      .= ( Start-At ((( IC ( Comput ((P +* ( Reloc (q,k))),(s1 +* ( IncIC (p,k))),i))) -' k),S)) by A34

      .= ( Start-At ((( IC ( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i))) -' k),S)) by A38, MEMSTR_0: 22

      .= (( DecIC (( Comput ((Q +* ( Reloc (q,k))),(s2 +* ( IncIC (p,k))),i)),k)) | ( dom ( Start-At (( IC p),S)))) by A32

      .= (( Comput (Q,s2,i)) | ( dom ( Start-At (( IC p),S)))) by A1, A24, A30, Th10, A27;

      

      thus (( Comput (P,s1,i)) | ( dom p)) = (( Comput (P,s1,i)) | ( dom (( Start-At (( IC p),S)) +* ( DataPart p)))) by A1, MEMSTR_0: 19

      .= (( Comput (P,s1,i)) | (( dom ( Start-At (( IC p),S))) \/ ( dom ( DataPart p)))) by FUNCT_4:def 1

      .= ((( Comput (Q,s2,i)) | ( dom ( Start-At (( IC p),S)))) \/ (( Comput (Q,s2,i)) | ( dom ( DataPart p)))) by A36, A40, RELAT_1: 78

      .= (( Comput (Q,s2,i)) | (( dom ( Start-At (( IC p),S))) \/ ( dom ( DataPart p)))) by RELAT_1: 78

      .= (( Comput (Q,s2,i)) | ( dom (( Start-At (( IC p),S)) +* ( DataPart p)))) by FUNCT_4:def 1

      .= (( Comput (Q,s2,i)) | ( dom p)) by A1, MEMSTR_0: 19;

    end;

    definition

      let N, S;

      :: AMISTD_5:def5

      attr S is relocable1 means

      : Def5: for k be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S, s1,s2 be State of S st p c= s1 & ( IncIC (p,k)) c= s2 holds for P1,P2 be Instruction-Sequence of S st q c= P1 & ( Reloc (q,k)) c= P2 holds for i be Nat holds ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),k)) = ( CurInstr (P2,( Comput (P2,s2,i))));

      :: AMISTD_5:def6

      attr S is relocable2 means

      : Def6: for k be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S, s1,s2 be State of S st p c= s1 & ( IncIC (p,k)) c= s2 holds for P1,P2 be Instruction-Sequence of S st q c= P1 & ( Reloc (q,k)) c= P2 holds for i be Nat holds (( Comput (P1,s1,i)) | ( dom ( DataPart p))) = (( Comput (P2,s2,i)) | ( dom ( DataPart p)));

    end

    

     Lm1: for k be Nat holds for q be non halt-free finitethe InstructionsF of ( STC N) -valued NAT -defined Function holds for p be non emptyq -autonomic FinPartState of ( STC N), s1,s2 be State of ( STC N) st p c= s1 & ( IncIC (p,k)) c= s2 holds for P1,P2 be Instruction-Sequence of ( STC N) st q c= P1 & ( Reloc (q,k)) c= P2 holds for i be Nat holds (( IC ( Comput (P1,s1,i))) + k) = ( IC ( Comput (P2,s2,i))) & ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),k)) = ( CurInstr (P2,( Comput (P2,s2,i))))

    proof

      let k be Nat;

      let q be non halt-free finitethe InstructionsF of ( STC N) -valued NAT -defined Function;

      let p be non emptyq -autonomic FinPartState of ( STC N), s1,s2 be State of ( STC N) such that

       A1: p c= s1 and

       A2: ( IncIC (p,k)) c= s2;

      

       A3: ( IC ( STC N)) in ( dom p) by Th6;

      let P1,P2 be Instruction-Sequence of ( STC N) such that

       A4: q c= P1 & ( Reloc (q,k)) c= P2;

      set s3 = (s1 +* ( DataPart s2));

      defpred Z[ Nat] means (( IC ( Comput (P1,s1,$1))) + k) = ( IC ( Comput (P2,s2,$1))) & ( IncAddr (( CurInstr (P1,( Comput (P1,s1,$1)))),k)) = ( CurInstr (P2,( Comput (P2,s2,$1))));

      

       A5: for i be Nat st Z[i] holds Z[(i + 1)]

      proof

        set DPp = ( DataPart p);

        let i be Nat such that

         A6: (( IC ( Comput (P1,s1,i))) + k) = ( IC ( Comput (P2,s2,i))) and

         A7: ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),k)) = ( CurInstr (P2,( Comput (P2,s2,i))));

        set Cs2i1 = ( Comput (P2,s2,(i + 1)));

        set Cs3i = ( Comput (P1,s3,i));

        set Cs2i = ( Comput (P2,s2,i));

        set Cs3i1 = ( Comput (P1,s3,(i + 1)));

        set Cs1i1 = ( Comput (P1,s1,(i + 1)));

        set Cs1i = ( Comput (P1,s1,i));

         A8:

        now

          reconsider loc = ( IC Cs1i1) as Nat;

          assume

           A9: (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1))));

          reconsider kk = loc as Nat;

          

           A10: loc in ( dom q) by Def4, A4, A1;

          

           A11: (loc + k) in ( dom ( Reloc (q,k))) by A10, COMPOS_1: 46;

          

           A12: ( dom P2) = NAT by PARTFUN1:def 2;

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

          

          then ( CurInstr (P1,Cs1i1)) = (P1 . loc) by PARTFUN1:def 6

          .= (q . loc) by A10, A4, GRFUNC_1: 2;

          

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = (( Reloc (q,k)) . (loc + k)) by A10, COMPOS_1: 35

          .= (P2 . ( IC ( Comput (P2,s2,(i + 1))))) by A9, A11, A4, GRFUNC_1: 2

          .= ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A12, PARTFUN1:def 6;

        end;

        set I = ( CurInstr (P1,Cs1i));

        

         A13: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

        reconsider j = ( IC Cs1i) as Nat;

        

         A14: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

        

         A15: the InstructionsF of ( STC N) = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} by AMISTD_1:def 7;

        per cases by A15, TARSKI:def 2;

          suppose I = [ 0 , 0 , 0 ];

          then

           A16: I = ( halt ( STC N));

          

          thus (( IC ( Comput (P1,s1,(i + 1)))) + k) = (( IC Cs1i) + k) by A14, A16, EXTPRO_1:def 3

          .= ( IC ( Comput (P2,s2,(i + 1)))) by A6, A13, A16, A7, EXTPRO_1:def 3;

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A8;

        end;

          suppose I = [1, 0 , 0 ];

          then

           A17: ( InsCode I) = 1;

          then

           A18: ( Exec (I,Cs2i)) = ( IncIC (Cs2i,1)) by AMISTD_1: 20;

          

          thus (( IC ( Comput (P1,s1,(i + 1)))) + k) = ((( IC Cs1i) + 1) + k) by A14, A17, AMISTD_1: 9

          .= ( IC ( Exec (I,Cs2i))) by A18, A6, MEMSTR_0: 53

          .= ( IC ( Comput (P2,s2,(i + 1)))) by A13, A7, COMPOS_0: 4;

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A8;

        end;

      end;

      

       A19: ( IC ( STC N)) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

      now

        

        thus (( IC ( Comput (P1,s1, 0 ))) + k) = (( IC p) + k) by A1, A3, GRFUNC_1: 2

        .= ( IC ( IncIC (p,k))) by MEMSTR_0: 53

        .= ( IC ( Comput (P2,s2, 0 ))) by A2, A19, GRFUNC_1: 2;

        reconsider loc = ( IC p) as Nat;

        

         A20: ( IC p) = ( IC s1) by A1, A3, GRFUNC_1: 2;

        ( IC p) = ( IC ( Comput (P1,s1, 0 ))) by A1, A3, GRFUNC_1: 2;

        then

         A21: loc in ( dom q) by Def4, A4, A1;

        

         A22: (( IC p) + k) in ( dom ( Reloc (q,k))) by A21, COMPOS_1: 46;

        

         A23: ( IC ( STC N)) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

        

         A24: (q . ( IC p)) = (P1 . ( IC s1)) by A20, A21, A4, GRFUNC_1: 2;

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

        

        then

         A25: ( CurInstr (P2,( Comput (P2,s2, 0 )))) = (P2 . ( IC ( Comput (P2,s2, 0 )))) by PARTFUN1:def 6

        .= (P2 . ( IC ( IncIC (p,k)))) by A2, A23, GRFUNC_1: 2

        .= (P2 . (( IC p) + k)) by MEMSTR_0: 53

        .= (( Reloc (q,k)) . (( IC p) + k)) by A22, A4, GRFUNC_1: 2;

        

         A26: ( dom P1) = NAT by PARTFUN1:def 2;

        ( CurInstr (P1,( Comput (P1,s1, 0 )))) = (P1 . ( IC s1)) by A26, PARTFUN1:def 6;

        hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1, 0 )))),k)) = ( CurInstr (P2,( Comput (P2,s2, 0 )))) by A25, A21, A24, COMPOS_1: 35;

      end;

      then

       A27: Z[ 0 ];

      thus for i be Nat holds Z[i] from NAT_1:sch 2( A27, A5);

    end;

    registration

      let N;

      cluster ( STC N) -> relocable1 relocable2;

      coherence by Lm1;

    end

    registration

      let N be with_zero set;

      cluster relocable1 relocable2 for relocable IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    reserve S for relocable1 relocable2 relocable IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

    theorem :: AMISTD_5:12

    

     Th12: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of S, k be Nat st ( IC S) in ( dom p) holds p is q -halted iff ( IncIC (p,k)) is ( Reloc (q,k)) -halted

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of S, k be Nat;

      assume ( IC S) in ( dom p);

      hereby

        assume

         A1: p is q -halted;

        thus ( IncIC (p,k)) is ( Reloc (q,k)) -halted

        proof

          let t be State of S;

          assume

           A2: ( IncIC (p,k)) c= t;

          let P be Instruction-Sequence of S such that

           A3: ( Reloc (q,k)) c= P;

          reconsider Q = (P +* q) as Instruction-Sequence of S;

          set s = (t +* p);

          

           A4: q c= Q by FUNCT_4: 25;

          

           A5: p c= (t +* p) by FUNCT_4: 25;

          then Q halts_on s by A1, A4;

          then

          consider u be Nat such that

           A6: ( CurInstr (Q,( Comput (Q,s,u)))) = ( halt S);

          take u;

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

          hence ( IC ( Comput (P,t,u))) in ( dom P);

          ( CurInstr (P,( Comput (P,t,u)))) = ( IncAddr (( halt S),k)) by A2, A6, Def5, A3, A4, A5

          .= ( halt S) by COMPOS_0: 4;

          hence thesis;

        end;

      end;

      assume

       A7: ( IncIC (p,k)) is ( Reloc (q,k)) -halted;

      let t be State of S;

      assume

       A8: p c= t;

      let P be Instruction-Sequence of S such that

       A9: q c= P;

      reconsider Q = (P +* ( Reloc (q,k))) as Instruction-Sequence of S;

      set s = (t +* ( IncIC (p,k)));

      

       A10: ( Reloc (q,k)) c= Q by FUNCT_4: 25;

      

       A11: ( IncIC (p,k)) c= (t +* ( IncIC (p,k))) by FUNCT_4: 25;

      then Q halts_on s by A7, A10;

      then

      consider u be Nat such that

       A12: ( CurInstr (Q,( Comput (Q,s,u)))) = ( halt S);

      take u;

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

      hence ( IC ( Comput (P,t,u))) in ( dom P);

      ( IncAddr (( CurInstr (P,( Comput (P,t,u)))),k)) = ( halt S) by A8, A12, Def5, A11, A9, A10

      .= ( IncAddr (( halt S),k)) by COMPOS_0: 4;

      hence ( CurInstr (P,( Comput (P,t,u)))) = ( halt S) by COMPOS_0: 6;

    end;

    theorem :: AMISTD_5:13

    

     Th13: for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -haltedq -autonomic non empty FinPartState of S st ( IC S) in ( dom p) holds for k be Nat holds ( DataPart ( Result (q,p))) = ( DataPart ( Result (( Reloc (q,k)),( IncIC (p,k)))))

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -haltedq -autonomic non empty FinPartState of S such that

       A1: ( IC S) in ( dom p);

      let k be Nat;

      consider s be State of S such that

       A2: p c= s by PBOOLE: 141;

      consider P be Instruction-Sequence of S such that

       A3: q c= P by PBOOLE: 145;

      

       A4: ( IncIC (p,k)) is ( Reloc (q,k)) -halted( Reloc (q,k)) -autonomic by A1, Th12, Th11;

      

       A5: ( IncIC (p,k)) is Autonomy of ( Reloc (q,k)) by A4, EXTPRO_1:def 12;

      P halts_on s by A2, A3, EXTPRO_1:def 11;

      then

      consider j1 be Nat such that

       A6: ( Result (P,s)) = ( Comput (P,s,j1)) and

       A7: ( CurInstr (P,( Result (P,s)))) = ( halt S) by EXTPRO_1:def 9;

      consider t be State of S such that

       A8: ( IncIC (p,k)) c= t by PBOOLE: 141;

      consider Q be Instruction-Sequence of S such that

       A9: ( Reloc (q,k)) c= Q by PBOOLE: 145;

      (Q . ( IC ( Comput (Q,t,j1)))) = ( CurInstr (Q,( Comput (Q,t,j1)))) by PBOOLE: 143

      .= ( IncAddr (( CurInstr (P,( Comput (P,s,j1)))),k)) by Def5, A3, A9, A2, A8

      .= ( halt S) by A6, A7, COMPOS_0: 4;

      then

       A10: ( Result (Q,t)) = ( Comput (Q,t,j1)) by EXTPRO_1: 7;

      

       A11: (( Comput (Q,t,j1)) | ( dom ( DataPart p))) = (( Comput (P,s,j1)) | ( dom ( DataPart p))) by Def6, A9, A3, A8, A2;

      

       A12: ( DataPart p) = ( DataPart ( IncIC (p,k))) by MEMSTR_0: 51;

      

       A13: p is Autonomy of q by EXTPRO_1:def 12;

      

      thus ( DataPart ( Result (q,p))) = ( DataPart (( Result (P,s)) | ( dom p))) by A2, A3, A13, EXTPRO_1:def 13

      .= (( Result (P,s)) | (( dom p) /\ ( Data-Locations S))) by RELAT_1: 71

      .= (( Result (P,s)) | ( dom ( DataPart p))) by MEMSTR_0: 14

      .= (( Result (Q,t)) | (( dom ( IncIC (p,k))) /\ ( Data-Locations S))) by A6, A10, A11, A12, MEMSTR_0: 14

      .= ((( Result (Q,t)) | ( dom ( IncIC (p,k)))) | ( Data-Locations S)) by RELAT_1: 71

      .= ( DataPart ( Result (( Reloc (q,k)),( IncIC (p,k))))) by A5, A9, A8, EXTPRO_1:def 13;

    end;

    registration

      let N, S;

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomicq -halted non empty FinPartState of S, k be Nat;

      cluster ( IncIC (p,k)) -> ( Reloc (q,k)) -halted;

      coherence

      proof

        ( IC S) in ( dom p) by Th6;

        hence thesis by Th12;

      end;

    end

    theorem :: AMISTD_5:14

    for F be data-only PartFunc of ( FinPartSt S), ( FinPartSt S), l be Nat holds for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function, p be q -autonomicq -halted non empty FinPartState of S st ( IC S) in ( dom p) holds for k be Nat holds (q,p) computes F iff (( Reloc (q,k)),( IncIC (p,k))) computes F

    proof

      let F be data-only PartFunc of ( FinPartSt S), ( FinPartSt S), l be Nat;

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function, p be q -autonomicq -halted non empty FinPartState of S such that

       A1: ( IC S) in ( dom p);

      let k be Nat;

      hereby

        assume

         A2: (q,p) computes F;

        thus (( Reloc (q,k)),( IncIC (p,k))) computes F

        proof

          let x be set;

          assume

           A3: x in ( dom F);

          then

          consider d1 be FinPartState of S such that

           A4: x = d1 and

           A5: (p +* d1) is Autonomy of q and

           A6: (F . d1) c= ( Result (q,(p +* d1))) by A2;

          ( dom F) c= ( FinPartSt S) by RELAT_1:def 18;

          then

          reconsider d = x as FinPartState of S by A3, MEMSTR_0: 76;

          reconsider d as data-only FinPartState of S by A3, MEMSTR_0:def 17;

          ( dom (p +* d)) = (( dom p) \/ ( dom d)) by FUNCT_4:def 1;

          then

           A7: ( IC S) in ( dom (p +* d)) by A1, XBOOLE_0:def 3;

          

           A8: (p +* d) is q -autonomic by A4, A5, EXTPRO_1:def 12;

          then

           A9: ( IncIC ((p +* d),k)) is ( Reloc (q,k)) -autonomic by A7, Th11;

          

           A10: (p +* d) is q -halted by A4, A5, EXTPRO_1:def 12;

          reconsider pd = (p +* d) as q -haltedq -autonomic non empty FinPartState of S by A4, A5, EXTPRO_1:def 12;

          

           A11: ( DataPart ( Result (q,pd))) = ( DataPart ( Result (( Reloc (q,k)),( IncIC ((p +* d),k))))) by A7, Th13

          .= ( DataPart ( Result (( Reloc (q,k)),(( IncIC (p,k)) +* d)))) by MEMSTR_0: 54;

          reconsider Fs1 = (F . d1) as FinPartState of S by A6;

          take d;

          thus x = d;

          (( IncIC (p,k)) +* d) = ( IncIC ((p +* d),k)) by MEMSTR_0: 54;

          hence (( IncIC (p,k)) +* d) is Autonomy of ( Reloc (q,k)) by A8, A10, A9, EXTPRO_1:def 12;

          

           A12: Fs1 is data-only by A3, A4, MEMSTR_0:def 17;

          (F . d1) c= ( DataPart ( Result (( Reloc (q,k)),(( IncIC (p,k)) +* d)))) by A6, A12, A4, A11, MEMSTR_0: 5;

          hence (F . d) c= ( Result (( Reloc (q,k)),(( IncIC (p,k)) +* d))) by A4, A12, MEMSTR_0: 5;

        end;

      end;

      assume

       A13: (( Reloc (q,k)),( IncIC (p,k))) computes F;

      let x be set;

      assume

       A14: x in ( dom F);

      then

      consider d1 be FinPartState of S such that

       A15: x = d1 and

       A16: (( IncIC (p,k)) +* d1) is Autonomy of ( Reloc (q,k)) and

       A17: (F . d1) c= ( Result (( Reloc (q,k)),(( IncIC (p,k)) +* d1))) by A13;

      ( dom F) c= ( FinPartSt S) by RELAT_1:def 18;

      then

      reconsider d = x as FinPartState of S by A14, MEMSTR_0: 76;

      reconsider d as data-only FinPartState of S by A14, MEMSTR_0:def 17;

      

       A18: ( dom (p +* d)) = (( dom p) \/ ( dom d)) by FUNCT_4:def 1;

      then

       A19: ( IC S) in ( dom (p +* d)) by A1, XBOOLE_0:def 3;

      

       A20: (( IncIC (p,k)) +* d) = ( IncIC ((p +* d),k)) by MEMSTR_0: 54;

      ( IncIC ((p +* d),k)) is ( Reloc (q,k)) -autonomic by A15, A16, A20, EXTPRO_1:def 12;

      then

       A21: (p +* d) is q -autonomic by A19, Th11;

      

       A22: ( IncIC ((p +* d),k)) is ( Reloc (q,k)) -halted by A15, A16, A20, EXTPRO_1:def 12;

      

       A23: (p +* d) is q -halted by A19, Th12, A21, A22;

      reconsider pd = (p +* d) as q -haltedq -autonomic non empty FinPartState of S by A19, Th12, A21, A22;

      

       A24: ( IC S) in ( dom pd) by A18, A1, XBOOLE_0:def 3;

      

       A25: ( DataPart ( Result (( Reloc (q,k)),(( IncIC (p,k)) +* d1)))) = ( DataPart ( Result (( Reloc (q,k)),( IncIC ((p +* d),k))))) by A15, MEMSTR_0: 54

      .= ( DataPart ( Result (q,(p +* d)))) by Th13, A24;

      take d;

      thus x = d;

      thus (p +* d) is Autonomy of q by A21, A23, EXTPRO_1:def 12;

      reconsider Fs1 = (F . d1) as FinPartState of S by A17;

      

       A26: Fs1 is data-only by A14, A15, MEMSTR_0:def 17;

      then (F . d1) c= ( DataPart ( Result (q,(p +* d)))) by A25, A17, MEMSTR_0: 5;

      hence thesis by A15, A26, MEMSTR_0: 5;

    end;

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

    theorem :: AMISTD_5:15

    for q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function holds for p be q -autonomic FinPartState of S st ( IC S) in ( dom p) holds ( IC p) in ( dom q)

    proof

      let q be non halt-free finitethe InstructionsF of S -valued NAT -defined Function;

      let p be q -autonomic FinPartState of S;

      assume

       A1: ( IC S) in ( dom p);

      then

       A2: p is non empty;

      consider s be State of S such that

       A3: p c= s by PBOOLE: 141;

      set P = ( the Instruction-Sequence of S +* q);

      

       A4: q c= P by FUNCT_4: 25;

      ( IC ( Comput (P,s, 0 ))) in ( dom q) by A4, Def4, A2, A3;

      hence ( IC p) in ( dom q) by A3, A1, GRFUNC_1: 2;

    end;

    definition

      let N be with_zero set;

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

      let k be Nat;

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

      :: AMISTD_5:def7

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

    end

    registration

      let N be with_zero set;

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

      cluster parahalting -> 0 -halting for NAT -definedthe InstructionsF of S -valued Function;

      coherence ;

      cluster 0 -halting -> parahalting for NAT -definedthe InstructionsF of S -valued Function;

      coherence ;

    end