scmfsa8a.miz



    begin

    reserve m for Nat;

    reserve P for Instruction-Sequence of SCM+FSA ;

    set A = NAT ;

    set D = ( Data-Locations SCM+FSA );

    set SA0 = ( Start-At ( 0 , SCM+FSA ));

    set T = (( intloc 0 ) .--> 1);

    ::$Canceled

    theorem :: SCMFSA8A:8

    

     Th1: for i be Instruction of SCM+FSA , a be Int-Location, n be Element of NAT holds not i destroys a implies not ( IncAddr (i,n)) destroys a

    proof

      let i be Instruction of SCM+FSA ;

      let a be Int-Location;

      let n be Element of NAT ;

      assume

       A1: not i destroys a;

      ( InsCode i) = 0 or ... or ( InsCode i) = 12 by SCMFSA_2: 16;

      per cases ;

        suppose ( InsCode i) = 0 ;

        then i = ( halt SCM+FSA ) by SCMFSA_2: 95;

        then ( IncAddr (i,n)) = ( halt SCM+FSA ) by COMPOS_0: 4;

        hence thesis by SCMFSA7B: 5;

      end;

        suppose ( InsCode i) = 1;

        then ex da,db be Int-Location st i = (da := db) by SCMFSA_2: 30;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 2;

        then ex da,db be Int-Location st i = ( AddTo (da,db)) by SCMFSA_2: 31;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 3;

        then ex da,db be Int-Location st i = ( SubFrom (da,db)) by SCMFSA_2: 32;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 4;

        then ex da,db be Int-Location st i = ( MultBy (da,db)) by SCMFSA_2: 33;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 5;

        then ex da,db be Int-Location st i = ( Divide (da,db)) by SCMFSA_2: 34;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 6;

        then

        consider loc be Nat such that

         A2: i = ( goto loc) by SCMFSA_2: 35;

        ( IncAddr (i,n)) = ( goto (loc + n)) by A2, SCMFSA_4: 1;

        hence thesis by SCMFSA7B: 11;

      end;

        suppose ( InsCode i) = 7;

        then

        consider loc be Nat, da be Int-Location such that

         A3: i = (da =0_goto loc) by SCMFSA_2: 36;

        ( IncAddr (i,n)) = (da =0_goto (loc + n)) by A3, SCMFSA_4: 2;

        hence thesis by SCMFSA7B: 12;

      end;

        suppose ( InsCode i) = 8;

        then

        consider loc be Nat, da be Int-Location such that

         A4: i = (da >0_goto loc) by SCMFSA_2: 37;

        ( IncAddr (i,n)) = (da >0_goto (loc + n)) by A4, SCMFSA_4: 3;

        hence thesis by SCMFSA7B: 13;

      end;

        suppose ( InsCode i) = 9;

        then ex db,da be Int-Location, g be FinSeq-Location st i = (da := (g,db)) by SCMFSA_2: 38;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 10;

        then ex db,da be Int-Location, g be FinSeq-Location st i = ((g,db) := da) by SCMFSA_2: 39;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 11;

        then ex da be Int-Location, g be FinSeq-Location st i = (da :=len g) by SCMFSA_2: 40;

        hence thesis by A1, COMPOS_0: 4;

      end;

        suppose ( InsCode i) = 12;

        then ex da be Int-Location, g be FinSeq-Location st i = (g :=<0,...,0> da) by SCMFSA_2: 41;

        hence thesis by A1, COMPOS_0: 4;

      end;

    end;

    theorem :: SCMFSA8A:9

    

     Th2: for P be preProgram of SCM+FSA , n be Element of NAT , a be Int-Location st not P destroys a holds not ( Reloc (P,n)) destroys a

    proof

      let I be preProgram of SCM+FSA ;

      let n be Element of NAT ;

      let a be Int-Location;

      

       A1: ( dom ( IncAddr (I,n))) = ( dom I) by COMPOS_1:def 21;

      

       A2: ( dom ( Shift (( IncAddr (I,n)),n))) = { (m + n) where m be Nat : m in ( dom ( IncAddr (I,n))) } by VALUED_1:def 12;

      assume

       A3: not I destroys a;

      now

        let i be Instruction of SCM+FSA ;

        assume i in ( rng ( Reloc (I,n)));

        then

        consider x be object such that

         A4: x in ( dom ( Shift (( IncAddr (I,n)),n))) and

         A5: i = (( Shift (( IncAddr (I,n)),n)) . x) by FUNCT_1:def 3;

        consider m be Nat such that

         A6: x = (m + n) and

         A7: m in ( dom ( IncAddr (I,n))) by A2, A4;

        

         A8: (I . m) in ( rng I) by A1, A7, FUNCT_1:def 3;

        ( rng I) c= the InstructionsF of SCM+FSA by RELAT_1:def 19;

        then

        reconsider ii = (I . m) as Instruction of SCM+FSA by A8;

        

         A9: not ii destroys a by A3, A8, SCMFSA7B:def 4;

        i = (( IncAddr (I,n)) . m) by A5, A6, A7, VALUED_1:def 12

        .= ( IncAddr ((I /. m),n)) by A1, A7, COMPOS_1:def 21

        .= ( IncAddr (ii,n)) by A1, A7, PARTFUN1:def 6;

        hence not i destroys a by A9, Th1;

      end;

      hence thesis by SCMFSA7B:def 4;

    end;

    theorem :: SCMFSA8A:10

    

     Th3: for P be good preProgram of SCM+FSA , n be Element of NAT holds ( Reloc (P,n)) is good

    proof

      let I be good preProgram of SCM+FSA ;

      let n be Element of NAT ;

       not I destroys ( intloc 0 ) by SCMFSA7B:def 5;

      then not ( Reloc (I,n)) destroys ( intloc 0 ) by Th2;

      hence thesis by SCMFSA7B:def 5;

    end;

    theorem :: SCMFSA8A:11

    

     Th4: for I,J be preProgram of SCM+FSA , a be Int-Location holds not I destroys a & not J destroys a implies not (I +* J) destroys a

    proof

      let I,J be preProgram of SCM+FSA ;

      let a be Int-Location;

      assume

       A1: not I destroys a;

      assume

       A2: not J destroys a;

      now

        let i be Instruction of SCM+FSA ;

        

         A3: ( rng (I +* J)) c= (( rng I) \/ ( rng J)) by FUNCT_4: 17;

        assume

         A4: i in ( rng (I +* J));

        per cases by A4, A3, XBOOLE_0:def 3;

          suppose i in ( rng I);

          hence not i destroys a by A1, SCMFSA7B:def 4;

        end;

          suppose i in ( rng J);

          hence not i destroys a by A2, SCMFSA7B:def 4;

        end;

      end;

      hence thesis by SCMFSA7B:def 4;

    end;

    theorem :: SCMFSA8A:12

    

     Th5: for I,J be good preProgram of SCM+FSA holds (I +* J) is good

    proof

      let I,J be good preProgram of SCM+FSA ;

       not I destroys ( intloc 0 ) & not J destroys ( intloc 0 ) by SCMFSA7B:def 5;

      then not (I +* J) destroys ( intloc 0 ) by Th4;

      hence thesis by SCMFSA7B:def 5;

    end;

    theorem :: SCMFSA8A:13

    

     Th6: for I be preProgram of SCM+FSA , a be Int-Location st not I destroys a holds not ( Directed I) destroys a

    proof

      let I be preProgram of SCM+FSA ;

      let a be Int-Location;

      assume

       A1: not I destroys a;

      now

        let i be Instruction of SCM+FSA ;

        

         A2: ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

        assume i in ( rng ( Directed I));

        then

        consider x be object such that

         A3: x in ( dom ( Directed I)) and

         A4: i = (( Directed I) . x) by FUNCT_1:def 3;

        per cases ;

          suppose (I . x) <> ( halt SCM+FSA );

          then i = (I . x) by A4, FUNCT_4: 105;

          then i in ( rng I) by A3, A2, FUNCT_1:def 3;

          hence not i destroys a by A1, SCMFSA7B:def 4;

        end;

          suppose (I . x) = ( halt SCM+FSA );

          then i = ( goto ( card I)) by A3, A4, A2, FUNCT_4: 106;

          hence not i destroys a by SCMFSA7B: 11;

        end;

      end;

      hence thesis by SCMFSA7B:def 4;

    end;

    registration

      let I be good Program of SCM+FSA ;

      cluster ( Directed I) -> good;

      correctness

      proof

         not I destroys ( intloc 0 ) by SCMFSA7B:def 5;

        then not ( Directed I) destroys ( intloc 0 ) by Th6;

        hence thesis by SCMFSA7B:def 5;

      end;

    end

    registration

      let I be Program of SCM+FSA ;

      cluster ( Directed I) -> initial;

      correctness ;

    end

    registration

      let I,J be good Program of SCM+FSA ;

      cluster (I ";" J) -> good;

      coherence

      proof

        

         A1: ( Reloc (J,( card I))) is good by Th3;

        (I ";" J) = (( CutLastLoc ( stop ( Directed I))) +* ( Reloc (J,(( card ( stop I)) -' 1)))) by SCMFSA6A: 37

        .= (( Directed I) +* ( Reloc (J,( card I)))) by COMPOS_1: 71;

        hence thesis by A1, Th5;

      end;

    end

    

     Lm1: for l be Nat holds ( dom ( Load ( goto l))) = { 0 } & 0 in ( dom ( Load ( goto l))) & (( Load ( goto l)) . 0 ) = ( goto l) & ( card ( Load ( goto l))) = 1 & not ( halt SCM+FSA ) in ( rng ( Load ( goto l)))

    proof

      let l be Nat;

      thus ( dom ( Load ( goto l))) = { 0 } by AFINSQ_1:def 4, CARD_1: 49;

      hence 0 in ( dom ( Load ( goto l))) by TARSKI:def 1;

      thus (( Load ( goto l)) . 0 ) = ( goto l);

      

      thus ( card ( Load ( goto l))) = ( card <%( goto l)%>)

      .= 1 by AFINSQ_1: 34;

      now

        

         A1: ( rng ( Load ( goto l))) = {( goto l)} by AFINSQ_1: 33;

        assume ( halt SCM+FSA ) in ( rng ( Load ( goto l)));

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis;

    end;

    definition

      let l be Nat;

      :: SCMFSA8A:def1

      func Goto l -> Program of SCM+FSA equals ( Load ( goto l));

      coherence ;

    end

    registration

      let l be Element of NAT ;

      cluster ( Goto l) -> halt-free good;

      coherence

      proof

        set I = ( Load ( goto l));

         not ( halt SCM+FSA ) in ( rng I) by Lm1;

        hence ( Goto l) is halt-free;

        now

          let x be Instruction of SCM+FSA ;

          

           A1: ( rng ( Load ( goto l))) = {( goto l)} by AFINSQ_1: 33;

          assume x in ( rng ( Load ( goto l)));

          then x = ( goto l) by A1, TARSKI:def 1;

          hence not x destroys ( intloc 0 ) by SCMFSA7B: 11;

        end;

        then not I destroys ( intloc 0 ) by SCMFSA7B:def 4;

        hence thesis by SCMFSA7B:def 5;

      end;

    end

    registration

      cluster halt-free good for Program of SCM+FSA ;

      existence

      proof

        take ( Goto 0 );

        thus thesis;

      end;

    end

    definition

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be initial Program of SCM+FSA ;

      :: SCMFSA8A:def2

      pred I is_pseudo-closed_on s,P means ex k be Nat st ( IC ( Comput ((P +* I),( Initialize s),k))) = ( card I) & for n be Nat st n < k holds ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I);

    end

    definition

      ::$Canceled

      let s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA , I be initial Program of SCM+FSA ;

      :: SCMFSA8A:def4

      func pseudo-LifeSpan (s,P,I) -> Nat means

      : Def3: ( IC ( Comput ((P +* I),( Initialize s),it ))) = ( card I) & for n be Nat st not ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) holds it <= n;

      existence

      proof

        consider k be Nat such that

         A2: ( IC ( Comput ((P +* I),( Initialize s),k))) = ( card I) & for n be Nat st n < k holds ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) by A1;

        take k;

        thus thesis by A2;

      end;

      uniqueness

      proof

        reconsider II = I as initial preProgram of SCM+FSA ;

        let k1,k2 be Nat such that

         A3: ( IC ( Comput ((P +* I),( Initialize s),k1))) = ( card I) and

         A4: (for n be Nat st not ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) holds k1 <= n) & ( IC ( Comput ((P +* I),( Initialize s),k2))) = ( card I) and

         A5: for n be Nat st not ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) holds k2 <= n;

         A6:

        now

          assume k2 < k1;

          then ( card II) in ( dom II) by A4;

          hence contradiction;

        end;

        now

          assume k1 < k2;

          then ( card II) in ( dom II) by A3, A5;

          hence contradiction;

        end;

        hence thesis by A6, XXREAL_0: 1;

      end;

    end

    theorem :: SCMFSA8A:14

    

     Th7: for I,J be Program of SCM+FSA , x be set holds x in ( dom I) implies ((I ";" J) . x) = (( Directed I) . x)

    proof

      let I,J be Program of SCM+FSA ;

      let x be set;

      assume x in ( dom I);

      then

       A1: x in ( dom ( Directed I)) by FUNCT_4: 99;

      ( Directed I) c= (I ";" J) by SCMFSA6A: 16;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: SCMFSA8A:15

    for l be Nat holds ( card ( Goto l)) = 1 by Lm1;

    theorem :: SCMFSA8A:16

    for P be preProgram of SCM+FSA , x be set st x in ( dom P) holds ((P . x) = ( halt SCM+FSA ) implies (( Directed P) . x) = ( goto ( card P))) & ((P . x) <> ( halt SCM+FSA ) implies (( Directed P) . x) = (P . x)) by FUNCT_4: 105, FUNCT_4: 106;

    theorem :: SCMFSA8A:17

    

     Th10: for s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA , I be initial Program of SCM+FSA st I is_pseudo-closed_on (s,P) holds for n be Nat st n < ( pseudo-LifeSpan (s,P,I)) holds ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) & ( CurInstr ((P +* I),( Comput ((P +* I),( Initialize s),n)))) <> ( halt SCM+FSA )

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be initial Program of SCM+FSA ;

      set k = ( pseudo-LifeSpan (s,P,I));

      assume

       A1: I is_pseudo-closed_on (s,P);

      then

       A2: ( IC ( Comput ((P +* I),( Initialize s),k))) = ( card I) by Def3;

      hereby

        let n be Nat;

        assume

         A3: n < k;

        hence

         A4: ( IC ( Comput ((P +* I),( Initialize s),n))) in ( dom I) by A1, Def3;

        assume ( CurInstr ((P +* I),( Comput ((P +* I),( Initialize s),n)))) = ( halt SCM+FSA );

        then ( IC ( Comput ((P +* I),( Initialize s),k))) = ( IC ( Comput ((P +* I),( Initialize s),n))) by A3, EXTPRO_1: 5;

        hence contradiction by A2, A4;

      end;

    end;

    theorem :: SCMFSA8A:18

    

     Th11: for s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA , I,J be Program of SCM+FSA st I is_pseudo-closed_on (s,P) holds for k be Nat st k <= ( pseudo-LifeSpan (s,P,I)) holds ( Comput ((P +* I),( Initialize s),k)) = ( Comput ((P +* (I ";" J)),( Initialize s),k))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I,J be Program of SCM+FSA ;

      set s1 = ( Initialize s);

      set s2 = ( Initialize s);

      defpred P[ Nat] means $1 <= ( pseudo-LifeSpan (s,P,I)) implies ( Comput ((P +* I),s1,$1)) = ( Comput ((P +* (I ";" J)),s2,$1));

      

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

      

       A2: ( dom (P +* (I ";" J))) = NAT by PARTFUN1:def 2;

      assume

       A3: I is_pseudo-closed_on (s,P);

       A4:

      now

        let k be Nat;

        assume

         A5: P[k];

        thus P[(k + 1)]

        proof

          

           A6: ( Comput ((P +* (I ";" J)),s2,(k + 1))) = ( Following ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),s2,k)))) by EXTPRO_1: 3

          .= ( Exec (( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),s2,k)))),( Comput ((P +* (I ";" J)),s2,k))));

          

           A7: ( Comput ((P +* I),s1,(k + 1))) = ( Following ((P +* I),( Comput ((P +* I),s1,k)))) by EXTPRO_1: 3

          .= ( Exec (( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))),( Comput ((P +* I),s1,k))));

          

           A8: ( dom I) c= ( dom (I ";" J)) by SCMFSA6A: 17;

          

           A9: (k + 0 ) < (k + 1) by XREAL_1: 6;

          assume

           A10: (k + 1) <= ( pseudo-LifeSpan (s,P,I));

          then

           A11: k < ( pseudo-LifeSpan (s,P,I)) by A9, XXREAL_0: 2;

          then

           A12: ( IC ( Comput ((P +* I),s1,k))) in ( dom I) by A3, Th10;

          

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

          

           A14: (I ";" J) c= (P +* (I ";" J)) by FUNCT_4: 25;

          

           A15: ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = ((P +* I) . ( IC ( Comput ((P +* I),s1,k)))) by A1, PARTFUN1:def 6

          .= (I . ( IC ( Comput ((P +* I),s1,k)))) by A12, A13, GRFUNC_1: 2;

          then (I . ( IC ( Comput ((P +* I),s1,k)))) <> ( halt SCM+FSA ) by A3, A11, Th10;

          

          then ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = ((I ";" J) . ( IC ( Comput ((P +* I),s1,k)))) by A12, A15, SCMFSA6A: 15

          .= ((P +* (I ";" J)) . ( IC ( Comput ((P +* I),s1,k)))) by A12, A8, A14, GRFUNC_1: 2

          .= ((P +* (I ";" J)) . ( IC ( Comput ((P +* (I ";" J)),s2,k)))) by A5, A10, A9, XXREAL_0: 2

          .= ( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),s2,k)))) by A2, PARTFUN1:def 6;

          hence thesis by A5, A10, A9, A7, A6, XXREAL_0: 2;

        end;

      end;

      

       A16: P[ 0 ];

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

    end;

    ::$Canceled

    theorem :: SCMFSA8A:21

    

     Th12: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (s,P) holds for k be Nat st k <= ( LifeSpan ((P +* I),( Initialize s))) holds ( Comput ((P +* I),( Initialize s),k)) = ( Comput ((P +* ( Directed I)),( Initialize s),k)) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),( Initialize s),k)))) <> ( halt SCM+FSA )

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      assume that

       A1: I is_halting_on (s,P);

      

       A2: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      

       A3: ( dom (P +* I)) = NAT by PARTFUN1:def 2;

      set s2 = ( Initialize s);

      set s1 = ( Initialize s);

      defpred P[ Nat] means $1 <= ( LifeSpan ((P +* I),s1)) implies ( Comput ((P +* I),s1,$1)) = ( Comput ((P +* ( Directed I)),s2,$1)) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,$1)))) <> ( halt SCM+FSA );

      ( IC s1) = 0 by MEMSTR_0: 47;

      then

       A4: ( IC s1) in ( dom I) by AFINSQ_1: 65;

      

       A5: I c= (P +* I) by FUNCT_4: 25;

       A6:

      now

        let k be Element of NAT ;

        ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

        then

         A7: ( IC ( Comput ((P +* I),s1,k))) in ( dom ( Directed I)) by AMISTD_1: 21, A4, A5;

        

         A8: ((P +* ( Directed I)) /. ( IC ( Comput ((P +* ( Directed I)),s2,k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,k)))) by A2, PARTFUN1:def 6;

        

         A9: ( Directed I) c= (P +* ( Directed I)) by FUNCT_4: 25;

        assume ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),s2,k));

        

        then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* I),s1,k)))) by A8

        .= (( Directed I) . ( IC ( Comput ((P +* I),s1,k)))) by A7, A9, GRFUNC_1: 2;

        then

         A10: ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) in ( rng ( Directed I)) by A7, FUNCT_1:def 3;

        assume ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) = ( halt SCM+FSA );

        hence contradiction by A10, SCMFSA6A: 1;

      end;

      now

        

         A11: (P +* I) halts_on s1 by A1, SCMFSA7B:def 7;

        

         A12: ( dom I) c= ( dom ( Directed I)) by FUNCT_4: 99;

        let k be Nat;

        assume

         A13: k <= ( LifeSpan ((P +* I),s1)) implies ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),s2,k));

        

         A14: ( Comput ((P +* ( Directed I)),s2,(k + 1))) = ( Following ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))),( Comput ((P +* ( Directed I)),s2,k))));

        

         A15: ( IC ( Comput ((P +* I),s1,k))) in ( dom I) by AMISTD_1: 21, A4, A5;

        

         A16: I c= (P +* I) by FUNCT_4: 25;

        

         A17: ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = ((P +* I) . ( IC ( Comput ((P +* I),s1,k)))) by A3, PARTFUN1:def 6

        .= (I . ( IC ( Comput ((P +* I),s1,k)))) by A15, A16, GRFUNC_1: 2;

        

         A18: (k + 0 ) < (k + 1) by XREAL_1: 6;

        

         A19: ((P +* ( Directed I)) /. ( IC ( Comput ((P +* ( Directed I)),s2,k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,k)))) by A2, PARTFUN1:def 6;

        

         A20: ( Directed I) c= (P +* ( Directed I)) by FUNCT_4: 25;

        assume

         A21: (k + 1) <= ( LifeSpan ((P +* I),s1));

        then k < ( LifeSpan ((P +* I),s1)) by A18, XXREAL_0: 2;

        then (I . ( IC ( Comput ((P +* I),s1,k)))) <> ( halt SCM+FSA ) by A17, A11, EXTPRO_1:def 15;

        

        then

         A22: ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = (( Directed I) . ( IC ( Comput ((P +* I),s1,k)))) by A17, FUNCT_4: 105

        .= ((P +* ( Directed I)) . ( IC ( Comput ((P +* I),s1,k)))) by A15, A12, A20, GRFUNC_1: 2

        .= ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) by A13, A21, A18, A19, XXREAL_0: 2;

        ( Comput ((P +* I),s1,(k + 1))) = ( Following ((P +* I),( Comput ((P +* I),s1,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))),( Comput ((P +* I),s1,k))));

        hence ( Comput ((P +* I),s1,(k + 1))) = ( Comput ((P +* ( Directed I)),s2,(k + 1))) by A13, A21, A18, A22, A14, XXREAL_0: 2;

        hence ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,(k + 1))))) <> ( halt SCM+FSA ) by A6;

      end;

      then

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

      now

        assume 0 <= ( LifeSpan ((P +* I),s1));

        thus ( Comput ((P +* I),s1, 0 )) = ( Comput ((P +* ( Directed I)),s2, 0 ));

        hence ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2, 0 )))) <> ( halt SCM+FSA ) by A6;

      end;

      then

       A24: P[ 0 ];

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

    end;

    theorem :: SCMFSA8A:22

    

     Th13: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (s,P) holds ( IC ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),( Initialize s),( LifeSpan ((P +* I),( Initialize s)))))) = ( DataPart ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1))))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      set s1 = ( Initialize s);

      set s2 = ( Initialize s);

      set m1 = ( LifeSpan ((P +* I),s1));

      

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

      

       A2: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      assume that

       A3: I is_halting_on (s,P);

      

       A4: (P +* I) halts_on s1 by A3, SCMFSA7B:def 7;

      set l1 = ( IC ( Comput ((P +* I),s1,m1)));

      ( IC s1) = 0 by MEMSTR_0: 47;

      then

       A5: ( IC s1) in ( dom I) by AFINSQ_1: 65;

      

       A6: I c= (P +* I) by FUNCT_4: 25;

      

       A7: l1 in ( dom I) by A5, A6, AMISTD_1: 21;

      

       A8: ( Comput ((P +* I),( Initialize s),m1)) = ( Comput ((P +* ( Directed I)),( Initialize s),m1)) by A3, Th12;

      then ( IC ( Comput ((P +* ( Directed I)),s2,m1))) in ( dom I) by A7;

      then

       A9: ( IC ( Comput ((P +* ( Directed I)),s2,m1))) in ( dom ( Directed I)) by FUNCT_4: 99;

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

      

      then

       A10: (I . l1) = ((P +* I) . ( IC ( Comput ((P +* I),s1,m1)))) by A7, GRFUNC_1: 2

      .= ( CurInstr ((P +* I),( Comput ((P +* I),s1,m1)))) by A1, PARTFUN1:def 6

      .= ( halt SCM+FSA ) by A4, EXTPRO_1:def 15;

      l1 = ( IC ( Comput ((P +* ( Directed I)),s2,m1))) by A8;

      

      then

       A11: ((P +* ( Directed I)) . l1) = (( Directed I) . l1) by A9, FUNCT_4: 13

      .= ( goto ( card I)) by A7, A10, FUNCT_4: 106;

      

       A12: ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,m1)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,m1)))) by A2, PARTFUN1:def 6

      .= ( goto ( card I)) by A11, A8;

      

       A13: ( Comput ((P +* ( Directed I)),s2,(m1 + 1))) = ( Following ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,m1)))) by EXTPRO_1: 3

      .= ( Exec (( goto ( card I)),( Comput ((P +* ( Directed I)),s2,m1)))) by A12;

      hence ( IC ( Comput ((P +* ( Directed I)),s2,(m1 + 1)))) = ( card I) by SCMFSA_2: 69;

      

       A14: (for a be Int-Location holds (( Comput ((P +* ( Directed I)),s2,(m1 + 1))) . a) = (( Comput ((P +* ( Directed I)),s2,m1)) . a)) & for f be FinSeq-Location holds (( Comput ((P +* ( Directed I)),s2,(m1 + 1))) . f) = (( Comput ((P +* ( Directed I)),s2,m1)) . f) by A13, SCMFSA_2: 69;

      ( DataPart ( Comput ((P +* I),s1,m1))) = ( DataPart ( Comput ((P +* ( Directed I)),s2,m1))) by A8;

      hence thesis by A14, SCMFSA_M: 2;

    end;

    

     Lm2: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (s,P) holds ( Directed I) is_pseudo-closed_on (s,P) & ( pseudo-LifeSpan (s,P,( Directed I))) = (( LifeSpan ((P +* I),( Initialize s))) + 1)

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      set s1 = ( Initialize s);

      set s2 = ( Initialize s);

      set m1 = ( LifeSpan ((P +* I),s1));

      ( IC s2) = 0 by MEMSTR_0: 47;

      then

       A1: ( IC s2) in ( dom I) by AFINSQ_1: 65;

      

       A2: I c= (P +* I) by FUNCT_4: 25;

      assume that

       A3: I is_halting_on (s,P);

      

       A4: ( dom I) = ( dom ( Directed I)) by FUNCT_4: 99;

       A5:

      now

        let n be Nat;

        assume n < (m1 + 1);

        then n <= m1 by NAT_1: 13;

        then ( Comput ((P +* I),s1,n)) = ( Comput ((P +* ( Directed I)),s2,n)) by A3, Th12;

        then ( IC ( Comput ((P +* I),s1,n))) = ( IC ( Comput ((P +* ( Directed I)),s2,n)));

        hence ( IC ( Comput ((P +* ( Directed I)),s2,n))) in ( dom ( Directed I)) by A4, AMISTD_1: 21, A1, A2;

      end;

      ( card I) = ( card ( Directed I)) by SCMFSA6A: 36;

      then

       A6: ( IC ( Comput ((P +* ( Directed I)),s2,(m1 + 1)))) = ( card ( Directed I)) by A3, Th13;

      hence

       A7: ( Directed I) is_pseudo-closed_on (s,P) by A5;

      for n be Nat st not ( IC ( Comput ((P +* ( Directed I)),s2,n))) in ( dom ( Directed I)) holds (m1 + 1) <= n by A5;

      hence thesis by A6, A7, Def3;

    end;

    theorem :: SCMFSA8A:23

    for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (s,P) holds ( Directed I) is_pseudo-closed_on (s,P) by Lm2;

    theorem :: SCMFSA8A:24

    for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (s,P) holds ( pseudo-LifeSpan (s,P,( Directed I))) = (( LifeSpan ((P +* I),( Initialize s))) + 1) by Lm2;

    theorem :: SCMFSA8A:25

    for I,J be Program of SCM+FSA holds (( Directed I) ";" J) = (I ";" J);

    theorem :: SCMFSA8A:26

    

     Th17: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA , J be Program of SCM+FSA st I is_halting_on (s,P) holds (for k be Nat st k <= ( LifeSpan ((P +* I),( Initialize s))) holds ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k))) = ( IC ( Comput ((P +* (I ";" J)),( Initialize s),k))) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),( Initialize s),k)))) = ( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),( Initialize s),k))))) & ( DataPart ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) = ( DataPart ( Comput ((P +* (I ";" J)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) & ( IC ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) = ( IC ( Comput ((P +* (I ";" J)),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1))))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      

       A1: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      

       A2: ( dom (P +* (I ";" J))) = NAT by PARTFUN1:def 2;

      set s2 = ( Initialize s);

      

       A3: (( Directed I) ";" J) = (I ";" J);

      set s1 = ( Initialize s);

      assume

       A4: I is_halting_on (s,P);

      then

       A5: (( LifeSpan ((P +* I),s1)) + 1) = ( pseudo-LifeSpan (s,P,( Directed I))) by Lm2;

      

       A6: ( Directed I) is_pseudo-closed_on (s,P) by A4, Lm2;

      hereby

        let k be Nat;

        assume k <= ( LifeSpan ((P +* I),s1));

        then

         A7: k < ( pseudo-LifeSpan (s,P,( Directed I))) by A5, NAT_1: 13;

        then

         A8: ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k))) in ( dom ( Directed I)) by A6, Def3;

        ( Comput ((P +* ( Directed I)),( Initialize s),k)) = ( Comput ((P +* (I ";" J)),s2,k)) by A3, A4, Lm2, A7, Th11;

        hence

         A9: ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k))) = ( IC ( Comput ((P +* (I ";" J)),s2,k)));

        

         A10: ( Directed I) c= (I ";" J) by SCMFSA6A: 16;

        then

         A11: ( dom ( Directed I)) c= ( dom (I ";" J)) by GRFUNC_1: 2;

        

        thus ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),( Initialize s),k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k)))) by A1, PARTFUN1:def 6

        .= (( Directed I) . ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k)))) by A8, FUNCT_4: 13

        .= ((I ";" J) . ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k)))) by A8, A10, GRFUNC_1: 2

        .= ((P +* (I ";" J)) . ( IC ( Comput ((P +* (I ";" J)),s2,k)))) by A9, A11, A8, FUNCT_4: 13

        .= ( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),s2,k)))) by A2, PARTFUN1:def 6;

      end;

      ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1))) = ( Comput ((P +* (I ";" J)),s2,(( LifeSpan ((P +* I),s1)) + 1))) by A4, A3, A5, Lm2, Th11;

      hence thesis;

    end;

    theorem :: SCMFSA8A:27

    

     Th18: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA , J be Program of SCM+FSA st I is_halting_on (( Initialized s),P) holds (for k be Nat st k <= ( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) holds ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))) = ( IC ( Comput ((P +* (I ";" J)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) = ( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))))) & ( DataPart ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( DataPart ( Comput ((P +* (I ";" J)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) & ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( IC ( Comput ((P +* (I ";" J)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1))))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      

       A1: ( dom (P +* (I ";" J))) = NAT by PARTFUN1:def 2;

      

       A2: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      set s2 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      

       A3: (s +* ( Initialize (( intloc 0 ) .--> 1))) = ( Initialize ( Initialized s)) & s2 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      

       A4: (( Directed I) ";" J) = (I ";" J);

      set s1 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      assume

       A5: I is_halting_on (( Initialized s),P);

      s1 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      then

       A6: (( LifeSpan ((P +* I),s1)) + 1) = ( pseudo-LifeSpan (( Initialized s),P,( Directed I))) by A5, Lm2;

      

       A7: ( Directed I) is_pseudo-closed_on (( Initialized s),P) by A5, Lm2;

      hereby

        let k be Nat;

        assume k <= ( LifeSpan ((P +* I),s1));

        then

         A8: k < ( pseudo-LifeSpan (( Initialized s),P,( Directed I))) by A6, NAT_1: 13;

        then ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)) = ( Comput ((P +* (I ";" J)),s2,k)) by A3, A4, A5, Lm2, Th11;

        hence

         A9: ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))) = ( IC ( Comput ((P +* (I ";" J)),s2,k)));

        (s +* ( Initialize (( intloc 0 ) .--> 1))) = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

        then

         A10: ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))) in ( dom ( Directed I)) by A7, A8, Def3;

        

         A11: ( Directed I) c= (I ";" J) by SCMFSA6A: 16;

        then

         A12: ( dom ( Directed I)) c= ( dom (I ";" J)) by GRFUNC_1: 2;

        

        thus ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) by A2, PARTFUN1:def 6

        .= (( Directed I) . ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) by A10, FUNCT_4: 13

        .= ((I ";" J) . ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) by A10, A11, GRFUNC_1: 2

        .= ((P +* (I ";" J)) . ( IC ( Comput ((P +* (I ";" J)),s2,k)))) by A9, A12, A10, FUNCT_4: 13

        .= ( CurInstr ((P +* (I ";" J)),( Comput ((P +* (I ";" J)),s2,k)))) by A1, PARTFUN1:def 6;

      end;

      ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),s1)) + 1))) = ( Comput ((P +* (I ";" J)),s2,(( LifeSpan ((P +* I),s1)) + 1))) by A5, A3, A4, A6, Lm2, Th11;

      hence thesis;

    end;

    theorem :: SCMFSA8A:28

    

     Th19: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (( Initialized s),P) holds for k be Nat st k <= ( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) holds ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)) = ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) <> ( halt SCM+FSA )

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      set s1 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      set s2 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      

       A1: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      

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

      

       A3: ( Directed I) c= (P +* ( Directed I)) by FUNCT_4: 25;

      defpred P[ Nat] means $1 <= ( LifeSpan ((P +* I),s1)) implies ( Comput ((P +* I),s1,$1)) = ( Comput ((P +* ( Directed I)),s2,$1)) & ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,$1)))) <> ( halt SCM+FSA );

      

       A4: s1 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      ( IC s1) = 0 by A4, MEMSTR_0: 47;

      then

       A5: ( IC s1) in ( dom I) by AFINSQ_1: 65;

      

       A6: I c= (P +* I) by FUNCT_4: 25;

       A7:

      now

        let k be Nat;

        ( dom ( Directed I)) = ( dom I) by FUNCT_4: 99;

        then

         A8: ( IC ( Comput ((P +* I),s1,k))) in ( dom ( Directed I)) by A5, A6, AMISTD_1: 21;

        

         A9: ((P +* ( Directed I)) /. ( IC ( Comput ((P +* ( Directed I)),s2,k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,k)))) by A1, PARTFUN1:def 6;

        assume ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),s2,k));

        

        then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* I),s1,k)))) by A9

        .= (( Directed I) . ( IC ( Comput ((P +* I),s1,k)))) by A8, A3, GRFUNC_1: 2;

        then

         A10: ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) in ( rng ( Directed I)) by A8, FUNCT_1:def 3;

        assume ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) = ( halt SCM+FSA );

        hence contradiction by A10, SCMFSA6A: 1;

      end;

      assume

       A11: I is_halting_on (( Initialized s),P);

      now

        

         A12: (P +* I) halts_on s1 by A11, A4, SCMFSA7B:def 7;

        

         A13: ( dom I) c= ( dom ( Directed I)) by FUNCT_4: 99;

        let k be Nat;

        assume

         A14: k <= ( LifeSpan ((P +* I),s1)) implies ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),s2,k));

        

         A15: ( Comput ((P +* ( Directed I)),s2,(k + 1))) = ( Following ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))),( Comput ((P +* ( Directed I)),s2,k))));

        

         A16: ( IC ( Comput ((P +* I),s1,k))) in ( dom I) by A5, A6, AMISTD_1: 21;

        

         A17: I c= (P +* I) by FUNCT_4: 25;

        

         A18: ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = ((P +* I) . ( IC ( Comput ((P +* I),s1,k)))) by A2, PARTFUN1:def 6

        .= (I . ( IC ( Comput ((P +* I),s1,k)))) by A16, A17, GRFUNC_1: 2;

        

         A19: (k + 0 ) < (k + 1) by XREAL_1: 6;

        assume

         A20: (k + 1) <= ( LifeSpan ((P +* I),s1));

        then k < ( LifeSpan ((P +* I),s1)) by A19, XXREAL_0: 2;

        then (I . ( IC ( Comput ((P +* I),s1,k)))) <> ( halt SCM+FSA ) by A18, A12, EXTPRO_1:def 15;

        

        then

         A21: ( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))) = (( Directed I) . ( IC ( Comput ((P +* I),s1,k)))) by A18, FUNCT_4: 105

        .= ((P +* ( Directed I)) . ( IC ( Comput ((P +* I),s1,k)))) by A3, A16, A13, GRFUNC_1: 2

        .= ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,k)))) by A14, A20, A19, XXREAL_0: 2

        .= ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,k)))) by A1, PARTFUN1:def 6;

        ( Comput ((P +* I),s1,(k + 1))) = ( Following ((P +* I),( Comput ((P +* I),s1,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P +* I),( Comput ((P +* I),s1,k)))),( Comput ((P +* I),s1,k))));

        hence ( Comput ((P +* I),s1,(k + 1))) = ( Comput ((P +* ( Directed I)),s2,(k + 1))) by A14, A20, A19, A21, A15, XXREAL_0: 2;

        hence ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,(k + 1))))) <> ( halt SCM+FSA ) by A7;

      end;

      then

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

      now

        assume 0 <= ( LifeSpan ((P +* I),s1));

        thus ( Comput ((P +* I),s1, 0 )) = ( Comput ((P +* ( Directed I)),s2, 0 ));

        hence ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2, 0 )))) <> ( halt SCM+FSA ) by A7;

      end;

      then

       A23: P[ 0 ];

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

    end;

    theorem :: SCMFSA8A:29

    

     Th20: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1)))))))) = ( DataPart ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1))))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      set s1 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      set s2 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      set m1 = ( LifeSpan ((P +* I),s1));

      

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

      

       A2: ( dom (P +* ( Directed I))) = NAT by PARTFUN1:def 2;

      set l1 = ( IC ( Comput ((P +* I),s1,m1)));

      

       A3: I c= (P +* I) by FUNCT_4: 25;

      

       A4: s1 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      then ( IC s1) = 0 by MEMSTR_0: 47;

      then ( IC s1) in ( dom I) by AFINSQ_1: 65;

      then

       A5: l1 in ( dom I) by A3, AMISTD_1: 21;

      assume

       A6: I is_halting_on (( Initialized s),P);

      then

       A7: ( Comput ((P +* I),s1,m1)) = ( Comput ((P +* ( Directed I)),s2,m1)) by Th19;

      then ( IC ( Comput ((P +* ( Directed I)),s2,m1))) in ( dom I) by A5;

      then

       A8: ( IC ( Comput ((P +* ( Directed I)),s2,m1))) in ( dom ( Directed I)) by FUNCT_4: 99;

      

       A9: (P +* I) halts_on s1 by A6, A4, SCMFSA7B:def 7;

      

       A10: I c= (P +* I) by FUNCT_4: 25;

      

       A11: (I . l1) = ((P +* I) . l1) by A5, A10, GRFUNC_1: 2

      .= ( CurInstr ((P +* I),( Comput ((P +* I),s1,m1)))) by A1, PARTFUN1:def 6

      .= ( halt SCM+FSA ) by A9, EXTPRO_1:def 15;

      l1 = ( IC ( Comput ((P +* ( Directed I)),s2,m1))) by A7;

      

      then

       A12: ((P +* ( Directed I)) . l1) = (( Directed I) . l1) by A8, FUNCT_4: 13

      .= ( goto ( card I)) by A5, A11, FUNCT_4: 106;

      

       A13: ((P +* ( Directed I)) /. ( IC ( Comput ((P +* ( Directed I)),s2,m1)))) = ((P +* ( Directed I)) . ( IC ( Comput ((P +* ( Directed I)),s2,m1)))) by A2, PARTFUN1:def 6;

      

       A14: ( Comput ((P +* ( Directed I)),s2,(m1 + 1))) = ( Following ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),s2,m1)))) by EXTPRO_1: 3

      .= ( Exec (( goto ( card I)),( Comput ((P +* ( Directed I)),s2,m1)))) by A12, A13, A7;

      hence ( IC ( Comput ((P +* ( Directed I)),s2,(m1 + 1)))) = ( card I) by SCMFSA_2: 69;

      

       A15: (for a be Int-Location holds (( Comput ((P +* ( Directed I)),s2,(m1 + 1))) . a) = (( Comput ((P +* ( Directed I)),s2,m1)) . a)) & for f be FinSeq-Location holds (( Comput ((P +* ( Directed I)),s2,(m1 + 1))) . f) = (( Comput ((P +* ( Directed I)),s2,m1)) . f) by A14, SCMFSA_2: 69;

      ( DataPart ( Comput ((P +* I),s1,m1))) = ( DataPart ( Comput ((P +* ( Directed I)),s2,m1))) by A7;

      hence thesis by A15, SCMFSA_M: 2;

    end;

    

     Lm3: for I be really-closed Program of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) holds ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),( Initialize s),( LifeSpan ((P +* I),( Initialize s)))))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) & (P +* (I ";" ( Stop SCM+FSA ))) halts_on ( Initialize s) & ( LifeSpan ((P +* (I ";" ( Stop SCM+FSA ))),( Initialize s))) = (( LifeSpan ((P +* I),( Initialize s))) + 1) & (I ";" ( Stop SCM+FSA )) is_halting_on (s,P)

    proof

      let I be really-closed Program of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let s be State of SCM+FSA ;

      ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      then ( card (I ";" ( Stop SCM+FSA ))) = (( card I) + 1) by SCMFSA6A: 21;

      then ( card I) < ( card (I ";" ( Stop SCM+FSA ))) by NAT_1: 13;

      then

       A1: ( card I) in ( dom (I ";" ( Stop SCM+FSA ))) by AFINSQ_1: 66;

      

       A2: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      ( 0 + ( card I)) in { (m + ( card I)) where m be Nat : m in ( dom ( Stop SCM+FSA )) } by A2;

      then

       A3: ( 0 + ( card I)) in ( dom ( Reloc (( Stop SCM+FSA ),( card I)))) by COMPOS_1: 33;

      set s2 = ( Initialize s);

      set s1 = ( Initialize s);

      

       A4: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      

       A5: (( Stop SCM+FSA ) . 0 ) = ( halt SCM+FSA );

      assume

       A6: I is_halting_on (s,P);

      then

       A7: ( IC ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1)))) = ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by Th17;

      

       A8: ((P +* (I ";" ( Stop SCM+FSA ))) . ( card I)) = ((I ";" ( Stop SCM+FSA )) . ( card I)) by A1, FUNCT_4: 13

      .= (( Reloc (( Stop SCM+FSA ),( card I))) . ( 0 + ( card I))) by A3, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),( card I))) by A5, A4, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      ( DataPart ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A6, Th17;

      hence ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A6, A7, Th13;

      ( dom (P +* (I ";" ( Stop SCM+FSA )))) = NAT by PARTFUN1:def 2;

      then

       A9: ((P +* (I ";" ( Stop SCM+FSA ))) /. ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) = ((P +* (I ";" ( Stop SCM+FSA ))) . ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) by PARTFUN1:def 6;

      

       A10: ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) = ( halt SCM+FSA ) by A8, A6, A7, Th13, A9;

      hence

       A11: (P +* (I ";" ( Stop SCM+FSA ))) halts_on s2 by EXTPRO_1: 29;

      now

        let k be Nat;

        assume k < (( LifeSpan ((P +* I),s1)) + 1);

        then

         A12: k <= ( LifeSpan ((P +* I),s1)) by NAT_1: 13;

        then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),( Initialize s),k)))) <> ( halt SCM+FSA ) by A6, Th12;

        hence ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,k)))) <> ( halt SCM+FSA ) by A6, A12, Th17;

      end;

      then for k be Nat st ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,k)))) = ( halt SCM+FSA ) holds (( LifeSpan ((P +* I),s1)) + 1) <= k;

      hence ( LifeSpan ((P +* (I ";" ( Stop SCM+FSA ))),s2)) = (( LifeSpan ((P +* I),s1)) + 1) by A10, A11, EXTPRO_1:def 15;

      thus thesis by A11, SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8A:30

    for I be really-closed Program of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) holds (I ";" ( Stop SCM+FSA )) is_halting_on (s,P) by Lm3;

    theorem :: SCMFSA8A:31

    for l be Nat holds 0 in ( dom ( Goto l)) & (( Goto l) . 0 ) = ( goto l) by Lm1;

    

     Lm4: for I be really-closed Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1)))))))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) & (P +* (I ";" ( Stop SCM+FSA ))) halts_on (s +* ( Initialize (( intloc 0 ) .--> 1))) & ( LifeSpan ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))))) = (( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)

    proof

      let I be really-closed Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      then ( card (I ";" ( Stop SCM+FSA ))) = (( card I) + 1) by SCMFSA6A: 21;

      then ( card I) < ( card (I ";" ( Stop SCM+FSA ))) by NAT_1: 13;

      then

       A1: ( card I) in ( dom (I ";" ( Stop SCM+FSA ))) by AFINSQ_1: 66;

      

       A2: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      ( 0 + ( card I)) in { (m + ( card I)) where m be Nat : m in ( dom ( Stop SCM+FSA )) } by A2;

      then

       A3: ( 0 + ( card I)) in ( dom ( Reloc (( Stop SCM+FSA ),( card I)))) by COMPOS_1: 33;

      set s2 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      set s1 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      assume

       A4: I is_halting_on (( Initialized s),P);

      then

       A5: ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),s1)) + 1)))) = ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by Th18;

      

       A6: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      

       A7: (( Stop SCM+FSA ) . 0 ) = ( halt SCM+FSA );

      

       A8: ((P +* (I ";" ( Stop SCM+FSA ))) . ( card I)) = ((I ";" ( Stop SCM+FSA )) . ( card I)) by A1, FUNCT_4: 13

      .= (( Reloc (( Stop SCM+FSA ),( card I))) . ( 0 + ( card I))) by A3, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),( card I))) by A7, A6, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      ( DataPart ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A4, Th18;

      hence ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( card I) & ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A4, A5, Th20;

      ( dom (P +* (I ";" ( Stop SCM+FSA )))) = NAT by PARTFUN1:def 2;

      then

       A9: ((P +* (I ";" ( Stop SCM+FSA ))) /. ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) = ((P +* (I ";" ( Stop SCM+FSA ))) . ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) by PARTFUN1:def 6;

      

       A10: ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,(( LifeSpan ((P +* I),s1)) + 1))))) = ( halt SCM+FSA ) by A8, A4, A5, Th20, A9;

      hence

       A11: (P +* (I ";" ( Stop SCM+FSA ))) halts_on s2 by EXTPRO_1: 29;

      now

        let k be Nat;

        assume k < (( LifeSpan ((P +* I),s1)) + 1);

        then

         A12: k <= ( LifeSpan ((P +* I),s1)) by NAT_1: 13;

        then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) <> ( halt SCM+FSA ) by A4, Th19;

        hence ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,k)))) <> ( halt SCM+FSA ) by A4, A12, Th18;

      end;

      then for k be Nat st ( CurInstr ((P +* (I ";" ( Stop SCM+FSA ))),( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s2,k)))) = ( halt SCM+FSA ) holds (( LifeSpan ((P +* I),s1)) + 1) <= k;

      hence thesis by A10, A11, EXTPRO_1:def 15;

    end;

    theorem :: SCMFSA8A:32

    for I be really-closed Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IC ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( card I) by Lm4;

    theorem :: SCMFSA8A:33

    for I be really-closed Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( DataPart ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1)))))))) = ( DataPart ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) by Lm4;

    theorem :: SCMFSA8A:34

    for I be really-closed Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (( Initialized s),P) holds (P +* (I ";" ( Stop SCM+FSA ))) halts_on (s +* ( Initialize (( intloc 0 ) .--> 1))) by Lm4;

    theorem :: SCMFSA8A:35

    for I be really-closed Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( LifeSpan ((P +* (I ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))))) = (( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1) by Lm4;

    theorem :: SCMFSA8A:36

    for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IExec ((I ";" ( Stop SCM+FSA )),P,s)) = (( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA )))

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      let I be really-closed Program of SCM+FSA ;

      set s1 = ( Initialized s);

      assume

       A1: I is_halting_on (( Initialized s),P);

      s1 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      then

       A2: (P +* I) halts_on s1 by A1, SCMFSA7B:def 7;

      (P +* (I ";" ( Stop SCM+FSA ))) halts_on s1 & ( LifeSpan ((P +* (I ";" ( Stop SCM+FSA ))),s1)) = (( LifeSpan ((P +* I),s1)) + 1) by A1, Lm4;

      then

       A3: ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1)) = ( Comput ((P +* (I ";" ( Stop SCM+FSA ))),s1,(( LifeSpan ((P +* I),s1)) + 1))) by EXTPRO_1: 23;

      then ( DataPart ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1))) = ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) by A1, Lm4;

      

      then

       A4: ( DataPart ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1))) = ( DataPart ( Result ((P +* I),s1))) by A2, EXTPRO_1: 23

      .= ( DataPart (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA )))) by MEMSTR_0: 79;

      ( IC ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1))) = ( card I) by A1, A3, Lm4

      .= ( IC (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA )))) by FUNCT_4: 113;

      then

       A5: ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1)) = (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA ))) by A4, MEMSTR_0: 78;

      

       A6: ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1)) = (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA ))) by A5;

      

      thus ( IExec ((I ";" ( Stop SCM+FSA )),P,s)) = ( Result ((P +* (I ";" ( Stop SCM+FSA ))),s1)) by SCMFSA6B:def 1

      .= (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA ))) by A6

      .= (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA )))

      .= (( Result ((P +* I),s1)) +* ( Start-At (( card I), SCM+FSA )))

      .= (( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA ))) by SCMFSA6B:def 1;

    end;

    

     Lm5: for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) holds ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 2)))) = ((( card I) + ( card J)) + 1) & ( DataPart ( Comput ((P +* I),( Initialize s),( LifeSpan ((P +* I),( Initialize s)))))) = ( DataPart ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 2)))) & (for k be Nat st k < (( LifeSpan ((P +* I),( Initialize s))) + 2) holds ( CurInstr ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s),k)))) <> ( halt SCM+FSA )) & (for k be Nat st k <= ( LifeSpan ((P +* I),( Initialize s))) holds ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s),k))) = ( IC ( Comput ((P +* I),( Initialize s),k)))) & ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 1)))) = ( card I) & (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))) halts_on ( Initialize s) & ( LifeSpan ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Initialize s))) = (( LifeSpan ((P +* I),( Initialize s))) + 2)

    proof

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      

       A1: ( card (( Goto (( card J) + 1)) ";" J)) = (( card ( Goto (( card J) + 1))) + ( card J)) by SCMFSA6A: 21

      .= (1 + ( card J)) by Lm1;

      

       A2: ( card (( Goto (( card J) + 1)) ";" J)) = (( card ( Goto (( card J) + 1))) + ( card J)) by SCMFSA6A: 21

      .= (( card J) + 1) by Lm1;

      

       A3: ((( card I) + ( card J)) + 1) = ((( card J) + 1) + ( card I));

      

       A4: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      set J2 = (( Goto (( card J) + 1)) ";" (J ";" ( Stop SCM+FSA )));

      set s2 = ( Initialize s);

      set P2 = (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )));

      set s1 = ( Initialize s);

      assume

       A5: I is_halting_on (s,P);

      ( dom ( Reloc (( Stop SCM+FSA ),(( card J) + 1)))) = { (m + (( card J) + 1)) where m be Nat : m in ( dom ( Stop SCM+FSA )) } by COMPOS_1: 33;

      then

       A6: ( 0 + (( card J) + 1)) in ( dom ( Reloc (( Stop SCM+FSA ),(( card J) + 1)))) by A4;

      

       A7: ( dom ( Goto (( card J) + 1))) c= ( dom (( Goto (( card J) + 1)) ";" J)) by SCMFSA6A: 17;

      

       A8: 0 in ( dom ( Goto (( card J) + 1))) by Lm1;

      

       A9: (J2 . 0 ) = (((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )) . 0 ) by SCMFSA6A: 25

      .= (( Directed (( Goto (( card J) + 1)) ";" J)) . 0 ) by A8, A7, Th7

      .= ((( Goto (( card J) + 1)) ";" ( Directed J)) . 0 ) by SCMFSA6A: 24

      .= (( Directed ( Goto (( card J) + 1))) . 0 ) by A8, Th7

      .= (( Goto (( card J) + 1)) . 0 ) by SCMFSA6A: 22

      .= ( goto (( card J) + 1));

      

       A10: (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )) = ((I ";" ( Goto (( card J) + 1))) ";" (J ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

      .= (I ";" J2) by SCMFSA6A: 25;

      then

       A11: ( DataPart ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A5, Th17;

      

       A12: ( card J2) = (( card ( Goto (( card J) + 1))) + ( card (J ";" ( Stop SCM+FSA )))) by SCMFSA6A: 21

      .= (1 + ( card (J ";" ( Stop SCM+FSA )))) by Lm1;

      then

       A13: ( 0 + 1) <= ( card J2) by NAT_1: 11;

      

       A14: ( card (I ";" J2)) = (( card I) + ( card J2)) by SCMFSA6A: 21;

      then (( card I) + 0 ) < ( card (I ";" J2)) by A13, XREAL_1: 6;

      then

       A15: ( card I) in ( dom (I ";" J2)) by AFINSQ_1: 66;

      

       A16: ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      ( card (I ";" J2)) = (( card I) + ( card ((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )))) by A14, SCMFSA6A: 25

      .= (( card I) + ((( card J) + 1) + 1)) by A2, A16, SCMFSA6A: 21

      .= (((( card I) + ( card J)) + 1) + 1);

      then ((( card I) + ( card J)) + 1) < ( card (I ";" J2)) by NAT_1: 13;

      then

       A17: ((( card I) + ( card J)) + 1) in ( dom (I ";" J2)) by AFINSQ_1: 66;

      

       A18: 0 in ( dom J2) by A13, AFINSQ_1: 66;

      then ( 0 + ( card I)) in { (m + ( card I)) where m be Nat : m in ( dom J2) };

      then

       A19: ( 0 + ( card I)) in ( dom ( Reloc (J2,( card I)))) by COMPOS_1: 33;

      

       A20: ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      

       A21: (( Stop SCM+FSA ) . 0 ) = ( halt SCM+FSA );

      ( card J2) = (1 + (( card J) + ( card ( Stop SCM+FSA )))) by A12, SCMFSA6A: 21

      .= (( card J) + (1 + ( card ( Stop SCM+FSA ))));

      then (( card J) + 1) < ( card J2) by A20, XREAL_1: 6;

      then

       A22: (( card J) + 1) in ( dom J2) by AFINSQ_1: 66;

      

       A23: (J2 . (( card J) + 1)) = (((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )) . (( card J) + 1)) by SCMFSA6A: 25

      .= (( Reloc (( Stop SCM+FSA ),(( card J) + 1))) . ( 0 + (( card J) + 1))) by A1, A6, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 1))) by A4, A21, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      ( dom ( Reloc (J2,( card I)))) = { (m + ( card I)) where m be Nat : m in ( dom J2) } by COMPOS_1: 33;

      then

       A24: ((( card I) + ( card J)) + 1) in ( dom ( Reloc (J2,( card I)))) by A22, A3;

      

       A25: ( IC ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1)))) = ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A5, A10, Th17;

      

       A26: ( CurInstr (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) = (P2 . ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) by PBOOLE: 143

      .= (P2 . ( IC ( Comput ((P +* ( Directed I)),( Initialize s),(( LifeSpan ((P +* I),s1)) + 1))))) by A5, A10, Th17

      .= (P2 . ( card I)) by A5, Th13

      .= ((I ";" J2) . ( card I)) by A10, A15, FUNCT_4: 13

      .= (( Reloc (J2,( card I))) . ( 0 + ( card I))) by A19, SCMFSA6A: 40

      .= ( IncAddr (( goto (( card J) + 1)),( card I))) by A18, A9, COMPOS_1: 35

      .= ( goto ((( card J) + 1) + ( card I))) by SCMFSA_4: 1

      .= ( goto ((( card I) + ( card J)) + 1));

       A27:

      now

        let f be FinSeq-Location;

        

        thus (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + (1 + 1)))) . f) = (( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))) . f)

        .= (( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) . f) by EXTPRO_1: 3

        .= (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))) . f) by A26, SCMFSA_2: 69;

      end;

      

      thus ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) = ( IC ( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))))

      .= ( IC ( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))))) by EXTPRO_1: 3

      .= ((( card I) + ( card J)) + 1) by A26, SCMFSA_2: 69;

      

      then

       A28: ( CurInstr (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2))))) = (P2 . ((( card I) + ( card J)) + 1)) by PBOOLE: 143

      .= ((I ";" J2) . ((( card I) + ( card J)) + 1)) by A10, A17, FUNCT_4: 13

      .= (( Reloc (J2,( card I))) . ((( card J) + 1) + ( card I))) by A24, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),( card I))) by A22, A23, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      now

        let a be Int-Location;

        

        thus (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + (1 + 1)))) . a) = (( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))) . a)

        .= (( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) . a) by EXTPRO_1: 3

        .= (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))) . a) by A26, SCMFSA_2: 69;

      end;

      then ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) by A27, SCMFSA_M: 2;

      hence ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) by A5, A11, Th13;

      now

        let k be Nat;

        assume

         A30: k < (( LifeSpan ((P +* I),s1)) + 2);

        per cases ;

          suppose

           A31: k <= ( LifeSpan ((P +* I),s1));

          then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),( Initialize s),k)))) <> ( halt SCM+FSA ) by A5, Th12;

          hence ( CurInstr (P2,( Comput (P2,s2,k)))) <> ( halt SCM+FSA ) by A5, A10, A31, Th17;

        end;

          suppose

           A32: ( LifeSpan ((P +* I),s1)) < k;

          k < ((( LifeSpan ((P +* I),s1)) + 1) + 1) by A30;

          then

           A33: k <= (( LifeSpan ((P +* I),s1)) + 1) by NAT_1: 13;

          (( LifeSpan ((P +* I),s1)) + 1) <= k by A32, NAT_1: 13;

          hence ( CurInstr (P2,( Comput (P2,s2,k)))) <> ( halt SCM+FSA ) by A26, A33, XXREAL_0: 1;

        end;

      end;

      hereby

        let k be Nat;

        assume

         A34: k <= ( LifeSpan ((P +* I),s1));

        then ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),( Initialize s),k)) by A5, Th12;

        then ( IC ( Comput ((P +* I),s1,k))) = ( IC ( Comput ((P +* ( Directed I)),( Initialize s),k)));

        hence ( IC ( Comput (P2,s2,k))) = ( IC ( Comput ((P +* I),s1,k))) by A5, A10, A34, Th17;

      end;

      thus ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( card I) by A5, A25, Th13;

      thus

       A35: P2 halts_on s2 by A28, EXTPRO_1: 29;

      for k be Nat st ( CurInstr (P2,( Comput (P2,s2,k)))) = ( halt SCM+FSA ) holds (( LifeSpan ((P +* I),s1)) + 2) <= k by A29;

      hence thesis by A28, A35, EXTPRO_1:def 15;

    end;

    theorem :: SCMFSA8A:37

    for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) holds (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )) is_halting_on (s,P)

    proof

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      set IJ2 = (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ));

      set s2 = ( Initialize s);

      set P2 = (P +* IJ2);

      assume I is_halting_on (s,P);

      then P2 halts_on s2 by Lm5;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8A:38

    for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st I is_halting_on (s,P) holds (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))) halts_on ( Initialize s) by Lm5;

    

     Lm6: for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 2)))) = ((( card I) + ( card J)) + 1) & ( DataPart ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1)))))))) = ( DataPart ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 2)))) & (for k be Nat st k < (( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 2) holds ( CurInstr ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) <> ( halt SCM+FSA )) & (for k be Nat st k <= ( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) holds ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),k))) = ( IC ( Comput ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) & ( IC ( Comput ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 1)))) = ( card I) & (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))) halts_on (s +* ( Initialize (( intloc 0 ) .--> 1))) & ( LifeSpan ((P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))),(s +* ( Initialize (( intloc 0 ) .--> 1))))) = (( LifeSpan ((P +* I),(s +* ( Initialize (( intloc 0 ) .--> 1))))) + 2)

    proof

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      

       A1: ( card (( Goto (( card J) + 1)) ";" J)) = (( card ( Goto (( card J) + 1))) + ( card J)) by SCMFSA6A: 21

      .= (1 + ( card J)) by Lm1;

      

       A2: ( card (( Goto (( card J) + 1)) ";" J)) = (( card ( Goto (( card J) + 1))) + ( card J)) by SCMFSA6A: 21

      .= (( card J) + 1) by Lm1;

      

       A3: ((( card I) + ( card J)) + 1) = ((( card J) + 1) + ( card I));

      

       A4: 0 in ( dom ( Stop SCM+FSA )) by COMPOS_1: 3;

      set J2 = (( Goto (( card J) + 1)) ";" (J ";" ( Stop SCM+FSA )));

      set s2 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      set P2 = (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )));

      set s1 = (s +* ( Initialize (( intloc 0 ) .--> 1)));

      assume

       A5: I is_halting_on (( Initialized s),P);

      ( dom ( Reloc (( Stop SCM+FSA ),(( card J) + 1)))) = { (m + (( card J) + 1)) where m be Nat : m in ( dom ( Stop SCM+FSA )) } by COMPOS_1: 33;

      then

       A6: ( 0 + (( card J) + 1)) in ( dom ( Reloc (( Stop SCM+FSA ),(( card J) + 1)))) by A4;

      

       A7: ( dom ( Goto (( card J) + 1))) c= ( dom (( Goto (( card J) + 1)) ";" J)) by SCMFSA6A: 17;

      

       A8: 0 in ( dom ( Goto (( card J) + 1))) by Lm1;

      

       A9: (J2 . 0 ) = (((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )) . 0 ) by SCMFSA6A: 25

      .= (( Directed (( Goto (( card J) + 1)) ";" J)) . 0 ) by A8, A7, Th7

      .= ((( Goto (( card J) + 1)) ";" ( Directed J)) . 0 ) by SCMFSA6A: 24

      .= (( Directed ( Goto (( card J) + 1))) . 0 ) by A8, Th7

      .= (( Goto (( card J) + 1)) . 0 ) by SCMFSA6A: 22

      .= ( goto (( card J) + 1));

      

       A10: (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )) = ((I ";" ( Goto (( card J) + 1))) ";" (J ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

      .= (I ";" J2) by SCMFSA6A: 25;

      then

       A11: ( DataPart ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A5, Th18;

      

       A12: ( card J2) = (( card ( Goto (( card J) + 1))) + ( card (J ";" ( Stop SCM+FSA )))) by SCMFSA6A: 21

      .= (1 + ( card (J ";" ( Stop SCM+FSA )))) by Lm1;

      then

       A13: ( 0 + 1) <= ( card J2) by NAT_1: 11;

      

       A14: ( card (I ";" J2)) = (( card I) + ( card J2)) by SCMFSA6A: 21;

      then (( card I) + 0 ) < ( card (I ";" J2)) by A13, XREAL_1: 6;

      then

       A15: ( card I) in ( dom (I ";" J2)) by AFINSQ_1: 66;

      

       A16: ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      ( card (I ";" J2)) = (( card I) + ( card ((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )))) by A14, SCMFSA6A: 25

      .= (( card I) + ((( card J) + 1) + 1)) by A2, A16, SCMFSA6A: 21

      .= (((( card I) + ( card J)) + 1) + 1);

      then ((( card I) + ( card J)) + 1) < ( card (I ";" J2)) by NAT_1: 13;

      then

       A17: ((( card I) + ( card J)) + 1) in ( dom (I ";" J2)) by AFINSQ_1: 66;

      

       A18: 0 in ( dom J2) by A13, AFINSQ_1: 66;

      then ( 0 + ( card I)) in { (m + ( card I)) where m be Nat : m in ( dom J2) };

      then

       A19: ( 0 + ( card I)) in ( dom ( Reloc (J2,( card I)))) by COMPOS_1: 33;

      

       A20: ( card ( Stop SCM+FSA )) = 1 by COMPOS_1: 4;

      

       A21: (( Stop SCM+FSA ) . 0 ) = ( halt SCM+FSA );

      ( card J2) = (1 + (( card J) + ( card ( Stop SCM+FSA )))) by A12, SCMFSA6A: 21

      .= (( card J) + (1 + ( card ( Stop SCM+FSA ))));

      then (( card J) + 1) < ( card J2) by A20, XREAL_1: 6;

      then

       A22: (( card J) + 1) in ( dom J2) by AFINSQ_1: 66;

      

       A23: (P2 /. ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) = (P2 . ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) by PBOOLE: 143;

      

       A24: (J2 . (( card J) + 1)) = (((( Goto (( card J) + 1)) ";" J) ";" ( Stop SCM+FSA )) . (( card J) + 1)) by SCMFSA6A: 25

      .= (( Reloc (( Stop SCM+FSA ),(( card J) + 1))) . ( 0 + (( card J) + 1))) by A1, A6, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 1))) by A4, A21, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      ( dom ( Reloc (J2,( card I)))) = { (m + ( card I)) where m be Nat : m in ( dom J2) } by COMPOS_1: 33;

      then

       A25: ((( card I) + ( card J)) + 1) in ( dom ( Reloc (J2,( card I)))) by A22, A3;

      

       A26: ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),(( LifeSpan ((P +* I),s1)) + 1)))) = ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) by A5, A10, Th18;

      

      then

       A27: ( CurInstr (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) = (P2 . ( card I)) by A5, Th20, A23

      .= ((I ";" J2) . ( card I)) by A10, A15, FUNCT_4: 13

      .= (( Reloc (J2,( card I))) . ( 0 + ( card I))) by A19, SCMFSA6A: 40

      .= ( IncAddr (( goto (( card J) + 1)),( card I))) by A18, A9, COMPOS_1: 35

      .= ( goto ((( card J) + 1) + ( card I))) by SCMFSA_4: 1

      .= ( goto ((( card I) + ( card J)) + 1));

       A28:

      now

        let f be FinSeq-Location;

        

        thus (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + (1 + 1)))) . f) = (( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))) . f)

        .= (( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) . f) by EXTPRO_1: 3

        .= (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))) . f) by A27, SCMFSA_2: 69;

      end;

      

      thus ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) = ( IC ( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))))

      .= ( IC ( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))))) by EXTPRO_1: 3

      .= ((( card I) + ( card J)) + 1) by A27, SCMFSA_2: 69;

      

      then

       A29: ( CurInstr (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2))))) = (P2 . ((( card I) + ( card J)) + 1)) by PBOOLE: 143

      .= ((I ";" J2) . ((( card I) + ( card J)) + 1)) by A10, A17, FUNCT_4: 13

      .= (( Reloc (J2,( card I))) . ((( card J) + 1) + ( card I))) by A25, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),( card I))) by A22, A24, COMPOS_1: 35

      .= ( halt SCM+FSA ) by COMPOS_0: 4;

      now

        let a be Int-Location;

        

        thus (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + (1 + 1)))) . a) = (( Comput (P2,s2,((( LifeSpan ((P +* I),s1)) + 1) + 1))) . a)

        .= (( Following (P2,( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))))) . a) by EXTPRO_1: 3

        .= (( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1))) . a) by A27, SCMFSA_2: 69;

      end;

      then ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) by A28, SCMFSA_M: 2;

      hence ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) = ( DataPart ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 2)))) by A5, A11, Th20;

      now

        let k be Nat;

        assume

         A31: k < (( LifeSpan ((P +* I),s1)) + 2);

        per cases ;

          suppose

           A32: k <= ( LifeSpan ((P +* I),s1));

          then ( CurInstr ((P +* ( Directed I)),( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)))) <> ( halt SCM+FSA ) by A5, Th19;

          hence ( CurInstr (P2,( Comput (P2,s2,k)))) <> ( halt SCM+FSA ) by A5, A10, A32, Th18;

        end;

          suppose

           A33: ( LifeSpan ((P +* I),s1)) < k;

          k < ((( LifeSpan ((P +* I),s1)) + 1) + 1) by A31;

          then

           A34: k <= (( LifeSpan ((P +* I),s1)) + 1) by NAT_1: 13;

          (( LifeSpan ((P +* I),s1)) + 1) <= k by A33, NAT_1: 13;

          hence ( CurInstr (P2,( Comput (P2,s2,k)))) <> ( halt SCM+FSA ) by A27, A34, XXREAL_0: 1;

        end;

      end;

      hereby

        let k be Nat;

        assume

         A35: k <= ( LifeSpan ((P +* I),s1));

        then ( Comput ((P +* I),s1,k)) = ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)) by A5, Th19;

        then ( IC ( Comput ((P +* I),s1,k))) = ( IC ( Comput ((P +* ( Directed I)),(s +* ( Initialize (( intloc 0 ) .--> 1))),k)));

        hence ( IC ( Comput (P2,s2,k))) = ( IC ( Comput ((P +* I),s1,k))) by A5, A10, A35, Th18;

      end;

      thus ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s1)) + 1)))) = ( card I) by A5, A26, Th20;

      thus

       A36: P2 halts_on s2 by A29, EXTPRO_1: 29;

      for k be Nat st ( CurInstr (P2,( Comput (P2,s2,k)))) = ( halt SCM+FSA ) holds (( LifeSpan ((P +* I),s1)) + 2) <= k by A30;

      hence thesis by A29, A36, EXTPRO_1:def 15;

    end;

    theorem :: SCMFSA8A:39

    for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (( Initialized s),P) holds (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA ))) halts_on (s +* ( Initialize (( intloc 0 ) .--> 1))) by Lm6;

    theorem :: SCMFSA8A:40

    for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IC ( IExec ((((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )),P,s))) = ((( card I) + ( card J)) + 1)

    proof

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      set s2 = ( Initialized s);

      set P2 = (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )));

      assume

       A1: I is_halting_on (( Initialized s),P);

      then P2 halts_on s2 & ( LifeSpan (P2,s2)) = (( LifeSpan ((P +* I),s2)) + 2) by Lm6;

      

      then ( IC ( Result (P2,s2))) = ( IC ( Comput (P2,s2,(( LifeSpan ((P +* I),s2)) + 2)))) by EXTPRO_1: 23

      .= ((( card I) + ( card J)) + 1) by A1, Lm6;

      hence thesis by SCMFSA6B:def 1;

    end;

    theorem :: SCMFSA8A:41

    for I be really-closed Program of SCM+FSA , J be Program of SCM+FSA , s be State of SCM+FSA st I is_halting_on (( Initialized s),P) holds ( IExec ((((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA )))

    proof

      let I be really-closed Program of SCM+FSA ;

      let J be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      set s1 = ( Initialized s);

      set P2 = (P +* (((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )));

      assume that

       A1: I is_halting_on (( Initialized s),P);

      s1 = ( Initialize ( Initialized s)) by MEMSTR_0: 44;

      then

       A2: (P +* I) halts_on s1 by A1, SCMFSA7B:def 7;

      P2 halts_on s1 & ( LifeSpan (P2,s1)) = (( LifeSpan ((P +* I),s1)) + 2) by A1, Lm6;

      then

       A3: ( Result (P2,s1)) = ( Comput (P2,s1,(( LifeSpan ((P +* I),s1)) + 2))) by EXTPRO_1: 23;

      then ( DataPart ( Result (P2,s1))) = ( DataPart ( Comput ((P +* I),s1,( LifeSpan ((P +* I),s1))))) by A1, Lm6;

      

      then

       A4: ( DataPart ( Result (P2,s1))) = ( DataPart ( Result ((P +* I),s1))) by A2, EXTPRO_1: 23

      .= ( DataPart (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA )))) by MEMSTR_0: 79;

      ( IC ( Result (P2,s1))) = ((( card I) + ( card J)) + 1) by A1, A3, Lm6

      .= ( IC (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA )))) by FUNCT_4: 113;

      then

       A5: ( Result (P2,s1)) = (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) by A4, MEMSTR_0: 78;

      

       A6: ( Result (P2,s1)) = (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) by A5;

      

      thus ( IExec ((((I ";" ( Goto (( card J) + 1))) ";" J) ";" ( Stop SCM+FSA )),P,s)) = ( Result (P2,s1)) by SCMFSA6B:def 1

      .= (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) by A6

      .= (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA )))

      .= (( Result ((P +* I),s1)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA )))

      .= (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) by SCMFSA6B:def 1;

    end;

    theorem :: SCMFSA8A:42

    for I be Program of SCM+FSA , a be Int-Location, k be Nat, i be Instruction of SCM+FSA st not I destroys a & not i destroys a holds not (I +* (k,i)) destroys a

    proof

      let I be Program of SCM+FSA , a be Int-Location, k be Nat, i be Instruction of SCM+FSA such that

       A1: not I destroys a and

       A2: not i destroys a;

      let j be Instruction of SCM+FSA such that

       A3: j in ( rng (I +* (k,i)));

      ( rng (I +* (k,i))) c= (( rng I) \/ {i}) by FUNCT_7: 100;

      then j in (( rng I) \/ {i}) by A3;

      per cases by XBOOLE_0:def 3;

        suppose j in ( rng I);

        hence thesis by A1, SCMFSA7B:def 4;

      end;

        suppose j in {i};

        hence not j destroys a by A2, TARSKI:def 1;

      end;

    end;

    registration

      let I,J be good preProgram of SCM+FSA ;

      cluster (I +* J) -> good;

      coherence

      proof

         not I destroys ( intloc 0 ) & not J destroys ( intloc 0 ) by SCMFSA7B:def 5;

        hence not (I +* J) destroys ( intloc 0 ) by Th4;

      end;

    end

    theorem :: SCMFSA8A:43

    for I be MacroInstruction of SCM+FSA , k be Nat holds (( Goto k) ";" I) = (( Macro ( goto k)) ';' I)

    proof

      let I be MacroInstruction of SCM+FSA , k be Nat;

      ( rng ( Goto k)) = {( goto k)} by AFINSQ_1: 33;

      then not ( halt SCM+FSA ) in ( rng ( Goto k)) by TARSKI:def 1;

      then ( Directed ( Goto k)) = ( Goto k) by FUNCT_4: 103;

      hence (( Goto k) ";" I) = (( Macro ( goto k)) ';' I);

    end;

    theorem :: SCMFSA8A:44

    for i,j be Nat holds ( IncAddr (( Goto i),j)) = <%( goto (i + j))%>

    proof

      let i,j be Nat;

      

       A1: ( dom <%( goto (i + j))%>) = ( Segm 1) by AFINSQ_1: 33

      .= ( dom ( Goto i)) by AFINSQ_1: 33;

      for m be Nat st m in ( dom ( Goto i)) holds ( <%( goto (i + j))%> . m) = ( IncAddr ((( Goto i) /. m),j))

      proof

        let m be Nat;

        assume

         A2: m in ( dom ( Goto i));

        then m in { 0 } by CARD_1: 49, AFINSQ_1: 33;

        then

         A3: m = 0 by TARSKI:def 1;

        

         A4: (( Goto i) /. m) = (( Goto i) . m) by A2, PARTFUN1:def 6

        .= ( goto i) by A3;

        

        thus ( <%( goto (i + j))%> . m) = ( goto (i + j)) by A3

        .= ( IncAddr ((( Goto i) /. m),j)) by A4, SCMFSA10: 41;

      end;

      hence ( IncAddr (( Goto i),j)) = <%( goto (i + j))%> by A1, COMPOS_1:def 21;

    end;

    theorem :: SCMFSA8A:45

    for I,J be NAT -definedthe InstructionsF of SCM+FSA -valued Function st I c= J holds for a be Int-Location st not J destroys a holds not I destroys a

    proof

      let I,J be NAT -definedthe InstructionsF of SCM+FSA -valued Function such that

       A1: I c= J;

      let a be Int-Location such that

       A2: not J destroys a;

      let i be Instruction of SCM+FSA such that

       A3: i in ( rng I);

      ( rng I) c= ( rng J) by A1, RELAT_1: 11;

      then i in ( rng J) by A3;

      hence not i destroys a by A2, SCMFSA7B:def 4;

    end;