amistd_2.miz

    begin

    reserve k,m for Nat,

x,x1,x2,x3,y,y1,y2,y3,X,Y,Z for set,

N for with_zero set;

    theorem :: AMISTD_2:1

    for I be Instruction of ( STC N) holds ( JumpPart I) = 0 ;

    definition

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

      :: AMISTD_2:def1

      attr I is with_explicit_jumps means

      : Def1: ( JUMP I) = ( rng ( JumpPart I));

    end

    definition

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

      :: AMISTD_2:def2

      attr S is with_explicit_jumps means

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

    end

    registration

      let N be with_zero set;

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

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    theorem :: AMISTD_2:2



     Th2: for S be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of S st for f be Element of NAT holds ( NIC (I,f)) = {(f + 1)} holds ( JUMP I) is empty

    proof

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

      assume

       A1: for f be Element of NAT holds ( NIC (I,f)) = {(f + 1)};

      set p = 1, q = 2;

      reconsider p, q as Element of NAT ;

      set X = the set of all ( NIC (I,f)) where f be Nat;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);



       A3: ( NIC (I,p)) = {(p + 1)} by A1;



       A4: ( NIC (I,q)) = {(q + 1)} by A1;



       A5: {( succ p)} in X by A3;



       A6: {( succ q)} in X by A4;



       A7: x in {( succ p)} by A2, A5, SETFAM_1:def 1;



       A8: x in {( succ q)} by A2, A6, SETFAM_1:def 1;

      x = ( succ p) by A7, TARSKI:def 1;

      hence contradiction by A8, TARSKI:def 1;

    end;

    registration

      let N be with_zero set, I be Instruction of ( STC N);

      cluster ( JUMP I) -> empty;

      coherence

      proof

        per cases by AMISTD_1: 6;

          suppose ( InsCode I) = 0 ;

          then for f be Nat holds ( NIC (I,f)) = {f} by AMISTD_1: 2, AMISTD_1: 4;

          hence thesis by AMISTD_1: 1;

        end;

          suppose ( InsCode I) = 1;

          then for f be Element of NAT holds ( NIC (I,f)) = {(f + 1)} by AMISTD_1: 10;

          hence thesis by Th2;

        end;

      end;

    end

    theorem :: AMISTD_2:3

    for T be InsType of the InstructionsF of ( STC N) holds ( JumpParts T) = { 0 }

    proof

      let T be InsType of the InstructionsF of ( STC N);

      set A = { ( JumpPart I) where I be Instruction of ( STC N) : ( InsCode I) = T };

       { 0 } = A

      proof

        hereby

          let a be object;

          assume a in { 0 };

          then

           A1: a = 0 by TARSKI:def 1;



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

          then

           A3: ( InsCodes the InstructionsF of ( STC N)) = { 0 , 1} by MCART_1: 91;

          per cases by A3, TARSKI:def 2;

            suppose

             A4: T = 0 ;

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



             A5: ( JumpPart I) = 0 ;

            ( InsCode I) = 0 ;

            hence a in A by A1, A4, A5;

          end;

            suppose

             A6: T = 1;

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



             A7: ( JumpPart I) = 0 ;

            ( InsCode I) = 1;

            hence a in A by A1, A6, A7;

          end;

        end;

        let a be object;

        assume a in A;

        then ex I be Instruction of ( STC N) st a = ( JumpPart I) & ( InsCode I) = T;

        then a = 0 ;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;



     Lm1: for I be Instruction of ( Trivial-AMI N) holds ( JumpPart I) = 0

    proof

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

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

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

      hence thesis;

    end;



     Lm2: for T be InsType of the InstructionsF of ( Trivial-AMI N) holds ( JumpParts T) = { 0 }

    proof

      let T be InsType of the InstructionsF of ( Trivial-AMI N);

      set A = { ( JumpPart I) where I be Instruction of ( Trivial-AMI N) : ( InsCode I) = T };

       { 0 } = A

      proof

        hereby

          let a be object;

          assume a in { 0 };

          then

           A1: a = 0 by TARSKI:def 1;



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

          then ( InsCodes the InstructionsF of ( Trivial-AMI N)) = { 0 } by MCART_1: 92;

          then

           A3: T = 0 by TARSKI:def 1;

          reconsider I = [ 0 , 0 , 0 ] as Instruction of ( Trivial-AMI N) by A2, TARSKI:def 1;



           A4: ( JumpPart I) = 0 ;

          ( InsCode I) = 0 ;

          hence a in A by A1, A3, A4;

        end;

        let a be object;

        assume a in A;

        then ex I be Instruction of ( Trivial-AMI N) st a = ( JumpPart I) & ( InsCode I) = T;

        then a = 0 by Lm1;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      let N be with_zero set;

      cluster ( STC N) -> with_explicit_jumps;

      coherence

      proof

        let I be Instruction of ( STC N);

        thus ( JUMP I) = ( rng ( JumpPart I));

      end;

    end

    registration

      let N be with_zero set;

      cluster standard halting with_explicit_jumps for 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, I be Instruction of ( Trivial-AMI N);

      cluster ( JUMP I) -> empty;

      coherence

      proof

        for f be Nat holds ( NIC (I,f)) = {f} by AMISTD_1: 2, AMISTD_1: 17;

        hence thesis by AMISTD_1: 1;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( Trivial-AMI N) -> with_explicit_jumps;

      coherence

      proof

        thus ( Trivial-AMI N) is with_explicit_jumps

        proof

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

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

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

          hence ( JUMP I) = ( rng ( JumpPart I));

        end;

      end;

    end

    registration

      let N be with_zero set;

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

      existence

      proof

        take ( Trivial-AMI N);

        thus thesis;

      end;

    end

    registration

      let N be with_zero set;

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

      cluster -> with_explicit_jumps for Instruction of S;

      coherence by Def2;

    end

    theorem :: AMISTD_2:4



     Th4: for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of S st I is halting holds ( JUMP I) is empty

    proof

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

      assume I is halting;

      then for l be Nat holds ( NIC (I,l)) = {l} by AMISTD_1: 2;

      hence thesis by AMISTD_1: 1;

    end;

    registration

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

      cluster ( JUMP I) -> empty;

      coherence by Th4;

    end

    theorem :: AMISTD_2:5

    for S be halting with_explicit_jumps IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of S st I is ins-loc-free holds ( JUMP I) is empty

    proof

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

       A1: ( JumpPart I) is empty;



       A2: ( rng ( JumpPart I)) = {} by A1;

      ( JUMP I) c= ( rng ( JumpPart I)) by Def1;

      hence thesis by A2;

    end;

    registration

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

      cluster halting -> ins-loc-free for Instruction of S;

      coherence

      proof

        let I be Instruction of S;

        assume I is halting;

        then

         A1: ( JUMP I) is empty by Th4;

        ( rng ( JumpPart I)) = ( JUMP I) by Def1;

        hence ( JumpPart I) is empty by A1;

      end;

    end

    registration

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

      cluster sequential -> ins-loc-free for Instruction of S;

      coherence

      proof

        let I be Instruction of S;

        assume I is sequential;

        then

         A1: ( JUMP I) is empty by AMISTD_1: 13;

        ( rng ( JumpPart I)) = ( JUMP I) by Def1;

        hence ( JumpPart I) is empty by A1;

      end;

    end

    begin

    registration

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

      cluster ( IncAddr (I,k)) -> halting;

      coherence by COMPOS_0: 4;

    end

    theorem :: AMISTD_2:6

    for S be standard halting with_explicit_jumps IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of S st I is sequential holds ( IncAddr (I,k)) is sequential by COMPOS_0: 4;

    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_2:def3

      attr I is IC-relocable means

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

    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_2:def4

      attr S is IC-relocable means

      : Def4: for I be Instruction of S holds I is IC-relocable;

    end

    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;

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

      coherence

      proof

        let I be Instruction of S such that

         A1: I is sequential;

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

        set s2 = ( IncIC (s1,k));

        ( IC S) in ( dom (( IC S) .--> (( IC s1) + k))) by TARSKI:def 1;



        then

         A2: ( IC s2) = ((( IC S) .--> (( IC s1) + k)) . ( IC S)) by FUNCT_4: 13

        .= (( IC s1) + k) by FUNCOP_1: 72;



         A3: ( IC ( Exec (I,s2))) = (( IC s2) + 1) by A1

        .= ((( IC s1) + 1) + k) by A2;



         A4: ( IncAddr (I,j)) = I by A1, COMPOS_0: 4;

        ( IC ( Exec (I,s1))) = (( IC s1) + 1) by A1;

        hence (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A1, A3, A4, COMPOS_0: 4;

      end;

    end

    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;

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

      coherence

      proof

        let I be Instruction of S such that

         A1: I is halting;

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

        set s2 = ( IncIC (s1,k));



         A2: ( IC S) in ( dom (( IC S) .--> (( IC s1) + k))) by TARSKI:def 1;



        thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC s1) + k) by A1, EXTPRO_1:def 3

        .= ((( IC S) .--> (( IC s1) + k)) . ( IC S)) by FUNCOP_1: 72

        .= ( IC s2) by A2, FUNCT_4: 13

        .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A1, EXTPRO_1:def 3;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> IC-relocable;

      coherence

      proof

        thus ( STC N) is IC-relocable

        proof

          let I be Instruction of ( STC N), j,k be Nat, s1 be State of ( STC N);

          set s2 = ( IncIC (s1,k));

          ( IC ( STC N)) in ( dom (( IC ( STC N)) .--> (( IC s1) + k))) by TARSKI:def 1;



          then

           A1: ( IC s2) = ((( IC ( STC N)) .--> (( IC s1) + k)) . ( IC ( STC N))) by FUNCT_4: 13

          .= (( IC s1) + k) by FUNCOP_1: 72;

          per cases by AMISTD_1: 6;

            suppose

             A2: ( InsCode I) = 1;

            then

             A3: ( InsCode ( IncAddr (I,k))) = 1 by COMPOS_0:def 9;



             A4: ( IncAddr (I,j)) = I by COMPOS_0: 4;

            ( IC ( Exec (I,s1))) = (( IC s1) + 1) by A2, AMISTD_1: 9;



            hence (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC s2) + 1) by A1, A4

            .= ( IC ( Exec (( IncAddr (( IncAddr (I,j)),k)),s2))) by A4, A3, AMISTD_1: 9

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

          end;

            suppose ( InsCode I) = 0 ;

            then

             A5: I is halting by AMISTD_1: 4;



            hence (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC s1) + k) by EXTPRO_1:def 3

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A1, A5, EXTPRO_1:def 3;

          end;

        end;

      end;

    end

    registration

      let N be with_zero set;

      cluster halting with_explicit_jumps for standard 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;

      cluster IC-relocable for with_explicit_jumps halting standard 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, S be IC-relocable IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N;

      cluster -> IC-relocable for Instruction of S;

      coherence by Def4;

    end

    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;

      cluster IC-relocable for Instruction of S;

      existence

      proof

        take the halting Instruction of S;

        thus thesis;

      end;

    end

    theorem :: AMISTD_2:7



     Th7: for S be halting with_explicit_jumps IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be IC-relocable Instruction of S holds for k be Nat, s be State of S holds (( IC ( Exec (I,s))) + k) = ( IC ( Exec (( IncAddr (I,k)),( IncIC (s,k)))))

    proof

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

      let k be Nat, s be State of S;



       A1: (k + 0 qua Nat) = k;



      thus (( IC ( Exec (I,s))) + k) = (( IC ( Exec (( IncAddr (I, 0 )),s))) + k) by COMPOS_0: 3

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

    end;

    registration

      let N be with_zero set, S be IC-relocable standard with_explicit_jumps halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F,G be really-closed Program of S;

      cluster (F ';' G) -> really-closed;

      coherence

      proof

        set P = (F ';' G), k = (( card F) -' 1);

        let f be Nat such that

         A1: f in ( dom P);



         A2: ( dom P) = (( dom ( CutLastLoc F)) \/ ( dom ( Reloc (G,k)))) by FUNCT_4:def 1;



         A3: ( dom ( CutLastLoc F)) c= ( dom F) by GRFUNC_1: 2;



         A4: ( dom ( Reloc (G,k))) = { (m + k) where m be Nat : m in ( dom ( IncAddr (G,k))) } by VALUED_1:def 12;

        let x be object;

        assume x in ( NIC ((P /. f),f));

        then

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

         A5: x = ( IC ( Exec ((P /. f),s2))) and

         A6: ( IC s2) = f;



         A7: (P /. f) = (P . f) by A1, PARTFUN1:def 6;

        per cases by A1, A2, XBOOLE_0:def 3;

          suppose

           A8: f in ( dom ( CutLastLoc F));

          then

           A9: ( NIC ((F /. f),f)) c= ( dom F) by A3, AMISTD_1:def 9;

          ( dom ( CutLastLoc F)) = (( dom F) \ {( LastLoc F)}) by VALUED_1: 36;

          then

           A10: f in ( dom F) by A8, XBOOLE_0:def 5;

          ( dom ( CutLastLoc F)) misses ( dom ( Reloc (G,(( card F) -' 1)))) by COMPOS_1: 18;

          then

           A11: not f in ( dom ( Reloc (G,(( card F) -' 1)))) by A8, XBOOLE_0: 3;



           A12: (P /. f) = (P . f) by A1, PARTFUN1:def 6

          .= (( CutLastLoc F) . f) by A11, FUNCT_4: 11

          .= (F . f) by A8, GRFUNC_1: 2

          .= (F /. f) by A10, PARTFUN1:def 6;

          ( IC ( Exec ((F /. f),s2))) in ( NIC ((F /. f),f)) by A6;

          then

           A13: x in ( dom F) by A5, A9, A12;

          ( dom F) c= ( dom P) by COMPOS_1: 21;

          hence thesis by A13;

        end;

          suppose

           A14: f in ( dom ( Reloc (G,k)));

          then

          consider m be Nat such that

           A15: f = (m + k) and

           A16: m in ( dom ( IncAddr (G,k))) by A4;



           A17: m in ( dom G) by A16, COMPOS_1:def 21;

          then

           A18: ( NIC ((G /. m),m)) c= ( dom G) by AMISTD_1:def 9;



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

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

          reconsider v = (( IC S) .--> m) as FinPartState of S by A19;

          set s1 = (s2 +* v);



           A20: (P /. f) = (( Reloc (G,k)) . f) by A7, A14, FUNCT_4: 13

          .= (( IncAddr (G,k)) . m) by A15, A16, VALUED_1:def 12;



           A21: ((( IC S) .--> m) . ( IC S)) = m by FUNCOP_1: 72;



           A22: ( IC S) in {( IC S)} by TARSKI:def 1;



           A23: ( dom (( IC S) .--> m)) = {( IC S)};

          reconsider w = (( IC S) .--> (( IC s1) + k)) as FinPartState of S by A19;



           A24: ( dom (s1 +* (( IC S) .--> (( IC s1) + k)))) = the carrier of S by PARTFUN1:def 2;



           A25: ( dom s2) = the carrier of S by PARTFUN1:def 2;

          for a be object st a in ( dom s2) holds (s2 . a) = ((s1 +* (( IC S) .--> (( IC s1) + k))) . a)

          proof

            let a be object such that a in ( dom s2);



             A26: ( dom (( IC S) .--> (( IC s1) + k))) = {( IC S)};

            per cases ;

              suppose

               A27: a = ( IC S);



              hence (s2 . a) = (( IC s1) + k) by A6, A15, A23, A21, A22, FUNCT_4: 13

              .= ((( IC S) .--> (( IC s1) + k)) . a) by A27, FUNCOP_1: 72

              .= ((s1 +* (( IC S) .--> (( IC s1) + k))) . a) by A22, A26, A27, FUNCT_4: 13;

            end;

              suppose

               A28: a <> ( IC S);

              then

               A29: not a in ( dom (( IC S) .--> (( IC s1) + k))) by TARSKI:def 1;

               not a in ( dom (( IC S) .--> m)) by A28, TARSKI:def 1;

              then (s1 . a) = (s2 . a) by FUNCT_4: 11;

              hence thesis by A29, FUNCT_4: 11;

            end;

          end;

          then

           A30: s2 = ( IncIC (s1,k)) by A24, A25, FUNCT_1: 2;

          set s3 = s1;



           A31: ( IC s3) = m by A21, A22, A23, FUNCT_4: 13;

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

          reconsider k, m as Element of NAT ;



           A32: x = ( IC ( Exec (( IncAddr ((G /. m),k)),s2))) by A5, A17, A20, COMPOS_1:def 21

          .= (( IC ( Exec ((G /. m),s3))) + k) by A30, Th7;

          ( IC ( Exec ((G /. m),s3))) in ( NIC ((G /. m),m)) by A31;

          then ( IC ( Exec ((G /. m),s3))) in ( dom G) by A18;

          then ( IC ( Exec ((G /. m),s3))) in ( dom ( IncAddr (G,k))) by COMPOS_1:def 21;

          then x in ( dom ( Reloc (G,k))) by A4, A32;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

      end;

    end

    theorem :: AMISTD_2:8

    for I be Instruction of ( Trivial-AMI N) holds ( JumpPart I) = 0 by Lm1;

    theorem :: AMISTD_2:9

    for T be InsType of the InstructionsF of ( Trivial-AMI N) holds ( JumpParts T) = { 0 } by Lm2;

    reserve n,m for Nat;

    theorem :: AMISTD_2:10

    for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds for s be State of S, I be Program of S holds for P1,P2 be Instruction-Sequence of S st I c= P1 & I c= P2 & for m st m < n holds ( IC ( Comput (P2,s,m))) in ( dom I) holds for m st m <= n holds ( Comput (P1,s,m)) = ( Comput (P2,s,m))

    proof

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

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

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

       A1: I c= P1 & I c= P2;

      assume that

       A2: for m st m < n holds ( IC ( Comput (P2,s,m))) in ( dom I);

      defpred X[ Nat] means $1 <= n implies ( Comput (P1,s,$1)) = ( Comput (P2,s,$1));



       A3: for m st X[m] holds X[(m + 1)]

      proof

        let m such that

         A4: X[m];



         A5: ( Comput (P2,s,(m + 1))) = ( Following (P2,( Comput (P2,s,m)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P2,( Comput (P2,s,m)))),( Comput (P2,s,m))));



         A6: ( Comput (P1,s,(m + 1))) = ( Following (P1,( Comput (P1,s,m)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P1,( Comput (P1,s,m)))),( Comput (P1,s,m))));

        assume

         A7: (m + 1) <= n;

        then m < n by NAT_1: 13;

        then

         A8: ( IC ( Comput (P1,s,m))) = ( IC ( Comput (P2,s,m))) by A4;

        m < n by A7, NAT_1: 13;

        then

         A9: ( IC ( Comput (P2,s,m))) in ( dom I) by A2;

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

        then

         A10: ( IC ( Comput (P2,s,m))) in ( dom P2);

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

        then ( IC ( Comput (P1,s,m))) in ( dom P1);



        then ( CurInstr (P1,( Comput (P1,s,m)))) = (P1 . ( IC ( Comput (P1,s,m)))) by PARTFUN1:def 6

        .= (I . ( IC ( Comput (P1,s,m)))) by A9, A8, A1, GRFUNC_1: 2

        .= (P2 . ( IC ( Comput (P2,s,m)))) by A9, A8, A1, GRFUNC_1: 2

        .= ( CurInstr (P2,( Comput (P2,s,m)))) by A10, PARTFUN1:def 6;

        hence thesis by A4, A6, A5, A7, NAT_1: 13;

      end;



       A11: X[ 0 ];

      thus for m holds X[m] from NAT_1:sch 2( A11, A3);

    end;

    theorem :: AMISTD_2:11

    for S be IC-Ins-separated halting 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 IC-Ins-separated halting 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

       A1: s = ( Following (P,s));



       A2: for n st X[n] holds X[(n + 1)] by A1, EXTPRO_1: 3;



       A3: X[ 0 ];

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

    end;