scmfsa8b.miz



    begin

    set A = NAT ;

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

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

    reserve P,P1,P2 for Instruction-Sequence of SCM+FSA ;

    ::$Canceled

    theorem :: SCMFSA8B:5

    

     Th1: for s1,s2 be State of SCM+FSA , I be really-closed Program of SCM+FSA st ( DataPart s1) = ( DataPart s2) holds I is_halting_on (s1,P1) implies I is_halting_on (s2,P2)

    proof

      let s1,s2 be State of SCM+FSA ;

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

      set S1 = ( Initialize s1), S2 = ( Initialize s2);

      ( IC S1) = 0 by MEMSTR_0: 47;

      then

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

      

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

      defpred P[ Nat] means ( IC ( Comput ((P1 +* I),S1,$1))) = ( IC ( Comput ((P2 +* I),S2,$1))) & ( CurInstr ((P1 +* I),( Comput ((P1 +* I),S1,$1)))) = ( CurInstr ((P2 +* I),( Comput ((P2 +* I),S2,$1)))) & ( DataPart ( Comput ((P1 +* I),S1,$1))) = ( DataPart ( Comput ((P2 +* I),S2,$1)));

      

       A3: ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

       A4: ( IC ( Comput ((P1 +* I),S1, 0 ))) = ( IC ( Start-At ( 0 , SCM+FSA ))) by A3, FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      

       A5: ( IC ( Comput ((P2 +* I),S2, 0 ))) = ( IC ( Start-At ( 0 , SCM+FSA ))) by A3, FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      assume ( DataPart s1) = ( DataPart s2);

      then

       A6: ( Comput ((P1 +* I),S1, 0 )) = ( Comput ((P2 +* I),S2, 0 )) by MEMSTR_0: 80;

       A7:

      now

        let k be Nat;

        

         A8: ( Comput ((P2 +* I),S2,(k + 1))) = ( Following ((P2 +* I),( Comput ((P2 +* I),S2,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P2 +* I),( Comput ((P2 +* I),S2,k)))),( Comput ((P2 +* I),S2,k))));

        assume

         A9: P[k];

        then

         A10: for f be FinSeq-Location holds (( Comput ((P1 +* I),S1,k)) . f) = (( Comput ((P2 +* I),S2,k)) . f) by SCMFSA_M: 2;

        for a be Int-Location holds (( Comput ((P1 +* I),S1,k)) . a) = (( Comput ((P2 +* I),S2,k)) . a) by A9, SCMFSA_M: 2;

        then

         A11: ( Comput ((P1 +* I),S1,k)) = ( Comput ((P2 +* I),S2,k)) by A9, A10, SCMFSA_2: 61;

        

         A12: ( IC ( Comput ((P1 +* I),S1,(k + 1)))) in ( dom I) by A1, A2, AMISTD_1: 21;

        ( Comput ((P1 +* I),S1,(k + 1))) = ( Following ((P1 +* I),( Comput ((P1 +* I),S1,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr ((P1 +* I),( Comput ((P1 +* I),S1,k)))),( Comput ((P1 +* I),S1,k))));

        then

         A13: ( Comput ((P1 +* I),S1,(k + 1))) = ( Comput ((P2 +* I),S2,(k + 1))) by A9, A11, A8;

        

         A14: ( IC ( Comput ((P1 +* I),S1,(k + 1)))) = ( IC ( Comput ((P2 +* I),S2,(k + 1)))) by A13;

        

         A15: ((P1 +* I) /. ( IC ( Comput ((P1 +* I),S1,(k + 1))))) = ((P1 +* I) . ( IC ( Comput ((P1 +* I),S1,(k + 1))))) by PBOOLE: 143;

        

         A16: ((P2 +* I) /. ( IC ( Comput ((P2 +* I),S2,(k + 1))))) = ((P2 +* I) . ( IC ( Comput ((P2 +* I),S2,(k + 1))))) by PBOOLE: 143;

        

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

        

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

        ( CurInstr ((P1 +* I),( Comput ((P1 +* I),S1,(k + 1))))) = (I . ( IC ( Comput ((P1 +* I),S1,(k + 1))))) by A12, A15, A17, GRFUNC_1: 2

        .= ( CurInstr ((P2 +* I),( Comput ((P2 +* I),S2,(k + 1))))) by A14, A12, A16, A18, GRFUNC_1: 2;

        hence P[(k + 1)] by A13;

      end;

      assume I is_halting_on (s1,P1);

      then (P1 +* I) halts_on ( Initialize s1) by SCMFSA7B:def 7;

      then

      consider m be Nat such that

       A19: ( CurInstr ((P1 +* I),( Comput ((P1 +* I),S1,m)))) = ( halt SCM+FSA );

      

       A20: ((P1 +* I) /. ( IC ( Comput ((P1 +* I),S1, 0 )))) = ((P1 +* I) . ( IC ( Comput ((P1 +* I),S1, 0 )))) by PBOOLE: 143;

      

       A21: ((P2 +* I) /. ( IC ( Comput ((P2 +* I),S2, 0 )))) = ((P2 +* I) . ( IC ( Comput ((P2 +* I),S2, 0 )))) by PBOOLE: 143;

      

       A22: 0 in ( dom I) by AFINSQ_1: 65;

      

      then ( CurInstr ((P1 +* I),( Comput ((P1 +* I),S1, 0 )))) = (I . 0 ) by A4, A20, FUNCT_4: 13

      .= ( CurInstr ((P2 +* I),( Comput ((P2 +* I),S2, 0 )))) by A5, A22, A21, FUNCT_4: 13;

      then

       A23: P[ 0 ] by A6;

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

      then ( CurInstr ((P2 +* I),( Comput ((P2 +* I),S2,m)))) = ( halt SCM+FSA ) by A19;

      then (P2 +* I) halts_on ( Initialize s2) by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    ::$Canceled

    theorem :: SCMFSA8B:8

    

     Th2: for s1 be 0 -started State of SCM+FSA , s2 be State of SCM+FSA , I be really-closed Program of SCM+FSA st I c= P1 holds for n be Nat st ( IC s2) = n & ( DataPart s1) = ( DataPart s2) & ( Reloc (I,n)) c= P2 holds for i be Nat holds (( IC ( Comput (P1,s1,i))) + n) = ( IC ( Comput (P2,s2,i))) & ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),n)) = ( CurInstr (P2,( Comput (P2,s2,i)))) & ( DataPart ( Comput (P1,s1,i))) = ( DataPart ( Comput (P2,s2,i)))

    proof

      let s1 be 0 -started State of SCM+FSA , s2 be State of SCM+FSA ;

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

      

       A1: ( Start-At ( 0 , SCM+FSA )) c= s1 by MEMSTR_0: 29;

      assume

       A2: I c= P1;

      let n be Nat;

      

       A3: ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

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

      

       A4: ( IC ( Comput (P1,s1, 0 ))) = ( IC s1)

      .= ( IC ( Start-At ( 0 , SCM+FSA ))) by A1, A3, GRFUNC_1: 2

      .= 0 by FUNCOP_1: 72;

      assume

       A5: ( IC s2) = n;

      

       A6: 0 in ( dom I) by AFINSQ_1: 65;

      then

       A7: ( 0 + n) in ( dom ( Reloc (I,n))) by COMPOS_1: 46;

      ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

      then

       A8: (P1 . ( IC s1)) = (P1 . ( IC ( Start-At ( 0 , SCM+FSA )))) by A1, GRFUNC_1: 2

      .= (P1 . 0 ) by FUNCOP_1: 72

      .= (I . 0 ) by A6, A2, GRFUNC_1: 2;

      assume ( DataPart s1) = ( DataPart s2);

      

      then

       A9: ( DataPart ( Comput (P1,s1, 0 ))) = ( DataPart s2)

      .= ( DataPart ( Comput (P2,s2, 0 )));

      assume

       A10: ( Reloc (I,n)) c= P2;

      let i be Nat;

      

       A11: (P2 /. ( IC s2)) = (P2 . ( IC s2)) by PBOOLE: 143;

      

       A12: ( CurInstr (P1,s1)) = (I . 0 ) by A8, PBOOLE: 143;

      ( IncAddr (( CurInstr (P1,( Comput (P1,s1, 0 )))),n)) = ( IncAddr (( CurInstr (P1,s1)),n))

      .= (( Reloc (I,n)) . ( 0 + n)) by A12, A6, COMPOS_1: 35

      .= ( CurInstr (P2,s2)) by A5, A7, A11, A10, GRFUNC_1: 2

      .= ( CurInstr (P2,( Comput (P2,s2, 0 ))));

      then

       A13: P[ 0 ] by A5, A4, A9;

      

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

      proof

        let k be Nat;

        

         A15: ( Comput (P1,s1,(k + 1))) = ( Following (P1,( Comput (P1,s1,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P1,( Comput (P1,s1,k)))),( Comput (P1,s1,k))));

        ( IC s1) = 0 by MEMSTR_0:def 11;

        then

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

        

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

        reconsider l = ( IC ( Comput (P1,s1,(k + 1)))) as Element of NAT ;

        reconsider j = ( CurInstr (P1,( Comput (P1,s1,(k + 1))))) as Instruction of SCM+FSA ;

        

         A18: ( Comput (P2,s2,(k + 1))) = ( Following (P2,( Comput (P2,s2,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P2,( Comput (P2,s2,k)))),( Comput (P2,s2,k))));

        

         A19: P1 = (P1 +* I) by A2, FUNCT_4: 98;

        then

         A20: ( IC ( Comput (P1,s1,(k + 1)))) in ( dom I) by A16, A17, AMISTD_1: 21;

        assume

         A21: P[k];

        hence

         A22: (( IC ( Comput (P1,s1,(k + 1)))) + n) = ( IC ( Comput (P2,s2,(k + 1)))) by A15, A18, SCMFSA6A: 8;

        then

         A23: ( IC ( Comput (P2,s2,(k + 1)))) in ( dom ( Reloc (I,n))) by A20, COMPOS_1: 46;

        

         A24: l in ( dom I) by A19, A16, A17, AMISTD_1: 21;

        j = (P1 . ( IC ( Comput (P1,s1,(k + 1))))) by PBOOLE: 143

        .= (I . l) by A20, A2, GRFUNC_1: 2;

        

        hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(k + 1))))),n)) = (( Reloc (I,n)) . (l + n)) by A24, COMPOS_1: 35

        .= (P2 . ( IC ( Comput (P2,s2,(k + 1))))) by A23, A22, A10, GRFUNC_1: 2

        .= ( CurInstr (P2,( Comput (P2,s2,(k + 1))))) by PBOOLE: 143;

        thus thesis by A21, A15, A18, SCMFSA6A: 8;

      end;

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

      hence thesis;

    end;

    theorem :: SCMFSA8B:9

    

     Th3: for s be State of SCM+FSA , i be keeping_0 sequential Instruction of SCM+FSA , J be parahalting really-closed Program of SCM+FSA , a be Int-Location holds (( IExec ((i ";" J),P,s)) . a) = (( IExec (J,P,( Exec (i,( Initialized s))))) . a)

    proof

      let s be State of SCM+FSA ;

      let i be keeping_0 sequential Instruction of SCM+FSA ;

      let J be parahalting really-closed Program of SCM+FSA ;

      let a be Int-Location;

      

       A1: ( IExec (( Macro i),P,s)) = ( Exec (i,( Initialized s))) by SCMFSA6C: 5;

      

      thus (( IExec ((i ";" J),P,s)) . a) = (( IExec (J,P,( IExec (( Macro i),P,s)))) . a) by SCMFSA6C: 1

      .= (( IExec (J,P,( IExec (( Macro i),P,s)))) . a)

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . a) by A1

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . a);

    end;

    theorem :: SCMFSA8B:10

    

     Th4: for s be State of SCM+FSA , i be keeping_0 sequential Instruction of SCM+FSA , J be parahalting really-closed Program of SCM+FSA , f be FinSeq-Location holds (( IExec ((i ";" J),P,s)) . f) = (( IExec (J,P,( Exec (i,( Initialized s))))) . f)

    proof

      let s be State of SCM+FSA ;

      let i be keeping_0 sequential Instruction of SCM+FSA ;

      let J be parahalting really-closed Program of SCM+FSA ;

      let f be FinSeq-Location;

      

       A1: ( IExec (( Macro i),P,s)) = ( Exec (i,( Initialized s))) by SCMFSA6C: 5;

      

      thus (( IExec ((i ";" J),P,s)) . f) = (( IExec (J,P,( IExec (( Macro i),P,s)))) . f) by SCMFSA6C: 2

      .= (( IExec (J,P,( IExec (( Macro i),P,s)))) . f)

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . f) by A1

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . f);

    end;

    definition

      let a be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      :: SCMFSA8B:def1

      func if=0 (a,I,J) -> Program of SCM+FSA equals (((((a =0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

      coherence ;

      :: SCMFSA8B:def2

      func if>0 (a,I,J) -> Program of SCM+FSA equals (((((a >0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

      coherence ;

    end

    ::$Canceled

    

     Lm1: for a be Int-Location, I,J be MacroInstruction of SCM+FSA holds 1 in ( dom ( if=0 (a,I,J))) & 1 in ( dom ( if>0 (a,I,J)))

    proof

      let a be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      set i = (a =0_goto (( card J) + 3));

      ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

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

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 29

      .= (( Macro i) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))));

      then

       A1: ( dom ( Macro i)) c= ( dom ( if=0 (a,I,J))) by SCMFSA6A: 17;

      ( dom ( Macro i)) = { 0 , 1} by COMPOS_1: 61;

      then 1 in ( dom ( Macro i)) by TARSKI:def 2;

      hence 1 in ( dom ( if=0 (a,I,J))) by A1;

      set i = (a >0_goto (( card J) + 3));

      ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

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

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 29

      .= (( Macro i) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))));

      then

       A2: ( dom ( Macro i)) c= ( dom ( if>0 (a,I,J))) by SCMFSA6A: 17;

      ( dom ( Macro i)) = { 0 , 1} by COMPOS_1: 61;

      then 1 in ( dom ( Macro i)) by TARSKI:def 2;

      hence thesis by A2;

    end;

    

     Lm2: for a be Int-Location, I,J be MacroInstruction of SCM+FSA holds (( if=0 (a,I,J)) . 0 ) = (a =0_goto (( card J) + 3)) & (( if=0 (a,I,J)) . 1) = ( goto 2) & (( if>0 (a,I,J)) . 0 ) = (a >0_goto (( card J) + 3)) & (( if>0 (a,I,J)) . 1) = ( goto 2)

    proof

      let a be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      set i = (a =0_goto (( card J) + 3));

      

       A1: ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

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

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 29

      .= (( Macro i) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))));

      

       A2: ( dom ( Macro i)) = { 0 , 1} by COMPOS_1: 61;

      then 0 in ( dom ( Macro i)) by TARSKI:def 2;

      

      hence (( if=0 (a,I,J)) . 0 ) = (( Directed ( Macro i)) . 0 ) by A1, SCMFSA8A: 14

      .= i by SCMFSA7B: 1;

      1 in ( dom ( Macro i)) by A2, TARSKI:def 2;

      

      hence (( if=0 (a,I,J)) . 1) = (( Directed ( Macro i)) . 1) by A1, SCMFSA8A: 14

      .= ( goto 2) by SCMFSA7B: 2;

      set i = (a >0_goto (( card J) + 3));

      

       A3: ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

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

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 29

      .= (( Macro i) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))));

      

       A4: ( dom ( Macro i)) = { 0 , 1} by COMPOS_1: 61;

      then 0 in ( dom ( Macro i)) by TARSKI:def 2;

      

      hence (( if>0 (a,I,J)) . 0 ) = (( Directed ( Macro i)) . 0 ) by A3, SCMFSA8A: 14

      .= i by SCMFSA7B: 1;

      1 in ( dom ( Macro i)) by A4, TARSKI:def 2;

      

      hence (( if>0 (a,I,J)) . 1) = (( Directed ( Macro i)) . 1) by A3, SCMFSA8A: 14

      .= ( goto 2) by SCMFSA7B: 2;

    end;

    theorem :: SCMFSA8B:11

    for I,J be MacroInstruction of SCM+FSA , a be Int-Location holds ( card ( if=0 (a,I,J))) = ((( card I) + ( card J)) + 4)

    proof

      let I,J be MacroInstruction of SCM+FSA ;

      let a be Int-Location;

      

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

      

      thus ( card ( if=0 (a,I,J))) = (( card (((( Macro (a =0_goto (( card J) + 3))) ";" J) ";" ( Goto (( card I) + 1))) ";" I)) + 1) by A1, SCMFSA6A: 21

      .= ((( card ((( Macro (a =0_goto (( card J) + 3))) ";" J) ";" ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

      .= (((( card (( Macro (a =0_goto (( card J) + 3))) ";" J)) + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

      .= (((( card (( Macro (a =0_goto (( card J) + 3))) ";" J)) + 1) + ( card I)) + 1) by SCMFSA8A: 15

      .= ((((( card ( Macro (a =0_goto (( card J) + 3)))) + ( card J)) + 1) + ( card I)) + 1) by SCMFSA6A: 21

      .= ((((2 + ( card J)) + 1) + ( card I)) + 1) by COMPOS_1: 56

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

    end;

    theorem :: SCMFSA8B:12

    for I,J be MacroInstruction of SCM+FSA , a be Int-Location holds ( card ( if>0 (a,I,J))) = ((( card I) + ( card J)) + 4)

    proof

      let I,J be MacroInstruction of SCM+FSA ;

      let a be Int-Location;

      

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

      

      thus ( card ( if>0 (a,I,J))) = (( card (((( Macro (a >0_goto (( card J) + 3))) ";" J) ";" ( Goto (( card I) + 1))) ";" I)) + 1) by A1, SCMFSA6A: 21

      .= ((( card ((( Macro (a >0_goto (( card J) + 3))) ";" J) ";" ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

      .= (((( card (( Macro (a >0_goto (( card J) + 3))) ";" J)) + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

      .= (((( card (( Macro (a >0_goto (( card J) + 3))) ";" J)) + 1) + ( card I)) + 1) by SCMFSA8A: 15

      .= ((((( card ( Macro (a >0_goto (( card J) + 3)))) + ( card J)) + 1) + ( card I)) + 1) by SCMFSA6A: 21

      .= ((((2 + ( card J)) + 1) + ( card I)) + 1) by COMPOS_1: 56

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

    end;

    theorem :: SCMFSA8B:13

    

     Th7: for s be State of SCM+FSA , I be really-closed MacroInstruction of SCM+FSA , J be MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) = 0 & I is_halting_on (s,P) holds ( if=0 (a,I,J)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

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

      let J be MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      set I1 = (I ";" ( Stop SCM+FSA ));

      set s1 = ( Initialize s), P1 = (P +* I1);

      set s3 = ( Initialize s), P3 = (P +* ( if=0 (a,I,J)));

      set s4 = ( Comput ((P +* ( if=0 (a,I,J))),s3,1));

      set i = (a =0_goto (( card J) + 3));

      

       A1: not a in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      

       A2: 0 in ( dom ( if=0 (a,I,J))) by AFINSQ_1: 65;

      

       A3: (P3 . 0 ) = (( if=0 (a,I,J)) . 0 ) by A2, FUNCT_4: 13

      .= i by Lm2;

      ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

      then

       A4: ( IC s3) = ( IC ( Start-At ( 0 , SCM+FSA ))) by FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      

       A5: ( if=0 (a,I,J)) c= P3 by FUNCT_4: 25;

      

       A6: ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25;

      ( card ((i ";" J) ";" ( Goto (( card I) + 1)))) = (( card (( Macro i) ";" J)) + ( card ( Goto (( card I) + 1)))) by SCMFSA6A: 21

      .= (( card (( Macro i) ";" J)) + 1) by SCMFSA8A: 15

      .= ((( card ( Macro i)) + ( card J)) + 1) by SCMFSA6A: 21

      .= ((( card J) + 2) + 1) by COMPOS_1: 56

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

      then

       A7: ( Reloc (I1,(( card J) + 3))) c= ( if=0 (a,I,J)) by A6, SCMFSA6A: 38;

      

       A8: ( Reloc (I1,(( card J) + 3))) c= P3 by A7, A5, XBOOLE_1: 1;

      

       A9: ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i,s3)) by A4, A3, PBOOLE: 143;

      

       A10: for f be FinSeq-Location holds (s1 . f) = (s4 . f) by A9, SCMFSA_2: 70;

      for a be Int-Location holds (s1 . a) = (s4 . a) by A9, SCMFSA_2: 70;

      then

       A11: ( DataPart s1) = ( DataPart s4) by A10, SCMFSA_M: 2;

      assume (s . a) = 0 ;

      then (s3 . a) = 0 by A1, FUNCT_4: 11;

      then

       A12: ( IC ( Comput (P3,s3,1))) = (( card J) + 3) by A9, SCMFSA_2: 70;

      assume

       A13: I is_halting_on (s,P);

      I1 is_halting_on (s,P) by A13, SCMFSA8A: 30;

      then

       A14: P1 halts_on s1 by SCMFSA7B:def 7;

      

       A15: I1 c= P1 by FUNCT_4: 25;

      ( CurInstr (P3,( Comput (P3,s3,(( LifeSpan (P1,s1)) + 1))))) = ( CurInstr (P3,( Comput (P3,s4,( LifeSpan (P1,s1)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P1,( Comput (P1,s1,( LifeSpan (P1,s1)))))),(( card J) + 3))) by A12, A11, Th2, A8, A15

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 3))) by A14, EXTPRO_1:def 15

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

      then P3 halts_on s3 by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8B:14

    

     Th8: for s be State of SCM+FSA , I be really-closed MacroInstruction of SCM+FSA , J be MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) = 0 & I is_halting_on (( Initialized s),P) holds ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))

    proof

      let s be State of SCM+FSA ;

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

      let J be MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      set I1 = (I ";" ( Stop SCM+FSA ));

      set s1 = ( Initialized s), P1 = (P +* I1), P3 = (P +* ( if=0 (a,I,J)));

      

       A1: I1 c= P1 by FUNCT_4: 25;

      set s4 = ( Comput (P3,s1,1));

      set i = (a =0_goto (( card J) + 3));

      

       A2: ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25;

      

       A3: 0 in ( dom ( if=0 (a,I,J))) by AFINSQ_1: 65;

      

       A4: (P3 . 0 ) = (( if=0 (a,I,J)) . 0 ) by A3, FUNCT_4: 13

      .= i by Lm2;

      

       A5: ( dom ( Initialize (( intloc 0 ) .--> 1))) = {( intloc 0 ), ( IC SCM+FSA )} by SCMFSA_M: 11;

      a <> ( intloc 0 ) & a <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then

       A6: not a in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A5, TARSKI:def 2;

      ( IC SCM+FSA ) in ( dom ( Initialize (( intloc 0 ) .--> 1))) by MEMSTR_0: 48;

      

      then

       A7: ( IC s1) = ( IC ( Initialize (( intloc 0 ) .--> 1))) by FUNCT_4: 13

      .= 0 by MEMSTR_0:def 11;

      

       A8: ( Comput (P3,s1,( 0 + 1))) = ( Following (P3,( Comput (P3,s1, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s1))

      .= ( Exec (i,s1)) by A7, A4, PBOOLE: 143;

      

       A9: ( if=0 (a,I,J)) c= P3 by FUNCT_4: 25;

      assume (s . a) = 0 ;

      then (s1 . a) = 0 by A6, FUNCT_4: 11;

      then

       A10: ( IC ( Comput (P3,s1,1))) = (( card J) + 3) by A8, SCMFSA_2: 70;

      

       A11: for f be FinSeq-Location holds (s1 . f) = (s4 . f) by A8, SCMFSA_2: 70;

      for a be Int-Location holds (s1 . a) = (s4 . a) by A8, SCMFSA_2: 70;

      then

       A12: ( DataPart s1) = ( DataPart s4) by A11, SCMFSA_M: 2;

      ( card ((i ";" J) ";" ( Goto (( card I) + 1)))) = (( card (( Macro i) ";" J)) + ( card ( Goto (( card I) + 1)))) by SCMFSA6A: 21

      .= (( card (( Macro i) ";" J)) + 1) by SCMFSA8A: 15

      .= ((( card ( Macro i)) + ( card J)) + 1) by SCMFSA6A: 21

      .= ((( card J) + 2) + 1) by COMPOS_1: 56

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

      then

       A13: ( Reloc (I1,(( card J) + 3))) c= ( if=0 (a,I,J)) by A2, SCMFSA6A: 38;

      

       A14: ( Reloc (I1,(( card J) + 3))) c= P3 by A13, A9, XBOOLE_1: 1;

      assume

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

      then

       A16: P1 halts_on s1 by SCMFSA8A: 34;

      

       A17: ( CurInstr (P3,( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1))))) = ( CurInstr (P3,( Comput (P3,s4,( LifeSpan (P1,s1)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P1,( Comput (P1,s1,( LifeSpan (P1,s1)))))),(( card J) + 3))) by A10, A12, Th2, A14, A1

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 3))) by A16, EXTPRO_1:def 15

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

      then

       A18: P3 halts_on s1 by EXTPRO_1: 29;

      now

        let l be Nat;

        assume

         A19: l < (( LifeSpan (P1,s1)) + 1);

        per cases ;

          suppose l = 0 ;

          hence ( CurInstr (P3,( Comput (P3,s1,l)))) <> ( halt SCM+FSA ) by A7, A4, PBOOLE: 143;

        end;

          suppose l <> 0 ;

          then

          consider n be Nat such that

           A20: l = (n + 1) by NAT_1: 6;

          assume

           A21: ( CurInstr (P3,( Comput (P3,s1,l)))) = ( halt SCM+FSA );

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

          

           A22: ( InsCode ( halt SCM+FSA )) = 0 by COMPOS_1: 70;

          ( InsCode ( CurInstr (P1,( Comput (P1,s1,n))))) = ( InsCode ( IncAddr (( CurInstr (P1,( Comput (P1,s1,n)))),(( card J) + 3)))) by COMPOS_0:def 9

          .= ( InsCode ( CurInstr (P3,( Comput (P3,s4,n))))) by A10, A12, Th2, A14, A1

          .= 0 by A20, A21, A22, EXTPRO_1: 4;

          then

           A23: ( CurInstr (P1,( Comput (P1,s1,n)))) = ( halt SCM+FSA ) by SCMFSA_2: 95;

          n < ( LifeSpan (P1,s1)) by A19, A20, XREAL_1: 6;

          hence contradiction by A16, A23, EXTPRO_1:def 15;

        end;

      end;

      then for l be Nat st ( CurInstr (P3,( Comput (P3,s1,l)))) = ( halt SCM+FSA ) holds (( LifeSpan (P1,s1)) + 1) <= l;

      then

       A24: ( LifeSpan (P3,s1)) = (( LifeSpan (P1,s1)) + 1) by A17, A18, EXTPRO_1:def 15;

      

       A25: ( DataPart ( Result (P1,s1))) = ( DataPart ( Comput (P1,s1,( LifeSpan (P1,s1))))) by A15, EXTPRO_1: 23, SCMFSA8A: 34

      .= ( DataPart ( Comput (P3,s4,( LifeSpan (P1,s1))))) by A10, A12, Th2, A1, A14

      .= ( DataPart ( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1)))) by EXTPRO_1: 4

      .= ( DataPart ( Result (P3,s1))) by A18, A24, EXTPRO_1: 23;

       A26:

      now

        let x be object;

        

         A27: ( IExec (I1,P,s)) = ( Result (P1,s1)) by SCMFSA6B:def 1;

        

         A29: ( IExec (( if=0 (a,I,J)),P,s)) = ( Result (P3,s1)) by SCMFSA6B:def 1;

        assume

         A30: x in ( dom ( IExec (( if=0 (a,I,J)),P,s)));

        per cases by A30, SCMFSA_M: 1;

          suppose

           A31: x is Int-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 56;

          then

           A32: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A29

          .= (( Result (P1,s1)) . x) by A25, A31, SCMFSA_M: 2

          .= (( IExec (I1,P,s)) . x) by A27

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A32, FUNCT_4: 11;

        end;

          suppose

           A33: x is FinSeq-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 57;

          then

           A34: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A29

          .= (( Result (P1,s1)) . x) by A25, A33, SCMFSA_M: 2

          .= (( IExec (I1,P,s)) . x) by A27

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A34, FUNCT_4: 11;

        end;

          suppose

           A35: x = ( IC SCM+FSA );

          then

           A36: x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

           A37: ( IC ( Result (P1,s1))) = (( IExec (I1,P,s)) . ( IC SCM+FSA )) by A27

          .= ( IC (( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA )))) by A15, SCMFSA8A: 36

          .= ( card I) by FUNCT_4: 113;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A29

          .= (( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1))) . x) by A18, A24, EXTPRO_1: 23

          .= ( IC ( Comput (P3,s4,( LifeSpan (P1,s1))))) by A35, EXTPRO_1: 4

          .= (( IC ( Comput (P1,s1,( LifeSpan (P1,s1))))) + (( card J) + 3)) by A10, A12, Th2, A14, A1

          .= (( IC ( Result (P1,s1))) + (( card J) + 3)) by A15, EXTPRO_1: 23, SCMFSA8A: 34

          .= (( Start-At ((( card I) + (( card J) + 3)), SCM+FSA )) . ( IC SCM+FSA )) by A37, FUNCOP_1: 72

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A35, A36, FUNCT_4: 13;

        end;

      end;

      ( dom ( IExec (( if=0 (a,I,J)),P,s))) = the carrier of SCM+FSA by PARTFUN1:def 2

      .= ( dom (( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) by PARTFUN1:def 2;

      

      hence ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A26, FUNCT_1: 2

      .= ((( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA ))) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A15, SCMFSA8A: 36

      .= (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by FUNCT_4: 114;

    end;

    

     Lm3: for I,J be really-closed MacroInstruction of SCM+FSA holds (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) is really-closed

    proof

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      

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

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

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

      ((( Goto (( card I) + 1)) ";" I) ";" ( Stop SCM+FSA )) is really-closed by SCMFSA_X: 28;

      hence thesis by A1;

    end;

    registration

      let I,J be really-closed MacroInstruction of SCM+FSA , a be Int-Location;

      cluster ( if=0 (a,I,J)) -> really-closed;

      coherence

      proof

        

         A1: ( if=0 (a,I,J)) = (((((a =0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ))

        .= ((((a =0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

        .= (((a =0_goto (( card J) + 3)) ";" J) ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))) by SCMFSA6A: 25

        .= ((a =0_goto (( card J) + 3)) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 25

        .= ((a =0_goto (( card J) + 3)) ";" ((J ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA )))) by SCMFSA6A: 25

        .= ((a =0_goto (( card J) + 3)) ";" (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25;

        

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

        .= (( card ((J ";" ( Goto (( card I) + 1))) ";" I)) + 1) by COMPOS_1: 4

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

        .= (((( card J) + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

        .= (((( card J) + 1) + ( card I)) + 1) by SCMFSA8A: 15

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

        ( 0 + 1) <= ( card I) by NAT_1: 13;

        then (1 + ( card J)) <= (( card I) + ( card J)) by XREAL_1: 7;

        then

         A3: ((1 + ( card J)) + 2) <= ((( card I) + ( card J)) + 2) by XREAL_1: 7;

        (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) is really-closed by Lm3;

        hence thesis by A3, SCMFSA_X: 31, A1, A2;

      end;

      cluster ( if>0 (a,I,J)) -> really-closed;

      coherence

      proof

        

         A4: ( if>0 (a,I,J)) = (((((a >0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ))

        .= ((((a >0_goto (( card J) + 3)) ";" J) ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25

        .= (((a >0_goto (( card J) + 3)) ";" J) ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA )))) by SCMFSA6A: 25

        .= ((a >0_goto (( card J) + 3)) ";" (J ";" (( Goto (( card I) + 1)) ";" (I ";" ( Stop SCM+FSA ))))) by SCMFSA6A: 25

        .= ((a >0_goto (( card J) + 3)) ";" ((J ";" ( Goto (( card I) + 1))) ";" (I ";" ( Stop SCM+FSA )))) by SCMFSA6A: 25

        .= ((a >0_goto (( card J) + 3)) ";" (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ))) by SCMFSA6A: 25;

        

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

        .= (( card ((J ";" ( Goto (( card I) + 1))) ";" I)) + 1) by COMPOS_1: 4

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

        .= (((( card J) + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 21

        .= (((( card J) + 1) + ( card I)) + 1) by SCMFSA8A: 15

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

        ( 0 + 1) <= ( card I) by NAT_1: 13;

        then (1 + ( card J)) <= (( card I) + ( card J)) by XREAL_1: 7;

        then

         A6: ((1 + ( card J)) + 2) <= ((( card I) + ( card J)) + 2) by XREAL_1: 7;

        (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) is really-closed by Lm3;

        hence thesis by A6, SCMFSA_X: 32, A4, A5;

      end;

    end

    theorem :: SCMFSA8B:15

    

     Th9: for s be State of SCM+FSA , I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) <> 0 & J is_halting_on (s,P) holds ( if=0 (a,I,J)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      set I1 = (I ";" ( Stop SCM+FSA ));

      reconsider JI2 = (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) as really-closed Program of SCM+FSA by Lm3;

      set s2 = ( Initialize s), P2 = (P +* JI2);

      

       A1: JI2 c= P2 by FUNCT_4: 25;

      set s3 = ( Initialize s), P3 = (P +* ( if=0 (a,I,J)));

      set s4 = ( Comput (P3,s3,1));

      set s5 = ( Comput (P3,s3,2));

      set i = (a =0_goto (( card J) + 3));

      ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

      then

       A2: ( IC s3) = ( IC ( Start-At ( 0 , SCM+FSA ))) by FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      

       A3: ( if=0 (a,I,J)) c= P3 by FUNCT_4: 25;

      ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25

      .= ((i ";" J) ";" (( Goto (( card I) + 1)) ";" I1)) by SCMFSA6A: 25

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" I1))) by SCMFSA6A: 29

      .= (i ";" ((J ";" ( Goto (( card I) + 1))) ";" I1)) by SCMFSA6A: 25

      .= (( Macro i) ";" JI2) by SCMFSA6A: 25;

      then ( Reloc (JI2,( card ( Macro i)))) c= ( if=0 (a,I,J)) by SCMFSA6A: 38;

      then

       A4: ( Reloc (JI2,2)) c= ( if=0 (a,I,J)) by COMPOS_1: 56;

      

       A5: ( Reloc (JI2,2)) c= P3 by A4, A3, XBOOLE_1: 1;

      

       A6: not a in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      

       A7: 0 in ( dom ( if=0 (a,I,J))) by AFINSQ_1: 65;

      

       A8: ( if=0 (a,I,J)) c= P3 by FUNCT_4: 25;

      

       A9: (P3 . 0 ) = (( if=0 (a,I,J)) . 0 ) by A7, FUNCT_4: 13

      .= i by Lm2;

      

       A10: 1 in ( dom ( if=0 (a,I,J))) by Lm1;

      

       A11: ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i,s3)) by A2, A9, PBOOLE: 143;

      assume (s . a) <> 0 ;

      then (s3 . a) <> 0 by A6, FUNCT_4: 11;

      then

       A12: ( IC ( Comput (P3,s3,1))) = ( 0 + 1) by A2, A11, SCMFSA_2: 70;

      

       A13: (P3 . 1) = (( if=0 (a,I,J)) . 1) by A10, A8, GRFUNC_1: 2

      .= ( goto 2) by Lm2;

      

       A14: ( Comput (P3,s3,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s4)) by A12, A13, PBOOLE: 143;

       A15:

      now

        let f be FinSeq-Location;

        

        thus (s2 . f) = (( Comput (P3,s3,1)) . f) by A11, SCMFSA_2: 70

        .= (s5 . f) by A14, SCMFSA_2: 69;

      end;

      now

        let a be Int-Location;

        

        thus (s2 . a) = (( Comput (P3,s3,1)) . a) by A11, SCMFSA_2: 70

        .= (s5 . a) by A14, SCMFSA_2: 69;

      end;

      then

       A16: ( DataPart s2) = ( DataPart s5) by A15, SCMFSA_M: 2;

      assume

       A17: J is_halting_on (s,P);

      

       A18: P2 halts_on s2 by A17, SCMFSA8A: 38;

      

       A19: ( IC s5) = 2 by A14, SCMFSA_2: 69;

      ( CurInstr (P3,( Comput (P3,s3,(( LifeSpan (P2,s2)) + 2))))) = ( CurInstr (P3,( Comput (P3,s5,( LifeSpan (P2,s2)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P2,( Comput (P2,s2,( LifeSpan (P2,s2)))))),2)) by A19, A16, Th2, A5, A1

      .= ( IncAddr (( halt SCM+FSA ),2)) by A18, EXTPRO_1:def 15

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

      then P3 halts_on s3 by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8B:16

    

     Th10: for I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds for s be State of SCM+FSA st (s . a) <> 0 & J is_halting_on (( Initialized s),P) holds ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))

    proof

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      let s be State of SCM+FSA ;

      set I1 = (I ";" ( Stop SCM+FSA ));

      reconsider JI2 = (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) as really-closed Program of SCM+FSA by Lm3;

      set s2 = ( Initialized s), P2 = (P +* JI2);

      

       A1: JI2 c= P2 by FUNCT_4: 25;

      set P3 = (P +* ( if=0 (a,I,J)));

      set s4 = ( Comput (P3,s2,1));

      set s5 = ( Comput (P3,s2,2));

      set i = (a =0_goto (( card J) + 3));

       0 in ( dom ( if=0 (a,I,J))) by AFINSQ_1: 65;

      

      then

       A2: (P3 . 0 ) = (( if=0 (a,I,J)) . 0 ) by FUNCT_4: 13

      .= i by Lm2;

      

       A3: 1 in ( dom ( if=0 (a,I,J))) by Lm1;

      

       A4: (P3 . 1) = (( if=0 (a,I,J)) . 1) by A3, FUNCT_4: 13

      .= ( goto 2) by Lm2;

      

       A5: ( dom ( Initialize (( intloc 0 ) .--> 1))) = {( intloc 0 ), ( IC SCM+FSA )} by SCMFSA_M: 11;

      a <> ( intloc 0 ) & a <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then

       A6: not a in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A5, TARSKI:def 2;

      ( IC SCM+FSA ) in ( dom ( Initialize (( intloc 0 ) .--> 1))) by MEMSTR_0: 48;

      

      then

       A7: ( IC s2) = ( IC ( Initialize (( intloc 0 ) .--> 1))) by FUNCT_4: 13

      .= 0 by MEMSTR_0:def 11;

      ( if=0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25

      .= ((i ";" J) ";" (( Goto (( card I) + 1)) ";" I1)) by SCMFSA6A: 25

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" I1))) by SCMFSA6A: 29

      .= (i ";" ((J ";" ( Goto (( card I) + 1))) ";" I1)) by SCMFSA6A: 25

      .= (( Macro i) ";" JI2) by SCMFSA6A: 25;

      then ( Reloc (JI2,( card ( Macro i)))) c= ( if=0 (a,I,J)) by SCMFSA6A: 38;

      then

       A8: ( Reloc (JI2,2)) c= ( if=0 (a,I,J)) by COMPOS_1: 56;

      ( if=0 (a,I,J)) c= P3 by FUNCT_4: 25;

      then

       A9: ( Reloc (JI2,2)) c= P3 by A8, XBOOLE_1: 1;

      

       A10: ( Comput (P3,s2,( 0 + 1))) = ( Following (P3,( Comput (P3,s2, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s2))

      .= ( Exec (i,s2)) by A7, A2, PBOOLE: 143;

      assume (s . a) <> 0 ;

      then (s2 . a) <> 0 by A6, FUNCT_4: 11;

      then

       A11: ( IC ( Comput (P3,s2,1))) = ( 0 + 1) by A7, A10, SCMFSA_2: 70;

      

       A12: ( Comput (P3,s2,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s4)) by A11, A4, PBOOLE: 143;

      then

       A13: ( IC s5) = 2 by SCMFSA_2: 69;

       A14:

      now

        let f be FinSeq-Location;

        

        thus (s2 . f) = (( Comput (P3,s2,1)) . f) by A10, SCMFSA_2: 70

        .= (s5 . f) by A12, SCMFSA_2: 69;

      end;

      now

        let a be Int-Location;

        

        thus (s2 . a) = (( Comput (P3,s2,1)) . a) by A10, SCMFSA_2: 70

        .= (s5 . a) by A12, SCMFSA_2: 69;

      end;

      then

       A15: ( DataPart s2) = ( DataPart s5) by A14, SCMFSA_M: 2;

      assume

       A16: J is_halting_on (( Initialized s),P);

      then

       A17: P2 halts_on s2 by SCMFSA8A: 39;

      

       A18: ( CurInstr (P3,( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2))))) = ( CurInstr (P3,( Comput (P3,s5,( LifeSpan (P2,s2)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P2,( Comput (P2,s2,( LifeSpan (P2,s2)))))),2)) by A9, A13, A15, Th2, A1

      .= ( IncAddr (( halt SCM+FSA ),2)) by A17, EXTPRO_1:def 15

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

      then

       A19: P3 halts_on s2 by EXTPRO_1: 29;

      now

        let l be Nat;

        assume

         A20: l < (( LifeSpan (P2,s2)) + 2);

        per cases ;

          suppose l = 0 ;

          hence ( CurInstr (P3,( Comput (P3,s2,l)))) <> ( halt SCM+FSA ) by A7, A2, PBOOLE: 143;

        end;

          suppose l = 1;

          hence ( CurInstr (P3,( Comput (P3,s2,l)))) <> ( halt SCM+FSA ) by A11, A4, PBOOLE: 143;

        end;

          suppose

           A21: l <> 0 & l <> 1;

          assume

           A22: ( CurInstr (P3,( Comput (P3,s2,l)))) = ( halt SCM+FSA );

          consider n be Nat such that

           A23: l = (n + 1) by A21, NAT_1: 6;

          n <> 0 by A21, A23;

          then

          consider l2 be Nat such that

           A24: n = (l2 + 1) by NAT_1: 6;

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

          

           A25: ( InsCode ( halt SCM+FSA )) = 0 by COMPOS_1: 70;

          

           A26: ( Comput (P3,s2,(l2 + (1 + 1)))) = ( Comput (P3,( Comput (P3,s2,(1 + 1))),l2)) by EXTPRO_1: 4;

          ( InsCode ( CurInstr (P2,( Comput (P2,s2,l2))))) = ( InsCode ( IncAddr (( CurInstr (P2,( Comput (P2,s2,l2)))),2))) by COMPOS_0:def 9

          .= 0 by A23, A24, A22, A26, A13, A15, Th2, A9, A1, A25;

          then

           A27: ( CurInstr (P2,( Comput (P2,s2,l2)))) = ( halt SCM+FSA ) by SCMFSA_2: 95;

          (n + 1) < ((( LifeSpan (P2,s2)) + 1) + 1) by A20, A23;

          then n < (( LifeSpan (P2,s2)) + 1) by XREAL_1: 6;

          then l2 < ( LifeSpan (P2,s2)) by A24, XREAL_1: 6;

          hence contradiction by A17, A27, EXTPRO_1:def 15;

        end;

      end;

      then for l be Nat st ( CurInstr (P3,( Comput (P3,s2,l)))) = ( halt SCM+FSA ) holds (( LifeSpan (P2,s2)) + 2) <= l;

      then

       A28: ( LifeSpan (P3,s2)) = (( LifeSpan (P2,s2)) + 2) by A18, A19, EXTPRO_1:def 15;

      

       A29: ( DataPart ( Result (P2,s2))) = ( DataPart ( Comput (P2,s2,( LifeSpan (P2,s2))))) by A16, EXTPRO_1: 23, SCMFSA8A: 39

      .= ( DataPart ( Comput (P3,s5,( LifeSpan (P2,s2))))) by A13, A15, Th2, A9, A1

      .= ( DataPart ( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2)))) by EXTPRO_1: 4

      .= ( DataPart ( Result (P3,s2))) by A19, A28, EXTPRO_1: 23;

       A30:

      now

        let x be object;

        

         A32: ( IExec (( if=0 (a,I,J)),P,s)) = ( Result (P3,s2)) by SCMFSA6B:def 1;

        

         A33: ( IExec (JI2,P,s)) = ( Result (P2,s2)) by SCMFSA6B:def 1;

        assume

         A34: x in ( dom ( IExec (( if=0 (a,I,J)),P,s)));

        per cases by A34, SCMFSA_M: 1;

          suppose

           A35: x is Int-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 56;

          then

           A36: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A32

          .= (( Result (P2,s2)) . x) by A29, A35, SCMFSA_M: 2

          .= (( IExec (JI2,P,s)) . x) by A33

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A36, FUNCT_4: 11;

        end;

          suppose

           A37: x is FinSeq-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 57;

          then

           A38: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A32

          .= (( Result (P2,s2)) . x) by A29, A37, SCMFSA_M: 2

          .= (( IExec (JI2,P,s)) . x) by A33

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A38, FUNCT_4: 11;

        end;

          suppose

           A39: x = ( IC SCM+FSA );

          then

           A40: x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

           A41: ( IC ( Result (P2,s2))) = ( IC ( IExec (JI2,P,s))) by A33

          .= ((( card I) + ( card J)) + 1) by A16, SCMFSA8A: 40;

          

          thus (( IExec (( if=0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A32

          .= (( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2))) . x) by A19, A28, EXTPRO_1: 23

          .= ( IC ( Comput (P3,s5,( LifeSpan (P2,s2))))) by A39, EXTPRO_1: 4

          .= (( IC ( Comput (P2,s2,( LifeSpan (P2,s2))))) + 2) by A13, A15, Th2, A9, A1

          .= (( IC ( Result (P2,s2))) + 2) by A16, EXTPRO_1: 23, SCMFSA8A: 39

          .= (( Start-At ((((( card I) + ( card J)) + 1) + 2), SCM+FSA )) . ( IC SCM+FSA )) by A41, FUNCOP_1: 72

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A39, A40, FUNCT_4: 13;

        end;

      end;

      ( dom ( IExec (( if=0 (a,I,J)),P,s))) = the carrier of SCM+FSA by PARTFUN1:def 2

      .= ( dom (( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) by PARTFUN1:def 2;

      

      hence ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A30, FUNCT_1: 2

      .= ((( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A16, SCMFSA8A: 41

      .= (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by FUNCT_4: 114;

    end;

    theorem :: SCMFSA8B:17

    

     Th11: for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds ( if=0 (a,I,J)) is parahalting & ((s . a) = 0 implies ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) & ((s . a) <> 0 implies ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      

       A1: I is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      for s be 0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st ( if=0 (a,I,J)) c= P holds P halts_on s

      proof

        let s be 0 -started State of SCM+FSA ;

        ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        then

         A2: s = ( Initialize s) by FUNCT_4: 98;

        let Q be Instruction-Sequence of SCM+FSA such that

         A3: ( if=0 (a,I,J)) c= Q;

        

         A4: ( if=0 (a,I,J)) c= Q by A3;

        

         A5: I is_halting_on (s,Q) by SCMFSA7B: 19;

        

         A6: J is_halting_on (s,Q) by SCMFSA7B: 19;

        

         A7: (Q +* ( if=0 (a,I,J))) = Q by A4, FUNCT_4: 98;

        per cases ;

          suppose (s . a) = 0 ;

          then ( if=0 (a,I,J)) is_halting_on (s,Q) by A5, Th7;

          hence Q halts_on s by A2, A7, SCMFSA7B:def 7;

        end;

          suppose (s . a) <> 0 ;

          then ( if=0 (a,I,J)) is_halting_on (s,Q) by A6, Th9;

          hence Q halts_on s by A2, A7, SCMFSA7B:def 7;

        end;

      end;

      hence ( if=0 (a,I,J)) is parahalting by AMISTD_1:def 11;

      thus (s . a) = 0 implies ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A1, Th8;

      J is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      hence thesis by Th10;

    end;

    theorem :: SCMFSA8B:18

    

     Th12: for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds ( IC ( IExec (( if=0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) & ((s . a) = 0 implies ((for d be Int-Location holds (( IExec (( if=0 (a,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if=0 (a,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f))) & ((s . a) <> 0 implies ((for d be Int-Location holds (( IExec (( if=0 (a,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if=0 (a,I,J)),P,s)) . f) = (( IExec (J,P,s)) . f)))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      hereby

        per cases ;

          suppose (s . a) = 0 ;

          then ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th11;

          hence ( IC ( IExec (( if=0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) by FUNCT_4: 113;

        end;

          suppose (s . a) <> 0 ;

          then ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th11;

          hence ( IC ( IExec (( if=0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) by FUNCT_4: 113;

        end;

      end;

      hereby

        assume (s . a) = 0 ;

        then

         A1: ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th11;

        hereby

          let d be Int-Location;

           not d in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 102;

          hence (( IExec (( if=0 (a,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d) by A1, FUNCT_4: 11;

        end;

        let f be FinSeq-Location;

         not f in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 103;

        hence (( IExec (( if=0 (a,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f) by A1, FUNCT_4: 11;

      end;

      assume (s . a) <> 0 ;

      then

       A2: ( IExec (( if=0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th11;

      hereby

        let d be Int-Location;

         not d in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 102;

        hence (( IExec (( if=0 (a,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d) by A2, FUNCT_4: 11;

      end;

      let f be FinSeq-Location;

       not f in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 103;

      hence thesis by A2, FUNCT_4: 11;

    end;

    theorem :: SCMFSA8B:19

    

     Th13: for s be State of SCM+FSA , I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) > 0 & I is_halting_on (s,P) holds ( if>0 (a,I,J)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      set I1 = (I ";" ( Stop SCM+FSA ));

      set s1 = ( Initialize s), P1 = (P +* I1);

      set s3 = ( Initialize s), P3 = (P +* ( if>0 (a,I,J)));

      set s4 = ( Comput (P3,s3,1));

      set i = (a >0_goto (( card J) + 3));

      

       A1: I1 c= P1 by FUNCT_4: 25;

      

       A2: not a in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      

       A3: 0 in ( dom ( if>0 (a,I,J))) by AFINSQ_1: 65;

      

       A4: (P3 . 0 ) = (( if>0 (a,I,J)) . 0 ) by A3, FUNCT_4: 13

      .= i by Lm2;

      ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

      then

       A5: ( IC s3) = ( IC ( Start-At ( 0 , SCM+FSA ))) by FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      

       A6: ( if>0 (a,I,J)) c= P3 by FUNCT_4: 25;

      

       A7: ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25;

      ( card ((i ";" J) ";" ( Goto (( card I) + 1)))) = (( card (( Macro i) ";" J)) + ( card ( Goto (( card I) + 1)))) by SCMFSA6A: 21

      .= (( card (( Macro i) ";" J)) + 1) by SCMFSA8A: 15

      .= ((( card ( Macro i)) + ( card J)) + 1) by SCMFSA6A: 21

      .= ((( card J) + 2) + 1) by COMPOS_1: 56

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

      then

       A8: ( Reloc (I1,(( card J) + 3))) c= ( if>0 (a,I,J)) by A7, SCMFSA6A: 38;

      

       A9: ( Reloc (I1,(( card J) + 3))) c= P3 by A8, A6, XBOOLE_1: 1;

      

       A10: ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i,s3)) by A5, A4, PBOOLE: 143;

      

       A11: for f be FinSeq-Location holds (s1 . f) = (s4 . f) by A10, SCMFSA_2: 71;

      for a be Int-Location holds (s1 . a) = (s4 . a) by A10, SCMFSA_2: 71;

      then

       A12: ( DataPart s1) = ( DataPart s4) by A11, SCMFSA_M: 2;

      assume (s . a) > 0 ;

      then (s3 . a) > 0 by A2, FUNCT_4: 11;

      then

       A13: ( IC ( Comput (P3,s3,1))) = (( card J) + 3) by A10, SCMFSA_2: 71;

      assume

       A14: I is_halting_on (s,P);

      I1 is_halting_on (s,P) by A14, SCMFSA8A: 30;

      then

       A15: P1 halts_on s1 by SCMFSA7B:def 7;

      ( CurInstr (P3,( Comput (P3,s3,(( LifeSpan (P1,s1)) + 1))))) = ( CurInstr (P3,( Comput (P3,s4,( LifeSpan (P1,s1)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P1,( Comput (P1,s1,( LifeSpan (P1,s1)))))),(( card J) + 3))) by A13, A12, Th2, A9, A1

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 3))) by A15, EXTPRO_1:def 15

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

      then P3 halts_on s3 by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8B:20

    

     Th14: for I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds for s be State of SCM+FSA st (s . a) > 0 & I is_halting_on (( Initialized s),P) holds ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))

    proof

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      let s be State of SCM+FSA ;

      set I1 = (I ";" ( Stop SCM+FSA ));

      set s1 = ( Initialized s), P1 = (P +* I1);

      set P3 = (P +* ( if>0 (a,I,J)));

      set s4 = ( Comput (P3,s1,1));

      set i = (a >0_goto (( card J) + 3));

      

       A1: I1 c= P1 by FUNCT_4: 25;

      

       A2: ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25;

      

       A3: 0 in ( dom ( if>0 (a,I,J))) by AFINSQ_1: 65;

      

       A4: (P3 . 0 ) = (( if>0 (a,I,J)) . 0 ) by A3, FUNCT_4: 13

      .= i by Lm2;

      

       A5: ( dom ( Initialize (( intloc 0 ) .--> 1))) = {( intloc 0 ), ( IC SCM+FSA )} by SCMFSA_M: 11;

      a <> ( intloc 0 ) & a <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then

       A6: not a in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A5, TARSKI:def 2;

      ( IC SCM+FSA ) in ( dom ( Initialize (( intloc 0 ) .--> 1))) by MEMSTR_0: 48;

      

      then

       A7: ( IC s1) = ( IC ( Initialize (( intloc 0 ) .--> 1))) by FUNCT_4: 13

      .= 0 by MEMSTR_0:def 11;

      

       A8: ( Comput (P3,s1,( 0 + 1))) = ( Following (P3,( Comput (P3,s1, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s1))

      .= ( Exec (i,s1)) by A7, A4, PBOOLE: 143;

      

       A9: ( if>0 (a,I,J)) c= P3 by FUNCT_4: 25;

      assume (s . a) > 0 ;

      then (s1 . a) > 0 by A6, FUNCT_4: 11;

      then

       A10: ( IC ( Comput (P3,s1,1))) = (( card J) + 3) by A8, SCMFSA_2: 71;

      

       A11: for f be FinSeq-Location holds (s1 . f) = (s4 . f) by A8, SCMFSA_2: 71;

      for a be Int-Location holds (s1 . a) = (s4 . a) by A8, SCMFSA_2: 71;

      then

       A12: ( DataPart s1) = ( DataPart s4) by A11, SCMFSA_M: 2;

      ( card ((i ";" J) ";" ( Goto (( card I) + 1)))) = (( card (( Macro i) ";" J)) + ( card ( Goto (( card I) + 1)))) by SCMFSA6A: 21

      .= (( card (( Macro i) ";" J)) + 1) by SCMFSA8A: 15

      .= ((( card ( Macro i)) + ( card J)) + 1) by SCMFSA6A: 21

      .= ((( card J) + 2) + 1) by COMPOS_1: 56

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

      then

       A13: ( Reloc (I1,(( card J) + 3))) c= ( if>0 (a,I,J)) by A2, SCMFSA6A: 38;

      

       A14: ( Reloc (I1,(( card J) + 3))) c= P3 by A13, A9, XBOOLE_1: 1;

      assume

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

      then

       A16: P1 halts_on s1 by SCMFSA8A: 34;

      

       A17: ( CurInstr (P3,( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1))))) = ( CurInstr (P3,( Comput (P3,s4,( LifeSpan (P1,s1)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P1,( Comput (P1,s1,( LifeSpan (P1,s1)))))),(( card J) + 3))) by A10, A12, Th2, A14, A1

      .= ( IncAddr (( halt SCM+FSA ),(( card J) + 3))) by A16, EXTPRO_1:def 15

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

      then

       A18: P3 halts_on s1 by EXTPRO_1: 29;

      now

        let l be Nat;

        assume

         A19: l < (( LifeSpan (P1,s1)) + 1);

        per cases ;

          suppose l = 0 ;

          hence ( CurInstr (P3,( Comput (P3,s1,l)))) <> ( halt SCM+FSA ) by A7, A4, PBOOLE: 143;

        end;

          suppose l <> 0 ;

          then

          consider n be Nat such that

           A20: l = (n + 1) by NAT_1: 6;

          assume

           A21: ( CurInstr (P3,( Comput (P3,s1,l)))) = ( halt SCM+FSA );

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

          

           A22: ( InsCode ( halt SCM+FSA )) = 0 by COMPOS_1: 70;

          ( InsCode ( CurInstr (P1,( Comput (P1,s1,n))))) = ( InsCode ( IncAddr (( CurInstr (P1,( Comput (P1,s1,n)))),(( card J) + 3)))) by COMPOS_0:def 9

          .= ( InsCode ( CurInstr (P3,( Comput (P3,s4,n))))) by A10, A12, Th2, A14, A1

          .= 0 by A20, A21, A22, EXTPRO_1: 4;

          then

           A23: ( CurInstr (P1,( Comput (P1,s1,n)))) = ( halt SCM+FSA ) by SCMFSA_2: 95;

          n < ( LifeSpan (P1,s1)) by A19, A20, XREAL_1: 6;

          hence contradiction by A16, A23, EXTPRO_1:def 15;

        end;

      end;

      then for l be Nat st ( CurInstr (P3,( Comput (P3,s1,l)))) = ( halt SCM+FSA ) holds (( LifeSpan (P1,s1)) + 1) <= l;

      then

       A24: ( LifeSpan (P3,s1)) = (( LifeSpan (P1,s1)) + 1) by A17, A18, EXTPRO_1:def 15;

      

       A25: ( DataPart ( Result (P1,s1))) = ( DataPart ( Comput (P1,s1,( LifeSpan (P1,s1))))) by A15, EXTPRO_1: 23, SCMFSA8A: 34

      .= ( DataPart ( Comput (P3,s4,( LifeSpan (P1,s1))))) by A10, A12, Th2, A14, A1

      .= ( DataPart ( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1)))) by EXTPRO_1: 4

      .= ( DataPart ( Result (P3,s1))) by A18, A24, EXTPRO_1: 23;

       A26:

      now

        let x be object;

        

         A28: ( IExec (( if>0 (a,I,J)),P,s)) = ( Result (P3,s1)) by SCMFSA6B:def 1;

        

         A29: ( IExec (I1,P,s)) = ( Result (P1,s1)) by SCMFSA6B:def 1;

        assume

         A30: x in ( dom ( IExec (( if>0 (a,I,J)),P,s)));

        per cases by A30, SCMFSA_M: 1;

          suppose

           A31: x is Int-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 56;

          then

           A32: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A28

          .= (( Result (P1,s1)) . x) by A25, A31, SCMFSA_M: 2

          .= (( IExec (I1,P,s)) . x) by A29

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A32, FUNCT_4: 11;

        end;

          suppose

           A33: x is FinSeq-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 57;

          then

           A34: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A28

          .= (( Result (P1,s1)) . x) by A25, A33, SCMFSA_M: 2

          .= (( IExec (I1,P,s)) . x) by A29

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A34, FUNCT_4: 11;

        end;

          suppose

           A35: x = ( IC SCM+FSA );

          then

           A36: x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

           A37: ( IC ( Result (P1,s1))) = (( IExec (I1,P,s)) . ( IC SCM+FSA )) by A29

          .= ( IC (( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA )))) by A15, SCMFSA8A: 36

          .= ( card I) by FUNCT_4: 113;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s1)) . x) by A28

          .= (( Comput (P3,s1,(( LifeSpan (P1,s1)) + 1))) . x) by A18, A24, EXTPRO_1: 23

          .= ( IC ( Comput (P3,s4,( LifeSpan (P1,s1))))) by A35, EXTPRO_1: 4

          .= (( IC ( Comput (P1,s1,( LifeSpan (P1,s1))))) + (( card J) + 3)) by A10, A12, Th2, A1, A14

          .= (( IC ( Result (P1,s1))) + (( card J) + 3)) by A15, EXTPRO_1: 23, SCMFSA8A: 34

          .= (( Start-At ((( card I) + (( card J) + 3)), SCM+FSA )) . ( IC SCM+FSA )) by A37, FUNCOP_1: 72

          .= ((( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A35, A36, FUNCT_4: 13;

        end;

      end;

      ( dom ( IExec (( if>0 (a,I,J)),P,s))) = the carrier of SCM+FSA by PARTFUN1:def 2

      .= ( dom (( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) by PARTFUN1:def 2;

      

      hence ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I1,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A26, FUNCT_1: 2

      .= ((( IExec (I,P,s)) +* ( Start-At (( card I), SCM+FSA ))) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A15, SCMFSA8A: 36

      .= (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by FUNCT_4: 114;

    end;

    theorem :: SCMFSA8B:21

    

     Th15: for s be State of SCM+FSA , I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) <= 0 & J is_halting_on (s,P) holds ( if>0 (a,I,J)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      set I1 = (I ";" ( Stop SCM+FSA ));

      reconsider JI2 = (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) as really-closed Program of SCM+FSA by Lm3;

      set s2 = ( Initialize s), P2 = (P +* JI2);

      

       A1: JI2 c= P2 by FUNCT_4: 25;

      set s3 = ( Initialize s), P3 = (P +* ( if>0 (a,I,J)));

      set s4 = ( Comput (P3,s3,1));

      set s5 = ( Comput (P3,s3,2));

      set i = (a >0_goto (( card J) + 3));

      ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

      

      then

       A2: ( IC s3) = ( IC ( Start-At ( 0 , SCM+FSA ))) by FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

      

       A3: ( if>0 (a,I,J)) c= P3 by FUNCT_4: 25;

      ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25

      .= ((i ";" J) ";" (( Goto (( card I) + 1)) ";" I1)) by SCMFSA6A: 25

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" I1))) by SCMFSA6A: 29

      .= (i ";" ((J ";" ( Goto (( card I) + 1))) ";" I1)) by SCMFSA6A: 25

      .= (( Macro i) ";" JI2) by SCMFSA6A: 25;

      then

       A4: ( Reloc (JI2,( card ( Macro i)))) c= ( if>0 (a,I,J)) by SCMFSA6A: 38;

      ( card ( Macro i)) = 2 by COMPOS_1: 56;

      then

       A5: ( Reloc (JI2,2)) c= P3 by A3, A4, XBOOLE_1: 1;

      

       A6: not a in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      

       A7: 0 in ( dom ( if>0 (a,I,J))) by AFINSQ_1: 65;

      

       A8: (P3 . 0 ) = (( if>0 (a,I,J)) . 0 ) by A7, FUNCT_4: 13

      .= i by Lm2;

      

       A9: 1 in ( dom ( if>0 (a,I,J))) by Lm1;

      

       A10: ( Comput (P3,s3,( 0 + 1))) = ( Following (P3,( Comput (P3,s3, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s3))

      .= ( Exec (i,s3)) by A2, A8, PBOOLE: 143;

      assume (s . a) <= 0 ;

      then (s3 . a) <= 0 by A6, FUNCT_4: 11;

      then

       A11: ( IC ( Comput (P3,s3,1))) = ( 0 + 1) by A2, A10, SCMFSA_2: 71;

      

       A12: (P3 . 1) = (( if>0 (a,I,J)) . 1) by A9, FUNCT_4: 13

      .= ( goto 2) by Lm2;

      

       A13: ( Comput (P3,s3,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s4)) by A11, A12, PBOOLE: 143;

       A14:

      now

        let f be FinSeq-Location;

        

        thus (s2 . f) = (( Comput (P3,s3,1)) . f) by A10, SCMFSA_2: 71

        .= (s5 . f) by A13, SCMFSA_2: 69;

      end;

      now

        let a be Int-Location;

        

        thus (s2 . a) = (( Comput (P3,s3,1)) . a) by A10, SCMFSA_2: 71

        .= (s5 . a) by A13, SCMFSA_2: 69;

      end;

      then

       A15: ( DataPart s2) = ( DataPart s5) by A14, SCMFSA_M: 2;

      assume

       A16: J is_halting_on (s,P);

      

       A17: P2 halts_on s2 by A16, SCMFSA8A: 38;

      

       A18: ( IC s5) = 2 by A13, SCMFSA_2: 69;

      ( CurInstr (P3,( Comput (P3,s3,(( LifeSpan (P2,s2)) + 2))))) = ( CurInstr (P3,( Comput (P3,s5,( LifeSpan (P2,s2)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P2,( Comput (P2,s2,( LifeSpan (P2,s2)))))),2)) by A5, A18, A15, Th2, A1

      .= ( IncAddr (( halt SCM+FSA ),2)) by A17, EXTPRO_1:def 15

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

      then P3 halts_on s3 by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8B:22

    

     Th16: for I,J be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds for s be State of SCM+FSA st (s . a) <= 0 & J is_halting_on (( Initialized s),P) holds ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))

    proof

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      let s be State of SCM+FSA ;

      set I1 = (I ";" ( Stop SCM+FSA ));

      reconsider JI2 = (((J ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA )) as really-closed Program of SCM+FSA by Lm3;

      set s2 = ( Initialized s), P2 = (P +* JI2);

      

       A1: JI2 c= P2 by FUNCT_4: 25;

      set P3 = (P +* ( if>0 (a,I,J)));

      set s4 = ( Comput (P3,s2,1));

      set s5 = ( Comput (P3,s2,2));

      set i = (a >0_goto (( card J) + 3));

       0 in ( dom ( if>0 (a,I,J))) by AFINSQ_1: 65;

      

      then

       A2: (P3 . 0 ) = (( if>0 (a,I,J)) . 0 ) by FUNCT_4: 13

      .= i by Lm2;

      

       A3: 1 in ( dom ( if>0 (a,I,J))) by Lm1;

      

       A4: (P3 . 1) = (( if>0 (a,I,J)) . 1) by A3, FUNCT_4: 13

      .= ( goto 2) by Lm2;

      

       A5: ( dom ( Initialize (( intloc 0 ) .--> 1))) = {( intloc 0 ), ( IC SCM+FSA )} by SCMFSA_M: 11;

      a <> ( intloc 0 ) & a <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then

       A6: not a in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A5, TARSKI:def 2;

      ( IC SCM+FSA ) in ( dom ( Initialize (( intloc 0 ) .--> 1))) by MEMSTR_0: 48;

      

      then

       A7: ( IC s2) = ( IC ( Initialize (( intloc 0 ) .--> 1))) by FUNCT_4: 13

      .= 0 by MEMSTR_0:def 11;

      ( if>0 (a,I,J)) = (((i ";" J) ";" ( Goto (( card I) + 1))) ";" I1) by SCMFSA6A: 25

      .= ((i ";" J) ";" (( Goto (( card I) + 1)) ";" I1)) by SCMFSA6A: 25

      .= (i ";" (J ";" (( Goto (( card I) + 1)) ";" I1))) by SCMFSA6A: 29

      .= (i ";" ((J ";" ( Goto (( card I) + 1))) ";" I1)) by SCMFSA6A: 25

      .= (( Macro i) ";" JI2) by SCMFSA6A: 25;

      then ( Reloc (JI2,( card ( Macro i)))) c= ( if>0 (a,I,J)) by SCMFSA6A: 38;

      then

       A8: ( Reloc (JI2,2)) c= ( if>0 (a,I,J)) by COMPOS_1: 56;

      ( if>0 (a,I,J)) c= P3 by FUNCT_4: 25;

      then

       A9: ( Reloc (JI2,2)) c= P3 by A8, XBOOLE_1: 1;

      

       A10: ( Comput (P3,s2,( 0 + 1))) = ( Following (P3,( Comput (P3,s2, 0 )))) by EXTPRO_1: 3

      .= ( Following (P3,s2))

      .= ( Exec (i,s2)) by A7, A2, PBOOLE: 143;

      assume (s . a) <= 0 ;

      then (s2 . a) <= 0 by A6, FUNCT_4: 11;

      then

       A11: ( IC ( Comput (P3,s2,1))) = ( 0 + 1) by A7, A10, SCMFSA_2: 71;

      

       A12: ( Comput (P3,s2,(1 + 1))) = ( Following (P3,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s4)) by A11, A4, PBOOLE: 143;

      then

       A13: ( IC s5) = 2 by SCMFSA_2: 69;

       A14:

      now

        let f be FinSeq-Location;

        

        thus (s2 . f) = (( Comput (P3,s2,1)) . f) by A10, SCMFSA_2: 71

        .= (s5 . f) by A12, SCMFSA_2: 69;

      end;

      now

        let a be Int-Location;

        

        thus (s2 . a) = (( Comput (P3,s2,1)) . a) by A10, SCMFSA_2: 71

        .= (s5 . a) by A12, SCMFSA_2: 69;

      end;

      then

       A15: ( DataPart s2) = ( DataPart s5) by A14, SCMFSA_M: 2;

      assume

       A16: J is_halting_on (( Initialized s),P);

      then

       A17: P2 halts_on s2 by SCMFSA8A: 39;

      

       A18: ( CurInstr (P3,( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2))))) = ( CurInstr (P3,( Comput (P3,s5,( LifeSpan (P2,s2)))))) by EXTPRO_1: 4

      .= ( IncAddr (( CurInstr (P2,( Comput (P2,s2,( LifeSpan (P2,s2)))))),2)) by A13, A15, Th2, A9, A1

      .= ( IncAddr (( halt SCM+FSA ),2)) by A17, EXTPRO_1:def 15

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

      then

       A19: P3 halts_on s2 by EXTPRO_1: 29;

      now

        let l be Nat;

        assume

         A20: l < (( LifeSpan (P2,s2)) + 2);

        per cases ;

          suppose l = 0 ;

          hence ( CurInstr (P3,( Comput (P3,s2,l)))) <> ( halt SCM+FSA ) by A7, A2, PBOOLE: 143;

        end;

          suppose l = 1;

          hence ( CurInstr (P3,( Comput (P3,s2,l)))) <> ( halt SCM+FSA ) by A11, A4, PBOOLE: 143;

        end;

          suppose

           A21: l <> 0 & l <> 1;

          assume

           A22: ( CurInstr (P3,( Comput (P3,s2,l)))) = ( halt SCM+FSA );

          consider n be Nat such that

           A23: l = (n + 1) by A21, NAT_1: 6;

          n <> 0 by A21, A23;

          then

          consider l2 be Nat such that

           A24: n = (l2 + 1) by NAT_1: 6;

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

          ( InsCode ( CurInstr (P2,( Comput (P2,s2,l2))))) = ( InsCode ( IncAddr (( CurInstr (P2,( Comput (P2,s2,l2)))),2))) by COMPOS_0:def 9

          .= ( InsCode ( CurInstr (P3,( Comput (P3,s5,l2))))) by A13, A15, Th2, A9, A1

          .= ( InsCode ( CurInstr (P3,( Comput (P3,s2,(l2 + (1 + 1))))))) by EXTPRO_1: 4

          .= 0 by A23, A24, A22, COMPOS_1: 70;

          then

           A25: ( CurInstr (P2,( Comput (P2,s2,l2)))) = ( halt SCM+FSA ) by SCMFSA_2: 95;

          (n + 1) < ((( LifeSpan (P2,s2)) + 1) + 1) by A20, A23;

          then n < (( LifeSpan (P2,s2)) + 1) by XREAL_1: 6;

          then l2 < ( LifeSpan (P2,s2)) by A24, XREAL_1: 6;

          hence contradiction by A17, A25, EXTPRO_1:def 15;

        end;

      end;

      then for l be Nat st ( CurInstr (P3,( Comput (P3,s2,l)))) = ( halt SCM+FSA ) holds (( LifeSpan (P2,s2)) + 2) <= l;

      then

       A26: ( LifeSpan (P3,s2)) = (( LifeSpan (P2,s2)) + 2) by A18, A19, EXTPRO_1:def 15;

      

       A27: ( DataPart ( Result (P2,s2))) = ( DataPart ( Comput (P2,s2,( LifeSpan (P2,s2))))) by A16, EXTPRO_1: 23, SCMFSA8A: 39

      .= ( DataPart ( Comput (P3,s5,( LifeSpan (P2,s2))))) by A13, A15, Th2, A9, A1

      .= ( DataPart ( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2)))) by EXTPRO_1: 4

      .= ( DataPart ( Result (P3,s2))) by A19, A26, EXTPRO_1: 23;

       A28:

      now

        let x be object;

        

         A30: ( IExec (( if>0 (a,I,J)),P,s)) = ( Result (P3,s2)) by SCMFSA6B:def 1;

        

         A31: ( IExec (JI2,P,s)) = ( Result (P2,s2)) by SCMFSA6B:def 1;

        assume

         A32: x in ( dom ( IExec (( if>0 (a,I,J)),P,s)));

        per cases by A32, SCMFSA_M: 1;

          suppose

           A33: x is Int-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 56;

          then

           A34: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A30

          .= (( Result (P2,s2)) . x) by A27, A33, SCMFSA_M: 2

          .= (( IExec (JI2,P,s)) . x) by A31

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A34, FUNCT_4: 11;

        end;

          suppose

           A35: x is FinSeq-Location;

          then x <> ( IC SCM+FSA ) by SCMFSA_2: 57;

          then

           A36: not x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A30

          .= (( Result (P2,s2)) . x) by A27, A35, SCMFSA_M: 2

          .= (( IExec (JI2,P,s)) . x) by A31

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A36, FUNCT_4: 11;

        end;

          suppose

           A37: x = ( IC SCM+FSA );

          then

           A38: x in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by TARSKI:def 1;

          

           A39: ( IC ( Result (P2,s2))) = ( IC ( IExec (JI2,P,s))) by A31

          .= ((( card I) + ( card J)) + 1) by A16, SCMFSA8A: 40;

          

          thus (( IExec (( if>0 (a,I,J)),P,s)) . x) = (( Result (P3,s2)) . x) by A30

          .= (( Comput (P3,s2,(( LifeSpan (P2,s2)) + 2))) . x) by A19, A26, EXTPRO_1: 23

          .= ( IC ( Comput (P3,s5,( LifeSpan (P2,s2))))) by A37, EXTPRO_1: 4

          .= (( IC ( Comput (P2,s2,( LifeSpan (P2,s2))))) + 2) by A13, A15, Th2, A9, A1

          .= (( IC ( Result (P2,s2))) + 2) by A16, EXTPRO_1: 23, SCMFSA8A: 39

          .= (( Start-At ((((( card I) + ( card J)) + 1) + 2), SCM+FSA )) . ( IC SCM+FSA )) by A39, FUNCOP_1: 72

          .= ((( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) . x) by A37, A38, FUNCT_4: 13;

        end;

      end;

      ( dom ( IExec (( if>0 (a,I,J)),P,s))) = the carrier of SCM+FSA by PARTFUN1:def 2

      .= ( dom (( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) by PARTFUN1:def 2;

      

      hence ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (JI2,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A28, FUNCT_1: 2

      .= ((( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 1), SCM+FSA ))) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A16, SCMFSA8A: 41

      .= (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by FUNCT_4: 114;

    end;

    theorem :: SCMFSA8B:23

    

     Th17: for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds ( if>0 (a,I,J)) is parahalting & ((s . a) > 0 implies ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA )))) & ((s . a) <= 0 implies ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      

       A1: I is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      for s be 0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA st ( if>0 (a,I,J)) c= P holds P halts_on s

      proof

        let s be 0 -started State of SCM+FSA ;

        ( Start-At ( 0 , SCM+FSA )) c= s by MEMSTR_0: 29;

        then

         A2: s = ( Initialize s) by FUNCT_4: 98;

        let Q be Instruction-Sequence of SCM+FSA such that

         A3: ( if>0 (a,I,J)) c= Q;

        

         A4: ( if>0 (a,I,J)) c= Q by A3;

        

         A5: I is_halting_on (s,Q) by SCMFSA7B: 19;

        

         A6: J is_halting_on (s,Q) by SCMFSA7B: 19;

        

         A7: (Q +* ( if>0 (a,I,J))) = Q by A4, FUNCT_4: 98;

        per cases ;

          suppose (s . a) > 0 ;

          then ( if>0 (a,I,J)) is_halting_on (s,Q) by A5, Th13;

          hence Q halts_on s by A2, A7, SCMFSA7B:def 7;

        end;

          suppose (s . a) <= 0 ;

          then ( if>0 (a,I,J)) is_halting_on (s,Q) by A6, Th15;

          hence Q halts_on s by A2, A7, SCMFSA7B:def 7;

        end;

      end;

      hence ( if>0 (a,I,J)) is parahalting by AMISTD_1:def 11;

      thus (s . a) > 0 implies ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by A1, Th14;

      J is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      hence thesis by Th16;

    end;

    theorem :: SCMFSA8B:24

    

     Th18: for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location holds ( IC ( IExec (( if>0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) & ((s . a) > 0 implies ((for d be Int-Location holds (( IExec (( if>0 (a,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if>0 (a,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f))) & ((s . a) <= 0 implies ((for d be Int-Location holds (( IExec (( if>0 (a,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if>0 (a,I,J)),P,s)) . f) = (( IExec (J,P,s)) . f)))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      hereby

        per cases ;

          suppose (s . a) > 0 ;

          then ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th17;

          hence ( IC ( IExec (( if>0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) by FUNCT_4: 113;

        end;

          suppose (s . a) <= 0 ;

          then ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th17;

          hence ( IC ( IExec (( if>0 (a,I,J)),P,s))) = ((( card I) + ( card J)) + 3) by FUNCT_4: 113;

        end;

      end;

      hereby

        assume (s . a) > 0 ;

        then

         A1: ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (I,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th17;

        hereby

          let d be Int-Location;

           not d in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 102;

          hence (( IExec (( if>0 (a,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d) by A1, FUNCT_4: 11;

        end;

        let f be FinSeq-Location;

         not f in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 103;

        hence (( IExec (( if>0 (a,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f) by A1, FUNCT_4: 11;

      end;

      assume (s . a) <= 0 ;

      then

       A2: ( IExec (( if>0 (a,I,J)),P,s)) = (( IExec (J,P,s)) +* ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by Th17;

      hereby

        let d be Int-Location;

         not d in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 102;

        hence (( IExec (( if>0 (a,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d) by A2, FUNCT_4: 11;

      end;

      let f be FinSeq-Location;

       not f in ( dom ( Start-At (((( card I) + ( card J)) + 3), SCM+FSA ))) by SCMFSA_2: 103;

      hence thesis by A2, FUNCT_4: 11;

    end;

    ::$Canceled

    registration

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      cluster ( if=0 (a,I,J)) -> parahalting;

      correctness by Th11;

      cluster ( if>0 (a,I,J)) -> parahalting;

      correctness by Th17;

    end

    definition

      let a,b be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      :: SCMFSA8B:def3

      func if=0 (a,b,I,J) -> Program of SCM+FSA equals (( SubFrom (a,b)) ";" ( if=0 (a,I,J)));

      coherence ;

      :: SCMFSA8B:def4

      func if>0 (a,b,I,J) -> Program of SCM+FSA equals (( SubFrom (a,b)) ";" ( if>0 (a,I,J)));

      coherence ;

    end

    registration

      let a be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      cluster ( if=0 (a,I,J)) -> halt-ending unique-halt;

      coherence ;

      cluster ( if>0 (a,I,J)) -> halt-ending unique-halt;

      coherence ;

    end

    registration

      let a,b be Int-Location;

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      cluster ( if=0 (a,b,I,J)) -> really-closed;

      coherence ;

      cluster ( if>0 (a,b,I,J)) -> really-closed;

      coherence ;

    end

    registration

      let a,b be Int-Location;

      let I,J be MacroInstruction of SCM+FSA ;

      cluster ( if=0 (a,b,I,J)) -> halt-ending unique-halt;

      coherence ;

      cluster ( if>0 (a,b,I,J)) -> halt-ending unique-halt;

      coherence ;

    end

    registration

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a,b be read-write Int-Location;

      cluster ( if=0 (a,b,I,J)) -> parahalting;

      correctness ;

      cluster ( if>0 (a,b,I,J)) -> parahalting;

      correctness ;

    end

    registration

      let I,J be really-closed MacroInstruction of SCM+FSA ;

      let a,b be read-write Int-Location;

      cluster ( if=0 (a,b,I,J)) -> really-closed;

      correctness ;

      cluster ( if>0 (a,b,I,J)) -> really-closed;

      correctness ;

    end

    theorem :: SCMFSA8B:32

    for s be State of SCM+FSA , I be Program of SCM+FSA holds ( DataPart ( Result ((P +* I),( Initialized s)))) = ( DataPart ( IExec (I,P,s))) by SCMFSA6B:def 1;

    theorem :: SCMFSA8B:33

    

     Th20: for s be State of SCM+FSA , I be Program of SCM+FSA holds ( Result ((P +* I),( Initialized s))) = ( IExec (I,P,s)) by SCMFSA6B:def 1;

    theorem :: SCMFSA8B:34

    

     Th21: for s1,s2 be State of SCM+FSA , i be Instruction of SCM+FSA , a be Int-Location holds (for b be Int-Location st a <> b holds (s1 . b) = (s2 . b)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) & not i refers a & ( IC s1) = ( IC s2) implies (for b be Int-Location st a <> b holds (( Exec (i,s1)) . b) = (( Exec (i,s2)) . b)) & (for f be FinSeq-Location holds (( Exec (i,s1)) . f) = (( Exec (i,s2)) . f)) & ( IC ( Exec (i,s1))) = ( IC ( Exec (i,s2)))

    proof

      let s1,s2 be State of SCM+FSA ;

      let i be Instruction of SCM+FSA ;

      let a be Int-Location;

      defpred S[ State of SCM+FSA , State of SCM+FSA ] means (for b be Int-Location st a <> b holds ($1 . b) = ($2 . b)) & for f be FinSeq-Location holds ($1 . f) = ($2 . f);

      assume

       A1: S[s1, s2];

      assume

       A2: not i refers a;

      

       A3: ( InsCode i) <= 12 by SCMFSA_2: 16;

       A4:

      now

        let b be Int-Location;

        assume

         A5: a <> b;

        ( InsCode i) = 0 or ... or ( InsCode i) = 12 by A3;

        per cases ;

          suppose ( InsCode i) = 0 ;

          then

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

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by EXTPRO_1:def 3

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A6, EXTPRO_1:def 3;

        end;

          suppose ( InsCode i) = 1;

          then

          consider da,db be Int-Location such that

           A7: i = (da := db) by SCMFSA_2: 30;

          

           A8: a <> db by A2, A7, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A9: b = da;

              

              hence (( Exec (i,s1)) . b) = (s1 . db) by A7, SCMFSA_2: 63

              .= (s2 . db) by A1, A8

              .= (( Exec (i,s2)) . b) by A7, A9, SCMFSA_2: 63;

            end;

              suppose

               A10: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A7, SCMFSA_2: 63

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A7, A10, SCMFSA_2: 63;

            end;

          end;

        end;

          suppose ( InsCode i) = 2;

          then

          consider da,db be Int-Location such that

           A11: i = ( AddTo (da,db)) by SCMFSA_2: 31;

          

           A12: a <> db by A2, A11, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A13: b = da;

              

              hence (( Exec (i,s1)) . b) = ((s1 . b) + (s1 . db)) by A11, SCMFSA_2: 64

              .= ((s2 . b) + (s1 . db)) by A1, A5

              .= ((s2 . b) + (s2 . db)) by A1, A12

              .= (( Exec (i,s2)) . b) by A11, A13, SCMFSA_2: 64;

            end;

              suppose

               A14: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A11, SCMFSA_2: 64

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A11, A14, SCMFSA_2: 64;

            end;

          end;

        end;

          suppose ( InsCode i) = 3;

          then

          consider da,db be Int-Location such that

           A15: i = ( SubFrom (da,db)) by SCMFSA_2: 32;

          

           A16: a <> db by A2, A15, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A17: b = da;

              

              hence (( Exec (i,s1)) . b) = ((s1 . b) - (s1 . db)) by A15, SCMFSA_2: 65

              .= ((s2 . b) - (s1 . db)) by A1, A5

              .= ((s2 . b) - (s2 . db)) by A1, A16

              .= (( Exec (i,s2)) . b) by A15, A17, SCMFSA_2: 65;

            end;

              suppose

               A18: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A15, SCMFSA_2: 65

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A15, A18, SCMFSA_2: 65;

            end;

          end;

        end;

          suppose ( InsCode i) = 4;

          then

          consider da,db be Int-Location such that

           A19: i = ( MultBy (da,db)) by SCMFSA_2: 33;

          

           A20: a <> db by A2, A19, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A21: b = da;

              

              hence (( Exec (i,s1)) . b) = ((s1 . b) * (s1 . db)) by A19, SCMFSA_2: 66

              .= ((s2 . b) * (s1 . db)) by A1, A5

              .= ((s2 . b) * (s2 . db)) by A1, A20

              .= (( Exec (i,s2)) . b) by A19, A21, SCMFSA_2: 66;

            end;

              suppose

               A22: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A19, SCMFSA_2: 66

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A19, A22, SCMFSA_2: 66;

            end;

          end;

        end;

          suppose ( InsCode i) = 5;

          then

          consider da,db be Int-Location such that

           A23: i = ( Divide (da,db)) by SCMFSA_2: 34;

          

           A24: a <> db by A2, A23, SCMFSA7B:def 1;

          

           A25: a <> da by A2, A23, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A26: b = db;

              

              hence (( Exec (i,s1)) . b) = ((s1 . da) mod (s1 . db)) by A23, SCMFSA_2: 67

              .= ((s2 . da) mod (s1 . db)) by A1, A25

              .= ((s2 . da) mod (s2 . db)) by A1, A24

              .= (( Exec (i,s2)) . b) by A23, A26, SCMFSA_2: 67;

            end;

              suppose

               A27: b = da & b <> db;

              

              hence (( Exec (i,s1)) . b) = ((s1 . da) div (s1 . db)) by A23, SCMFSA_2: 67

              .= ((s1 . da) div (s2 . db)) by A1, A24

              .= ((s2 . da) div (s2 . db)) by A1, A25

              .= (( Exec (i,s2)) . b) by A23, A27, SCMFSA_2: 67;

            end;

              suppose

               A28: b <> da & b <> db;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A23, SCMFSA_2: 67

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A23, A28, SCMFSA_2: 67;

            end;

          end;

        end;

          suppose ( InsCode i) = 6;

          then

           A29: ex loc be Nat st i = ( goto loc) by SCMFSA_2: 35;

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by SCMFSA_2: 69

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A29, SCMFSA_2: 69;

        end;

          suppose ( InsCode i) = 7;

          then

           A30: ex loc be Nat, da be Int-Location st i = (da =0_goto loc) by SCMFSA_2: 36;

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by SCMFSA_2: 70

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A30, SCMFSA_2: 70;

        end;

          suppose ( InsCode i) = 8;

          then

           A31: ex loc be Nat, da be Int-Location st i = (da >0_goto loc) by SCMFSA_2: 37;

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by SCMFSA_2: 71

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A31, SCMFSA_2: 71;

        end;

          suppose ( InsCode i) = 9;

          then

          consider db,da be Int-Location, g be FinSeq-Location such that

           A32: i = (da := (g,db)) by SCMFSA_2: 38;

          

           A33: a <> db by A2, A32, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A34: b = da;

              then

              consider m2 be Nat such that

               A35: m2 = |.(s2 . db).| and

               A36: (( Exec ((da := (g,db)),s2)) . b) = ((s2 . g) /. m2) by SCMFSA_2: 72;

              consider m1 be Nat such that

               A37: m1 = |.(s1 . db).| and

               A38: (( Exec ((da := (g,db)),s1)) . b) = ((s1 . g) /. m1) by A34, SCMFSA_2: 72;

              m1 = m2 by A1, A33, A37, A35;

              hence (( Exec (i,s1)) . b) = (( Exec (i,s2)) . b) by A1, A32, A38, A36;

            end;

              suppose

               A39: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A32, SCMFSA_2: 72

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A32, A39, SCMFSA_2: 72;

            end;

          end;

        end;

          suppose ( InsCode i) = 10;

          then

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

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by SCMFSA_2: 73

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A40, SCMFSA_2: 73;

        end;

          suppose ( InsCode i) = 11;

          then

          consider da be Int-Location, g be FinSeq-Location such that

           A41: i = (da :=len g) by SCMFSA_2: 40;

          hereby

            per cases ;

              suppose

               A42: b = da;

              

              hence (( Exec (i,s1)) . b) = ( len (s1 . g)) by A41, SCMFSA_2: 74

              .= ( len (s2 . g)) by A1

              .= (( Exec (i,s2)) . b) by A41, A42, SCMFSA_2: 74;

            end;

              suppose

               A43: b <> da;

              

              hence (( Exec (i,s1)) . b) = (s1 . b) by A41, SCMFSA_2: 74

              .= (s2 . b) by A1, A5

              .= (( Exec (i,s2)) . b) by A41, A43, SCMFSA_2: 74;

            end;

          end;

        end;

          suppose ( InsCode i) = 12;

          then

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

          

          hence (( Exec (i,s1)) . b) = (s1 . b) by SCMFSA_2: 75

          .= (s2 . b) by A1, A5

          .= (( Exec (i,s2)) . b) by A44, SCMFSA_2: 75;

        end;

      end;

      assume

       A45: ( IC s1) = ( IC s2);

      now

        let f be FinSeq-Location;

        ( InsCode i) = 0 or ... or ( InsCode i) = 12 by A3;

        per cases ;

          suppose ( InsCode i) = 0 ;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by EXTPRO_1:def 3

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A46, EXTPRO_1:def 3;

        end;

          suppose ( InsCode i) = 1;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 63

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A47, SCMFSA_2: 63;

        end;

          suppose ( InsCode i) = 2;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 64

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A48, SCMFSA_2: 64;

        end;

          suppose ( InsCode i) = 3;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 65

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A49, SCMFSA_2: 65;

        end;

          suppose ( InsCode i) = 4;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 66

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A50, SCMFSA_2: 66;

        end;

          suppose ( InsCode i) = 5;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 67

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A51, SCMFSA_2: 67;

        end;

          suppose ( InsCode i) = 6;

          then

           A52: ex loc be Nat st i = ( goto loc) by SCMFSA_2: 35;

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 69

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A52, SCMFSA_2: 69;

        end;

          suppose ( InsCode i) = 7;

          then

           A53: ex loc be Nat, da be Int-Location st i = (da =0_goto loc) by SCMFSA_2: 36;

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 70

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A53, SCMFSA_2: 70;

        end;

          suppose ( InsCode i) = 8;

          then

           A54: ex loc be Nat, da be Int-Location st i = (da >0_goto loc) by SCMFSA_2: 37;

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 71

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A54, SCMFSA_2: 71;

        end;

          suppose ( InsCode i) = 9;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 72

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A55, SCMFSA_2: 72;

        end;

          suppose ( InsCode i) = 10;

          then

          consider db,da be Int-Location, g be FinSeq-Location such that

           A56: i = ((g,db) := da) by SCMFSA_2: 39;

          

           A57: a <> db by A2, A56, SCMFSA7B:def 1;

          

           A58: a <> da by A2, A56, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A59: f = g;

              

               A60: (s1 . da) = (s2 . da) by A1, A58;

              consider m2 be Nat such that

               A61: m2 = |.(s2 . db).| and

               A62: (( Exec (((g,db) := da),s2)) . g) = ((s2 . g) +* (m2,(s2 . da))) by SCMFSA_2: 73;

              consider m1 be Nat such that

               A63: m1 = |.(s1 . db).| and

               A64: (( Exec (((g,db) := da),s1)) . g) = ((s1 . g) +* (m1,(s1 . da))) by SCMFSA_2: 73;

              m1 = m2 by A1, A57, A63, A61;

              hence (( Exec (i,s1)) . f) = (( Exec (i,s2)) . f) by A1, A56, A59, A64, A62, A60;

            end;

              suppose

               A65: f <> g;

              

              hence (( Exec (i,s1)) . f) = (s1 . f) by A56, SCMFSA_2: 73

              .= (s2 . f) by A1

              .= (( Exec (i,s2)) . f) by A56, A65, SCMFSA_2: 73;

            end;

          end;

        end;

          suppose ( InsCode i) = 11;

          then

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

          

          hence (( Exec (i,s1)) . f) = (s1 . f) by SCMFSA_2: 74

          .= (s2 . f) by A1

          .= (( Exec (i,s2)) . f) by A66, SCMFSA_2: 74;

        end;

          suppose ( InsCode i) = 12;

          then

          consider da be Int-Location, g be FinSeq-Location such that

           A67: i = (g :=<0,...,0> da) by SCMFSA_2: 41;

          

           A68: a <> da by A2, A67, SCMFSA7B:def 1;

          hereby

            per cases ;

              suppose

               A69: f = g;

              

               A70: ex m2 be Nat st m2 = |.(s2 . da).| & (( Exec ((g :=<0,...,0> da),s2)) . g) = (m2 |-> 0 ) by SCMFSA_2: 75;

              ex m1 be Nat st m1 = |.(s1 . da).| & (( Exec ((g :=<0,...,0> da),s1)) . g) = (m1 |-> 0 ) by SCMFSA_2: 75;

              hence (( Exec (i,s1)) . f) = (( Exec (i,s2)) . f) by A1, A67, A68, A69, A70;

            end;

              suppose

               A71: f <> g;

              

              hence (( Exec (i,s1)) . f) = (s1 . f) by A67, SCMFSA_2: 75

              .= (s2 . f) by A1

              .= (( Exec (i,s2)) . f) by A67, A71, SCMFSA_2: 75;

            end;

          end;

        end;

      end;

      hence S[( Exec (i,s1)), ( Exec (i,s2))] by A4;

      now

        ( InsCode i) = 0 or ... or ( InsCode i) = 12 by A3;

        per cases ;

          suppose ( InsCode i) = 0 ;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = ( IC s1) by EXTPRO_1:def 3

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A72, EXTPRO_1:def 3;

        end;

          suppose ( InsCode i) = 1;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 63

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A73, SCMFSA_2: 63;

        end;

          suppose ( InsCode i) = 2;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 64

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A74, SCMFSA_2: 64;

        end;

          suppose ( InsCode i) = 3;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 65

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A75, SCMFSA_2: 65;

        end;

          suppose ( InsCode i) = 4;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 66

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A76, SCMFSA_2: 66;

        end;

          suppose ( InsCode i) = 5;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 67

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A77, SCMFSA_2: 67;

        end;

          suppose ( InsCode i) = 6;

          then

          consider loc be Nat such that

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

          

          thus (( Exec (i,s1)) . ( IC SCM+FSA )) = loc by A78, SCMFSA_2: 69

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A78, SCMFSA_2: 69;

        end;

          suppose ( InsCode i) = 7;

          then

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

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

          a <> da by A2, A79, SCMFSA7B:def 1;

          then

           A80: (s1 . da) = (s2 . da) by A1;

          hereby

            per cases ;

              suppose

               A81: (s1 . da) = 0 ;

              

              hence (( Exec (i,s1)) . ( IC SCM+FSA )) = loc by A79, SCMFSA_2: 70

              .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A79, A80, A81, SCMFSA_2: 70;

            end;

              suppose

               A82: (s1 . da) <> 0 ;

              

              hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by A79, SCMFSA_2: 70

              .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A79, A80, A82, SCMFSA_2: 70;

            end;

          end;

        end;

          suppose ( InsCode i) = 8;

          then

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

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

          a <> da by A2, A83, SCMFSA7B:def 1;

          then

           A84: (s1 . da) = (s2 . da) by A1;

          hereby

            per cases ;

              suppose

               A85: (s1 . da) > 0 ;

              

              hence (( Exec (i,s1)) . ( IC SCM+FSA )) = loc by A83, SCMFSA_2: 71

              .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A83, A84, A85, SCMFSA_2: 71;

            end;

              suppose

               A86: (s1 . da) <= 0 ;

              

              hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by A83, SCMFSA_2: 71

              .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A83, A84, A86, SCMFSA_2: 71;

            end;

          end;

        end;

          suppose ( InsCode i) = 9;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 72

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A87, SCMFSA_2: 72;

        end;

          suppose ( InsCode i) = 10;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 73

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A88, SCMFSA_2: 73;

        end;

          suppose ( InsCode i) = 11;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 74

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A89, SCMFSA_2: 74;

        end;

          suppose ( InsCode i) = 12;

          then

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

          

          hence (( Exec (i,s1)) . ( IC SCM+FSA )) = (( IC s1) + 1) by SCMFSA_2: 75

          .= (( Exec (i,s2)) . ( IC SCM+FSA )) by A45, A90, SCMFSA_2: 75;

        end;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA8B:35

    

     Th22: for s1,s2 be State of SCM+FSA , I be really-closed Program of SCM+FSA , a be Int-Location st not I refers a & (for b be Int-Location st a <> b holds (s1 . b) = (s2 . b)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) holds for k be Nat holds (for b be Int-Location st a <> b holds (( Comput ((P1 +* I),( Initialize s1),k)) . b) = (( Comput ((P2 +* I),( Initialize s2),k)) . b)) & (for f be FinSeq-Location holds (( Comput ((P1 +* I),( Initialize s1),k)) . f) = (( Comput ((P2 +* I),( Initialize s2),k)) . f)) & ( IC ( Comput ((P1 +* I),( Initialize s1),k))) = ( IC ( Comput ((P2 +* I),( Initialize s2),k))) & ( CurInstr ((P1 +* I),( Comput ((P1 +* I),( Initialize s1),k)))) = ( CurInstr ((P2 +* I),( Comput ((P2 +* I),( Initialize s2),k))))

    proof

      let s1,s2 be State of SCM+FSA ;

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

      let a be Int-Location;

      assume

       A1: not I refers a;

      set S2 = ( Initialize s2), Q2 = (P2 +* I);

      set S1 = ( Initialize s1), Q1 = (P1 +* I);

      

       A2: I c= Q1 by FUNCT_4: 25;

      

       A3: I c= Q2 by FUNCT_4: 25;

      defpred S[ State of SCM+FSA , State of SCM+FSA ] means (for b be Int-Location st a <> b holds ($1 . b) = ($2 . b)) & for f be FinSeq-Location holds ($1 . f) = ($2 . f);

      assume that

       A4: for b be Int-Location st a <> b holds (s1 . b) = (s2 . b) and

       A5: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

      

       A6: ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by MEMSTR_0: 15;

       A7:

      now

        let f be FinSeq-Location;

        

         A8: not f in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 103;

        

        hence (S1 . f) = (s1 . f) by FUNCT_4: 11

        .= (s2 . f) by A5

        .= (S2 . f) by A8, FUNCT_4: 11;

      end;

      defpred P[ Nat] means S[( Comput (Q1,S1,$1)), ( Comput (Q2,S2,$1))] & ( IC ( Comput (Q1,S1,$1))) = ( IC ( Comput (Q2,S2,$1))) & ( CurInstr (Q1,( Comput (Q1,S1,$1)))) = ( CurInstr (Q2,( Comput (Q2,S2,$1))));

      

       A9: ( IC ( Comput (Q1,S1, 0 ))) = ( IC S1)

      .= ( IC ( Start-At ( 0 , SCM+FSA ))) by A6, FUNCT_4: 13

      .= ( IC S2) by A6, FUNCT_4: 13

      .= ( IC ( Comput (Q2,S2, 0 )));

       A10:

      now

        let b be Int-Location;

        assume

         A11: a <> b;

        

         A12: not b in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

        

        hence (S1 . b) = (s1 . b) by FUNCT_4: 11

        .= (s2 . b) by A4, A11

        .= (S2 . b) by A12, FUNCT_4: 11;

      end;

      ( IC S1) = 0 by MEMSTR_0:def 11;

      then

       A13: ( IC S1) in ( dom I) by AFINSQ_1: 65;

      then

       A14: ( IC ( Comput (Q1,S1, 0 ))) in ( dom I);

      

       A15: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        

         A16: ( Comput (Q1,S1,(k + 1))) = ( Following (Q1,( Comput (Q1,S1,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (Q1,( Comput (Q1,S1,k)))),( Comput (Q1,S1,k))));

        

         A17: ( IC ( Comput (Q1,S1,k))) in ( dom I) by A2, A13, AMISTD_1: 21;

        

         A18: ( Comput (Q2,S2,(k + 1))) = ( Following (Q2,( Comput (Q2,S2,k)))) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (Q2,( Comput (Q2,S2,k)))),( Comput (Q2,S2,k))));

        

         A19: (Q1 /. ( IC ( Comput (Q1,S1,k)))) = (Q1 . ( IC ( Comput (Q1,S1,k)))) by PBOOLE: 143;

        ( CurInstr (Q1,( Comput (Q1,S1,k)))) = (I . ( IC ( Comput (Q1,S1,k)))) by A17, A19, A2, GRFUNC_1: 2;

        then ( CurInstr (Q1,( Comput (Q1,S1,k)))) in ( rng I) by A17, FUNCT_1:def 3;

        then

         A20: not ( CurInstr (Q1,( Comput (Q1,S1,k)))) refers a by A1, SCMFSA7B:def 2;

        assume

         A21: P[k];

        hence S[( Comput (Q1,S1,(k + 1))), ( Comput (Q2,S2,(k + 1)))] by A16, A18, A20, Th21;

        thus

         A22: ( IC ( Comput (Q1,S1,(k + 1)))) = ( IC ( Comput (Q2,S2,(k + 1)))) by A21, A16, A18, A20, Th21;

        

         A23: ( IC ( Comput (Q1,S1,(k + 1)))) in ( dom I) by A2, A13, AMISTD_1: 21;

        

         A24: (Q1 /. ( IC ( Comput (Q1,S1,(k + 1))))) = (Q1 . ( IC ( Comput (Q1,S1,(k + 1))))) by PBOOLE: 143;

        

         A25: (Q2 /. ( IC ( Comput (Q2,S2,(k + 1))))) = (Q2 . ( IC ( Comput (Q2,S2,(k + 1))))) by PBOOLE: 143;

        

        thus ( CurInstr (Q1,( Comput (Q1,S1,(k + 1))))) = (I . ( IC ( Comput (Q1,S1,(k + 1))))) by A23, A24, A2, GRFUNC_1: 2

        .= ( CurInstr (Q2,( Comput (Q2,S2,(k + 1))))) by A22, A23, A25, A3, GRFUNC_1: 2;

      end;

      ( CurInstr (Q1,( Comput (Q1,S1, 0 )))) = (Q1 . ( IC ( Comput (Q1,S1, 0 )))) by PBOOLE: 143

      .= (I . ( IC ( Comput (Q1,S1, 0 )))) by A14, A2, GRFUNC_1: 2

      .= (Q2 . ( IC ( Comput (Q2,S2, 0 )))) by A9, A14, A3, GRFUNC_1: 2

      .= ( CurInstr (Q2,( Comput (Q2,S2, 0 )))) by PBOOLE: 143;

      then

       A26: P[ 0 ] by A10, A7, A9;

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

      hence thesis;

    end;

    theorem :: SCMFSA8B:36

    for s be State of SCM+FSA , I be really-closed Program of SCM+FSA , l be Nat holds I is_halting_on (s,P) iff I is_halting_on ((s +* ( Start-At (l, SCM+FSA ))),(P +* I))

    proof

      let s be State of SCM+FSA ;

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

      let l be Nat;

      ( DataPart s) = ( DataPart (s +* ( Start-At (l, SCM+FSA )))) by MEMSTR_0: 79;

      hence thesis by Th1;

    end;

    theorem :: SCMFSA8B:37

    

     Th24: for s1,s2 be State of SCM+FSA , I be really-closed Program of SCM+FSA , a be Int-Location st not I refers a & (for b be Int-Location st a <> b holds (s1 . b) = (s2 . b)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) & I is_halting_on (s1,P1) holds I is_halting_on (s2,P2)

    proof

      let s1,s2 be State of SCM+FSA ;

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

      let a be Int-Location;

      assume

       A1: not I refers a;

      set S2 = ( Initialize s2), Q2 = (P2 +* I);

      set S1 = ( Initialize s1), Q1 = (P1 +* I);

      assume

       A2: for b be Int-Location st a <> b holds (s1 . b) = (s2 . b);

      assume

       A3: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

      assume that

       A4: I is_halting_on (s1,P1);

      Q1 halts_on S1 by A4, SCMFSA7B:def 7;

      then

      consider n be Nat such that

       A5: ( CurInstr (Q1,( Comput (Q1,S1,n)))) = ( halt SCM+FSA );

      ( CurInstr (Q2,( Comput (Q2,S2,n)))) = ( halt SCM+FSA ) by A1, A5, Th22, A3, A2;

      then Q2 halts_on S2 by EXTPRO_1: 29;

      hence thesis by SCMFSA7B:def 7;

    end;

    theorem :: SCMFSA8B:38

    

     Th25: for s1,s2 be State of SCM+FSA , I be really-closed Program of SCM+FSA , a be Int-Location holds (for d be read-write Int-Location st a <> d holds (s1 . d) = (s2 . d)) & (for f be FinSeq-Location holds (s1 . f) = (s2 . f)) & not I refers a & I is_halting_on (( Initialized s1),P1) implies (for d be Int-Location st a <> d holds (( IExec (I,P1,s1)) . d) = (( IExec (I,P2,s2)) . d)) & (for f be FinSeq-Location holds (( IExec (I,P1,s1)) . f) = (( IExec (I,P2,s2)) . f)) & ( IC ( IExec (I,P1,s1))) = ( IC ( IExec (I,P2,s2)))

    proof

      let s1,s2 be State of SCM+FSA ;

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

      let a be Int-Location;

      assume that

       A1: for d be read-write Int-Location st a <> d holds (s1 . d) = (s2 . d) and

       A2: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

       A3:

      now

        let d be Int-Location;

        assume

         A4: a <> d;

        per cases ;

          suppose

           A5: d = ( intloc 0 );

          

          hence (( Initialized s1) . d) = 1 by SCMFSA_M: 9

          .= (( Initialized s2) . d) by A5, SCMFSA_M: 9;

        end;

          suppose d <> ( intloc 0 );

          then

           A6: d is read-write;

          

          hence (( Initialized s1) . d) = (s1 . d) by SCMFSA_M: 37

          .= (s2 . d) by A1, A4, A6

          .= (( Initialized s2) . d) by A6, SCMFSA_M: 37;

        end;

      end;

      set S1 = ( Initialized s1), Q1 = (P1 +* I);

      set S2 = ( Initialized s2), Q2 = (P2 +* I);

      assume

       A7: not I refers a;

      

       A8: S2 = ( Initialize ( Initialized s2)) by MEMSTR_0: 44;

      assume that

       A9: I is_halting_on (( Initialized s1),P1);

       A10:

      now

        let f be FinSeq-Location;

        

        thus (( Initialized s1) . f) = (s1 . f) by SCMFSA_M: 37

        .= (s2 . f) by A2

        .= (( Initialized s2) . f) by SCMFSA_M: 37;

      end;

      then I is_halting_on (( Initialized s2),P2) by A7, A9, A3, Th24;

      then

       A11: Q2 halts_on S2 by A8, SCMFSA7B:def 7;

      

       A12: S1 = ( Initialize ( Initialized s1)) by MEMSTR_0: 44;

      then

       A13: Q1 halts_on S1 by A9, SCMFSA7B:def 7;

      now

        let l be Nat;

        assume l < ( LifeSpan (Q1,S1));

        then ( CurInstr (Q1,( Comput (Q1,S1,l)))) <> ( halt SCM+FSA ) by A13, EXTPRO_1:def 15;

        hence ( CurInstr (Q2,( Comput (Q2,S2,l)))) <> ( halt SCM+FSA ) by A7, A3, A10, A12, A8, Th22;

      end;

      then

       A14: for l be Nat st ( CurInstr (Q2,( Comput (Q2,S2,l)))) = ( halt SCM+FSA ) holds ( LifeSpan (Q1,S1)) <= l;

      ( CurInstr (Q2,( Comput (Q2,S2,( LifeSpan (Q1,S1)))))) = ( CurInstr (Q1,( Comput (Q1,S1,( LifeSpan (Q1,S1)))))) by A7, A3, A10, A12, A8, Th22

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

      then

       A15: ( LifeSpan (Q1,S1)) = ( LifeSpan (Q2,S2)) by A11, A14, EXTPRO_1:def 15;

      then

       A16: ( Result (Q2,S2)) = ( Comput (Q2,S2,( LifeSpan (Q1,S1)))) by A11, EXTPRO_1: 23;

      

       A17: ( Result (Q1,S1)) = ( Comput (Q1,S1,( LifeSpan (Q1,S1)))) by A13, EXTPRO_1: 23;

      

       A18: ( Result ((P1 +* I),( Initialized s1))) = ( IExec (I,P1,s1)) by Th20;

      

       A19: ( Result ((P2 +* I),( Initialized s2))) = ( IExec (I,P2,s2)) by Th20;

      thus for d be Int-Location st a <> d holds (( IExec (I,P1,s1)) . d) = (( IExec (I,P2,s2)) . d) by A19, A18, A7, A3, A10, A12, A8, A16, A17, Th22;

      thus for f be FinSeq-Location holds (( IExec (I,P1,s1)) . f) = (( IExec (I,P2,s2)) . f) by A19, A18, A7, A3, A10, A12, A8, A16, A17, Th22;

      

      thus ( IC ( IExec (I,P1,s1))) = ( IC ( Result (Q1,S1))) by SCMFSA6B:def 1

      .= ( IC ( Comput (Q1,S1,( LifeSpan (Q1,S1))))) by A13, EXTPRO_1: 23

      .= ( IC ( Comput (Q2,S2,( LifeSpan (Q2,S2))))) by A7, A3, A10, A12, A8, A15, Th22

      .= ( IC ( Result (Q2,S2))) by A11, EXTPRO_1: 23

      .= ( IC ( IExec (I,P2,s2))) by SCMFSA6B:def 1;

    end;

    theorem :: SCMFSA8B:39

    for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a,b be read-write Int-Location st not I refers a & not J refers a holds ( IC ( IExec (( if=0 (a,b,I,J)),P,s))) = ((( card I) + ( card J)) + 5) & ((s . a) = (s . b) implies ((for d be Int-Location st a <> d holds (( IExec (( if=0 (a,b,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if=0 (a,b,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f))) & ((s . a) <> (s . b) implies ((for d be Int-Location st a <> d holds (( IExec (( if=0 (a,b,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if=0 (a,b,I,J)),P,s)) . f) = (( IExec (J,P,s)) . f)))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a,b be read-write Int-Location;

      assume that

       A1: not I refers a and

       A2: not J refers a;

      reconsider JJ = ( if=0 (a,I,J)) as parahalting Program of SCM+FSA ;

      reconsider II = ( Macro ( SubFrom (a,b))) as keeping_0 parahalting Program of SCM+FSA ;

      set i = ( SubFrom (a,b));

      set s1 = ( Exec (i,( Initialized s)));

       A3:

      now

        let c be read-write Int-Location;

        assume a <> c;

        

        hence (s1 . c) = (( Initialized s) . c) by SCMFSA_2: 65

        .= (s . c) by SCMFSA_M: 37;

      end;

      ( IExec (( if=0 (a,b,I,J)),P,s)) = ( IncIC (( IExec (JJ,P,( IExec (II,P,s)))),( card II))) by SCMFSA6B: 20;

      

      hence ( IC ( IExec (( if=0 (a,b,I,J)),P,s))) = (( IC ( IExec (JJ,P,( IExec (II,P,s))))) + ( card II)) by FUNCT_4: 113

      .= (((( card I) + ( card J)) + 3) + ( card II)) by Th12

      .= (((( card I) + ( card J)) + 3) + 2) by COMPOS_1: 56

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

       A4:

      now

        let f be FinSeq-Location;

        

        thus (s1 . f) = (( Initialized s) . f) by SCMFSA_2: 65

        .= (s . f) by SCMFSA_M: 37;

      end;

      hereby

        assume

         A5: (s . a) = (s . b);

        

         A6: I is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

        

         A7: (( Exec (i,( Initialized s))) . a) = ((( Initialized s) . a) - (( Initialized s) . b)) by SCMFSA_2: 65

        .= ((s . a) - (( Initialized s) . b)) by SCMFSA_M: 37

        .= ((s . a) - (s . b)) by SCMFSA_M: 37

        .= 0 by A5;

        hereby

          let d be Int-Location;

          assume

           A8: a <> d;

          

          thus (( IExec (( if=0 (a,b,I,J)),P,s)) . d) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . d) by Th3

          .= (( IExec (I,P,( Exec (i,( Initialized s))))) . d) by A7, Th12

          .= (( IExec (I,P,s)) . d) by A1, A3, A4, A6, A8, Th25;

        end;

        let f be FinSeq-Location;

        

        thus (( IExec (( if=0 (a,b,I,J)),P,s)) . f) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . f) by Th4

        .= (( IExec (I,P,( Exec (i,( Initialized s))))) . f) by A7, Th12

        .= (( IExec (I,P,s)) . f) by A1, A3, A4, A6, Th25;

      end;

      

       A9: (( Exec (i,( Initialized s))) . a) = ((( Initialized s) . a) - (( Initialized s) . b)) by SCMFSA_2: 65

      .= ((s . a) - (( Initialized s) . b)) by SCMFSA_M: 37

      .= ((s . a) - (s . b)) by SCMFSA_M: 37;

      

       A10: J is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      assume (s . a) <> (s . b);

      then

       A11: ((s . a) + ( - (s . b))) <> ((s . b) + ( - (s . b)));

      hereby

        let d be Int-Location;

        assume

         A12: a <> d;

        

        thus (( IExec (( if=0 (a,b,I,J)),P,s)) . d) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . d) by Th3

        .= (( IExec (J,P,( Exec (i,( Initialized s))))) . d) by A9, A11, Th12

        .= (( IExec (J,P,s)) . d) by A2, A3, A4, A10, A12, Th25;

      end;

      let f be FinSeq-Location;

      

      thus (( IExec (( if=0 (a,b,I,J)),P,s)) . f) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . f) by Th4

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . f) by A9, A11, Th12

      .= (( IExec (J,P,s)) . f) by A2, A3, A4, A10, Th25;

    end;

    theorem :: SCMFSA8B:40

    for s be State of SCM+FSA , I,J be parahalting really-closed MacroInstruction of SCM+FSA , a,b be read-write Int-Location st not I refers a & not J refers a holds ( IC ( IExec (( if>0 (a,b,I,J)),P,s))) = ((( card I) + ( card J)) + 5) & ((s . a) > (s . b) implies (for d be Int-Location st a <> d holds (( IExec (( if>0 (a,b,I,J)),P,s)) . d) = (( IExec (I,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if>0 (a,b,I,J)),P,s)) . f) = (( IExec (I,P,s)) . f)) & ((s . a) <= (s . b) implies (for d be Int-Location st a <> d holds (( IExec (( if>0 (a,b,I,J)),P,s)) . d) = (( IExec (J,P,s)) . d)) & for f be FinSeq-Location holds (( IExec (( if>0 (a,b,I,J)),P,s)) . f) = (( IExec (J,P,s)) . f))

    proof

      let s be State of SCM+FSA ;

      let I,J be parahalting really-closed MacroInstruction of SCM+FSA ;

      let a,b be read-write Int-Location;

      assume that

       A1: not I refers a and

       A2: not J refers a;

      reconsider JJ = ( if>0 (a,I,J)) as parahalting Program of SCM+FSA ;

      reconsider II = ( Macro ( SubFrom (a,b))) as keeping_0 parahalting Program of SCM+FSA ;

      set i = ( SubFrom (a,b));

      set s1 = ( Exec (i,( Initialized s)));

       A3:

      now

        let c be read-write Int-Location;

        assume a <> c;

        

        hence (s1 . c) = (( Initialized s) . c) by SCMFSA_2: 65

        .= (s . c) by SCMFSA_M: 37;

      end;

      ( IExec (( if>0 (a,b,I,J)),P,s)) = ( IncIC (( IExec (JJ,P,( IExec (II,P,s)))),( card II))) by SCMFSA6B: 20;

      

      hence ( IC ( IExec (( if>0 (a,b,I,J)),P,s))) = (( IC ( IExec (JJ,P,( IExec (II,P,s))))) + ( card II)) by FUNCT_4: 113

      .= (((( card I) + ( card J)) + 3) + ( card II)) by Th18

      .= (((( card I) + ( card J)) + 3) + 2) by COMPOS_1: 56

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

       A4:

      now

        let f be FinSeq-Location;

        

        thus (s1 . f) = (( Initialized s) . f) by SCMFSA_2: 65

        .= (s . f) by SCMFSA_M: 37;

      end;

      hereby

        

         A5: (( Exec (i,( Initialized s))) . a) = ((( Initialized s) . a) - (( Initialized s) . b)) by SCMFSA_2: 65

        .= ((s . a) - (( Initialized s) . b)) by SCMFSA_M: 37

        .= ((s . a) - (s . b)) by SCMFSA_M: 37;

        assume (s . a) > (s . b);

        then

         A6: (( Exec (i,( Initialized s))) . a) > 0 by A5, XREAL_1: 50;

        

         A7: I is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

        hereby

          let d be Int-Location;

          assume

           A8: a <> d;

          

          thus (( IExec (( if>0 (a,b,I,J)),P,s)) . d) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . d) by Th3

          .= (( IExec (I,P,( Exec (i,( Initialized s))))) . d) by A6, Th18

          .= (( IExec (I,P,s)) . d) by A1, A3, A4, A7, A8, Th25;

        end;

        let f be FinSeq-Location;

        

        thus (( IExec (( if>0 (a,b,I,J)),P,s)) . f) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . f) by Th4

        .= (( IExec (I,P,( Exec (i,( Initialized s))))) . f) by A6, Th18

        .= (( IExec (I,P,s)) . f) by A1, A3, A4, A7, Th25;

      end;

      

       A9: (( Exec (i,( Initialized s))) . a) = ((( Initialized s) . a) - (( Initialized s) . b)) by SCMFSA_2: 65

      .= ((s . a) - (( Initialized s) . b)) by SCMFSA_M: 37

      .= ((s . a) - (s . b)) by SCMFSA_M: 37;

      

       A10: J is_halting_on (( Initialized s),P) by SCMFSA7B: 19;

      assume (s . a) <= (s . b);

      then

       A11: (( Exec (i,( Initialized s))) . a) <= 0 by A9, XREAL_1: 47;

      hereby

        let d be Int-Location;

        assume

         A12: a <> d;

        

        thus (( IExec (( if>0 (a,b,I,J)),P,s)) . d) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . d) by Th3

        .= (( IExec (J,P,( Exec (i,( Initialized s))))) . d) by A11, Th18

        .= (( IExec (J,P,s)) . d) by A2, A3, A4, A10, A12, Th25;

      end;

      let f be FinSeq-Location;

      

      thus (( IExec (( if>0 (a,b,I,J)),P,s)) . f) = (( IExec (JJ,P,( Exec (i,( Initialized s))))) . f) by Th4

      .= (( IExec (J,P,( Exec (i,( Initialized s))))) . f) by A11, Th18

      .= (( IExec (J,P,s)) . f) by A2, A3, A4, A10, Th25;

    end;

    reserve s for State of SCM+FSA ,

I for Program of SCM+FSA ,

p for Instruction-Sequence of SCM+FSA ;

    ::$Canceled

    theorem :: SCMFSA8B:42

    for I be really-closed Program of SCM+FSA st (s . ( intloc 0 )) = 1 holds I is_halting_on (s,p) iff I is_halting_on (( Initialized s),p)

    proof

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

      assume (s . ( intloc 0 )) = 1;

      then ( DataPart ( Initialized s)) = ( DataPart s) by SCMFSA_M: 19;

      hence thesis by Th1;

    end;