scmfsa_9.miz



    begin

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

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

    reserve m,n for Nat;

    ::$Canceled

    ::$Canceled

    theorem :: SCMFSA_9:18

    

     Th1: for s be State of SCM+FSA , I be MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) <> 0 holds ( while=0 (a,I)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

      let I be MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      assume

       A1: (s . a) <> 0 ;

      set i = (a =0_goto 3);

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      

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

      

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

      .= 0 by FUNCOP_1: 72;

      set loc5 = (( card I) + 4);

      set s5 = ( Comput (P1,s1,3));

      set s4 = ( Comput (P1,s1,2));

      set s2 = ( Comput (P1,s1,1));

      

       A4: 1 in ( dom ( while=0 (a,I))) by SCMFSA_X: 5;

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

      then

       A5: (s1 . a) = (s . a) by FUNCT_4: 11;

      

       A6: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

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

      

      then (P1 . 0 ) = (( while=0 (a,I)) . 0 ) by FUNCT_4: 13

      .= i by SCMFSA_X: 10;

      then

       A7: ( CurInstr (P1,s1)) = i by A3, A6;

      

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

      .= ( Exec (i,s1)) by A7;

      

       A9: ( IC ( Comput (P1,s1,1))) = ( 0 + 1) by A1, A3, A8, A5, SCMFSA_2: 70;

      

       A10: (P1 /. ( IC ( Comput (P1,s1,1)))) = (P1 . ( IC ( Comput (P1,s1,1)))) by PBOOLE: 143;

      (P1 . 1) = (( while=0 (a,I)) . 1) by A4, FUNCT_4: 13

      .= ( goto 2) by SCMFSA_X: 10;

      then

       A11: ( CurInstr (P1,( Comput (P1,s1,1)))) = ( goto 2) by A9, A10;

      

       A12: ( Comput (P1,s1,(1 + 1))) = ( Following (P1,s2)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s2)) by A11;

      

       A13: ( IC s4) = 2 by A12, SCMFSA_2: 69;

      

       A14: 2 in ( dom ( while=0 (a,I))) by SCMFSA_X: 5;

      

       A15: loc5 in ( dom ( while=0 (a,I))) by SCMFSA_X: 6;

      

       A16: (P1 /. ( IC s4)) = (P1 . ( IC s4)) by PBOOLE: 143;

      (P1 . 2) = (( while=0 (a,I)) . 2) by A14, FUNCT_4: 13

      .= ( goto loc5) by SCMFSA_X: 12;

      then

       A17: ( CurInstr (P1,s4)) = ( goto loc5) by A13, A16;

      

       A18: ( Comput (P1,s1,(2 + 1))) = ( Following (P1,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto loc5),s4)) by A17;

      

       A19: ( IC s5) = loc5 by A18, SCMFSA_2: 69;

      

       A20: (P1 /. ( IC s5)) = (P1 . ( IC s5)) by PBOOLE: 143;

      (P1 . loc5) = (( while=0 (a,I)) . loc5) by A15, FUNCT_4: 13

      .= ( halt SCM+FSA ) by SCMFSA_X: 11;

      then ( CurInstr (P1,s5)) = ( halt SCM+FSA ) by A19, A20;

      then P1 halts_on s1 by EXTPRO_1: 29;

      hence ( while=0 (a,I)) is_halting_on (s,P) by SCMFSA7B:def 7;

      thus thesis;

    end;

    theorem :: SCMFSA_9:19

    

     Th2: for a be Int-Location, I be really-closed MacroInstruction of SCM+FSA , s be State of SCM+FSA , k be Nat st I is_halting_on (s,P) & k < ( LifeSpan ((P +* I),( Initialize s))) & ( IC ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(1 + k)))) = (( IC ( Comput ((P +* I),( Initialize s),k))) + 3) & ( DataPart ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(1 + k)))) = ( DataPart ( Comput ((P +* I),( Initialize s),k))) holds ( IC ( Comput ((P +* ( while=0 (a,I))),( Initialize s),((1 + k) + 1)))) = (( IC ( Comput ((P +* I),( Initialize s),(k + 1)))) + 3) & ( DataPart ( Comput ((P +* ( while=0 (a,I))),( Initialize s),((1 + k) + 1)))) = ( DataPart ( Comput ((P +* I),( Initialize s),(k + 1))))

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      set D = ( Int-Locations \/ FinSeq-Locations );

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

      let s be State of SCM+FSA ;

      let k be Nat;

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      set sI = ( Initialize s), PI = (P +* I);

      

       A1: I c= PI by FUNCT_4: 25;

      set sK1 = ( Comput (P1,s1,(1 + k)));

      set sK2 = ( Comput (PI,sI,k));

      set l3 = ( IC ( Comput (PI,sI,k)));

      set I1 = (I ';' ( goto 0 ));

      set i = (a =0_goto 3);

      reconsider n = l3 as Element of NAT ;

      set Mi = (i ";" ( Goto (( card I1) + 1)));

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

      

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

      

       A3: I c= PI by FUNCT_4: 25;

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

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

      then

       A4: n in ( dom I) by AMISTD_1: 21, A3;

      then n < ( card I) by AFINSQ_1: 66;

      then

       A5: (n + 3) < (( card I) + 5) by XREAL_1: 8;

      

       A6: (PI /. ( IC sK2)) = (PI . ( IC sK2)) by PBOOLE: 143;

      

       A7: ( CurInstr (PI,sK2)) = (I . n) by A4, A1, GRFUNC_1: 2, A6;

      assume I is_halting_on (s,P);

      then

       A8: PI halts_on sI by SCMFSA7B:def 7;

      assume k < ( LifeSpan (PI,sI));

      then (I . n) <> ( halt SCM+FSA ) by A7, A8, EXTPRO_1:def 15;

      then

       A9: n <> ( LastLoc I) by COMPOS_1:def 14;

      n <= ( LastLoc I) by A4, VALUED_1: 32;

      then

       A10: n < ( LastLoc I) by A9, XXREAL_0: 1;

      then

       A11: n in ( dom ( CutLastLoc I)) by COMPOS_2: 26;

      ( dom I) c= ( dom I1) by COMPOS_1: 21;

      then

       A12: n in ( dom I1) by A4;

      ( dom I1) = (( dom ( CutLastLoc I)) \/ ( dom ( Reloc (( Macro ( goto 0 )),(( card I) -' 1))))) by FUNCT_4:def 1;

      then

       A13: ( dom ( CutLastLoc I)) c= ( dom I1) by XBOOLE_1: 7;

      

       A14: ( dom ( CutLastLoc I)) misses ( dom ( Reloc (( Macro ( goto 0 )),(( card I) -' 1)))) by COMPOS_1: 18;

      

       A15: n in ( dom I1) by A11, A13;

      ( dom I) c= ( dom I1) by COMPOS_1: 21;

      then ( LastLoc I) <= ( LastLoc I1) by VALUED_1: 68;

      then n < ( LastLoc I1) by A10, XXREAL_0: 2;

      then

       A16: (I1 . n) <> ( halt SCM+FSA ) by A15, COMPOS_1:def 15;

      ( dom I1) c= ( dom J2) by SCMFSA6A: 17;

      then

       A17: n in ( dom J2) by A12;

      then (n + 3) in { (il + 3) where il be Nat : il in ( dom J2) };

      then

       A18: (n + 3) in ( dom ( Shift (J2,3))) by VALUED_1:def 12;

      

      then

       A19: (( Shift (J2,3)) /. (n + 3)) = (( Shift (J2,3)) . (n + 3)) by PARTFUN1:def 6

      .= (J2 . n) by A17, VALUED_1:def 12

      .= (I1 . n) by A16, A15, SCMFSA6A: 15

      .= (( CutLastLoc I) . n) by A11, FUNCT_4: 16, A14

      .= (I . n) by A10, COMPOS_2: 27;

      ( card ( while=0 (a,I))) = (( card I) + 5) by SCMFSA_X: 3;

      then

       A20: (n + 3) in ( dom ( while=0 (a,I))) by A5, AFINSQ_1: 66;

      (I . n) in ( rng I) by A4, FUNCT_1:def 3;

      then

      reconsider j = (I . n) as Instruction of SCM+FSA by A2;

      

       A21: ( card Mi) = (( card ( Macro i)) + ( card ( Goto (( card I1) + 1)))) by SCMFSA6A: 21

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

      .= (2 + 1) by COMPOS_1: 56

      .= 3;

      then (n + 3) >= ( card Mi) by NAT_1: 11;

      then

       A22: not (n + 3) in ( dom Mi) by AFINSQ_1: 66;

      

       A23: ( Comput (PI,sI,(k + 1))) = ( Following (PI,sK2)) by EXTPRO_1: 3

      .= ( Exec (j,sK2)) by A7;

      assume

       A24: ( IC ( Comput (P1,s1,(1 + k)))) = (l3 + 3);

      (n + 3) < (( LastLoc I) + 3) by A10, XREAL_1: 6;

      then

       A25: (n + 3) <> ((( card I) - 1) + 3) by AFINSQ_1: 91;

      ( dom ( while=0 (a,I))) = ( dom ( if=0 (a,I1))) by FUNCT_7: 30;

      then

       A26: (n + 3) in ( dom ( if=0 (a,I1))) by A20;

      

       A27: ( if=0 (a,I1)) = (Mi ";" J2) by SCMFSA6A: 25;

      then ( dom ( if=0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J2,3)))) by SCMFSA6A: 39, A21;

      then

       A28: (n + 3) in ( dom ( Reloc (J2,3))) by A26, A22, XBOOLE_0:def 3;

      

       A29: (P1 /. ( IC sK1)) = (P1 . ( IC sK1)) by PBOOLE: 143;

      

       A30: ( Reloc (J2,3)) = ( IncAddr (( Shift (J2,3)),3)) by COMPOS_1: 34;

      (P1 . (n + 3)) = (( while=0 (a,I)) . (n + 3)) by A20, FUNCT_4: 13

      .= ((Mi ";" J2) . (n + 3)) by A27, FUNCT_7: 32, A25

      .= (( Reloc (J2,3)) . (n + 3)) by A28, SCMFSA6A: 40, A21

      .= ( IncAddr (j,3)) by A18, A19, A30, COMPOS_1:def 21;

      then

       A31: ( CurInstr (P1,sK1)) = ( IncAddr (j,3)) by A24, A29;

      assume

       A32: ( DataPart sK1) = ( DataPart sK2);

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

      .= ( Exec (( IncAddr (j,3)),sK1)) by A31;

      hence thesis by A24, A32, A23, SCMFSA6A: 8;

    end;

    theorem :: SCMFSA_9:20

    

     Th3: for a be Int-Location, I be really-closed MacroInstruction of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) & ( IC ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(1 + ( LifeSpan ((P +* I),( Initialize s))))))) = (( IC ( Comput ((P +* I),( Initialize s),( LifeSpan ((P +* I),( Initialize s)))))) + 3) holds ( CurInstr ((P +* ( while=0 (a,I))),( Comput ((P +* ( while=0 (a,I))),( Initialize s),(1 + ( LifeSpan ((P +* I),( Initialize s)))))))) = ( goto 0 )

    proof

      set J3 = (( Goto 0 ) ";" ( Stop SCM+FSA ));

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

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

      let s be State of SCM+FSA ;

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      set sI = ( Initialize s), PI = (P +* I);

      

       A1: I c= PI by FUNCT_4: 25;

      set life = ( LifeSpan ((P +* I),( Initialize s)));

      set sK1 = ( Comput (P1,s1,(1 + life)));

      set sK2 = ( Comput (PI,sI,life));

      set I1 = (I ';' ( goto 0 ));

      set i = (a =0_goto 3);

      reconsider n = ( IC sK2) as Element of NAT ;

      set Mi = (i ";" ( Goto (( card I1) + 1)));

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

      

       A2: I c= PI by FUNCT_4: 25;

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

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

      then

       A3: n in ( dom I) by AMISTD_1: 21, A2;

      then n < ( card I) by AFINSQ_1: 66;

      then

       A4: (n + 3) < (( card I) + 5) by XREAL_1: 8;

      assume I is_halting_on (s,P);

      then

       A5: PI halts_on sI by SCMFSA7B:def 7;

      

       A6: (PI /. ( IC sK2)) = (PI . ( IC sK2)) by PBOOLE: 143;

      

       A7: (P1 /. ( IC sK1)) = (P1 . ( IC sK1)) by PBOOLE: 143;

      assume

       A8: ( IC sK1) = (( IC sK2) + 3);

      ( CurInstr (PI,sK2)) = (I . n) by A3, A1, GRFUNC_1: 2, A6;

      then

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

      ( IC sK2) = ( LastLoc I) by A3, A9, COMPOS_1:def 15

      .= (( card I) - 1) by AFINSQ_1: 91;

      then

       A10: (( IC sK2) + 3) = (( card I) + 2);

      ( card ( while=0 (a,I))) = (( card I) + 5) by SCMFSA_X: 3;

      then

       A11: (n + 3) in ( dom ( while=0 (a,I))) by A4, AFINSQ_1: 66;

      

       A12: (n + 3) in ( dom ( if=0 (a,I1))) by A11, FUNCT_7: 30;

      (P1 . (n + 3)) = (( while=0 (a,I)) . (n + 3)) by FUNCT_4: 13, A11

      .= (( while=0 (a,I)) . (( card I) + 2)) by A10

      .= ( goto 0 ) by FUNCT_7: 31, A10, A12;

      hence thesis by A8, A7;

    end;

    reserve f for FinSeq-Location,

c for Int-Location;

    ::$Canceled

    theorem :: SCMFSA_9:22

    

     Th4: for s be State of SCM+FSA , I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st I is_halting_on (s,P) & (s . a) = 0 holds ( IC ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 2)))) = 0 & for k be Nat st k <= (( LifeSpan ((P +* I),( Initialize s))) + 2) holds ( IC ( Comput ((P +* ( while=0 (a,I))),( Initialize s),k))) in ( dom ( while=0 (a,I)))

    proof

      set D = ( Int-Locations \/ FinSeq-Locations );

      let s be State of SCM+FSA ;

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

      let a be read-write Int-Location;

      set sI = ( Initialize s), PI = (P +* I);

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      defpred P[ Nat] means $1 <= ( LifeSpan (PI,sI)) implies ( IC ( Comput (P1,s1,(1 + $1)))) = (( IC ( Comput (PI,sI,$1))) + 3) & ( DataPart ( Comput (P1,s1,(1 + $1)))) = ( DataPart ( Comput (PI,sI,$1)));

      assume

       A1: I is_halting_on (s,P);

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        now

          

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

          assume (k + 1) <= ( LifeSpan (PI,sI));

          then k < ( LifeSpan (PI,sI)) by A4, XXREAL_0: 2;

          hence ( IC ( Comput (P1,s1,((1 + k) + 1)))) = (( IC ( Comput (PI,sI,(k + 1)))) + 3) & ( DataPart ( Comput (P1,s1,((1 + k) + 1)))) = ( DataPart ( Comput (PI,sI,(k + 1)))) by A1, A3, Th2;

        end;

        hence P[(k + 1)];

      end;

      reconsider l = ( LifeSpan (PI,sI)) as Element of NAT by ORDINAL1:def 12;

      set loc4 = (( card I) + 3);

      set i = (a =0_goto 3);

      set s2 = ( Comput (P1,s1,1));

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

      

      then

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

      .= 0 by FUNCOP_1: 72;

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

      then

       A6: (s1 . a) = (s . a) by FUNCT_4: 11;

      assume

       A7: (s . a) = 0 ;

      

       A8: 0 in ( dom ( while=0 (a,I))) by AFINSQ_1: 65;

      

       A9: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

      (P1 . 0 ) = (( while=0 (a,I)) . 0 ) by A8, FUNCT_4: 13

      .= i by SCMFSA_X: 10;

      then

       A10: ( CurInstr (P1,s1)) = i by A5, A9;

      

       A11: ( Comput (P1,s1,( 0 + 1))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

      .= ( Exec (i,s1)) by A10;

      then (for c holds (s2 . c) = (s1 . c)) & for f holds (s2 . f) = (s1 . f) by SCMFSA_2: 70;

      then

       A12: ( DataPart s2) = ( DataPart sI) by SCMFSA_M: 2;

      

       A13: ( IC s2) = 3 by A7, A11, A6, SCMFSA_2: 70;

      

       A14: P[ 0 ]

      proof

        assume 0 <= ( LifeSpan (PI,sI));

        

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

        ( IC ( Comput (PI,sI, 0 ))) = ( IC ( Start-At ( 0 , SCM+FSA ))) by A15, FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        hence thesis by A13, A12;

      end;

      

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

      set s4 = ( Comput (P1,s1,((1 + ( LifeSpan (PI,sI))) + 1)));

      set s3 = ( Comput (P1,s1,(1 + ( LifeSpan (PI,sI)))));

      set s2 = ( Comput (P1,s1,(1 + ( LifeSpan (PI,sI)))));

       P[l] by A16;

      then

       A17: ( CurInstr (P1,s2)) = ( goto 0 ) by A1, Th3;

      

       A18: ( CurInstr (P1,s3)) = ( goto 0 ) by A17;

      

       A19: s4 = ( Following (P1,s3)) by EXTPRO_1: 3

      .= ( Exec (( goto 0 ),s3)) by A18;

      

       A20: ( IC s4) = 0 by A19, SCMFSA_2: 69;

      hence ( IC ( Comput (P1,s1,(( LifeSpan (PI,sI)) + 2)))) = 0 ;

       A21:

      now

        let k be Nat;

        assume

         A22: k <= (( LifeSpan (PI,sI)) + 2);

        assume k <> 0 ;

        then

        consider n be Nat such that

         A23: k = (n + 1) by NAT_1: 6;

        k <= (( LifeSpan (PI,sI)) + 1) or k >= ((( LifeSpan (PI,sI)) + 1) + 1) by NAT_1: 13;

        then

         A24: k <= (( LifeSpan (PI,sI)) + 1) or k = (( LifeSpan (PI,sI)) + 2) by A22, XXREAL_0: 1;

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

        per cases by A24;

          suppose k <= (( LifeSpan (PI,sI)) + 1);

          then n <= ( LifeSpan (PI,sI)) by A23, XREAL_1: 6;

          then

           A25: ( IC ( Comput (P1,s1,(1 + n)))) = (( IC ( Comput (PI,sI,n))) + 3) by A16;

          reconsider m = ( IC ( Comput (PI,sI,n))) as Element of NAT ;

          

           A26: I c= PI by FUNCT_4: 25;

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

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

          then m in ( dom I) by AMISTD_1: 21, A26;

          then m < ( card I) by AFINSQ_1: 66;

          then

           A27: (m + 3) < (( card I) + 5) by XREAL_1: 8;

          ( card ( while=0 (a,I))) = (( card I) + 5) by SCMFSA_X: 3;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while=0 (a,I))) by A23, A25, A27, AFINSQ_1: 66;

        end;

          suppose k >= (( LifeSpan (PI,sI)) + 2);

          then k = (( LifeSpan (PI,sI)) + 2) by A22, XXREAL_0: 1;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while=0 (a,I))) by A20, AFINSQ_1: 65;

        end;

      end;

      now

        let k be Nat;

        assume

         A28: k <= (( LifeSpan (PI,sI)) + 2);

        per cases ;

          suppose k = 0 ;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while=0 (a,I))) by A8, A5;

        end;

          suppose k <> 0 ;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while=0 (a,I))) by A21, A28;

        end;

      end;

      hence thesis;

    end;

    reserve s for State of SCM+FSA ,

I for MacroInstruction of SCM+FSA ,

a for read-write Int-Location;

    definition

      let s, I, a, P;

      deffunc U( Nat, State of SCM+FSA ) = ( Comput ((P +* ( while=0 (a,I))),( Initialize $2),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize $2))) + 2)));

      deffunc V( Nat, State of SCM+FSA ) = ( down U($1,$2));

      :: SCMFSA_9:def1

      func StepWhile=0 (a,I,P,s) -> sequence of ( product ( the_Values_of SCM+FSA )) means

      : Def1: (it . 0 ) = s & for i be Nat holds (it . (i + 1)) = ( Comput ((P +* ( while=0 (a,I))),( Initialize (it . i)),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize (it . i)))) + 2)));

      existence

      proof

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

        consider f be sequence of ( product ( the_Values_of SCM+FSA )) such that

         A1: (f . 0 ) = ss and

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

        take f;

        thus (f . 0 ) = s by A1;

        let i be Nat;

        (f . (i + 1)) = V(i,.) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be sequence of ( product ( the_Values_of SCM+FSA )) such that

         A3: (F1 . 0 ) = s and

         A4: for i be Nat holds (F1 . (i + 1)) = U(i,.) and

         A5: (F2 . 0 ) = s and

         A6: for i be Nat holds (F2 . (i + 1)) = U(i,.);

        reconsider s as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A7: (F1 . 0 ) = s by A3;

        

         A8: for i be Nat holds (F1 . (i + 1)) = V(i,.) by A4;

        

         A9: (F2 . 0 ) = s by A5;

        

         A10: for i be Nat holds (F2 . (i + 1)) = V(i,.) by A6;

        thus F1 = F2 from NAT_1:sch 16( A7, A8, A9, A10);

      end;

    end

    reserve i,k,m,n for Nat;

    theorem :: SCMFSA_9:23

    

     Th5: (( StepWhile=0 (a,I,P,s)) . (k + 1)) = (( StepWhile=0 (a,I,P,(( StepWhile=0 (a,I,P,s)) . k))) . 1)

    proof

      set sk = (( StepWhile=0 (a,I,P,s)) . k);

      set sk0 = (( StepWhile=0 (a,I,P,sk)) . 0 );

      sk0 = sk by Def1;

      

      hence (( StepWhile=0 (a,I,P,s)) . (k + 1)) = ( Comput ((P +* ( while=0 (a,I))),( Initialize sk0),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize sk0))) + 2))) by Def1

      .= (( StepWhile=0 (a,I,P,sk)) . ( 0 + 1)) by Def1

      .= (( StepWhile=0 (a,I,P,sk)) . 1);

    end;

    ::$Canceled

    theorem :: SCMFSA_9:25

    

     Th6: for I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA holds (( StepWhile=0 (a,I,P,s)) . 1) = ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize s))) + 2)))

    proof

      let I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      

       A1: (( StepWhile=0 (a,I,P,s)) . 0 ) = s by Def1;

      

      thus (( StepWhile=0 (a,I,P,s)) . 1) = (( StepWhile=0 (a,I,P,s)) . ( 0 + 1))

      .= ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize s))) + 2))) by A1, Def1;

    end;

    theorem :: SCMFSA_9:26

    

     Th7: for I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA , k,n be Nat st ( IC (( StepWhile=0 (a,I,P,s)) . k)) = 0 & (( StepWhile=0 (a,I,P,s)) . k) = ( Comput ((P +* ( while=0 (a,I))),( Initialize s),n)) holds (( StepWhile=0 (a,I,P,s)) . k) = ( Initialize (( StepWhile=0 (a,I,P,s)) . k)) & (( StepWhile=0 (a,I,P,s)) . (k + 1)) = ( Comput ((P +* ( while=0 (a,I))),( Initialize s),(n + (( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize (( StepWhile=0 (a,I,P,s)) . k)))) + 2))))

    proof

      set D = ( Int-Locations \/ FinSeq-Locations );

      let I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA , k,n be Nat;

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      set sk = (( StepWhile=0 (a,I,P,s)) . k);

      set s2 = ( Initialize sk);

      assume

       A1: ( IC sk) = 0 ;

      assume

       A2: sk = ( Comput (P1,s1,n));

      sk is 0 -started by A1;

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

      hence s2 = sk by FUNCT_4: 98;

      

      hence (( StepWhile=0 (a,I,P,s)) . (k + 1)) = ( Comput (P1,sk,(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize sk))) + 2))) by Def1

      .= ( Comput (P1,s1,(n + (( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize sk))) + 2)))) by A2, EXTPRO_1: 4;

    end;

    theorem :: SCMFSA_9:27

    

     Th8: for I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA st (for k be Nat holds I is_halting_on ((( StepWhile=0 (a,I,P,s)) . k),(P +* ( while=0 (a,I))))) & ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st for k be Nat holds (((f . (( StepWhile=0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile=0 (a,I,P,s)) . k)) or (f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile=0 (a,I,P,s)) . k) . a) <> 0 )) holds ( while=0 (a,I)) is_halting_on (s,P)

    proof

      let I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      assume

       A1: for k be Nat holds I is_halting_on ((( StepWhile=0 (a,I,P,s)) . k),(P +* ( while=0 (a,I))));

      set s1 = ( Initialize s), P1 = (P +* ( while=0 (a,I)));

      

       A2: (P1 +* ( while=0 (a,I))) = P1;

      given f be Function of ( product ( the_Values_of SCM+FSA )), NAT such that

       A3: for k be Nat holds ((f . (( StepWhile=0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile=0 (a,I,P,s)) . k)) or (f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile=0 (a,I,P,s)) . k) . a) <> 0 );

      deffunc F( Nat) = (f . (( StepWhile=0 (a,I,P,s)) . $1));

      

       A4: for k be Nat holds ( F(+) < F(k) or F(k) = 0 ) by A3;

      consider m be Nat such that

       A5: F(m) = 0 and

       A6: for n be Nat st F(n) = 0 holds m <= n from NAT_1:sch 17( A4);

      defpred P[ Nat] means ($1 + 1) <= m implies ex k st (( StepWhile=0 (a,I,P,s)) . ($1 + 1)) = ( Comput (P1,s1,k));

       A7:

      now

        let k be Nat;

        assume

         A8: P[k];

        now

          set sk1 = (( StepWhile=0 (a,I,P,s)) . (k + 1));

          set sk = (( StepWhile=0 (a,I,P,s)) . k);

          assume

           A9: ((k + 1) + 1) <= m;

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

          then k < m by A9, XXREAL_0: 2;

          then F(k) <> 0 by A6;

          then

           A10: (sk . a) = 0 by A3;

          

           A11: I is_halting_on (sk,(P +* ( while=0 (a,I)))) by A1;

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

          then

          consider n be Nat such that

           A12: sk1 = ( Comput (P1,s1,n)) by A8, A9, XXREAL_0: 2;

          take m = (n + (( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize sk1))) + 2));

          

           A13: ((P +* ( while=0 (a,I))) +* ( while=0 (a,I))) = (P +* ( while=0 (a,I)));

          sk1 = ( Comput ((P +* ( while=0 (a,I))),( Initialize sk),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize sk))) + 2))) by Def1;

          then ( IC sk1) = 0 by A11, A10, Th4, A13;

          hence (( StepWhile=0 (a,I,P,s)) . ((k + 1) + 1)) = ( Comput (P1,s1,m)) by A12, Th7;

        end;

        hence P[(k + 1)];

      end;

      

       A14: P[ 0 ]

      proof

        assume ( 0 + 1) <= m;

        take n = (( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize s))) + 2);

        thus thesis by Th6;

      end;

      

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

      now

        per cases ;

          suppose m = 0 ;

          then ((( StepWhile=0 (a,I,P,s)) . 0 ) . a) <> 0 by A3, A5;

          then (s . a) <> 0 by Def1;

          hence thesis by Th1;

        end;

          suppose m <> 0 ;

          then

          consider i be Nat such that

           A16: m = (i + 1) by NAT_1: 6;

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

          set sm = (( StepWhile=0 (a,I,P,s)) . m);

          set si = (( StepWhile=0 (a,I,P,s)) . i);

          i < m by A16, NAT_1: 13;

          then F(i) <> 0 by A6;

          then

           A17: (si . a) = 0 by A3;

          

           A18: I is_halting_on (si,(P +* ( while=0 (a,I)))) by A1;

          sm = ( Comput ((P +* ( while=0 (a,I))),( Initialize si),(( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize si))) + 2))) by A16, Def1;

          then sm is 0 -started by A18, A17, Th4, A2;

          then

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

          set p = (( LifeSpan (((P +* ( while=0 (a,I))) +* I),( Initialize s))) + 3);

          set sm1 = ( Initialize sm);

          consider n be Nat such that

           A20: sm = ( Comput (P1,s1,n)) by A15, A16;

          

           A21: sm1 = sm by A19, FUNCT_4: 98;

          (sm . a) <> 0 by A3, A5;

          then ( while=0 (a,I)) is_halting_on (sm,P) by Th1;

          then (P +* ( while=0 (a,I))) halts_on ( Initialize sm) by SCMFSA7B:def 7;

          then (P +* ( while=0 (a,I))) halts_on ( Initialize sm);

          then P1 halts_on sm1;

          then

          consider j be Nat such that

           A22: ( CurInstr (P1,( Comput (P1,sm,j)))) = ( halt SCM+FSA ) by A21;

          

           A23: ( Comput (P1,s1,(n + j))) = ( Comput (P1,( Comput (P1,s1,n)),j)) by EXTPRO_1: 4;

          ( CurInstr (P1,( Comput (P1,s1,(n + j))))) = ( halt SCM+FSA ) by A20, A22, A23;

          then P1 halts_on s1 by EXTPRO_1: 29;

          hence ( while=0 (a,I)) is_halting_on (s,P) by SCMFSA7B:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA_9:28

    

     Th9: for I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA st ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st for k be Nat holds ((f . (( StepWhile=0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile=0 (a,I,P,s)) . k)) or (f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile=0 (a,I,P,s)) . k) . a) <> 0 ) holds ( while=0 (a,I)) is_halting_on (s,P)

    proof

      let I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      

       A1: for k be Nat holds I is_halting_on ((( StepWhile=0 (a,I,P,s)) . k),(P +* ( while=0 (a,I)))) by SCMFSA7B: 19;

      assume ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st for k be Nat holds ((f . (( StepWhile=0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile=0 (a,I,P,s)) . k)) or (f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile=0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile=0 (a,I,P,s)) . k) . a) <> 0 );

      hence thesis by A1, Th8;

    end;

    theorem :: SCMFSA_9:29

    for I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st (for s be State of SCM+FSA , P holds ((f . (( StepWhile=0 (a,I,P,s)) . 1)) < (f . s) or (f . s) = 0 ) & ((f . s) = 0 iff (s . a) <> 0 )) holds ( while=0 (a,I)) is parahalting

    proof

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

      given f be Function of ( product ( the_Values_of SCM+FSA )), NAT such that

       A1: for s be State of SCM+FSA , P holds ((f . (( StepWhile=0 (a,I,P,s)) . 1)) < (f . s) or (f . s) = 0 ) & ((f . s) = 0 iff (s . a) <> 0 );

      now

        let t be State of SCM+FSA ;

        let Q;

        now

          let k be Nat;

          (f . (( StepWhile=0 (a,I,Q,(( StepWhile=0 (a,I,Q,t)) . k))) . 1)) < (f . (( StepWhile=0 (a,I,Q,t)) . k)) or (f . (( StepWhile=0 (a,I,Q,t)) . k)) = 0 by A1;

          hence ((f . (( StepWhile=0 (a,I,Q,t)) . (k + 1))) < (f . (( StepWhile=0 (a,I,Q,t)) . k)) or (f . (( StepWhile=0 (a,I,Q,t)) . k)) = 0 ) & ((f . (( StepWhile=0 (a,I,Q,t)) . k)) = 0 iff ((( StepWhile=0 (a,I,Q,t)) . k) . a) <> 0 ) by A1, Th5;

        end;

        hence ( while=0 (a,I)) is_halting_on (t,Q) by Th9;

      end;

      hence thesis by SCMFSA7B: 19;

    end;

    ::$Canceled

    theorem :: SCMFSA_9:31

    

     Th11: for i be Instruction of SCM+FSA st not i destroys ( intloc 0 ) holds ( Macro i) is good

    proof

      let i be Instruction of SCM+FSA ;

      set I = ( Macro i);

      

       A1: ( rng I) = {i, ( halt SCM+FSA )} by COMPOS_1: 67;

      assume

       A2: not i destroys ( intloc 0 );

      now

        let x be Instruction of SCM+FSA ;

        assume

         A3: x in ( rng I);

        per cases by A1, A3, TARSKI:def 2;

          suppose x = i;

          hence not x destroys ( intloc 0 ) by A2;

        end;

          suppose x = ( halt SCM+FSA );

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

        end;

      end;

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

      hence thesis by SCMFSA7B:def 5;

    end;

    registration

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

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

      correctness

      proof

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

        reconsider Mi = ( Macro i) as good Program of SCM+FSA by Th11, SCMFSA7B: 12;

        ( if=0 (a,I,J)) = ((((Mi ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

        hence thesis;

      end;

    end

    registration

      let I be good MacroInstruction of SCM+FSA , a be Int-Location;

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

      correctness

      proof

        set i = (a =0_goto 3);

        reconsider Mi = ( Macro i) as good Program of SCM+FSA by Th11, SCMFSA7B: 12;

        ( if=0 (a,I)) = (((Mi ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

        hence thesis;

      end;

    end

    registration

      let I be good MacroInstruction of SCM+FSA , a be Int-Location;

      cluster ( while=0 (a,I)) -> good;

      correctness

      proof

        

         A1: not ( goto 0 ) destroys ( intloc 0 ) by SCMFSA7B: 11;

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

        then not ( if=0 (a,(I ';' ( goto 0 )))) destroys ( intloc 0 ) by SCMFSA8C: 99;

        then not ( while=0 (a,I)) destroys ( intloc 0 ) by SCMFSA8A: 42, A1;

        hence thesis by SCMFSA7B:def 5;

      end;

    end

    ::$Canceled

    theorem :: SCMFSA_9:38

    

     Th12: for s be State of SCM+FSA , I be MacroInstruction of SCM+FSA , a be read-write Int-Location st (s . a) <= 0 holds ( while>0 (a,I)) is_halting_on (s,P)

    proof

      let s be State of SCM+FSA ;

      let I be MacroInstruction of SCM+FSA ;

      let a be read-write Int-Location;

      assume

       A1: (s . a) <= 0 ;

      set i = (a >0_goto 3);

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

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

      then

       A2: ( IC SCM+FSA ) in ( dom ( Start-At ( 0 , SCM+FSA )));

      

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

      .= 0 by FUNCOP_1: 72;

      set loc5 = (( card I) + 4);

      set s5 = ( Comput (P1,s1,3));

      set s4 = ( Comput (P1,s1,2));

      set s2 = ( Comput (P1,s1,1));

      

       A4: 1 in ( dom ( while>0 (a,I))) by SCMFSA_X: 9;

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

      then

       A5: (s1 . a) = (s . a) by FUNCT_4: 11;

      

       A6: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

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

      

      then (P1 . 0 ) = (( while>0 (a,I)) . 0 ) by FUNCT_4: 13

      .= i by SCMFSA_X: 10;

      then

       A7: ( CurInstr (P1,s1)) = i by A3, A6;

      

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

      .= ( Exec (i,s1)) by A7;

      

       A9: ( IC ( Comput (P1,s1,1))) = ( 0 + 1) by A1, A3, A8, A5, SCMFSA_2: 71;

      

       A10: (P1 /. ( IC ( Comput (P1,s1,1)))) = (P1 . ( IC ( Comput (P1,s1,1)))) by PBOOLE: 143;

      (P1 . 1) = (( while>0 (a,I)) . 1) by A4, FUNCT_4: 13

      .= ( goto 2) by SCMFSA_X: 10;

      then

       A11: ( CurInstr (P1,( Comput (P1,s1,1)))) = ( goto 2) by A9, A10;

      

       A12: ( Comput (P1,s1,(1 + 1))) = ( Following (P1,s2)) by EXTPRO_1: 3

      .= ( Exec (( goto 2),s2)) by A11;

      

       A13: ( IC s4) = 2 by A12, SCMFSA_2: 69;

      

       A14: 2 in ( dom ( while>0 (a,I))) by SCMFSA_X: 7;

      

       A15: loc5 in ( dom ( while>0 (a,I))) by SCMFSA_X: 8;

      

       A16: (P1 /. ( IC s4)) = (P1 . ( IC s4)) by PBOOLE: 143;

      (P1 . 2) = (( while>0 (a,I)) . 2) by A14, FUNCT_4: 13

      .= ( goto loc5) by SCMFSA_X: 17;

      then

       A17: ( CurInstr (P1,s4)) = ( goto loc5) by A13, A16;

      

       A18: ( Comput (P1,s1,(2 + 1))) = ( Following (P1,s4)) by EXTPRO_1: 3

      .= ( Exec (( goto loc5),s4)) by A17;

      

       A19: ( IC s5) = loc5 by A18, SCMFSA_2: 69;

      

       A20: (P1 /. ( IC s5)) = (P1 . ( IC s5)) by PBOOLE: 143;

      (P1 . loc5) = (( while>0 (a,I)) . loc5) by A15, FUNCT_4: 13

      .= ( halt SCM+FSA ) by SCMFSA_X: 16;

      then ( CurInstr (P1,s5)) = ( halt SCM+FSA ) by A19, A20;

      then P1 halts_on s1 by EXTPRO_1: 29;

      hence ( while>0 (a,I)) is_halting_on (s,P) by SCMFSA7B:def 7;

      thus thesis;

    end;

    theorem :: SCMFSA_9:39

    

     Th13: for a be Int-Location, I be really-closed MacroInstruction of SCM+FSA , s be State of SCM+FSA , k be Nat st I is_halting_on (s,P) & k < ( LifeSpan ((P +* I),( Initialize s))) & ( IC ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(1 + k)))) = (( IC ( Comput ((P +* I),( Initialize s),k))) + 3) & ( DataPart ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(1 + k)))) = ( DataPart ( Comput ((P +* I),( Initialize s),k))) holds ( IC ( Comput ((P +* ( while>0 (a,I))),( Initialize s),((1 + k) + 1)))) = (( IC ( Comput ((P +* I),( Initialize s),(k + 1)))) + 3) & ( DataPart ( Comput ((P +* ( while>0 (a,I))),( Initialize s),((1 + k) + 1)))) = ( DataPart ( Comput ((P +* I),( Initialize s),(k + 1))))

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      set D = ( Int-Locations \/ FinSeq-Locations );

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

      let s be State of SCM+FSA ;

      let k be Nat;

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

      set sI = ( Initialize s), PI = (P +* I);

      

       A1: I c= PI by FUNCT_4: 25;

      set sK1 = ( Comput (P1,s1,(1 + k)));

      set sK2 = ( Comput (PI,sI,k));

      set l3 = ( IC ( Comput (PI,sI,k)));

      set I1 = (I ';' ( goto 0 ));

      set i = (a >0_goto 3);

      reconsider n = l3 as Element of NAT ;

      set Mi = (i ";" ( Goto (( card I1) + 1)));

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

      

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

      

       A3: I c= PI by FUNCT_4: 25;

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

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

      then

       A4: n in ( dom I) by AMISTD_1: 21, A3;

      then n < ( card I) by AFINSQ_1: 66;

      then

       A5: (n + 3) < (( card I) + 5) by XREAL_1: 8;

      

       A6: (PI /. ( IC sK2)) = (PI . ( IC sK2)) by PBOOLE: 143;

      

       A7: ( CurInstr (PI,sK2)) = (I . n) by A4, A1, GRFUNC_1: 2, A6;

      assume I is_halting_on (s,P);

      then

       A8: PI halts_on sI by SCMFSA7B:def 7;

      assume k < ( LifeSpan (PI,sI));

      then (I . n) <> ( halt SCM+FSA ) by A7, A8, EXTPRO_1:def 15;

      then

       A9: n <> ( LastLoc I) by COMPOS_1:def 14;

      n <= ( LastLoc I) by A4, VALUED_1: 32;

      then

       A10: n < ( LastLoc I) by A9, XXREAL_0: 1;

      then

       A11: n in ( dom ( CutLastLoc I)) by COMPOS_2: 26;

      ( dom I) c= ( dom I1) by COMPOS_1: 21;

      then

       A12: n in ( dom I1) by A4;

      ( dom I1) = (( dom ( CutLastLoc I)) \/ ( dom ( Reloc (( Macro ( goto 0 )),(( card I) -' 1))))) by FUNCT_4:def 1;

      then

       A13: ( dom ( CutLastLoc I)) c= ( dom I1) by XBOOLE_1: 7;

      

       A14: ( dom ( CutLastLoc I)) misses ( dom ( Reloc (( Macro ( goto 0 )),(( card I) -' 1)))) by COMPOS_1: 18;

      

       A15: n in ( dom I1) by A11, A13;

      ( dom I) c= ( dom I1) by COMPOS_1: 21;

      then ( LastLoc I) <= ( LastLoc I1) by VALUED_1: 68;

      then n < ( LastLoc I1) by A10, XXREAL_0: 2;

      then

       A16: (I1 . n) <> ( halt SCM+FSA ) by A15, COMPOS_1:def 15;

      ( dom I1) c= ( dom J2) by SCMFSA6A: 17;

      then

       A17: n in ( dom J2) by A12;

      then (n + 3) in { (il + 3) where il be Nat : il in ( dom J2) };

      then

       A18: (n + 3) in ( dom ( Shift (J2,3))) by VALUED_1:def 12;

      

      then

       A19: (( Shift (J2,3)) /. (n + 3)) = (( Shift (J2,3)) . (n + 3)) by PARTFUN1:def 6

      .= (J2 . n) by A17, VALUED_1:def 12

      .= (I1 . n) by A16, A15, SCMFSA6A: 15

      .= (( CutLastLoc I) . n) by A11, FUNCT_4: 16, A14

      .= (I . n) by A10, COMPOS_2: 27;

      ( card ( while>0 (a,I))) = (( card I) + 5) by SCMFSA_X: 4;

      then

       A20: (n + 3) in ( dom ( while>0 (a,I))) by A5, AFINSQ_1: 66;

      (I . n) in ( rng I) by A4, FUNCT_1:def 3;

      then

      reconsider j = (I . n) as Instruction of SCM+FSA by A2;

      

       A21: ( card Mi) = (( card ( Macro i)) + ( card ( Goto (( card I1) + 1)))) by SCMFSA6A: 21

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

      .= (2 + 1) by COMPOS_1: 56

      .= 3;

      then (n + 3) >= ( card Mi) by NAT_1: 11;

      then

       A22: not (n + 3) in ( dom Mi) by AFINSQ_1: 66;

      

       A23: ( Comput (PI,sI,(k + 1))) = ( Following (PI,sK2)) by EXTPRO_1: 3

      .= ( Exec (j,sK2)) by A7;

      assume

       A24: ( IC ( Comput (P1,s1,(1 + k)))) = (l3 + 3);

      (n + 3) < (( LastLoc I) + 3) by A10, XREAL_1: 6;

      then

       A25: (n + 3) <> ((( card I) - 1) + 3) by AFINSQ_1: 91;

      ( dom ( while>0 (a,I))) = ( dom ( if>0 (a,I1))) by FUNCT_7: 30;

      then

       A26: (n + 3) in ( dom ( if>0 (a,I1))) by A20;

      

       A27: ( if>0 (a,I1)) = (Mi ";" J2) by SCMFSA6A: 25;

      then ( dom ( if>0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J2,3)))) by SCMFSA6A: 39, A21;

      then

       A28: (n + 3) in ( dom ( Reloc (J2,3))) by A26, A22, XBOOLE_0:def 3;

      

       A29: (P1 /. ( IC sK1)) = (P1 . ( IC sK1)) by PBOOLE: 143;

      

       A30: ( Reloc (J2,3)) = ( IncAddr (( Shift (J2,3)),3)) by COMPOS_1: 34;

      (P1 . (n + 3)) = (( while>0 (a,I)) . (n + 3)) by A20, FUNCT_4: 13

      .= ((Mi ";" J2) . (n + 3)) by A27, FUNCT_7: 32, A25

      .= (( Reloc (J2,3)) . (n + 3)) by A28, SCMFSA6A: 40, A21

      .= ( IncAddr (j,3)) by A18, A19, A30, COMPOS_1:def 21;

      then

       A31: ( CurInstr (P1,sK1)) = ( IncAddr (j,3)) by A24, A29;

      assume

       A32: ( DataPart sK1) = ( DataPart sK2);

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

      .= ( Exec (( IncAddr (j,3)),sK1)) by A31;

      hence thesis by A24, A32, A23, SCMFSA6A: 8;

    end;

    theorem :: SCMFSA_9:40

    

     Th14: for a be Int-Location, I be really-closed MacroInstruction of SCM+FSA , s be State of SCM+FSA st I is_halting_on (s,P) & ( IC ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(1 + ( LifeSpan ((P +* I),( Initialize s))))))) = (( IC ( Comput ((P +* I),( Initialize s),( LifeSpan ((P +* I),( Initialize s)))))) + 3) holds ( CurInstr ((P +* ( while>0 (a,I))),( Comput ((P +* ( while>0 (a,I))),( Initialize s),(1 + ( LifeSpan ((P +* I),( Initialize s)))))))) = ( goto 0 )

    proof

      set J3 = (( Goto 0 ) ";" ( Stop SCM+FSA ));

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

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

      let s be State of SCM+FSA ;

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

      set sI = ( Initialize s), PI = (P +* I);

      

       A1: I c= PI by FUNCT_4: 25;

      set life = ( LifeSpan ((P +* I),( Initialize s)));

      set sK1 = ( Comput (P1,s1,(1 + life)));

      set sK2 = ( Comput (PI,sI,life));

      set I1 = (I ';' ( goto 0 ));

      set i = (a >0_goto 3);

      reconsider n = ( IC sK2) as Element of NAT ;

      set Mi = (i ";" ( Goto (( card I1) + 1)));

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

      

       A2: I c= PI by FUNCT_4: 25;

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

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

      then

       A3: n in ( dom I) by AMISTD_1: 21, A2;

      then n < ( card I) by AFINSQ_1: 66;

      then

       A4: (n + 3) < (( card I) + 5) by XREAL_1: 8;

      assume I is_halting_on (s,P);

      then

       A5: PI halts_on sI by SCMFSA7B:def 7;

      

       A6: (PI /. ( IC sK2)) = (PI . ( IC sK2)) by PBOOLE: 143;

      

       A7: (P1 /. ( IC sK1)) = (P1 . ( IC sK1)) by PBOOLE: 143;

      assume

       A8: ( IC sK1) = (( IC sK2) + 3);

      ( CurInstr (PI,sK2)) = (I . n) by A3, A1, GRFUNC_1: 2, A6;

      then

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

      ( IC sK2) = ( LastLoc I) by A3, A9, COMPOS_1:def 15

      .= (( card I) - 1) by AFINSQ_1: 91;

      then

       A10: (( IC sK2) + 3) = (( card I) + 2);

      ( card ( while>0 (a,I))) = (( card I) + 5) by SCMFSA_X: 4;

      then

       A11: (n + 3) in ( dom ( while>0 (a,I))) by A4, AFINSQ_1: 66;

      

       A12: (n + 3) in ( dom ( if>0 (a,I1))) by A11, FUNCT_7: 30;

      (P1 . (n + 3)) = (( while>0 (a,I)) . (n + 3)) by FUNCT_4: 13, A11

      .= (( while>0 (a,I)) . (( card I) + 2)) by A10

      .= ( goto 0 ) by FUNCT_7: 31, A10, A12;

      hence thesis by A8, A7;

    end;

    ::$Canceled

    theorem :: SCMFSA_9:42

    

     Th15: for s be State of SCM+FSA , I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st I is_halting_on (s,P) & (s . a) > 0 holds ( IC ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(( LifeSpan ((P +* I),( Initialize s))) + 2)))) = 0 & for k be Nat st k <= (( LifeSpan ((P +* I),( Initialize s))) + 2) holds ( IC ( Comput ((P +* ( while>0 (a,I))),( Initialize s),k))) in ( dom ( while>0 (a,I)))

    proof

      set D = ( Int-Locations \/ FinSeq-Locations );

      let s be State of SCM+FSA ;

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

      let a be read-write Int-Location;

      set sI = ( Initialize s), PI = (P +* I);

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

      defpred P[ Nat] means $1 <= ( LifeSpan (PI,sI)) implies ( IC ( Comput (P1,s1,(1 + $1)))) = (( IC ( Comput (PI,sI,$1))) + 3) & ( DataPart ( Comput (P1,s1,(1 + $1)))) = ( DataPart ( Comput (PI,sI,$1)));

      assume

       A1: I is_halting_on (s,P);

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        now

          

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

          assume (k + 1) <= ( LifeSpan (PI,sI));

          then k < ( LifeSpan (PI,sI)) by A4, XXREAL_0: 2;

          hence ( IC ( Comput (P1,s1,((1 + k) + 1)))) = (( IC ( Comput (PI,sI,(k + 1)))) + 3) & ( DataPart ( Comput (P1,s1,((1 + k) + 1)))) = ( DataPart ( Comput (PI,sI,(k + 1)))) by A1, A3, Th13;

        end;

        hence P[(k + 1)];

      end;

      reconsider l = ( LifeSpan (PI,sI)) as Element of NAT by ORDINAL1:def 12;

      set loc4 = (( card I) + 3);

      set i = (a >0_goto 3);

      set s2 = ( Comput (P1,s1,1));

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

      

      then

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

      .= 0 by FUNCOP_1: 72;

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

      then

       A6: (s1 . a) = (s . a) by FUNCT_4: 11;

      assume

       A7: (s . a) > 0 ;

      

       A8: 0 in ( dom ( while>0 (a,I))) by AFINSQ_1: 65;

      

       A9: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

      (P1 . 0 ) = (( while>0 (a,I)) . 0 ) by A8, FUNCT_4: 13

      .= i by SCMFSA_X: 10;

      then

       A10: ( CurInstr (P1,s1)) = i by A5, A9;

      

       A11: ( Comput (P1,s1,( 0 + 1))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

      .= ( Exec (i,s1)) by A10;

      then (for c holds (s2 . c) = (s1 . c)) & for f holds (s2 . f) = (s1 . f) by SCMFSA_2: 71;

      then

       A12: ( DataPart s2) = ( DataPart sI) by SCMFSA_M: 2;

      

       A13: ( IC s2) = 3 by A7, A11, A6, SCMFSA_2: 71;

      

       A14: P[ 0 ]

      proof

        assume 0 <= ( LifeSpan (PI,sI));

        

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

        ( IC ( Comput (PI,sI, 0 ))) = ( IC ( Start-At ( 0 , SCM+FSA ))) by A15, FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        hence thesis by A13, A12;

      end;

      

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

      set s4 = ( Comput (P1,s1,((1 + ( LifeSpan (PI,sI))) + 1)));

      set s3 = ( Comput (P1,s1,(1 + ( LifeSpan (PI,sI)))));

      set s2 = ( Comput (P1,s1,(1 + ( LifeSpan (PI,sI)))));

       P[l] by A16;

      then

       A17: ( CurInstr (P1,s2)) = ( goto 0 ) by A1, Th14;

      

       A18: ( CurInstr (P1,s3)) = ( goto 0 ) by A17;

      

       A19: s4 = ( Following (P1,s3)) by EXTPRO_1: 3

      .= ( Exec (( goto 0 ),s3)) by A18;

      

       A20: ( IC s4) = 0 by A19, SCMFSA_2: 69;

      hence ( IC ( Comput (P1,s1,(( LifeSpan (PI,sI)) + 2)))) = 0 ;

       A21:

      now

        let k be Nat;

        assume

         A22: k <= (( LifeSpan (PI,sI)) + 2);

        assume k <> 0 ;

        then

        consider n be Nat such that

         A23: k = (n + 1) by NAT_1: 6;

        k <= (( LifeSpan (PI,sI)) + 1) or k >= ((( LifeSpan (PI,sI)) + 1) + 1) by NAT_1: 13;

        then

         A24: k <= (( LifeSpan (PI,sI)) + 1) or k = (( LifeSpan (PI,sI)) + 2) by A22, XXREAL_0: 1;

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

        per cases by A24;

          suppose k <= (( LifeSpan (PI,sI)) + 1);

          then n <= ( LifeSpan (PI,sI)) by A23, XREAL_1: 6;

          then

           A25: ( IC ( Comput (P1,s1,(1 + n)))) = (( IC ( Comput (PI,sI,n))) + 3) by A16;

          reconsider m = ( IC ( Comput (PI,sI,n))) as Element of NAT ;

          

           A26: I c= PI by FUNCT_4: 25;

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

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

          then m in ( dom I) by AMISTD_1: 21, A26;

          then m < ( card I) by AFINSQ_1: 66;

          then

           A27: (m + 3) < (( card I) + 5) by XREAL_1: 8;

          ( card ( while>0 (a,I))) = (( card I) + 5) by SCMFSA_X: 4;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while>0 (a,I))) by A23, A25, A27, AFINSQ_1: 66;

        end;

          suppose k >= (( LifeSpan (PI,sI)) + 2);

          then k = (( LifeSpan (PI,sI)) + 2) by A22, XXREAL_0: 1;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while>0 (a,I))) by A20, AFINSQ_1: 65;

        end;

      end;

      now

        let k be Nat;

        assume

         A28: k <= (( LifeSpan (PI,sI)) + 2);

        per cases ;

          suppose k = 0 ;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while>0 (a,I))) by A8, A5;

        end;

          suppose k <> 0 ;

          hence ( IC ( Comput (P1,s1,k))) in ( dom ( while>0 (a,I))) by A21, A28;

        end;

      end;

      hence thesis;

    end;

    reserve s for State of SCM+FSA ,

I for MacroInstruction of SCM+FSA ,

a for read-write Int-Location;

    definition

      let s, I, a, P;

      deffunc U( Nat, State of SCM+FSA ) = ( Comput ((P +* ( while>0 (a,I))),( Initialize $2),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize $2))) + 2)));

      deffunc V( Nat, State of SCM+FSA ) = ( down U($1,$2));

      :: SCMFSA_9:def2

      func StepWhile>0 (a,I,P,s) -> sequence of ( product ( the_Values_of SCM+FSA )) means

      : Def2: (it . 0 ) = s & for i be Nat holds (it . (i + 1)) = ( Comput ((P +* ( while>0 (a,I))),( Initialize (it . i)),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize (it . i)))) + 2)));

      existence

      proof

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

        consider f be sequence of ( product ( the_Values_of SCM+FSA )) such that

         A1: (f . 0 ) = ss and

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

        take f;

        thus (f . 0 ) = s by A1;

        let i be Nat;

        (f . (i + 1)) = V(i,.) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be sequence of ( product ( the_Values_of SCM+FSA )) such that

         A3: (F1 . 0 ) = s and

         A4: for i be Nat holds (F1 . (i + 1)) = U(i,.) and

         A5: (F2 . 0 ) = s and

         A6: for i be Nat holds (F2 . (i + 1)) = U(i,.);

        reconsider s as Element of ( product ( the_Values_of SCM+FSA )) by CARD_3: 107;

        

         A7: (F1 . 0 ) = s by A3;

        

         A8: for i be Nat holds (F1 . (i + 1)) = V(i,.) by A4;

        

         A9: (F2 . 0 ) = s by A5;

        

         A10: for i be Nat holds (F2 . (i + 1)) = V(i,.) by A6;

        F1 = F2 from NAT_1:sch 16( A7, A8, A9, A10);

        hence thesis;

      end;

    end

    theorem :: SCMFSA_9:43

    

     Th16: (( StepWhile>0 (a,I,P,s)) . (k + 1)) = (( StepWhile>0 (a,I,P,(( StepWhile>0 (a,I,P,s)) . k))) . 1)

    proof

      set sk = (( StepWhile>0 (a,I,P,s)) . k);

      set sk0 = (( StepWhile>0 (a,I,P,sk)) . 0 );

      sk0 = sk by Def2;

      

      hence (( StepWhile>0 (a,I,P,s)) . (k + 1)) = ( Comput ((P +* ( while>0 (a,I))),( Initialize sk0),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize sk0))) + 2))) by Def2

      .= (( StepWhile>0 (a,I,P,sk)) . ( 0 + 1)) by Def2

      .= (( StepWhile>0 (a,I,P,sk)) . 1);

    end;

    theorem :: SCMFSA_9:44

    

     Th17: for I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA holds (( StepWhile>0 (a,I,P,s)) . 1) = ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize s))) + 2)))

    proof

      let I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      

       A1: (( StepWhile>0 (a,I,P,s)) . 0 ) = s by Def2;

      

      thus (( StepWhile>0 (a,I,P,s)) . 1) = (( StepWhile>0 (a,I,P,s)) . ( 0 + 1))

      .= ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize s))) + 2))) by A1, Def2;

    end;

    theorem :: SCMFSA_9:45

    

     Th18: for I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA , k,n be Nat st ( IC (( StepWhile>0 (a,I,P,s)) . k)) = 0 & (( StepWhile>0 (a,I,P,s)) . k) = ( Comput ((P +* ( while>0 (a,I))),( Initialize s),n)) holds (( StepWhile>0 (a,I,P,s)) . k) = ( Initialize (( StepWhile>0 (a,I,P,s)) . k)) & (( StepWhile>0 (a,I,P,s)) . (k + 1)) = ( Comput ((P +* ( while>0 (a,I))),( Initialize s),(n + (( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize (( StepWhile>0 (a,I,P,s)) . k)))) + 2))))

    proof

      let I be MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA , k,n be Nat;

      set D = ( Int-Locations \/ FinSeq-Locations );

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

      set sk = (( StepWhile>0 (a,I,P,s)) . k);

      set s2 = ( Initialize sk);

      assume

       A1: ( IC sk) = 0 ;

      assume

       A2: sk = ( Comput (P1,s1,n));

      sk is 0 -started by A1;

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

      hence s2 = sk by FUNCT_4: 98;

      

      hence (( StepWhile>0 (a,I,P,s)) . (k + 1)) = ( Comput (P1,sk,(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize sk))) + 2))) by Def2

      .= ( Comput (P1,s1,(n + (( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize sk))) + 2)))) by A2, EXTPRO_1: 4;

    end;

    theorem :: SCMFSA_9:46

    

     Th19: for I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA st (for k be Nat holds I is_halting_on ((( StepWhile>0 (a,I,P,s)) . k),(P +* ( while>0 (a,I))))) & ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st (for k be Nat holds ((f . (( StepWhile>0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile>0 (a,I,P,s)) . k)) or (f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile>0 (a,I,P,s)) . k) . a) <= 0 )) holds ( while>0 (a,I)) is_halting_on (s,P)

    proof

      let I be really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      set D = ( Int-Locations \/ FinSeq-Locations );

      assume

       A1: for k be Nat holds I is_halting_on ((( StepWhile>0 (a,I,P,s)) . k),(P +* ( while>0 (a,I))));

      set s1 = ( Initialize s), P1 = (P +* ( while>0 (a,I)));

      

       A2: (P1 +* ( while>0 (a,I))) = P1;

      given f be Function of ( product ( the_Values_of SCM+FSA )), NAT such that

       A3: for k be Nat holds ((f . (( StepWhile>0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile>0 (a,I,P,s)) . k)) or (f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile>0 (a,I,P,s)) . k) . a) <= 0 );

      deffunc F( Nat) = (f . (( StepWhile>0 (a,I,P,s)) . $1));

      

       A4: for k be Nat holds F(+) < F(k) or F(k) = 0 by A3;

      consider m be Nat such that

       A5: F(m) = 0 and

       A6: for n be Nat st F(n) = 0 holds m <= n from NAT_1:sch 17( A4);

      defpred P[ Nat] means ($1 + 1) <= m implies ex k st (( StepWhile>0 (a,I,P,s)) . ($1 + 1)) = ( Comput (P1,s1,k));

       A7:

      now

        let k be Nat;

        assume

         A8: P[k];

        now

          set sk1 = (( StepWhile>0 (a,I,P,s)) . (k + 1));

          set sk = (( StepWhile>0 (a,I,P,s)) . k);

          assume

           A9: ((k + 1) + 1) <= m;

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

          then k < m by A9, XXREAL_0: 2;

          then F(k) <> 0 by A6;

          then

           A10: (sk . a) > 0 by A3;

          

           A11: I is_halting_on (sk,(P +* ( while>0 (a,I)))) by A1;

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

          then

          consider n be Nat such that

           A12: sk1 = ( Comput (P1,s1,n)) by A8, A9, XXREAL_0: 2;

          take m = (n + (( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize sk1))) + 2));

          sk1 = ( Comput ((P +* ( while>0 (a,I))),( Initialize sk),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize sk))) + 2))) by Def2;

          then ( IC sk1) = 0 by A11, A10, Th15, A2;

          hence (( StepWhile>0 (a,I,P,s)) . ((k + 1) + 1)) = ( Comput (P1,s1,m)) by A12, Th18;

        end;

        hence P[(k + 1)];

      end;

      

       A13: P[ 0 ]

      proof

        assume ( 0 + 1) <= m;

        take n = (( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize s))) + 2);

        thus thesis by Th17;

      end;

      

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

      now

        per cases ;

          suppose m = 0 ;

          then ((( StepWhile>0 (a,I,P,s)) . 0 ) . a) <= 0 by A3, A5;

          then (s . a) <= 0 by Def2;

          hence thesis by Th12;

        end;

          suppose

           A15: m <> 0 ;

          set p = (( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize s))) + 3);

          set sm = (( StepWhile>0 (a,I,P,s)) . m);

          set sm1 = ( Initialize sm);

          consider i be Nat such that

           A16: m = (i + 1) by A15, NAT_1: 6;

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

          consider n be Nat such that

           A17: sm = ( Comput (P1,s1,n)) by A14, A16;

          set si = (( StepWhile>0 (a,I,P,s)) . i);

          i < m by A16, NAT_1: 13;

          then F(i) <> 0 by A6;

          then

           A18: (si . a) > 0 by A3;

          

           A19: I is_halting_on (si,(P +* ( while>0 (a,I)))) by A1;

          sm = ( Comput ((P +* ( while>0 (a,I))),( Initialize si),(( LifeSpan (((P +* ( while>0 (a,I))) +* I),( Initialize si))) + 2))) by A16, Def2;

          then sm is 0 -started by A19, A18, Th15, A2;

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

          then

           A20: sm1 = sm by FUNCT_4: 98;

          (sm . a) <= 0 by A3, A5;

          then ( while>0 (a,I)) is_halting_on (sm,P1) by Th12;

          then (P1 +* ( while>0 (a,I))) halts_on ( Initialize sm) by SCMFSA7B:def 7;

          then P1 halts_on sm1;

          then

          consider j be Nat such that

           A21: ( CurInstr (P1,( Comput (P1,sm,j)))) = ( halt SCM+FSA ) by A20;

          

           A22: ( Comput (P1,s1,(n + j))) = ( Comput (P1,( Comput (P1,s1,n)),j)) by EXTPRO_1: 4;

          ( CurInstr (P1,( Comput (P1,s1,(n + j))))) = ( halt SCM+FSA ) by A17, A21, A22;

          then P1 halts_on s1 by EXTPRO_1: 29;

          hence ( while>0 (a,I)) is_halting_on (s,P) by SCMFSA7B:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA_9:47

    

     Th20: for I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA st ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st (for k be Nat holds ((f . (( StepWhile>0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile>0 (a,I,P,s)) . k)) or (f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile>0 (a,I,P,s)) . k) . a) <= 0 )) holds ( while>0 (a,I)) is_halting_on (s,P)

    proof

      let I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location, s be State of SCM+FSA ;

      

       A1: for k be Nat holds I is_halting_on ((( StepWhile>0 (a,I,P,s)) . k),(P +* ( while>0 (a,I)))) by SCMFSA7B: 19;

      assume ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st for k be Nat holds ((f . (( StepWhile>0 (a,I,P,s)) . (k + 1))) < (f . (( StepWhile>0 (a,I,P,s)) . k)) or (f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 ) & ((f . (( StepWhile>0 (a,I,P,s)) . k)) = 0 iff ((( StepWhile>0 (a,I,P,s)) . k) . a) <= 0 );

      hence thesis by A1, Th19;

    end;

    theorem :: SCMFSA_9:48

    for I be parahalting really-closed MacroInstruction of SCM+FSA , a be read-write Int-Location st ex f be Function of ( product ( the_Values_of SCM+FSA )), NAT st (for s be State of SCM+FSA , P holds ((f . (( StepWhile>0 (a,I,P,s)) . 1)) < (f . s) or (f . s) = 0 ) & ((f . s) = 0 iff (s . a) <= 0 )) holds ( while>0 (a,I)) is parahalting

    proof

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

      given f be Function of ( product ( the_Values_of SCM+FSA )), NAT such that

       A1: for s be State of SCM+FSA , P holds ((f . (( StepWhile>0 (a,I,P,s)) . 1)) < (f . s) or (f . s) = 0 ) & ((f . s) = 0 iff (s . a) <= 0 );

      now

        let t be State of SCM+FSA ;

        let Q;

        now

          let k be Nat;

          (f . (( StepWhile>0 (a,I,Q,(( StepWhile>0 (a,I,Q,t)) . k))) . 1)) < (f . (( StepWhile>0 (a,I,Q,t)) . k)) or (f . (( StepWhile>0 (a,I,Q,t)) . k)) = 0 by A1;

          hence ((f . (( StepWhile>0 (a,I,Q,t)) . (k + 1))) < (f . (( StepWhile>0 (a,I,Q,t)) . k)) or (f . (( StepWhile>0 (a,I,Q,t)) . k)) = 0 ) & ((f . (( StepWhile>0 (a,I,Q,t)) . k)) = 0 iff ((( StepWhile>0 (a,I,Q,t)) . k) . a) <= 0 ) by A1, Th16;

        end;

        hence ( while>0 (a,I)) is_halting_on (t,Q) by Th20;

      end;

      hence thesis by SCMFSA7B: 19;

    end;

    registration

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

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

      coherence

      proof

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

        reconsider Mi = ( Macro i) as good Program of SCM+FSA by Th11, SCMFSA7B: 13;

        ( if>0 (a,I,J)) = ((((Mi ";" J) ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

        hence thesis;

      end;

    end

    registration

      let I be good MacroInstruction of SCM+FSA , a be Int-Location;

      cluster ( if>0 (a,I)) -> good;

      correctness

      proof

        set i = (a >0_goto 3);

        reconsider Mi = ( Macro i) as good Program of SCM+FSA by Th11, SCMFSA7B: 13;

        ( if>0 (a,I)) = (((Mi ";" ( Goto (( card I) + 1))) ";" I) ";" ( Stop SCM+FSA ));

        hence thesis;

      end;

    end

    registration

      let I be good MacroInstruction of SCM+FSA , a be Int-Location;

      cluster ( while>0 (a,I)) -> good;

      correctness

      proof

        

         A1: not ( goto 0 ) destroys ( intloc 0 ) by SCMFSA7B: 11;

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

        then not ( if>0 (a,(I ';' ( goto 0 )))) destroys ( intloc 0 ) by SCMFSA8C: 98;

        then not ( while>0 (a,I)) destroys ( intloc 0 ) by SCMFSA8A: 42, A1;

        hence thesis by SCMFSA7B:def 5;

      end;

    end

    theorem :: SCMFSA_9:49

    for p be preProgram of SCM+FSA , l be Nat, ic be Instruction of SCM+FSA st (ex pc be Instruction of SCM+FSA st pc = (p . l) & ( UsedIntLoc pc) = ( UsedIntLoc ic)) holds ( UsedILoc p) = ( UsedILoc (p +* (l,ic)))

    proof

      let p be preProgram of SCM+FSA , l be Nat, ic be Instruction of SCM+FSA ;

      given pc be Instruction of SCM+FSA such that

       A1: pc = (p . l) and

       A2: ( UsedIntLoc pc) = ( UsedIntLoc ic);

      { ( UsedIntLoc i) where i be Instruction of SCM+FSA : i in ( rng p) } = { ( UsedIntLoc j) where j be Instruction of SCM+FSA : j in ( rng (p +* (l,ic))) } from FUNCT_7:sch 7( A2, A1);

      hence thesis;

    end;

    theorem :: SCMFSA_9:50

    for p be preProgram of SCM+FSA , l be Nat, ic be Instruction of SCM+FSA st (ex pc be Instruction of SCM+FSA st pc = (p . l) & ( UsedInt*Loc pc) = ( UsedInt*Loc ic)) holds ( UsedI*Loc p) = ( UsedI*Loc (p +* (l,ic)))

    proof

      let p be preProgram of SCM+FSA , l be Nat, ic be Instruction of SCM+FSA ;

      given pc be Instruction of SCM+FSA such that

       A1: pc = (p . l) and

       A2: ( UsedInt*Loc pc) = ( UsedInt*Loc ic);

      { ( UsedInt*Loc i) where i be Instruction of SCM+FSA : i in ( rng p) } = { ( UsedInt*Loc j) where j be Instruction of SCM+FSA : j in ( rng (p +* (l,ic))) } from FUNCT_7:sch 7( A2, A1);

      hence thesis;

    end;