scmfsa_x.miz



    begin

    definition

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

      :: SCMFSA_X:def1

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

      correctness ;

    end

    definition

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

      :: SCMFSA_X:def2

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

      correctness ;

    end

    

     Lm1: ( card ( Stop SCM+FSA )) = 1 by AFINSQ_1: 34;

    

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

    

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

    theorem :: SCMFSA_X:1

    

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

    proof

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

      

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

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

      .= (((2 + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 33

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

      .= (( card I) + 4);

    end;

    theorem :: SCMFSA_X:2

    

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

    proof

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

      

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

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

      .= (((2 + ( card ( Goto (( card I) + 1)))) + ( card I)) + 1) by SCMFSA6A: 33

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

      .= (( card I) + 4);

    end;

    definition

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

      :: SCMFSA_X:def3

      func while=0 (a,I) -> Program of SCM+FSA equals (( if=0 (a,(I ';' ( goto 0 )))) +* ((( card I) + 2),( goto 0 )));

      correctness ;

      :: SCMFSA_X:def4

      func while>0 (a,I) -> Program of SCM+FSA equals (( if>0 (a,(I ';' ( goto 0 )))) +* ((( card I) + 2),( goto 0 )));

      correctness ;

    end

    theorem :: SCMFSA_X:3

    

     Th3: for I be MacroInstruction of SCM+FSA , a be Int-Location holds ( card ( while=0 (a,I))) = (( card I) + 5)

    proof

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

      

      thus ( card ( while=0 (a,I))) = ( card ( if=0 (a,(I ';' ( goto 0 ))))) by FUNCT_7: 30

      .= (( card (I ';' ( goto 0 ))) + 4) by Th1

      .= ((( card I) + 1) + 4) by COMPOS_2: 11

      .= (( card I) + 5);

    end;

    theorem :: SCMFSA_X:4

    

     Th4: for I be MacroInstruction of SCM+FSA , a be Int-Location holds ( card ( while>0 (a,I))) = (( card I) + 5)

    proof

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

      

      thus ( card ( while>0 (a,I))) = ( card ( if>0 (a,(I ';' ( goto 0 ))))) by FUNCT_7: 30

      .= (( card (I ';' ( goto 0 ))) + 4) by Th2

      .= ((( card I) + 1) + 4) by COMPOS_2: 11

      .= (( card I) + 5);

    end;

    theorem :: SCMFSA_X:5

    

     Th5: for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < 5 holds k in ( dom ( while=0 (a,I)))

    proof

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

      

       A1: 5 <= (( card I) + 5) by NAT_1: 11;

      

       A2: ( card ( while=0 (a,I))) = (( card I) + 5) by Th3;

      assume k < 5;

      then k < (( card I) + 5) by A1, XXREAL_0: 2;

      hence thesis by A2, AFINSQ_1: 66;

    end;

    theorem :: SCMFSA_X:6

    

     Th6: for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < 5 holds (( card I) + k) in ( dom ( while=0 (a,I)))

    proof

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

      assume

       A1: k < 5;

      ( card ( while=0 (a,I))) = (( card I) + 5) by Th3;

      hence thesis by A1, AFINSQ_1: 66, XREAL_1: 6;

    end;

    theorem :: SCMFSA_X:7

    

     Th7: for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < 5 holds k in ( dom ( while>0 (a,I)))

    proof

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

      

       A1: 5 <= (( card I) + 5) by NAT_1: 11;

      

       A2: ( card ( while>0 (a,I))) = (( card I) + 5) by Th4;

      assume k < 5;

      then k < (( card I) + 5) by A1, XXREAL_0: 2;

      hence thesis by A2, AFINSQ_1: 66;

    end;

    theorem :: SCMFSA_X:8

    

     Th8: for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < 5 holds (( card I) + k) in ( dom ( while>0 (a,I)))

    proof

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

      assume

       A1: k < 5;

      ( card ( while>0 (a,I))) = (( card I) + 5) by Th4;

      hence thesis by A1, AFINSQ_1: 66, XREAL_1: 6;

    end;

    theorem :: SCMFSA_X:9

    for a be Int-Location, I be MacroInstruction of SCM+FSA holds 1 in ( dom ( while=0 (a,I))) & 1 in ( dom ( while>0 (a,I))) by Th5, Th7;

    theorem :: SCMFSA_X:10

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

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set i = (a =0_goto 3);

      

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

      then

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

      

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

      

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

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

      

       A5: 1 <> (( card I) + 2) by NAT_1: 11;

      

      thus (( while=0 (a,I)) . 0 ) = (( if=0 (a,I1)) . 0 ) by FUNCT_7: 32

      .= (( Directed ( Macro i)) . 0 ) by A4, A2, SCMFSA8A: 14

      .= (a =0_goto 3) by SCMFSA7B: 1;

      

      thus (( while=0 (a,I)) . 1) = (( if=0 (a,I1)) . 1) by FUNCT_7: 32, A5

      .= (( Directed ( Macro i)) . 1) by A4, A3, SCMFSA8A: 14

      .= ( goto 2) by SCMFSA7B: 2;

      set i = (a >0_goto 3);

      

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

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

      

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

      then

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

      

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

      

      thus (( while>0 (a,I)) . 0 ) = (( if>0 (a,I1)) . 0 ) by FUNCT_7: 32

      .= (( Directed ( Macro i)) . 0 ) by A6, A8, SCMFSA8A: 14

      .= (a >0_goto 3) by SCMFSA7B: 1;

      

      thus (( while>0 (a,I)) . 1) = (( if>0 (a,I1)) . 1) by FUNCT_7: 32, A5

      .= (( Directed ( Macro i)) . 1) by A6, A9, SCMFSA8A: 14

      .= ( goto 2) by SCMFSA7B: 2;

    end;

    theorem :: SCMFSA_X:11

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

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set i = (a =0_goto 3);

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

      

       A1: c5 = ((( card I) + 1) + 3)

      .= (( card I1) + 3) by COMPOS_2: 11;

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

      ( 0 + c5) in { (il + c5) where il be Nat : il in ( dom J) } by Lm3;

      then

       A2: c5 in ( dom ( Shift (J,c5))) by VALUED_1:def 12;

      

      then

       A3: (( Shift (J,c5)) /. c5) = (( Shift (J,c5)) . ( 0 + c5)) by PARTFUN1:def 6

      .= ( halt SCM+FSA ) by Lm2, Lm3, VALUED_1:def 12;

      

       A4: c5 in ( dom ( while=0 (a,I))) & ( dom ( while=0 (a,I))) = ( dom ( if=0 (a,I1))) by Th6, FUNCT_7: 30;

      ( card ( if=0 (a,I1))) = (( card Mi) + ( card J)) by SCMFSA6A: 21;

      

      then

       A5: ( card Mi) = (( card ( if=0 (a,I1))) - ( card J))

      .= ((( card I1) + 4) - 1) by Th1, Lm1

      .= c5 by A1;

      then

       A6: not c5 in ( dom Mi);

      ( dom ( if=0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J,c5)))) by A5, SCMFSA6A: 39;

      then

       A7: c5 in ( dom ( Reloc (J,c5))) by A4, A6, XBOOLE_0:def 3;

      

       A8: ( Reloc (J,c5)) = ( IncAddr (( Shift (J,c5)),c5)) by COMPOS_1: 34;

      

       A9: c5 <> (( card I) + 2);

      

      thus (( while=0 (a,I)) . (( card I) + 4)) = ((Mi ";" J) . c5) by FUNCT_7: 32, A9

      .= (( Reloc (J,c5)) . c5) by A5, A7, SCMFSA6A: 40

      .= ( IncAddr (( halt SCM+FSA ),c5)) by A2, A3, A8, COMPOS_1:def 21

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

    end;

    theorem :: SCMFSA_X:12

    for a be Int-Location, I be MacroInstruction of SCM+FSA holds (( while=0 (a,I)) . 2) = ( goto (( card I) + 4))

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set i = (a =0_goto 3);

      set Mi = ( Macro i);

      set G = ( Goto (( card I1) + 1));

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

      set J1 = (G ";" J2);

      

       A1: 0 in ( dom G) by SCMFSA8A: 31;

      

       A2: (G . 0 ) = ( goto (( card I1) + 1));

      ( dom J1) = (( dom G) \/ ( dom ( Reloc (J2,( card G))))) by SCMFSA6A: 39;

      then

       A3: 0 in ( dom J1) by A1, XBOOLE_0:def 3;

      then ( 0 + 2) in { (il + 2) where il be Nat : il in ( dom J1) };

      then

       A4: 2 in ( dom ( Shift (J1,2))) by VALUED_1:def 12;

      

      then

       A5: (( Shift (J1,2)) /. 2) = (( Shift (J1,2)) . ( 0 + 2)) by PARTFUN1:def 6

      .= (J1 . 0 ) by A3, VALUED_1:def 12

      .= (( Directed G) . 0 ) by SCMFSA8A: 14, SCMFSA8A: 31

      .= ( goto (( card I1) + 1)) by A1, A2, SCMFSA8A: 16;

      

       A6: ( card Mi) = 2 by COMPOS_1: 56;

      then

       A7: not 2 in ( dom Mi);

      

       A8: 2 in ( dom ( while=0 (a,I))) & ( dom ( while=0 (a,I))) = ( dom ( if=0 (a,I1))) by Th5, FUNCT_7: 30;

      

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

      .= (Mi ";" J1) by SCMFSA6A: 25;

      then ( dom ( if=0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J1,2)))) by A6, SCMFSA6A: 39;

      then

       A10: 2 in ( dom ( Reloc (J1,2))) by A8, A7, XBOOLE_0:def 3;

      

       A11: ( Reloc (J1,2)) = ( IncAddr (( Shift (J1,2)),2)) by COMPOS_1: 34;

      ( 0 + 2) <> (( card I) + 2);

      

      hence (( while=0 (a,I)) . 2) = ((Mi ";" J1) . 2) by A9, FUNCT_7: 32

      .= (( Reloc (J1,2)) . 2) by A10, SCMFSA6A: 40, A6

      .= ( IncAddr (( goto (( card I1) + 1)),2)) by A4, A5, A11, COMPOS_1:def 21

      .= ( goto ((( card I1) + 1) + 2)) by SCMFSA_4: 1

      .= ( goto (((( card I) + 1) + 1) + 2)) by COMPOS_2: 11

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

    end;

    ::$Canceled

    theorem :: SCMFSA_X:14

    for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < (( card I) + 5) holds k in ( dom ( while=0 (a,I)))

    proof

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

      assume

       A1: k < (( card I) + 5);

      ( card ( while=0 (a,I))) = (( card I) + 5) by Th3;

      hence thesis by A1, AFINSQ_1: 66;

    end;

    theorem :: SCMFSA_X:15

    for a be Int-Location, I be MacroInstruction of SCM+FSA holds (( while=0 (a,I)) . (( card I) + 2)) = ( goto 0 )

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set Lc4 = (( card I) + 2);

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

      hence (( while=0 (a,I)) . Lc4) = ( goto 0 ) by FUNCT_7: 31;

    end;

    theorem :: SCMFSA_X:16

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

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set i = (a >0_goto 3);

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

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

      ( 0 + c5) in { (il + c5) where il be Nat : il in ( dom J) } by Lm3;

      then

       A1: c5 in ( dom ( Shift (J,c5))) by VALUED_1:def 12;

      

      then

       A2: (( Shift (J,c5)) /. c5) = (( Shift (J,c5)) . ( 0 + c5)) by PARTFUN1:def 6

      .= ( halt SCM+FSA ) by Lm2, Lm3, VALUED_1:def 12;

      

       A3: c5 in ( dom ( while>0 (a,I))) & ( dom ( while>0 (a,I))) = ( dom ( if>0 (a,I1))) by Th8, FUNCT_7: 30;

      ( card ( if>0 (a,I1))) = (( card Mi) + ( card J)) by SCMFSA6A: 21;

      

      then

       A4: ( card Mi) = (( card ( if>0 (a,I1))) - ( card J))

      .= ((( card I1) + 4) - 1) by Th2, Lm1

      .= (((( card I) + 1) + 4) - 1) by COMPOS_2: 11

      .= c5;

      then

       A5: not c5 in ( dom Mi);

      ( dom ( if>0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J,c5)))) by A4, SCMFSA6A: 39;

      then

       A6: c5 in ( dom ( Reloc (J,c5))) by A3, A5, XBOOLE_0:def 3;

      

       A7: ( Reloc (J,c5)) = ( IncAddr (( Shift (J,c5)),c5)) by COMPOS_1: 34;

      c5 <> (( card I) + 2);

      

      hence (( while>0 (a,I)) . c5) = ((Mi ";" J) . c5) by FUNCT_7: 32

      .= (( Reloc (J,c5)) . c5) by A6, SCMFSA6A: 40, A4

      .= ( IncAddr (( halt SCM+FSA ),c5)) by A1, A2, A7, COMPOS_1:def 21

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

    end;

    theorem :: SCMFSA_X:17

    for a be Int-Location, I be MacroInstruction of SCM+FSA holds (( while>0 (a,I)) . 2) = ( goto (( card I) + 4))

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set i = (a >0_goto 3);

      set Mi = ( Macro i);

      set G = ( Goto (( card I1) + 1));

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

      set J1 = (G ";" J2);

      

       A1: 0 in ( dom G) by SCMFSA8A: 31;

      

       A2: (G . 0 ) = ( goto (( card I1) + 1));

      ( dom J1) = (( dom G) \/ ( dom ( Reloc (J2,( card G))))) by SCMFSA6A: 39;

      then

       A3: 0 in ( dom J1) by A1, XBOOLE_0:def 3;

      then ( 0 + 2) in { (il + 2) where il be Nat : il in ( dom J1) };

      then

       A4: 2 in ( dom ( Shift (J1,2))) by VALUED_1:def 12;

      

      then

       A5: (( Shift (J1,2)) /. 2) = (( Shift (J1,2)) . ( 0 + 2)) by PARTFUN1:def 6

      .= (J1 . 0 ) by A3, VALUED_1:def 12

      .= (( Directed G) . 0 ) by A1, SCMFSA8A: 14

      .= ( goto (( card I1) + 1)) by A1, A2, SCMFSA8A: 16;

      

       A6: ( card Mi) = 2 by COMPOS_1: 56;

      then

       A7: not 2 in ( dom Mi);

      

       A8: 2 in ( dom ( while>0 (a,I))) & ( dom ( while>0 (a,I))) = ( dom ( if>0 (a,I1))) by Th7, FUNCT_7: 30;

      

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

      .= (Mi ";" J1) by SCMFSA6A: 25;

      then ( dom ( if>0 (a,I1))) = (( dom Mi) \/ ( dom ( Reloc (J1,2)))) by SCMFSA6A: 39, A6;

      then

       A10: 2 in ( dom ( Reloc (J1,2))) by A8, A7, XBOOLE_0:def 3;

      

       A11: ( Reloc (J1,2)) = ( IncAddr (( Shift (J1,2)),2)) by COMPOS_1: 34;

      ( 0 + 2) <> (( card I) + 2);

      

      hence (( while>0 (a,I)) . 2) = ((Mi ";" J1) . 2) by A9, FUNCT_7: 32

      .= (( Reloc (J1,2)) . 2) by A10, SCMFSA6A: 40, A6

      .= ( IncAddr (( goto (( card I1) + 1)),2)) by A4, A5, A11, COMPOS_1:def 21

      .= ( goto ((( card I1) + 1) + 2)) by SCMFSA_4: 1

      .= ( goto (((( card I) + 1) + 1) + 2)) by COMPOS_2: 11

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

    end;

    ::$Canceled

    theorem :: SCMFSA_X:19

    for a be Int-Location, I be MacroInstruction of SCM+FSA , k be Nat st k < (( card I) + 5) holds k in ( dom ( while>0 (a,I)))

    proof

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

      assume

       A1: k < (( card I) + 5);

      ( card ( while>0 (a,I))) = (( card I) + 5) by Th4;

      hence thesis by A1, AFINSQ_1: 66;

    end;

    theorem :: SCMFSA_X:20

    for a be Int-Location, I be MacroInstruction of SCM+FSA holds (( while>0 (a,I)) . (( card I) + 2)) = ( goto 0 )

    proof

      set J = ( Stop SCM+FSA );

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

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

      set Lc4 = (( card I) + 2);

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

      hence (( while>0 (a,I)) . Lc4) = ( goto 0 ) by FUNCT_7: 31;

    end;

    definition

      let a be Int-Location;

      let I be Program of SCM+FSA ;

      :: SCMFSA_X:def5

      func if<0 (a,I) -> Program of SCM+FSA equals (((a =0_goto (( card I) + 4)) ";" ((a >0_goto (( card I) + 2)) ";" I)) ";" ( Stop SCM+FSA ));

      coherence ;

    end

    theorem :: SCMFSA_X:21

    

     Th19: for I be Program of SCM+FSA , a be Int-Location holds ( card ( if<0 (a,I))) = (( card I) + 5)

    proof

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

      

      thus ( card ( if<0 (a,I))) = (( card ((a =0_goto (( card I) + 4)) ";" ((a >0_goto (( card I) + 2)) ";" I))) + 1) by Lm1, SCMFSA6A: 21

      .= ((2 + ( card ((a >0_goto (( card I) + 2)) ";" I))) + 1) by SCMFSA6A: 33

      .= ((2 + (( card I) + 2)) + 1) by SCMFSA6A: 33

      .= (( card I) + 5);

    end;

    definition

      let a be Int-Location;

      let I be MacroInstruction of SCM+FSA ;

      :: SCMFSA_X:def6

      func while<0 (a,I) -> Program of SCM+FSA equals (( if<0 (a,(I ';' ( goto 0 )))) +* ((( card I) + 1),( goto 0 )));

      correctness ;

    end

    theorem :: SCMFSA_X:22

    for I be MacroInstruction of SCM+FSA , a be Int-Location holds ( card ( while<0 (a,I))) = (( card I) + 6)

    proof

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

      

      thus ( card ( while<0 (a,I))) = ( card ( if<0 (a,(I ';' ( goto 0 ))))) by FUNCT_7: 30

      .= (( card (I ';' ( goto 0 ))) + 5) by Th19

      .= ((( card I) + 1) + 5) by COMPOS_2: 11

      .= (( card I) + 6);

    end;

    theorem :: SCMFSA_X:23

    

     Th21: for I be MacroInstruction of SCM+FSA , i be No-StopCode Instruction of SCM+FSA , n be Nat st (n + 1) < ( card I) holds (I +* (n,i)) is MacroInstruction of SCM+FSA

    proof

      let I be MacroInstruction of SCM+FSA , i be No-StopCode Instruction of SCM+FSA , n be Nat such that

       A1: (n + 1) < ( card I);

      set F = (I +* (n,i));

      

       A2: ( dom F) = ( dom I) by FUNCT_7: 30;

      then

       A3: ( LastLoc F) = ( LastLoc I);

      

       A4: (n + 1) < ( card F) by A1, A2;

      

       A5: ( card F) >= ( 0 + 1) by NAT_1: 13;

      ( LastLoc F) = (( card F) -' 1) by AFINSQ_1: 70

      .= (( card F) - 1) by A5, XREAL_1: 233;

      then ((n + 1) - 1) < ( LastLoc F) by A4, XREAL_1: 14;

      then n < ( LastLoc I) by A3;

      

      then (F . ( LastLoc F)) = (I . ( LastLoc I)) by A3, FUNCT_7: 32

      .= ( halt SCM+FSA ) by COMPOS_1:def 14;

      then

       A6: F is halt-ending;

      F is unique-halt

      proof

        let f be Nat such that

         A7: (F . f) = ( halt SCM+FSA ) and

         A8: f in ( dom F);

        now

          assume

           A9: (I . f) <> ( halt SCM+FSA );

          per cases ;

            suppose f = n;

            then (F . f) = i by FUNCT_7: 31, A8, A2;

            hence contradiction by A7, COMPOS_0:def 12;

          end;

            suppose f <> n;

            then (F . f) = (I . f) by FUNCT_7: 32;

            hence contradiction by A9, A7;

          end;

        end;

        hence f = ( LastLoc F) by A2, A8, A3, COMPOS_1:def 15;

      end;

      hence thesis by A6;

    end;

    registration

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

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

      coherence

      proof

        set W = ( if=0 (a,(I ';' ( goto 0 ))));

        ( card W) = (( card (I ';' ( goto 0 ))) + 4) by Th1

        .= ((( card I) + 1) + 4) by COMPOS_2: 11

        .= (( card I) + 5);

        then (( card I) + 3) < ( card W) by XREAL_1: 8;

        then ((( card I) + 2) + 1) < ( card W);

        hence thesis by Th21;

      end;

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

      coherence

      proof

        set W = ( if>0 (a,(I ';' ( goto 0 ))));

        ( card W) = (( card (I ';' ( goto 0 ))) + 4) by Th2

        .= ((( card I) + 1) + 4) by COMPOS_2: 11

        .= (( card I) + 5);

        then (( card I) + 3) < ( card W) by XREAL_1: 8;

        then ((( card I) + 2) + 1) < ( card W);

        hence thesis by Th21;

      end;

    end

    begin

    theorem :: SCMFSA_X:24

    

     Th22: for I be really-closed MacroInstruction of SCM+FSA , n,k be Nat st n < ( card I) & k < ( card I) holds (I +* (n,( goto k))) is really-closed

    proof

      let I be really-closed MacroInstruction of SCM+FSA , n,k be Nat such that

       A1: n < ( card I) and

       A2: k < ( card I);

      set F = (I +* (n,( goto k)));

      

       A3: n in ( dom I) by A1, AFINSQ_1: 66;

      

       A4: k in ( dom I) by A2, AFINSQ_1: 66;

      

       A5: ( dom F) = ( dom I) by FUNCT_7: 30;

      let l be Nat such that

       A6: l in ( dom F);

      

       A7: (F /. l) = (F . l) by A6, PARTFUN1:def 6;

      per cases ;

        suppose n = l;

        then (F . l) = ( goto k) by A3, FUNCT_7: 31;

        then ( NIC ((F /. l),l)) = {k} by A7, SCMFSA10: 33;

        hence ( NIC ((F /. l),l)) c= ( dom F) by A5, ZFMISC_1: 31, A4;

      end;

        suppose n <> l;

        then (F . l) = (I . l) by FUNCT_7: 32;

        

        then (F /. l) = (I . l) by A6, PARTFUN1:def 6

        .= (I /. l) by A6, A5, PARTFUN1:def 6;

        hence ( NIC ((F /. l),l)) c= ( dom F) by A5, A6, AMISTD_1:def 9;

      end;

    end;

    theorem :: SCMFSA_X:25

    

     Th23: for I be really-closed MacroInstruction of SCM+FSA holds (I ';' ( goto 0 )) is really-closed

    proof

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

      

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

      

       A2: 1 in ( dom ( Macro ( goto 0 ))) & 0 in ( dom ( Macro ( goto 0 ))) by COMPOS_1: 60;

      set F = ( Macro ( goto 0 ));

      ( Macro ( goto 0 )) is really-closed

      proof

        let l be Nat;

        assume

         A3: l in ( dom F);

        per cases by A1, TARSKI:def 2;

          suppose

           A4: l = 0 ;

          

          then (F /. l) = (F . l) by A2, PARTFUN1:def 6

          .= ( goto 0 ) by A4, COMPOS_1: 58;

          then ( NIC ((F /. l),l)) = { 0 } by SCMFSA10: 33;

          hence ( NIC ((F /. l),l)) c= ( dom F) by A2, ZFMISC_1: 31;

        end;

          suppose

           A5: l = 1;

          

          then (F /. l) = (F . l) by A2, PARTFUN1:def 6

          .= ( halt SCM+FSA ) by A5, COMPOS_1: 59;

          then ( NIC ((F /. l),l)) = {l} by AMISTD_1: 2;

          hence ( NIC ((F /. l),l)) c= ( dom F) by A3, ZFMISC_1: 31;

        end;

      end;

      then (I ';' ( Macro ( goto 0 ))) is really-closed;

      hence (I ';' ( goto 0 )) is really-closed;

    end;

    theorem :: SCMFSA_X:26

    

     Th24: for I be really-closed Program of SCM+FSA , k be Nat st k <= ( card I) holds (( Macro ( goto k)) ';' I) is really-closed

    proof

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

      assume

       A1: l <= ( card I);

      set F = ( Macro ( goto l));

      set G = I;

      set S = SCM+FSA ;

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

      let f be Nat such that

       A2: f in ( dom P);

      

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

      

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

      let x be object;

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

      then

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

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

       A6: ( IC s2) = f;

      

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

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

        suppose

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

        then

         A9: f < ( card ( CutLastLoc F)) by AFINSQ_1: 66;

        ( card ( CutLastLoc F)) = (( card F) - 1) by VALUED_1: 38

        .= (2 - 1) by COMPOS_1: 56;

        then

         A10: f = 0 by A9, NAT_1: 14;

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

        then

         A11: not f in ( dom ( Reloc (G,k))) by A8, XBOOLE_0: 3;

        (P /. f) = (( CutLastLoc F) . 0 ) by A10, FUNCT_4: 11, A11, A7

        .= ( goto l);

        then

         A12: x = l by SCMFSA_2: 69, A5;

        ( card P) = ((( card F) + ( card I)) - 1) by COMPOS_1: 20

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

        .= (( card I) + 1);

        then ( card I) < ( card P) by XREAL_1: 29;

        then l < ( card P) by A1, XXREAL_0: 2;

        hence x in ( dom P) by AFINSQ_1: 66, A12;

      end;

        suppose

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

        then

        consider m be Nat such that

         A14: f = (m + k) and

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

        

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

        then

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

        

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

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

        reconsider v = (( IC S) .--> m) as PartState of S by A18;

        set s1 = (s2 +* v);

        

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

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

        

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

        

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

        

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

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

        

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

        

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

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

        proof

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

          

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

          per cases ;

            suppose

             A26: a = ( IC S);

            

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

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

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

          end;

            suppose

             A27: a <> ( IC S);

            then

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

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

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

            hence thesis by A28, FUNCT_4: 11;

          end;

        end;

        then

         A29: s2 = ( IncIC (s1,k)) by A23, A24, FUNCT_1: 2;

        set s3 = s1;

        

         A30: ( IC s3) = m by A20, A21, A22, FUNCT_4: 13;

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

        reconsider k, m as Element of NAT ;

        

         A31: x = ( IC ( Exec (( IncAddr ((G /. m),k)),s2))) by A5, A16, A19, COMPOS_1:def 21

        .= (( IC ( Exec ((G /. m),s3))) + k) by A29, AMISTD_2: 7;

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

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

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

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

        hence thesis by A3, XBOOLE_0:def 3;

      end;

    end;

    theorem :: SCMFSA_X:27

    

     Th25: for I be really-closed MacroInstruction of SCM+FSA , k be Nat st k <= ( card I) holds (( Goto k) ";" I) is really-closed

    proof

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

      (( Goto k) ";" I) = (( Macro ( goto k)) ';' I) by SCMFSA8A: 43;

      hence thesis by Th24;

    end;

    theorem :: SCMFSA_X:28

    

     Th26: for I be really-closed Program of SCM+FSA holds ((( Goto (( card I) + 1)) ";" I) ";" ( Stop SCM+FSA )) is really-closed

    proof

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

      

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

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

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

      hence thesis by Th25, A1;

    end;

    theorem :: SCMFSA_X:29

    

     Th27: for I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat st k <= ( card I) holds (( Macro (a =0_goto k)) ';' I) is really-closed

    proof

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

      assume

       A1: l <= ( card I);

      set F = ( Macro (a =0_goto l));

      set G = I;

      set S = SCM+FSA ;

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

      let f be Nat such that

       A2: f in ( dom P);

      

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

      

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

      let x be object;

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

      then

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

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

       A6: ( IC s2) = f;

      

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

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

        suppose

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

        then

         A9: f < ( card ( CutLastLoc F)) by AFINSQ_1: 66;

        ( card ( CutLastLoc F)) = (( card F) - 1) by VALUED_1: 38

        .= (2 - 1) by COMPOS_1: 56;

        then

         A10: f = 0 by A9, NAT_1: 14;

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

        then

         A11: not f in ( dom ( Reloc (G,k))) by A8, XBOOLE_0: 3;

        (P /. f) = (( CutLastLoc F) . 0 ) by A10, FUNCT_4: 11, A11, A7

        .= (a =0_goto l);

        then

         A12: x = ( IC ( Exec ((a =0_goto l),s2))) by A5;

        (s2 . a) = 0 or (s2 . a) <> 0 ;

        then x = l or x = (( IC s2) + 1) by SCMFSA_2: 70, A12;

        per cases ;

          suppose

           A13: x = l;

          ( card P) = ((( card F) + ( card I)) - 1) by COMPOS_1: 20

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

          .= (( card I) + 1);

          then ( card I) < ( card P) by XREAL_1: 29;

          then l < ( card P) by A1, XXREAL_0: 2;

          hence x in ( dom P) by AFINSQ_1: 66, A13;

        end;

          suppose x = (( IC s2) + 1);

          then

           A14: x = (f + 1) by A6;

          f < (( card F) - 1) by A9, VALUED_1: 38;

          then (f + 1) < ( card F) by XREAL_1: 20;

          then

           A15: x in ( dom F) by A14, AFINSQ_1: 66;

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

          hence thesis by A15;

        end;

      end;

        suppose

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

        then

        consider m be Nat such that

         A17: f = (m + k) and

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

        

         A19: m in ( dom G) by A18, COMPOS_1:def 21;

        then

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

        

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

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

        reconsider v = (( IC S) .--> m) as PartState of S by A21;

        set s1 = (s2 +* v);

        

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

        .= (( IncAddr (G,k)) . m) by A17, A18, VALUED_1:def 12;

        

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

        

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

        

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

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

        

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

        

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

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

        proof

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

          

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

          per cases ;

            suppose

             A29: a = ( IC S);

            

            hence (s2 . a) = (( IC s1) + k) by A6, A17, A25, A23, A24, FUNCT_4: 13

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

            .= ((s1 +* (( IC S) .--> (( IC s1) + k))) . a) by A24, A28, A29, FUNCT_4: 13;

          end;

            suppose

             A30: a <> ( IC S);

            then

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

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

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

            hence thesis by A31, FUNCT_4: 11;

          end;

        end;

        then

         A32: s2 = ( IncIC (s1,k)) by A26, A27, FUNCT_1: 2;

        set s3 = s1;

        

         A33: ( IC s3) = m by A23, A24, A25, FUNCT_4: 13;

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

        reconsider k, m as Element of NAT ;

        

         A34: x = ( IC ( Exec (( IncAddr ((G /. m),k)),s2))) by A5, A19, A22, COMPOS_1:def 21

        .= (( IC ( Exec ((G /. m),s3))) + k) by A32, AMISTD_2: 7;

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

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

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

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

        hence thesis by A3, XBOOLE_0:def 3;

      end;

    end;

    

     Lm4: for i be No-StopCode Instruction of SCM+FSA holds ( Directed ( Macro i)) = (( Macro i) ';' ( Goto 1))

    proof

      let i be No-StopCode Instruction of SCM+FSA ;

      set A = {i, ( halt SCM+FSA )};

      

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

      then (( card ( Macro i)) - 1) = 1;

      then

       A2: (( card ( Macro i)) -' 1) = 1 by XREAL_0:def 2;

      

       A3: ( card ( Load i)) = 1 by AFINSQ_1: 34;

      

       A4: i <> ( halt SCM+FSA ) by COMPOS_0:def 12;

      ( rng ( Load i)) = {i} by AFINSQ_1: 33;

      then not ( halt SCM+FSA ) in ( rng ( Load i)) by TARSKI:def 1, A4;

      then

       A5: (( Load i) +~ (( halt SCM+FSA ),( goto 2))) = ( CutLastLoc ( Macro i)) by FUNCT_4: 103;

      

       A6: (( Shift (( Stop SCM+FSA ),1)) +~ (( halt SCM+FSA ),( goto 2))) = ( Shift ((( Stop SCM+FSA ) +~ (( halt SCM+FSA ),( goto 2))),1)) by VALUED_1: 67

      .= ( Shift ( <%( goto (1 + 1))%>,1)) by AFINSQ_1: 90

      .= ( Reloc (( Goto 1),1)) by SCMFSA8A: 44;

      

      thus ( Directed ( Macro i)) = ((( Load i) +* ( Shift (( Stop SCM+FSA ),1))) +~ (( halt SCM+FSA ),( goto 2))) by A3, AFINSQ_1: 77, A1

      .= (( Macro i) ';' ( Goto 1)) by A5, A6, A2, FUNCT_7: 117;

    end;

    

     Lm5: for I be Program of SCM+FSA , k be Nat holds ( stop (I ';' ( Goto k))) = (I ';' ( Macro ( goto k)))

    proof

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

      

       A1: ( IncAddr (( Macro ( goto k)),(( card I) -' 1))) = (( IncAddr (( Goto k),(( card I) -' 1))) ^ ( Stop SCM+FSA )) by COMPOS_1: 76;

      

      thus ( stop (I ';' ( Goto k))) = ((( CutLastLoc I) ^ ( IncAddr (( Goto k),(( card I) -' 1)))) ^ ( Stop SCM+FSA )) by COMPOS_1: 75

      .= (( CutLastLoc I) ^ ( IncAddr (( Macro ( goto k)),(( card I) -' 1)))) by A1, AFINSQ_1: 27

      .= (I ';' ( Macro ( goto k))) by COMPOS_1: 75;

    end;

    theorem :: SCMFSA_X:30

    

     Th28: for I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat st k <= ( card I) holds (( Macro (a >0_goto k)) ';' I) is really-closed

    proof

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

      assume

       A1: l <= ( card I);

      set F = ( Macro (a >0_goto l));

      set G = I;

      set S = SCM+FSA ;

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

      let f be Nat such that

       A2: f in ( dom P);

      

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

      

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

      let x be object;

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

      then

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

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

       A6: ( IC s2) = f;

      

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

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

        suppose

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

        then

         A9: f < ( card ( CutLastLoc F)) by AFINSQ_1: 66;

        ( card ( CutLastLoc F)) = (( card F) - 1) by VALUED_1: 38

        .= (2 - 1) by COMPOS_1: 56;

        then

         A10: f = 0 by A9, NAT_1: 14;

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

        then

         A11: not f in ( dom ( Reloc (G,k))) by A8, XBOOLE_0: 3;

        (P /. f) = (( CutLastLoc F) . 0 ) by A10, FUNCT_4: 11, A11, A7

        .= (a >0_goto l);

        then

         A12: x = ( IC ( Exec ((a >0_goto l),s2))) by A5;

        (s2 . a) = 0 or (s2 . a) <> 0 ;

        then x = l or x = (( IC s2) + 1) by SCMFSA_2: 71, A12;

        per cases ;

          suppose

           A13: x = l;

          ( card P) = ((( card F) + ( card I)) - 1) by COMPOS_1: 20

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

          .= (( card I) + 1);

          then ( card I) < ( card P) by XREAL_1: 29;

          then l < ( card P) by A1, XXREAL_0: 2;

          hence x in ( dom P) by AFINSQ_1: 66, A13;

        end;

          suppose x = (( IC s2) + 1);

          then

           A14: x = (f + 1) by A6;

          f < (( card F) - 1) by A9, VALUED_1: 38;

          then (f + 1) < ( card F) by XREAL_1: 20;

          then

           A15: x in ( dom F) by A14, AFINSQ_1: 66;

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

          hence thesis by A15;

        end;

      end;

        suppose

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

        then

        consider m be Nat such that

         A17: f = (m + k) and

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

        

         A19: m in ( dom G) by A18, COMPOS_1:def 21;

        then

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

        

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

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

        reconsider v = (( IC S) .--> m) as PartState of S by A21;

        set s1 = (s2 +* v);

        

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

        .= (( IncAddr (G,k)) . m) by A17, A18, VALUED_1:def 12;

        

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

        

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

        

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

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

        

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

        

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

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

        proof

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

          

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

          per cases ;

            suppose

             A29: a = ( IC S);

            

            hence (s2 . a) = (( IC s1) + k) by A6, A17, A25, A23, A24, FUNCT_4: 13

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

            .= ((s1 +* (( IC S) .--> (( IC s1) + k))) . a) by A24, A28, A29, FUNCT_4: 13;

          end;

            suppose

             A30: a <> ( IC S);

            then

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

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

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

            hence thesis by A31, FUNCT_4: 11;

          end;

        end;

        then

         A32: s2 = ( IncIC (s1,k)) by A26, A27, FUNCT_1: 2;

        set s3 = s1;

        

         A33: ( IC s3) = m by A23, A24, A25, FUNCT_4: 13;

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

        reconsider k, m as Element of NAT ;

        

         A34: x = ( IC ( Exec (( IncAddr ((G /. m),k)),s2))) by A5, A19, A22, COMPOS_1:def 21

        .= (( IC ( Exec ((G /. m),s3))) + k) by A32, AMISTD_2: 7;

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

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

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

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

        hence thesis by A3, XBOOLE_0:def 3;

      end;

    end;

    theorem :: SCMFSA_X:31

    

     Th29: for I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat st k <= ( card I) holds ((a =0_goto k) ";" I) is really-closed

    proof

      let I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat such that

       A1: k <= ( card I);

      

       A2: ((a =0_goto k) ";" I) = (( stop (( Macro (a =0_goto k)) ';' ( Goto 1))) ';' I) by Lm4

      .= ((( Macro (a =0_goto k)) ';' ( Macro ( goto 1))) ';' I) by Lm5

      .= (( Macro (a =0_goto k)) ';' (( Macro ( goto 1)) ';' I)) by COMPOS_1: 29;

      

       A3: ( card (( Macro ( goto 1)) ';' I)) = ((( card ( Macro ( goto 1))) + ( card I)) - 1) by COMPOS_1: 20

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

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

      then

       A4: k <= ( card (( Macro ( goto 1)) ';' I)) by A3, A1, XXREAL_0: 2;

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

      then (( Macro ( goto 1)) ';' I) is really-closed by Th24;

      hence ((a =0_goto k) ";" I) is really-closed by A4, A2, Th27;

    end;

    theorem :: SCMFSA_X:32

    

     Th30: for I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat st k <= ( card I) holds ((a >0_goto k) ";" I) is really-closed

    proof

      let I be really-closed MacroInstruction of SCM+FSA , a be Int-Location, k be Nat such that

       A1: k <= ( card I);

      

       A2: ((a >0_goto k) ";" I) = (( stop (( Macro (a >0_goto k)) ';' ( Goto 1))) ';' I) by Lm4

      .= ((( Macro (a >0_goto k)) ';' ( Macro ( goto 1))) ';' I) by Lm5

      .= (( Macro (a >0_goto k)) ';' (( Macro ( goto 1)) ';' I)) by COMPOS_1: 29;

      

       A3: ( card (( Macro ( goto 1)) ';' I)) = ((( card ( Macro ( goto 1))) + ( card I)) - 1) by COMPOS_1: 20

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

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

      then

       A4: k <= ( card (( Macro ( goto 1)) ';' I)) by A3, A1, XXREAL_0: 2;

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

      then (( Macro ( goto 1)) ';' I) is really-closed by Th24;

      hence ((a >0_goto k) ";" I) is really-closed by A4, A2, Th28;

    end;

    registration

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

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

      coherence

      proof

        

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

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

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

        

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

        .= (( card (( Goto (( card I) + 1)) ";" I)) + 1)

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

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

        .= (( card I) + 2);

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

        then

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

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

        hence thesis by A3, Th29, A1, A2;

      end;

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

      coherence

      proof

        

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

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

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

        

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

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

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

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

        .= (( card I) + 2);

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

        then

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

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

        hence thesis by A6, Th30, A4, A5;

      end;

    end

    registration

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

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

      coherence

      proof

        reconsider IG = (I ';' ( goto 0 )) as really-closed MacroInstruction of SCM+FSA by Th23;

        reconsider W = ( if=0 (a,IG)) as really-closed MacroInstruction of SCM+FSA ;

        ( card W) = (( card (I ';' ( goto 0 ))) + 4) by Th1

        .= ((( card I) + 1) + 4) by COMPOS_2: 11

        .= (( card I) + 5);

        then

         A1: (( card I) + 2) < ( card W) by XREAL_1: 8;

        (W +* ((( card I) + 2),( goto 0 ))) is really-closed by Th22, A1;

        hence thesis;

      end;

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

      coherence

      proof

        reconsider IG = (I ';' ( goto 0 )) as really-closed MacroInstruction of SCM+FSA by Th23;

        reconsider W = ( if>0 (a,IG)) as really-closed MacroInstruction of SCM+FSA ;

        ( card W) = (( card (I ';' ( goto 0 ))) + 4) by Th2

        .= ((( card I) + 1) + 4) by COMPOS_2: 11

        .= (( card I) + 5);

        then

         A2: (( card I) + 2) < ( card W) by XREAL_1: 8;

        (W +* ((( card I) + 2),( goto 0 ))) is really-closed by Th22, A2;

        hence thesis;

      end;

    end

    theorem :: SCMFSA_X:33

    for I,J,K be MacroInstruction of SCM+FSA holds ((I ";" J) ';' K) = (I ";" (J ';' K)) by COMPOS_1: 29;

    theorem :: SCMFSA_X:34

    for I be MacroInstruction of SCM+FSA holds ( stop ( Directed I)) = (I ";" ( Stop SCM+FSA ));

    theorem :: SCMFSA_X:35

    for I be MacroInstruction of SCM+FSA , a be Int-Location holds ( if=0 (a,(I ';' ( goto 0 )))) = (((((a =0_goto 3) ";" ( Goto (( card (I ';' ( goto 0 ))) + 1))) ";" I) ';' ( goto 0 )) ";" ( Stop SCM+FSA )) by COMPOS_1: 29;

    theorem :: SCMFSA_X:36

    for I be MacroInstruction of SCM+FSA , a be Int-Location holds ( if>0 (a,(I ';' ( goto 0 )))) = (((((a >0_goto 3) ";" ( Goto (( card (I ';' ( goto 0 ))) + 1))) ";" I) ';' ( goto 0 )) ";" ( Stop SCM+FSA )) by COMPOS_1: 29;