scmfsa7b.miz



    begin

    reserve m for Nat;

    reserve P for Instruction-Sequence of SCM+FSA ;

    set A = NAT ;

    theorem :: SCMFSA7B:1

    for i be Instruction of SCM+FSA holds (i = ( halt SCM+FSA ) implies (( Directed ( Macro i)) . 0 ) = ( goto 2)) & (i <> ( halt SCM+FSA ) implies (( Directed ( Macro i)) . 0 ) = i)

    proof

      

       A1: ( dom ( id the InstructionsF of SCM+FSA )) = the InstructionsF of SCM+FSA ;

      let i be Instruction of SCM+FSA ;

      

       A2: (( Macro i) . 0 ) = i by COMPOS_1: 58;

       0 in { 0 , 1} by TARSKI:def 2;

      then

       A3: 0 in ( dom ( Macro i)) by COMPOS_1: 61;

      

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

      hereby

        

         A5: ( dom ( id the InstructionsF of SCM+FSA )) = the InstructionsF of SCM+FSA ;

        assume

         A6: i = ( halt SCM+FSA );

        

         A7: i in ( dom (( halt SCM+FSA ) .--> ( goto 2))) by A6, TARSKI:def 1;

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

        

        hence (( Directed ( Macro i)) . 0 ) = (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ),( goto 2))) * ( Macro i)) . 0 ) by A4, FUNCT_7: 116

        .= (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) * ( Macro i)) . 0 ) by A5, FUNCT_7:def 3

        .= ((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) . i) by A3, A2, FUNCT_1: 13

        .= ((( halt SCM+FSA ) .--> ( goto 2)) . i) by A7, FUNCT_4: 13

        .= ( goto 2) by A6, FUNCOP_1: 72;

      end;

      assume i <> ( halt SCM+FSA );

      then

       A9: not i in ( dom (( halt SCM+FSA ) .--> ( goto 2))) by TARSKI:def 1;

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

      

      hence (( Directed ( Macro i)) . 0 ) = (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ),( goto 2))) * ( Macro i)) . 0 ) by A4, FUNCT_7: 116

      .= (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) * ( Macro i)) . 0 ) by A1, FUNCT_7:def 3

      .= ((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) . i) by A3, A2, FUNCT_1: 13

      .= (( id the InstructionsF of SCM+FSA ) . i) by A9, FUNCT_4: 11

      .= i;

    end;

    theorem :: SCMFSA7B:2

    for i be Instruction of SCM+FSA holds (( Directed ( Macro i)) . 1) = ( goto 2)

    proof

      let i be Instruction of SCM+FSA ;

      

       A1: (( Macro i) . 1) = ( halt SCM+FSA ) by COMPOS_1: 59;

      1 in { 0 , 1} by TARSKI:def 2;

      then

       A2: 1 in ( dom ( Macro i)) by COMPOS_1: 61;

      

       A3: ( halt SCM+FSA ) in ( dom (( halt SCM+FSA ) .--> ( goto 2))) by TARSKI:def 1;

      

       A4: ( dom ( id the InstructionsF of SCM+FSA )) = the InstructionsF of SCM+FSA ;

      ( card ( Macro i)) = 2 & ( rng ( Macro i)) c= the InstructionsF of SCM+FSA by COMPOS_1: 56, RELAT_1:def 19;

      

      hence (( Directed ( Macro i)) . 1) = (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ),( goto 2))) * ( Macro i)) . 1) by FUNCT_7: 116

      .= (((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) * ( Macro i)) . 1) by A4, FUNCT_7:def 3

      .= ((( id the InstructionsF of SCM+FSA ) +* (( halt SCM+FSA ) .--> ( goto 2))) . ( halt SCM+FSA )) by A2, A1, FUNCT_1: 13

      .= ((( halt SCM+FSA ) .--> ( goto 2)) . ( halt SCM+FSA )) by A3, FUNCT_4: 13

      .= ( goto 2) by FUNCOP_1: 72;

    end;

    registration

      let a be Int-Location, k be Integer;

      cluster (a := k) -> initial non empty NAT -definedthe InstructionsF of SCM+FSA -valued;

      coherence

      proof

        (a := k) = (( aSeq (a,k)) ^ ( Stop SCM+FSA )) by SCMFSA_7: 1;

        hence thesis;

      end;

    end

    

     Lm1: for s be State of SCM+FSA st ( IC s) = 0 holds for P be Instruction-Sequence of SCM+FSA holds for a be Int-Location, k be Integer st (a := k) c= P holds P halts_on s

    proof

      let s be State of SCM+FSA ;

      assume

       A1: ( IC s) = 0 ;

      let P be Instruction-Sequence of SCM+FSA ;

      

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

      let a be Int-Location, k be Integer;

      assume

       A3: (a := k) c= P;

      per cases ;

        suppose

         A4: k > 0 ;

        then

        consider k1 be Nat such that

         A5: (k1 + 1) = k and

         A6: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by SCMFSA_7:def 1;

        

         A7: ( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 )))))) = (( len <%(a := ( intloc 0 ))%>) + ( len (k1 --> ( AddTo (a,( intloc 0 )))))) by AFINSQ_1: 17

        .= (1 + ( len (k1 --> ( AddTo (a,( intloc 0 )))))) by AFINSQ_1: 34

        .= k by A5;

        set f = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ));

        

         A8: (f . 0 ) = (( <%(a := ( intloc 0 ))%> ^ ((k1 --> ( AddTo (a,( intloc 0 )))) ^ ( Stop SCM+FSA ))) . 0 ) by AFINSQ_1: 27

        .= (a := ( intloc 0 )) by AFINSQ_1: 35;

        reconsider k as Element of NAT by A4, INT_1: 3;

        

         A9: ( len f) = (( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 )))))) + ( len ( Stop SCM+FSA ))) by AFINSQ_1: 17

        .= (k + 1) by A7, AFINSQ_1: 34;

         A10:

        now

          let i be Element of NAT ;

          assume that

           A11: i <= k;

          i < (k + 1) by A11, NAT_1: 13;

          hence i in ( dom f) by A9, AFINSQ_1: 86;

        end;

        

         A12: for i be Element of NAT st i <= k holds (P . i) = (f . i) by A3, A6, A10, GRFUNC_1: 2;

        then

         A13: (P . 0 ) = (a := ( intloc 0 )) by A8;

         A14:

        now

          let n be Element of NAT ;

          assume n = 0 ;

          hence

           A15: ( Comput (P,s,n)) = s;

          hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A1, A13, A2, PARTFUN1:def 6;

          

          thus ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

          .= ( Exec ((a := ( intloc 0 )),s)) by A15, A1, A13, A2, PARTFUN1:def 6;

        end;

         A16:

        now

          let i be Element of NAT ;

          assume that

           A17: 1 <= i and

           A18: i < k;

          reconsider i1 = (i - 1) as Element of NAT by A17, INT_1: 5;

          (i - 1) < (k - 1) by A18, XREAL_1: 9;

          then

           A19: i1 in ( Segm k1) by A5, NAT_1: 44;

          

           A20: ( len <%(a := ( intloc 0 ))%>) = 1 by AFINSQ_1: 33;

          

           A21: ( len (k1 --> ( AddTo (a,( intloc 0 ))))) = k1;

          i in ( dom ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 )))))) by A18, A7, AFINSQ_1: 86;

          

          hence (f . i) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) . i) by AFINSQ_1:def 3

          .= ((k1 --> ( AddTo (a,( intloc 0 )))) . (i - 1)) by A17, A18, A20, A21, A5, AFINSQ_1: 18

          .= ( AddTo (a,( intloc 0 ))) by A19, FUNCOP_1: 7;

        end;

         A22:

        now

          let i be Nat;

          assume that

           A23: 0 < i and

           A24: i < k;

          

           A25: ( 0 + 1) <= i by A23, NAT_1: 13;

          

           A26: i in NAT by ORDINAL1:def 12;

          

          hence (P . i) = (f . i) by A12, A24

          .= ( AddTo (a,( intloc 0 ))) by A16, A25, A24, A26;

        end;

        

         A27: for i be Element of NAT st i <= k holds ( IC ( Comput (P,s,i))) = i

        proof

          defpred P[ Nat] means $1 <= k implies ( IC ( Comput (P,s,$1))) = $1;

          let i be Element of NAT ;

          assume

           A28: i <= k;

          

           A29: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            assume

             A30: P[n];

            assume

             A31: (n + 1) <= k;

            then

             A32: n < k by NAT_1: 13;

            per cases ;

              suppose

               A33: n = 0 ;

              

              hence ( IC ( Comput (P,s,(n + 1)))) = (( Exec ((a := ( intloc 0 )),s)) . ( IC SCM+FSA )) by A14

              .= (n + 1) by A1, A33, SCMFSA_2: 63;

            end;

              suppose

               A34: n > 0 ;

              (n + 0 ) <= (n + 1) by XREAL_1: 7;

              

              then

               A35: ( CurInstr (P,( Comput (P,s,n)))) = (P . n) by A30, A31, A2, PARTFUN1:def 6, XXREAL_0: 2

              .= ( AddTo (a,( intloc 0 ))) by A22, A32, A34;

              

               A36: ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

              .= ( Exec (( AddTo (a,( intloc 0 ))),( Comput (P,s,n)))) by A35;

              

              thus ( IC ( Comput (P,s,(n + 1)))) = (( IC ( Comput (P,s,n))) + 1) by A36, SCMFSA_2: 64

              .= (n + 1) by A30, A31, NAT_1: 13;

            end;

          end;

          

           A37: P[ 0 ] by A1;

          for i be Nat holds P[i] from NAT_1:sch 2( A37, A29);

          hence thesis by A28;

        end;

        k < (k + ( len ( Stop SCM+FSA ))) by XREAL_1: 29;

        

        then

         A38: (f . k) = (( Stop SCM+FSA ) . (k - k)) by A7, AFINSQ_1: 18

        .= ( halt SCM+FSA ) by AFINSQ_1: 34;

        ( CurInstr (P,( Comput (P,s,k)))) = (P . ( IC ( Comput (P,s,k)))) by A2, PARTFUN1:def 6

        .= (P . k) by A27

        .= ( halt SCM+FSA ) by A38, A12;

        hence thesis by EXTPRO_1: 29;

      end;

        suppose

         A39: k <= 0 ;

        then

        reconsider mk = ( - k) as Element of NAT by INT_1: 3;

        consider k1 be Nat such that

         A40: (k1 + k) = 1 and

         A41: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by A39, SCMFSA_7:def 1;

        

         A42: ( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) = (( len <%(a := ( intloc 0 ))%>) + ( len (k1 --> ( SubFrom (a,( intloc 0 )))))) by AFINSQ_1: 17

        .= (1 + ( len (k1 --> ( SubFrom (a,( intloc 0 )))))) by AFINSQ_1: 34

        .= ((mk + 1) + 1) by A40;

        set f = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ));

        

         A43: (f . 0 ) = (( <%(a := ( intloc 0 ))%> ^ ((k1 --> ( SubFrom (a,( intloc 0 )))) ^ ( Stop SCM+FSA ))) . 0 ) by AFINSQ_1: 27

        .= (a := ( intloc 0 )) by AFINSQ_1: 35;

        

         A44: ( len f) = (( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) + ( len ( Stop SCM+FSA ))) by AFINSQ_1: 17

        .= (((mk + 1) + 1) + 1) by A42, AFINSQ_1: 34;

         A45:

        now

          let i be Nat;

          assume that 0 <= i and

           A46: i <= ((mk + 1) + 1);

          i < (((mk + 1) + 1) + 1) by A46, NAT_1: 13;

          hence i in ( dom f) by A44, AFINSQ_1: 86;

        end;

        

         A47: for i be Nat st 0 <= i & i <= ((mk + 1) + 1) holds (P . i) = (f . i) by A3, A41, A45, GRFUNC_1: 2;

        then

         A48: (P . 0 ) = (a := ( intloc 0 )) by A43;

         A49:

        now

          let n be Element of NAT ;

          assume n = 0 ;

          hence

           A50: ( Comput (P,s,n)) = s;

          hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A1, A48, A2, PARTFUN1:def 6;

          

          thus ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

          .= ( Exec ((a := ( intloc 0 )),s)) by A50, A1, A48, A2, PARTFUN1:def 6;

        end;

         A51:

        now

          

           A52: ( len <%(a := ( intloc 0 ))%>) = 1 by AFINSQ_1: 33;

          let i be Nat;

          assume that

           A53: 1 <= i and

           A54: i < ((mk + 1) + 1);

          reconsider i1 = (i - 1) as Element of NAT by A53, INT_1: 5;

          (i - 1) < ((k1 + 1) - 1) by A54, A40, XREAL_1: 9;

          then

           A55: i1 in ( Segm k1) by NAT_1: 44;

          

           A56: ( len (k1 --> ( SubFrom (a,( intloc 0 ))))) = k1;

          i in ( dom ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) by A54, A42, AFINSQ_1: 86;

          

          hence (f . i) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) . i) by AFINSQ_1:def 3

          .= ((k1 --> ( SubFrom (a,( intloc 0 )))) . (i - 1)) by A40, A53, A54, A52, A56, AFINSQ_1: 18

          .= ( SubFrom (a,( intloc 0 ))) by A55, FUNCOP_1: 7;

        end;

         A57:

        now

          let i be Nat;

          assume that

           A58: 0 < i and

           A59: i < ((mk + 1) + 1);

          

           A60: ( 0 + 1) <= i by A58, NAT_1: 13;

          

          thus (P . i) = (f . i) by A47, A59

          .= ( SubFrom (a,( intloc 0 ))) by A51, A60, A59;

        end;

        

         A61: for i be Nat st i <= ((mk + 1) + 1) holds ( IC ( Comput (P,s,i))) = i

        proof

          defpred P[ Nat] means $1 <= ((mk + 1) + 1) implies ( IC ( Comput (P,s,$1))) = $1;

          let i be Nat;

          assume

           A62: i <= ((mk + 1) + 1);

          

           A63: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            assume

             A64: P[n];

            assume

             A65: (n + 1) <= ((mk + 1) + 1);

            then

             A66: n < ((mk + 1) + 1) by NAT_1: 13;

            per cases ;

              suppose

               A67: n = 0 ;

              

              hence ( IC ( Comput (P,s,(n + 1)))) = (( Exec ((a := ( intloc 0 )),s)) . ( IC SCM+FSA )) by A49

              .= (n + 1) by A1, A67, SCMFSA_2: 63;

            end;

              suppose

               A68: n > 0 ;

              (n + 0 ) <= (n + 1) by XREAL_1: 7;

              

              then

               A69: ( CurInstr (P,( Comput (P,s,n)))) = (P . n) by A64, A65, A2, PARTFUN1:def 6, XXREAL_0: 2

              .= ( SubFrom (a,( intloc 0 ))) by A57, A66, A68;

              

               A70: ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

              .= ( Exec (( SubFrom (a,( intloc 0 ))),( Comput (P,s,n)))) by A69;

              

              thus ( IC ( Comput (P,s,(n + 1)))) = (( IC ( Comput (P,s,n))) + 1) by A70, SCMFSA_2: 65

              .= (n + 1) by A64, A65, NAT_1: 13;

            end;

          end;

          

           A71: P[ 0 ] by A1;

          for i be Nat holds P[i] from NAT_1:sch 2( A71, A63);

          hence thesis by A62;

        end;

        ( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) <= ((mk + 1) + 1) & ((mk + 1) + 1) < (( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) + ( len ( Stop SCM+FSA ))) implies (f . ((mk + 1) + 1)) = (( Stop SCM+FSA ) . (((mk + 1) + 1) - ( len ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))))) by AFINSQ_1: 18;

        then

         A72: (f . ((mk + 1) + 1)) = ( halt SCM+FSA ) by A42, XREAL_1: 29;

        ( CurInstr (P,( Comput (P,s,((mk + 1) + 1))))) = (P . ( IC ( Comput (P,s,((mk + 1) + 1))))) by A2, PARTFUN1:def 6

        .= (P . ((mk + 1) + 1)) by A61

        .= ( halt SCM+FSA ) by A72, A47;

        hence thesis by EXTPRO_1: 29;

      end;

    end;

    registration

      let a be Int-Location, k be Integer;

      cluster (a := k) -> parahalting;

      correctness

      proof

        

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

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

        

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

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

         A3: (a := k) c= P;

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

        .= 0 ;

        hence P halts_on s by Lm1, A3;

      end;

    end

    theorem :: SCMFSA7B:3

    for s be State of SCM+FSA holds for a be read-write Int-Location, k be Integer holds (( IExec ((a := k),P,s)) . a) = k & (for b be read-write Int-Location st b <> a holds (( IExec ((a := k),P,s)) . b) = (s . b)) & for f be FinSeq-Location holds (( IExec ((a := k),P,s)) . f) = (s . f)

    proof

      let s be State of SCM+FSA ;

      let a be read-write Int-Location;

      let k be Integer;

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

      

       A1: (s1 . ( intloc 0 )) = (( Initialize (( intloc 0 ) .--> 1)) . ( intloc 0 )) by FUNCT_4: 13, SCMFSA_M: 10

      .= 1 by SCMFSA_M: 12;

      reconsider s1 as 0 -started State of SCM+FSA ;

      

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

      

      thus (( IExec ((a := k),P,s)) . a) = (( Result ((P +* (a := k)),s1)) . a)

      .= k by A1, A2, SCMFSA_7: 6;

      hereby

        let b be read-write Int-Location;

        assume

         A3: b <> a;

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

        then

         A4: not b in ( dom ( Initialize (( intloc 0 ) .--> 1))) by SCMFSA_M: 11, TARSKI:def 2;

        

        thus (( IExec ((a := k),P,s)) . b) = (( Result ((P +* (a := k)),s1)) . b)

        .= (s1 . b) by A1, A2, A3, SCMFSA_7: 6

        .= (s . b) by A4, FUNCT_4: 11;

      end;

      let f be FinSeq-Location;

      f <> ( intloc 0 ) & f <> ( IC SCM+FSA ) by SCMFSA_2: 57, SCMFSA_2: 58;

      then

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

      

      thus (( IExec ((a := k),P,s)) . f) = (( Result ((P +* (a := k)),s1)) . f)

      .= (s1 . f) by A1, A2, SCMFSA_7: 6

      .= (s . f) by A5, FUNCT_4: 11;

    end;

    

     Lm2: for p1,p2,p3,p4 be XFinSequence holds (((p1 ^ p2) ^ p3) ^ p4) = (p1 ^ ((p2 ^ p3) ^ p4))

    proof

      let p1,p2,p3,p4 be XFinSequence;

      

      thus (((p1 ^ p2) ^ p3) ^ p4) = ((p1 ^ (p2 ^ p3)) ^ p4) by AFINSQ_1: 27

      .= (p1 ^ ((p2 ^ p3) ^ p4)) by AFINSQ_1: 27;

    end;

    

     Lm3: for c0 be Element of NAT holds for s be c0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds for a be Int-Location, k be Integer st for c be Element of NAT st c < ( len ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . (c0 + c)) holds for i be Element of NAT st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i)

    proof

      let c0 be Element of NAT ;

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

      let P be Instruction-Sequence of SCM+FSA ;

      

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

      

       A2: ( IC s) = c0 by MEMSTR_0:def 12;

      let a be Int-Location;

      let k be Integer;

      assume

       A3: for c be Element of NAT st c < ( len ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . (c0 + c));

      

       A4: for c be Element of NAT st c in ( dom ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . (c0 + c)) by A3, AFINSQ_1: 66;

      per cases ;

        suppose

         A5: k > 0 ;

        then

        reconsider k9 = k as Element of NAT by INT_1: 3;

        consider k1 be Nat such that

         A6: (k1 + 1) = k9 and

         A7: ( aSeq (a,k9)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) by A5, SCMFSA_7:def 2;

        defpred Q[ Nat] means $1 <= k9 implies ( IC ( Comput (P,s,$1))) = (c0 + $1);

        

         A8: ( len ( aSeq (a,k9))) = (( len <%(a := ( intloc 0 ))%>) + ( len (k1 --> ( AddTo (a,( intloc 0 )))))) by A7, AFINSQ_1: 17

        .= (1 + ( len (k1 --> ( AddTo (a,( intloc 0 )))))) by AFINSQ_1: 34

        .= k9 by A6;

        for i be Element of NAT st i <= ( len ( aSeq (a,k9))) holds ( IC ( Comput (P,s,i))) = (c0 + i)

        proof

           A9:

          now

            let i be Element of NAT ;

            assume that

             A10: 1 <= i and

             A11: i < k9;

            reconsider i1 = (i - 1) as Element of NAT by A10, INT_1: 5;

            i = (i1 + 1);

            then i1 < k1 by A11, A6, XREAL_1: 6;

            then

             A12: i1 in ( Segm k1) by NAT_1: 44;

            

             A13: ( len (k1 --> ( AddTo (a,( intloc 0 ))))) = k1;

            ( len <%(a := ( intloc 0 ))%>) = 1 by AFINSQ_1: 33;

            

            hence (( aSeq (a,k9)) . i) = ((k1 --> ( AddTo (a,( intloc 0 )))) . (i - 1)) by A10, A7, A13, A6, A11, AFINSQ_1: 18

            .= ( AddTo (a,( intloc 0 ))) by A12, FUNCOP_1: 7;

          end;

          

           A14: for i be Element of NAT st i < k9 holds i in ( dom ( aSeq (a,k9))) by A8, AFINSQ_1: 86;

           A15:

          now

            let i be Nat;

            assume that

             A16: 0 < i and

             A17: i < k9;

            

             A18: ( 0 + 1) <= i by A16, NAT_1: 13;

            

             A19: i in NAT by ORDINAL1:def 12;

            

            hence (P . (c0 + i)) = (( aSeq (a,k9)) . i) by A4, A14, A17

            .= ( AddTo (a,( intloc 0 ))) by A9, A18, A17, A19;

          end;

          

           A20: (P . (c0 + 0 )) = (( aSeq (a,k9)) . 0 ) by A3, A5, A8

          .= (a := ( intloc 0 )) by A7, AFINSQ_1: 35;

           A21:

          now

            let n be Element of NAT ;

            assume n = 0 ;

            hence

             A22: ( Comput (P,s,n)) = s;

            

            thus ( CurInstr (P,( Comput (P,s,n)))) = (P . ( IC ( Comput (P,s,n)))) by A1, PARTFUN1:def 6

            .= (a := ( intloc 0 )) by A20, A22, MEMSTR_0:def 12;

            

            thus ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

            .= ( Exec ((a := ( intloc 0 )),s)) by A22, A2, A20, A1, PARTFUN1:def 6;

          end;

          

           A23: for n be Nat st Q[n] holds Q[(n + 1)]

          proof

            let n be Nat;

            assume

             A24: Q[n];

            assume

             A25: (n + 1) <= k9;

            per cases ;

              suppose

               A26: n = 0 ;

              

              hence ( IC ( Comput (P,s,(n + 1)))) = (( Exec ((a := ( intloc 0 )),s)) . ( IC SCM+FSA )) by A21

              .= ((c0 + 1) + n) by A2, A26, SCMFSA_2: 63

              .= (c0 + (n + 1));

            end;

              suppose

               A27: n > 0 ;

              

               A28: n < k9 by A25, NAT_1: 13;

              

               A29: (n + 0 ) <= (n + 1) by XREAL_1: 7;

              

               A30: ( CurInstr (P,( Comput (P,s,n)))) = (P . (c0 + n)) by A24, A25, A29, A1, PARTFUN1:def 6, XXREAL_0: 2

              .= ( AddTo (a,( intloc 0 ))) by A15, A27, A28;

              

               A31: ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

              .= ( Exec (( AddTo (a,( intloc 0 ))),( Comput (P,s,n)))) by A30;

              

              thus ( IC ( Comput (P,s,(n + 1)))) = (( IC ( Comput (P,s,n))) + 1) by A31, SCMFSA_2: 64

              .= ((c0 + n) + 1) by A24, A25, A29, XXREAL_0: 2

              .= (c0 + (n + 1));

            end;

          end;

          let i be Element of NAT ;

          assume

           A32: i <= ( len ( aSeq (a,k9)));

          

           A33: Q[ 0 ] by A2;

          for i be Nat holds Q[i] from NAT_1:sch 2( A33, A23);

          hence thesis by A8, A32;

        end;

        hence thesis;

      end;

        suppose

         A34: k <= 0 ;

        then

        reconsider mk = ( - k) as Element of NAT by INT_1: 3;

        defpred Q[ Nat] means $1 <= ((mk + 1) + 1) implies ( IC ( Comput (P,s,$1))) = (c0 + $1);

        consider k1 be Nat such that

         A35: (k1 + k) = 1 and

         A36: ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) by A34, SCMFSA_7:def 2;

        

         A37: ( len ( aSeq (a,k))) = (( len <%(a := ( intloc 0 ))%>) + ( len (k1 --> ( SubFrom (a,( intloc 0 )))))) by A36, AFINSQ_1: 17

        .= (1 + ( len (k1 --> ( SubFrom (a,( intloc 0 )))))) by AFINSQ_1: 34

        .= ((mk + 1) + 1) by A35;

        for i be Element of NAT st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i)

        proof

           A38:

          now

            let i be Element of NAT ;

            assume that

             A39: 1 <= i and

             A40: i < ((mk + 1) + 1);

            

             A41: (i - 1) < (((mk + 1) + 1) - 1) by A40, XREAL_1: 9;

            reconsider i1 = (i - 1) as Element of NAT by A39, INT_1: 5;

            

             A42: i1 in ( Segm k1) by A35, A41, NAT_1: 44;

            

             A43: ( len (k1 --> ( SubFrom (a,( intloc 0 ))))) = k1;

            ( len <%(a := ( intloc 0 ))%>) = 1 by AFINSQ_1: 33;

            

            hence (( aSeq (a,k)) . i) = ((k1 --> ( SubFrom (a,( intloc 0 )))) . (i - 1)) by A36, A39, A43, A35, A40, AFINSQ_1: 18

            .= ( SubFrom (a,( intloc 0 ))) by A42, FUNCOP_1: 7;

          end;

          

           A44: for i be Element of NAT st i < ((mk + 1) + 1) holds i in ( dom ( aSeq (a,k))) by A37, AFINSQ_1: 86;

           A45:

          now

            let i be Nat;

            assume that

             A46: 0 < i and

             A47: i < ((mk + 1) + 1);

            

             A48: ( 0 + 1) <= i by A46, NAT_1: 13;

            

             A49: i in NAT by ORDINAL1:def 12;

            

            hence (P . (c0 + i)) = (( aSeq (a,k)) . i) by A4, A44, A47

            .= ( SubFrom (a,( intloc 0 ))) by A38, A48, A47, A49;

          end;

          

           A50: (P . (c0 + 0 )) = (( aSeq (a,k)) . 0 ) by A3, A37

          .= (a := ( intloc 0 )) by A36, AFINSQ_1: 35;

          

           A51: for n be Element of NAT st n = 0 holds ( Comput (P,s,n)) = s & ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) & ( Comput (P,s,(n + 1))) = ( Exec ((a := ( intloc 0 )),s))

          proof

            let n be Element of NAT ;

            assume n = 0 ;

            hence

             A52: ( Comput (P,s,n)) = s;

            

            thus ( CurInstr (P,( Comput (P,s,n)))) = (P . ( IC ( Comput (P,s,n)))) by A1, PARTFUN1:def 6

            .= (a := ( intloc 0 )) by A50, A52, MEMSTR_0:def 12;

            

            thus ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

            .= ( Exec ((a := ( intloc 0 )),s)) by A52, A2, A50, A1, PARTFUN1:def 6;

          end;

          

           A53: for n be Nat st Q[n] holds Q[(n + 1)]

          proof

            let n be Nat;

            assume

             A54: Q[n];

            assume

             A55: (n + 1) <= ((mk + 1) + 1);

            per cases ;

              suppose

               A56: n = 0 ;

              

              hence ( IC ( Comput (P,s,(n + 1)))) = (( Exec ((a := ( intloc 0 )),s)) . ( IC SCM+FSA )) by A51

              .= ((c0 + n) + 1) by A2, A56, SCMFSA_2: 63

              .= (c0 + (n + 1));

            end;

              suppose

               A57: n > 0 ;

              

               A58: n < ((mk + 1) + 1) by A55, NAT_1: 13;

              

               A59: (n + 0 ) <= (n + 1) by XREAL_1: 7;

              

               A60: ( CurInstr (P,( Comput (P,s,n)))) = (P . (c0 + n)) by A54, A55, A59, A1, PARTFUN1:def 6, XXREAL_0: 2

              .= ( SubFrom (a,( intloc 0 ))) by A45, A57, A58;

              

               A61: ( Comput (P,s,(n + 1))) = ( Following (P,( Comput (P,s,n)))) by EXTPRO_1: 3

              .= ( Exec (( SubFrom (a,( intloc 0 ))),( Comput (P,s,n)))) by A60;

              

              thus ( IC ( Comput (P,s,(n + 1)))) = (( IC ( Comput (P,s,n))) + 1) by A61, SCMFSA_2: 65

              .= ((c0 + n) + 1) by A54, A55, A59, XXREAL_0: 2

              .= (c0 + (n + 1));

            end;

          end;

          let i be Element of NAT ;

          assume

           A62: i <= ( len ( aSeq (a,k)));

          

           A63: Q[ 0 ] by A2;

          for i be Nat holds Q[i] from NAT_1:sch 2( A63, A53);

          hence thesis by A37, A62;

        end;

        hence thesis;

      end;

    end;

    

     Lm4: for s be 0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds for a be Int-Location, k be Integer st ( aSeq (a,k)) c= P holds for i be Element of NAT st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = i

    proof

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

      let P be Instruction-Sequence of SCM+FSA ;

      let a be Int-Location;

      let k be Integer;

      assume

       A1: ( aSeq (a,k)) c= P;

      

       A2: for c be Element of NAT st c < ( len ( aSeq (a,k))) holds (P . ( 0 + c)) = (( aSeq (a,k)) . c) by A1, AFINSQ_1: 86, GRFUNC_1: 2;

      let i be Element of NAT ;

      assume i <= ( len ( aSeq (a,k)));

      then ( IC ( Comput (P,s,i))) = ( 0 + i) by A2, Lm3;

      hence thesis;

    end;

    

     Lm5: for s be 0 -started State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds for f be FinSeq-Location, p be FinSequence of INT st (f := p) c= P holds P halts_on s

    proof

      set a2 = ( intloc 2);

      set a1 = ( intloc 1);

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

      let P be Instruction-Sequence of SCM+FSA ;

      

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

      set D = the InstructionsF of SCM+FSA ;

      let f be FinSeq-Location;

      let p be FinSequence of INT ;

      set q = (((( aSeq (a1,( len p))) ^ <%(f :=<0,...,0> a1)%>) ^ ( aSeq (f,p))) ^ ( Stop SCM+FSA ));

      set q0 = (( aSeq (a1,( len p))) ^ <%(f :=<0,...,0> a1)%>);

      assume

       A2: (f := p) c= P;

      set q = (((( aSeq (a1,( len p))) ^ <%(f :=<0,...,0> a1)%>) ^ ( aSeq (f,p))) ^ ( Stop SCM+FSA ));

      

       A3: for i,k be Element of NAT st i < ( len q) holds (P . i) = (q . i) by A2, AFINSQ_1: 86, GRFUNC_1: 2;

      consider pp be XFinSequence of (D ^omega ) such that

       A4: ( len pp) = ( len p) & for k be Nat st k < ( len pp) holds ex i be Integer st i = (p . (k + 1)) & (pp . k) = ((( aSeq (a1,(k + 1))) ^ ( aSeq (a2,i))) ^ <%((f,a1) := a2)%>) and

       A5: ( aSeq (f,p)) = ( FlattenSeq pp) by SCMFSA_7:def 3;

      ( len q) = (( len (q0 ^ ( FlattenSeq pp))) + 1) by A5, AFINSQ_1: 75;

      then

       A6: ( len (q0 ^ ( FlattenSeq pp))) < ( len q) by NAT_1: 13;

      defpred P[ XFinSequence] means $1 c= pp implies ex pp0 be XFinSequence of (D ^omega ) st (pp0 = $1 & for i be Element of NAT st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i);

      

       A7: for r be XFinSequence, x be object st P[r] holds P[(r ^ <%x%>)]

      proof

        let r be XFinSequence;

        let x be object;

        assume

         A8: P[r];

        set r1 = ( len r);

        ( len <%x%>) = 1 by AFINSQ_1: 34;

        then ( len (r ^ <%x%>)) = (r1 + 1) by AFINSQ_1: 17;

        then r1 < ( len (r ^ <%x%>)) by XREAL_1: 29;

        then

         A9: r1 in ( dom (r ^ <%x%>)) by AFINSQ_1: 86;

        assume

         A10: (r ^ <%x%>) c= pp;

        then

         A11: ( dom (r ^ <%x%>)) c= ( dom pp) by GRFUNC_1: 2;

        then r1 < ( len pp) by A9, AFINSQ_1: 86;

        then

        consider pr1 be Integer such that pr1 = (p . (r1 + 1)) and

         A12: (pp . r1) = ((( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1))) ^ <%((f,a1) := a2)%>) by A4;

        r c= (r ^ <%x%>) by AFINSQ_1: 74;

        then

        consider pp0 be XFinSequence of (D ^omega ) such that

         A13: pp0 = r and

         A14: for i be Element of NAT st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i by A8, A10, XBOOLE_1: 1;

        set c2 = ( len ((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))));

        set c1 = ( len (q0 ^ ( FlattenSeq pp0)));

        ( IC ( Comput (P,s,c1))) = c1 by A14;

        then

        reconsider s1 = ( Comput (P,s,c1)) as c1 -started State of SCM+FSA by MEMSTR_0:def 12;

        

         A15: x = ((r ^ <%x%>) . r1) by AFINSQ_1: 36

        .= (pp . r1) by A10, A9, GRFUNC_1: 2;

        then x in (D ^omega ) by A9, A11, FUNCT_1: 102;

        then

        reconsider pp1 = (pp0 ^ <%x%>) as XFinSequence of (D ^omega );

        take pp1;

        thus pp1 = (r ^ <%x%>) by A13;

        reconsider x as Element of (D ^omega ) by A9, A11, A15, FUNCT_1: 102;

        

         A16: ( FlattenSeq pp1) = (( FlattenSeq pp0) ^ ( FlattenSeq <%x%>)) by AFINSQ_2: 75

        .= (( FlattenSeq pp0) ^ x) by AFINSQ_2: 73;

        set s2 = ( Comput (P,s,c2));

        

         A17: x = (( aSeq (a1,(r1 + 1))) ^ (( aSeq (a2,pr1)) ^ <%((f,a1) := a2)%>)) by A12, A15, AFINSQ_1: 27;

        

        then

         A18: (( len q0) + ( len ( FlattenSeq pp1))) = (( len q0) + ( len ((( FlattenSeq pp0) ^ ( aSeq (a1,(r1 + 1)))) ^ (( aSeq (a2,pr1)) ^ <%((f,a1) := a2)%>)))) by A16, AFINSQ_1: 27

        .= ( len (q0 ^ ((( FlattenSeq pp0) ^ ( aSeq (a1,(r1 + 1)))) ^ (( aSeq (a2,pr1)) ^ <%((f,a1) := a2)%>)))) by AFINSQ_1: 17

        .= ( len (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ (( aSeq (a2,pr1)) ^ <%((f,a1) := a2)%>))) by Lm2

        .= (c2 + ( len (( aSeq (a2,pr1)) ^ <%((f,a1) := a2)%>))) by AFINSQ_1: 17

        .= (c2 + (( len ( aSeq (a2,pr1))) + ( len <%((f,a1) := a2)%>))) by AFINSQ_1: 17

        .= (c2 + (( len ( aSeq (a2,pr1))) + 1)) by AFINSQ_1: 34

        .= ((c2 + ( len ( aSeq (a2,pr1)))) + 1);

        then

         A19: ( len (q0 ^ ( FlattenSeq pp1))) = ((c2 + ( len ( aSeq (a2,pr1)))) + 1) by AFINSQ_1: 17;

        then

         A20: ( len (q0 ^ ( FlattenSeq pp1))) > (c2 + ( len ( aSeq (a2,pr1)))) by NAT_1: 13;

        

         A21: ( FlattenSeq pp1) c= ( FlattenSeq pp) by A10, A13, AFINSQ_2: 82;

         A22:

        now

          let p be XFinSequence;

          assume p c= x;

          then (( FlattenSeq pp0) ^ p) c= (( FlattenSeq pp0) ^ x) by AFINSQ_2: 81;

          then (( FlattenSeq pp0) ^ p) c= ( FlattenSeq pp) by A21, A16;

          then (q0 ^ (( FlattenSeq pp0) ^ p)) c= (q0 ^ ( FlattenSeq pp)) by AFINSQ_2: 81;

          then

           A23: ((q0 ^ ( FlattenSeq pp0)) ^ p) c= (q0 ^ ( FlattenSeq pp)) by AFINSQ_1: 27;

          (q0 ^ ( FlattenSeq pp)) c= q by A5, AFINSQ_1: 74;

          hence ((q0 ^ ( FlattenSeq pp0)) ^ p) c= q by A23;

        end;

        

         A24: for c be Element of NAT st c < ( len ( aSeq (a1,(r1 + 1)))) holds (( aSeq (a1,(r1 + 1))) . c) = (P . (c1 + c))

        proof

          let c be Element of NAT ;

          assume c < ( len ( aSeq (a1,(r1 + 1))));

          then

           A25: c in ( dom ( aSeq (a1,(r1 + 1)))) by AFINSQ_1: 66;

          then

           A26: (c1 + c) in ( dom ((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1))))) by AFINSQ_1: 23;

          

           A27: ((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) c= q by A17, A22, AFINSQ_1: 74;

          then

           A28: ( dom ((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1))))) c= ( dom q) by GRFUNC_1: 2;

          

          thus (( aSeq (a1,(r1 + 1))) . c) = (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) . (c1 + c)) by A25, AFINSQ_1:def 3

          .= (q . (c1 + c)) by A27, A26, GRFUNC_1: 2

          .= (P . (c1 + c)) by A2, A28, A26, GRFUNC_1: 2;

        end;

        set c3 = ( len (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ ( aSeq (a2,pr1))));

        

         A29: c2 = (c1 + ( len ( aSeq (a1,(r1 + 1))))) by AFINSQ_1: 17;

        

         A30: (q0 ^ ( FlattenSeq pp1)) = ((q0 ^ ( FlattenSeq pp0)) ^ x) by A16, AFINSQ_1: 27;

        then ( len (q0 ^ ( FlattenSeq pp1))) <= ( len q) by A22, NAT_1: 43;

        then

         A31: (c2 + ( len ( aSeq (a2,pr1)))) < ( len q) by A19, NAT_1: 13;

        

         A32: c3 = (c2 + ( len ( aSeq (a2,pr1)))) by AFINSQ_1: 17;

        

         A33: ( Comput (P,s,c2)) = ( Comput (P,s1,( len ( aSeq (a1,(r1 + 1)))))) by A29, EXTPRO_1: 4;

        ( IC ( Comput (P,s,c2))) = c2 by A29, A33, A24, Lm3;

        then

        reconsider s2 as c2 -started State of SCM+FSA by MEMSTR_0:def 12;

        

         A34: for c be Element of NAT st c < ( len ( aSeq (a2,pr1))) holds (( aSeq (a2,pr1)) . c) = (P . (c2 + c))

        proof

          let c be Element of NAT ;

          assume c < ( len ( aSeq (a2,pr1)));

          then

           A35: c in ( dom ( aSeq (a2,pr1))) by AFINSQ_1: 66;

          then

           A36: (c2 + c) in ( dom (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ ( aSeq (a2,pr1)))) by AFINSQ_1: 23;

          ((q0 ^ ( FlattenSeq pp0)) ^ (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))) c= q by A12, A15, A22, AFINSQ_1: 74;

          then

           A37: (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ ( aSeq (a2,pr1))) c= q by AFINSQ_1: 27;

          then

           A38: ( dom (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ ( aSeq (a2,pr1)))) c= ( dom q) by GRFUNC_1: 2;

          

          thus (( aSeq (a2,pr1)) . c) = ((((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (a1,(r1 + 1)))) ^ ( aSeq (a2,pr1))) . (c2 + c)) by A35, AFINSQ_1:def 3

          .= (q . (c2 + c)) by A36, A37, GRFUNC_1: 2

          .= (P . (c2 + c)) by A2, A38, A36, GRFUNC_1: 2;

        end;

         A39:

        now

          let i be Element of NAT ;

          assume i <= ( len ( aSeq (a2,pr1)));

          

          hence (c2 + i) = ( IC ( Comput (P,s2,i))) by A34, Lm3

          .= ( IC ( Comput (P,s,(c2 + i)))) by EXTPRO_1: 4;

        end;

         A40:

        now

          let i be Element of NAT ;

          assume i <= ( len ( aSeq (a1,(r1 + 1))));

          

          hence (c1 + i) = ( IC ( Comput (P,s1,i))) by A24, Lm3

          .= ( IC ( Comput (P,s,(c1 + i)))) by EXTPRO_1: 4;

        end;

        

         A41: for i be Element of NAT st i < ( len (q0 ^ ( FlattenSeq pp1))) holds ( IC ( Comput (P,s,i))) = i

        proof

          let i be Element of NAT ;

          assume

           A42: i < ( len (q0 ^ ( FlattenSeq pp1)));

           A43:

          now

            

             A44: i < (( len q0) + ( len ( FlattenSeq pp1))) by A42, AFINSQ_1: 17;

            assume

             A45: not i <= c1;

            assume not ((c1 + 1) <= i & i <= c2);

            hence (c2 + 1) <= i & i <= (c2 + ( len ( aSeq (a2,pr1)))) by A18, A45, A44, NAT_1: 13;

          end;

          per cases by A43;

            suppose i <= ( len (q0 ^ ( FlattenSeq pp0)));

            hence thesis by A14;

          end;

            suppose

             A46: (c1 + 1) <= i & i <= c2;

            then ((c1 + 1) - c1) <= (i - c1) by XREAL_1: 9;

            then

            reconsider ii = (i - c1) as Element of NAT by INT_1: 3;

            (i - c1) <= (c2 - c1) by A46, XREAL_1: 9;

            

            hence i = ( IC ( Comput (P,s,(c1 + ii)))) by A29, A40

            .= ( IC ( Comput (P,s,i)));

            thus thesis;

          end;

            suppose

             A47: (c2 + 1) <= i & i <= (c2 + ( len ( aSeq (a2,pr1))));

            then ((c2 + 1) - c2) <= (i - c2) by XREAL_1: 9;

            then

            reconsider ii = (i - c2) as Element of NAT by INT_1: 3;

            (i - c2) <= ((c2 + ( len ( aSeq (a2,pr1)))) - c2) by A47, XREAL_1: 9;

            

            hence i = ( IC ( Comput (P,s,(c2 + ii)))) by A39

            .= ( IC ( Comput (P,s,i)));

          end;

        end;

        ((q0 ^ ( FlattenSeq pp0)) ^ x) c= q by A22;

        then

        consider rq be XFinSequence of D such that

         A48: (((q0 ^ ( FlattenSeq pp0)) ^ x) ^ rq) = q by AFINSQ_2: 80;

        ( len (q0 ^ ( FlattenSeq pp1))) = ((c2 + ( len ( aSeq (a2,pr1)))) + 1) by A18, AFINSQ_1: 17;

        then

         A49: ( len (q0 ^ ( FlattenSeq pp1))) > (c2 + ( len ( aSeq (a2,pr1)))) by NAT_1: 13;

        then

         A50: c3 in ( dom ((q0 ^ ( FlattenSeq pp0)) ^ x)) by A30, A32, AFINSQ_1: 66;

        ( dom <%((f,a1) := a2)%>) = 1 by AFINSQ_1: 33;

        then

         A51: 0 in ( dom <%((f,a1) := a2)%>) by CARD_1: 49, TARSKI:def 1;

        ( len <%((f,a1) := a2)%>) = 1 by AFINSQ_1: 34;

        then ( len ((( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1))) ^ <%((f,a1) := a2)%>)) = (( len (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))) + 1) by AFINSQ_1: 17;

        then ( len (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))) < ( len ((( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1))) ^ <%((f,a1) := a2)%>)) by XREAL_1: 29;

        then

         A52: ( len (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))) in ( dom ((( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1))) ^ <%((f,a1) := a2)%>)) by AFINSQ_1: 66;

        

         A53: c3 = ((c1 + ( len ( aSeq (a1,(r1 + 1))))) + ( len ( aSeq (a2,pr1)))) by A29, AFINSQ_1: 17;

        

         A54: (P /. ( IC ( Comput (P,s,c3)))) = (P . ( IC ( Comput (P,s,c3)))) by A1, PARTFUN1:def 6;

        ( CurInstr (P,( Comput (P,s,c3)))) = (P . c3) by A32, A41, A54, A49

        .= (q . c3) by A3, A32, A31

        .= (((q0 ^ ( FlattenSeq pp0)) ^ x) . (c1 + (( len ( aSeq (a1,(r1 + 1)))) + ( len ( aSeq (a2,pr1)))))) by A53, A50, A48, AFINSQ_1:def 3

        .= (((q0 ^ ( FlattenSeq pp0)) ^ x) . (c1 + ( len (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))))) by AFINSQ_1: 17;

        

        then

         A55: ( CurInstr (P,( Comput (P,s,c3)))) = (((( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1))) ^ <%((f,a1) := a2)%>) . (( len (( aSeq (a1,(r1 + 1))) ^ ( aSeq (a2,pr1)))) + 0 )) by A52, A12, A15, AFINSQ_1:def 3

        .= ( <%((f,a1) := a2)%> . 0 ) by A51, AFINSQ_1:def 3

        .= ((f,a1) := a2);

        ( Comput (P,s,(c3 + 1))) = ( Following (P,( Comput (P,s,c3)))) by EXTPRO_1: 3

        .= ( Exec (((f,a1) := a2),( Comput (P,s,c3)))) by A55;

        

        then

         A56: ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1)))))) = (( Exec (((f,a1) := a2),( Comput (P,s,c3)))) . ( IC SCM+FSA )) by A19, AFINSQ_1: 17

        .= (( IC ( Comput (P,s,c3))) + 1) by SCMFSA_2: 73

        .= (c3 + 1) by A32, A41, A20;

        thus for i be Element of NAT st i <= ( len (q0 ^ ( FlattenSeq pp1))) holds ( IC ( Comput (P,s,i))) = i

        proof

          let i be Element of NAT ;

          assume

           A57: i <= ( len (q0 ^ ( FlattenSeq pp1)));

          per cases by A57, XXREAL_0: 1;

            suppose i < ( len (q0 ^ ( FlattenSeq pp1)));

            hence thesis by A41;

          end;

            suppose i = ( len (q0 ^ ( FlattenSeq pp1)));

            hence thesis by A32, A19, A56;

          end;

        end;

      end;

      set k = ( len ( aSeq (a1,( len p))));

      

       A58: ( len q0) = (k + 1) by AFINSQ_1: 75;

      q = ((( aSeq (a1,( len p))) ^ <%(f :=<0,...,0> a1)%>) ^ (( aSeq (f,p)) ^ ( Stop SCM+FSA ))) by AFINSQ_1: 27

      .= (( aSeq (a1,( len p))) ^ ( <%(f :=<0,...,0> a1)%> ^ (( aSeq (f,p)) ^ ( Stop SCM+FSA )))) by AFINSQ_1: 27;

      then

       A59: ( aSeq (a1,( len p))) c= (f := p) by AFINSQ_1: 74;

      

       A60: P[ {} ]

      proof

        assume {} c= pp;

        take ( <%> (D ^omega ));

        thus ( <%> (D ^omega )) = {} ;

        

         A61: q = ((( aSeq (a1,( len p))) ^ <%(f :=<0,...,0> a1)%>) ^ (( aSeq (f,p)) ^ ( Stop SCM+FSA ))) by AFINSQ_1: 27;

        then ( len q) = (( len q0) + ( len (( aSeq (f,p)) ^ ( Stop SCM+FSA )))) by AFINSQ_1: 17;

        then ( len q0) <= ( len q) by NAT_1: 11;

        then

         A62: k < ( len q) by A58, NAT_1: 13;

         A63:

        now

          let i be Element of NAT ;

          assume i < ( len q0);

          then i <= ( len ( aSeq (a1,( len p)))) by A58, NAT_1: 13;

          hence ( IC ( Comput (P,s,i))) = i by A2, A59, Lm4, XBOOLE_1: 1;

        end;

        

         A64: k < ( len q0) by A58, NAT_1: 13;

        then

         A65: k in ( dom q0) by AFINSQ_1: 66;

        

         A66: ( IC ( Comput (P,s,k))) = k by A63, A64;

        

        then

         A67: ( CurInstr (P,( Comput (P,s,k)))) = (P . k) by A1, PARTFUN1:def 6

        .= (q . k) by A3, A62

        .= (q0 . k) by A61, A65, AFINSQ_1:def 3

        .= (f :=<0,...,0> a1) by AFINSQ_1: 36;

        

         A68: ( Comput (P,s,( len q0))) = ( Following (P,( Comput (P,s,k)))) by A58, EXTPRO_1: 3

        .= ( Exec ((f :=<0,...,0> a1),( Comput (P,s,k)))) by A67;

        

         A69: ( IC ( Comput (P,s,( len q0)))) = (( IC ( Comput (P,s,k))) + 1) by A68, SCMFSA_2: 75

        .= ( len q0) by A58, A66;

         A70:

        now

          let i be Element of NAT ;

          assume i <= ( len q0);

          then i < ( len q0) or i = ( len q0) by XXREAL_0: 1;

          hence ( IC ( Comput (P,s,i))) = i by A63, A69;

        end;

        (q0 ^ ( FlattenSeq ( <%> (D ^omega )))) = (q0 ^ ( <%> D)) by AFINSQ_2: 74

        .= (q0 ^ {} )

        .= q0;

        hence thesis by A70;

      end;

      for r be XFinSequence holds P[r] from AFINSQ_1:sch 3( A60, A7);

      then ex pp0 be XFinSequence of (D ^omega ) st pp0 = pp & for i be Element of NAT st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i;

      then ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp)))))) = ( len (q0 ^ ( FlattenSeq pp)));

      

      then ( CurInstr (P,( Comput (P,s,( len (q0 ^ ( FlattenSeq pp))))))) = (P . ( len (q0 ^ ( FlattenSeq pp)))) by A1, PARTFUN1:def 6

      .= (q . ( len (q0 ^ ( FlattenSeq pp)))) by A3, A6

      .= ( halt SCM+FSA ) by A5, AFINSQ_1: 36;

      hence thesis by EXTPRO_1: 29;

    end;

    registration

      let f be FinSeq-Location, p be FinSequence of INT ;

      cluster (f := p) -> initial non empty NAT -definedthe InstructionsF of SCM+FSA -valued;

      coherence ;

    end

    registration

      let f be FinSeq-Location, p be FinSequence of INT ;

      cluster (f := p) -> parahalting;

      correctness by Lm5;

    end

    theorem :: SCMFSA7B:4

    for s be State of SCM+FSA , f be FinSeq-Location, p be FinSequence of INT holds (( IExec ((f := p),P,s)) . f) = p & (for a be read-write Int-Location st a <> ( intloc 1) & a <> ( intloc 2) holds (( IExec ((f := p),P,s)) . a) = (s . a)) & for g be FinSeq-Location st g <> f holds (( IExec ((f := p),P,s)) . g) = (s . g)

    proof

      let s be State of SCM+FSA ;

      let f be FinSeq-Location;

      let p be FinSequence of INT ;

      

       A1: ((s +* ( Initialize (( intloc 0 ) .--> 1))) . ( intloc 0 )) = (( Initialize (( intloc 0 ) .--> 1)) . ( intloc 0 )) by FUNCT_4: 13, SCMFSA_M: 10

      .= 1 by SCMFSA_M: 12;

      reconsider s1 = (s +* ( Initialize (( intloc 0 ) .--> 1))) as 0 -started State of SCM+FSA ;

      

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

      

      thus (( IExec ((f := p),P,s)) . f) = (( Result ((P +* (f := p)),s1)) . f)

      .= p by A1, A2, SCMFSA_7: 7;

      hereby

        let a be read-write Int-Location;

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

        then

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

        assume

         A4: a <> ( intloc 1) & a <> ( intloc 2);

        

        thus (( IExec ((f := p),P,s)) . a) = (( Result ((P +* (f := p)),(s +* ( Initialize (( intloc 0 ) .--> 1))))) . a)

        .= (s1 . a) by A1, A2, A4, SCMFSA_7: 7

        .= (s . a) by A3, FUNCT_4: 11;

      end;

      let g be FinSeq-Location;

      assume

       A5: g <> f;

      g <> ( intloc 0 ) & g <> ( IC SCM+FSA ) by SCMFSA_2: 57, SCMFSA_2: 58;

      then

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

      

      thus (( IExec ((f := p),P,s)) . g) = (( Result ((P +* (f := p)),(s +* ( Initialize (( intloc 0 ) .--> 1))))) . g)

      .= (s1 . g) by A1, A2, A5, SCMFSA_7: 7

      .= (s . g) by A6, FUNCT_4: 11;

    end;

    definition

      let i be Instruction of SCM+FSA ;

      let a be Int-Location;

      :: SCMFSA7B:def1

      pred i refers a means not for b be Int-Location, l be Nat holds for f be FinSeq-Location holds (b := a) <> i & ( AddTo (b,a)) <> i & ( SubFrom (b,a)) <> i & ( MultBy (b,a)) <> i & ( Divide (b,a)) <> i & ( Divide (a,b)) <> i & (a =0_goto l) <> i & (a >0_goto l) <> i & (b := (f,a)) <> i & ((f,b) := a) <> i & ((f,a) := b) <> i & (f :=<0,...,0> a) <> i;

    end

    definition

      let I be preProgram of SCM+FSA ;

      let a be Int-Location;

      :: SCMFSA7B:def2

      pred I refers a means ex i be Instruction of SCM+FSA st i in ( rng I) & i refers a;

    end

    definition

      let i be Instruction of SCM+FSA ;

      let a be Int-Location;

      :: SCMFSA7B:def3

      pred i destroys a means not for b be Int-Location holds for f be FinSeq-Location holds (a := b) <> i & ( AddTo (a,b)) <> i & ( SubFrom (a,b)) <> i & ( MultBy (a,b)) <> i & ( Divide (a,b)) <> i & ( Divide (b,a)) <> i & (a := (f,b)) <> i & (a :=len f) <> i;

    end

    definition

      let I be NAT -definedthe InstructionsF of SCM+FSA -valued Function;

      let a be Int-Location;

      :: SCMFSA7B:def4

      pred I destroys a means ex i be Instruction of SCM+FSA st i in ( rng I) & i destroys a;

    end

    definition

      let I be NAT -definedthe InstructionsF of SCM+FSA -valued Function;

      :: SCMFSA7B:def5

      attr I is good means not I destroys ( intloc 0 );

    end

    theorem :: SCMFSA7B:5

    for a be Int-Location holds not ( halt SCM+FSA ) destroys a;

    theorem :: SCMFSA7B:6

    

     Th6: for a,b,c be Int-Location holds a <> b implies not (b := c) destroys a

    proof

      let a,b,c be Int-Location;

      assume

       A1: a <> b;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let f be FinSeq-Location;

        thus (a := e) <> (b := c) by A1, SF_MASTR: 1;

        

         A2: ( InsCode (b := c)) = 1 by SCMFSA_2: 18;

        hence ( AddTo (a,e)) <> (b := c) by SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> (b := c) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> (b := c) by A2, SCMFSA_2: 21;

        thus ( Divide (a,e)) <> (b := c) & ( Divide (e,a)) <> (b := c) by A2, SCMFSA_2: 22;

        thus (a := (f,e)) <> (b := c) by A2, SCMFSA_2: 26;

        thus (a :=len f) <> (b := c) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:7

    

     Th7: for a,b,c be Int-Location holds a <> b implies not ( AddTo (b,c)) destroys a

    proof

      let a,b,c be Int-Location;

      assume

       A1: a <> b;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let f be FinSeq-Location;

        

         A2: ( InsCode ( AddTo (b,c))) = 2 by SCMFSA_2: 19;

        hence (a := e) <> ( AddTo (b,c)) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> ( AddTo (b,c)) by A1, SF_MASTR: 2;

        thus ( SubFrom (a,e)) <> ( AddTo (b,c)) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> ( AddTo (b,c)) by A2, SCMFSA_2: 21;

        thus ( Divide (a,e)) <> ( AddTo (b,c)) & ( Divide (e,a)) <> ( AddTo (b,c)) by A2, SCMFSA_2: 22;

        thus (a := (f,e)) <> ( AddTo (b,c)) by A2, SCMFSA_2: 26;

        thus (a :=len f) <> ( AddTo (b,c)) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:8

    

     Th8: for a,b,c be Int-Location holds a <> b implies not ( SubFrom (b,c)) destroys a

    proof

      let a,b,c be Int-Location;

      assume

       A1: a <> b;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let f be FinSeq-Location;

        

         A2: ( InsCode ( SubFrom (b,c))) = 3 by SCMFSA_2: 20;

        hence (a := e) <> ( SubFrom (b,c)) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> ( SubFrom (b,c)) by A2, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> ( SubFrom (b,c)) by A1, SF_MASTR: 3;

        thus ( MultBy (a,e)) <> ( SubFrom (b,c)) by A2, SCMFSA_2: 21;

        thus ( Divide (a,e)) <> ( SubFrom (b,c)) & ( Divide (e,a)) <> ( SubFrom (b,c)) by A2, SCMFSA_2: 22;

        thus (a := (f,e)) <> ( SubFrom (b,c)) by A2, SCMFSA_2: 26;

        thus (a :=len f) <> ( SubFrom (b,c)) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:9

    for a,b,c be Int-Location holds a <> b implies not ( MultBy (b,c)) destroys a

    proof

      let a,b,c be Int-Location;

      assume

       A1: a <> b;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let f be FinSeq-Location;

        

         A2: ( InsCode ( MultBy (b,c))) = 4 by SCMFSA_2: 21;

        hence (a := e) <> ( MultBy (b,c)) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> ( MultBy (b,c)) by A2, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> ( MultBy (b,c)) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> ( MultBy (b,c)) by A1, SF_MASTR: 4;

        thus ( Divide (a,e)) <> ( MultBy (b,c)) & ( Divide (e,a)) <> ( MultBy (b,c)) by A2, SCMFSA_2: 22;

        thus (a := (f,e)) <> ( MultBy (b,c)) by A2, SCMFSA_2: 26;

        thus (a :=len f) <> ( MultBy (b,c)) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:10

    for a,b,c be Int-Location holds a <> b & a <> c implies not ( Divide (b,c)) destroys a

    proof

      let a,b,c be Int-Location;

      assume

       A1: a <> b & a <> c;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let h be FinSeq-Location;

        

         A2: ( InsCode ( Divide (b,c))) = 5 by SCMFSA_2: 22;

        hence (a := e) <> ( Divide (b,c)) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> ( Divide (b,c)) by A2, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> ( Divide (b,c)) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> ( Divide (b,c)) by A2, SCMFSA_2: 21;

        thus ( Divide (e,a)) <> ( Divide (b,c)) & ( Divide (a,e)) <> ( Divide (b,c)) by A1, SF_MASTR: 5;

        thus (a := (h,e)) <> ( Divide (b,c)) by A2, SCMFSA_2: 26;

        thus (a :=len h) <> ( Divide (b,c)) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:11

    for a be Int-Location, l be Nat holds not ( goto l) destroys a;

    theorem :: SCMFSA7B:12

    for a,b be Int-Location, l be Nat holds not (b =0_goto l) destroys a;

    theorem :: SCMFSA7B:13

    for a,b be Int-Location, l be Nat holds not (b >0_goto l) destroys a;

    theorem :: SCMFSA7B:14

    for a,b,c be Int-Location, f be FinSeq-Location holds a <> b implies not (b := (f,c)) destroys a

    proof

      let a,b,c be Int-Location;

      let f be FinSeq-Location;

      assume

       A1: a <> b;

      now

        let e be Int-Location;

        let l be Element of NAT ;

        let h be FinSeq-Location;

        

         A2: ( InsCode (b := (f,c))) = 9 by SCMFSA_2: 26;

        hence (a := e) <> (b := (f,c)) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> (b := (f,c)) by A2, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> (b := (f,c)) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> (b := (f,c)) by A2, SCMFSA_2: 21;

        thus ( Divide (a,e)) <> (b := (f,c)) & ( Divide (e,a)) <> (b := (f,c)) by A2, SCMFSA_2: 22;

        thus (a := (h,e)) <> (b := (f,c)) by A1, SF_MASTR: 9;

        thus (a :=len h) <> (b := (f,c)) by A2, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:15

    for a,b,c be Int-Location, f be FinSeq-Location holds not ((f,c) := b) destroys a

    proof

      let a,b,c be Int-Location;

      let f be FinSeq-Location;

      now

        let e be Int-Location;

        let h be FinSeq-Location;

        

         A1: ( InsCode ((f,c) := b)) = 10 by SCMFSA_2: 27;

        hence (a := e) <> ((f,c) := b) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> ((f,c) := b) by A1, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> ((f,c) := b) by A1, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> ((f,c) := b) by A1, SCMFSA_2: 21;

        thus ( Divide (e,a)) <> ((f,c) := b) & ( Divide (a,e)) <> ((f,c) := b) by A1, SCMFSA_2: 22;

        thus (a := (h,e)) <> ((f,c) := b) by A1, SCMFSA_2: 26;

        thus (a :=len h) <> ((f,c) := b) by A1, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:16

    for a,b be Int-Location, f be FinSeq-Location holds a <> b implies not (b :=len f) destroys a

    proof

      let a,b be Int-Location;

      let f be FinSeq-Location;

      assume

       A1: a <> b;

      now

        let c be Int-Location;

        let g be FinSeq-Location;

        

         A2: ( InsCode (b :=len f)) = 11 by SCMFSA_2: 28;

        hence (a := c) <> (b :=len f) by SCMFSA_2: 18;

        thus ( AddTo (a,c)) <> (b :=len f) by A2, SCMFSA_2: 19;

        thus ( SubFrom (a,c)) <> (b :=len f) by A2, SCMFSA_2: 20;

        thus ( MultBy (a,c)) <> (b :=len f) by A2, SCMFSA_2: 21;

        thus ( Divide (a,c)) <> (b :=len f) & ( Divide (c,a)) <> (b :=len f) by A2, SCMFSA_2: 22;

        thus (a := (g,c)) <> (b :=len f) by A2, SCMFSA_2: 26;

        thus (a :=len g) <> (b :=len f) by A1, SF_MASTR: 11;

      end;

      hence thesis;

    end;

    theorem :: SCMFSA7B:17

    for a,b be Int-Location, f be FinSeq-Location holds not (f :=<0,...,0> b) destroys a

    proof

      let a,b be Int-Location;

      let f be FinSeq-Location;

      now

        let e be Int-Location;

        let h be FinSeq-Location;

        

         A1: ( InsCode (f :=<0,...,0> b)) = 12 by SCMFSA_2: 29;

        hence (a := e) <> (f :=<0,...,0> b) by SCMFSA_2: 18;

        thus ( AddTo (a,e)) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 19;

        thus ( SubFrom (a,e)) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 20;

        thus ( MultBy (a,e)) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 21;

        thus ( Divide (a,e)) <> (f :=<0,...,0> b) & ( Divide (e,a)) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 22;

        thus (a := (h,e)) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 26;

        thus (a :=len h) <> (f :=<0,...,0> b) by A1, SCMFSA_2: 28;

      end;

      hence thesis;

    end;

    ::$Canceled

    definition

      let I be Program of SCM+FSA ;

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

      :: SCMFSA7B:def6

      pred I is_halting_on s,P means (P +* I) halts_on ( Initialize s);

    end

    ::$Canceled

    theorem :: SCMFSA7B:19

    for I be Program of SCM+FSA holds I is parahalting iff for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds I is_halting_on (s,P)

    proof

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

      let I be Program of SCM+FSA ;

      thus I is parahalting implies for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds I is_halting_on (s,P) by FUNCT_4: 25;

      assume

       A1: for s be State of SCM+FSA holds for P be Instruction-Sequence of SCM+FSA holds I is_halting_on (s,P);

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

      

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

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

       A3: I c= P;

      

       A4: P = (P +* I) by A3, FUNCT_4: 98;

      

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

      I is_halting_on (s,P) by A1;

      hence P halts_on s by A4, A5;

    end;

    theorem :: SCMFSA7B:20

    

     Th19: for i be Instruction of SCM+FSA , a be Int-Location, s be State of SCM+FSA st not i destroys a holds (( Exec (i,s)) . a) = (s . a)

    proof

      let i be Instruction of SCM+FSA ;

      let a be Int-Location;

      let s be State of SCM+FSA ;

      assume

       A1: not i destroys a;

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

      per cases ;

        suppose ( InsCode i) = 0 ;

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

        hence thesis by EXTPRO_1:def 3;

      end;

        suppose ( InsCode i) = 1;

        then

        consider da,db be Int-Location such that

         A2: i = (da := db) by SCMFSA_2: 30;

        da <> a by A1, A2;

        hence thesis by A2, SCMFSA_2: 63;

      end;

        suppose ( InsCode i) = 2;

        then

        consider da,db be Int-Location such that

         A3: i = ( AddTo (da,db)) by SCMFSA_2: 31;

        da <> a by A1, A3;

        hence thesis by A3, SCMFSA_2: 64;

      end;

        suppose ( InsCode i) = 3;

        then

        consider da,db be Int-Location such that

         A4: i = ( SubFrom (da,db)) by SCMFSA_2: 32;

        da <> a by A1, A4;

        hence thesis by A4, SCMFSA_2: 65;

      end;

        suppose ( InsCode i) = 4;

        then

        consider da,db be Int-Location such that

         A5: i = ( MultBy (da,db)) by SCMFSA_2: 33;

        da <> a by A1, A5;

        hence thesis by A5, SCMFSA_2: 66;

      end;

        suppose ( InsCode i) = 5;

        then

        consider da,db be Int-Location such that

         A6: i = ( Divide (da,db)) by SCMFSA_2: 34;

        da <> a & db <> a by A1, A6;

        hence thesis by A6, SCMFSA_2: 67;

      end;

        suppose ( InsCode i) = 6;

        then ex loc be Nat st i = ( goto loc) by SCMFSA_2: 35;

        hence thesis by SCMFSA_2: 69;

      end;

        suppose ( InsCode i) = 7;

        then ex loc be Nat, da be Int-Location st i = (da =0_goto loc) by SCMFSA_2: 36;

        hence thesis by SCMFSA_2: 70;

      end;

        suppose ( InsCode i) = 8;

        then ex loc be Nat, da be Int-Location st i = (da >0_goto loc) by SCMFSA_2: 37;

        hence thesis by SCMFSA_2: 71;

      end;

        suppose ( InsCode i) = 9;

        then

        consider db,da be Int-Location, g be FinSeq-Location such that

         A7: i = (da := (g,db)) by SCMFSA_2: 38;

        da <> a by A1, A7;

        hence thesis by A7, SCMFSA_2: 72;

      end;

        suppose ( InsCode i) = 10;

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

        hence thesis by SCMFSA_2: 73;

      end;

        suppose ( InsCode i) = 11;

        then

        consider da be Int-Location, g be FinSeq-Location such that

         A8: i = (da :=len g) by SCMFSA_2: 40;

        da <> a by A1, A8;

        hence thesis by A8, SCMFSA_2: 74;

      end;

        suppose ( InsCode i) = 12;

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

        hence thesis by SCMFSA_2: 75;

      end;

    end;

    theorem :: SCMFSA7B:21

    

     Th20: for s be State of SCM+FSA , P be Instruction-Sequence of SCM+FSA , I be really-closed Program of SCM+FSA , a be Int-Location st not I destroys a holds for k be Nat holds (( Comput ((P +* I),( Initialize s),k)) . a) = (s . a)

    proof

      let s be State of SCM+FSA ;

      let P be Instruction-Sequence of SCM+FSA ;

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

      let a be Int-Location;

      assume

       A1: not I destroys a;

      defpred P[ Nat] means (( Comput ((P +* I),( Initialize s),$1)) . a) = (s . a);

      

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

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        set l = ( IC ( Comput ((P +* I),( Initialize s),k)));

        ( IC ( Initialize s)) = 0 by MEMSTR_0: 47;

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

        then

         A5: l in ( dom I) by A2, AMISTD_1: 21;

        then ((P +* I) . l) = (I . l) by A2, GRFUNC_1: 2;

        then ((P +* I) . l) in ( rng I) by A5, FUNCT_1:def 3;

        then

         A6: not ((P +* I) . l) destroys a by A1;

        

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

        (( Comput ((P +* I),( Initialize s),(k + 1))) . a) = (( Following ((P +* I),( Comput ((P +* I),( Initialize s),k)))) . a) by EXTPRO_1: 3

        .= (( Exec (((P +* I) . ( IC ( Comput ((P +* I),( Initialize s),k)))),( Comput ((P +* I),( Initialize s),k)))) . a) by A7, PARTFUN1:def 6

        .= (( Comput ((P +* I),(s +* ( Start-At ( 0 , SCM+FSA ))),k)) . a) by A6, Th19

        .= (s . a) by A4;

        hence P[(k + 1)];

      end;

      

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

      (( Comput ((P +* I),( Initialize s), 0 )) . a) = (( Initialize s) . a)

      .= (s . a) by A8, FUNCT_4: 11;

      then

       A9: P[ 0 ];

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

    end;

    registration

      cluster ( Stop SCM+FSA ) -> parahalting good;

      coherence

      proof

        thus ( Stop SCM+FSA ) is parahalting;

        let i be Instruction of SCM+FSA ;

        

         A6: ( rng ( Stop SCM+FSA )) = {( halt SCM+FSA )} by AFINSQ_1: 33;

        assume i in ( rng ( Stop SCM+FSA ));

        then i = ( halt SCM+FSA ) by A6, TARSKI:def 1;

        hence not i destroys ( intloc 0 );

      end;

    end

    registration

      cluster parahalting good halt-ending unique-halt for Program of SCM+FSA ;

      existence

      proof

        take ( Stop SCM+FSA );

        thus thesis;

      end;

    end

    registration

      cluster really-closed good -> keeping_0 for Program of SCM+FSA ;

      correctness

      proof

        let I be Program of SCM+FSA ;

        assume

         A1: I is really-closed good;

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

        

         A2: ( Initialize s) = s by MEMSTR_0: 44;

        let P such that

         A3: I c= P;

        let k be Nat;

        (P +* I) = P by A3, FUNCT_4: 98;

        hence (( Comput (P,s,k)) . ( intloc 0 )) = (s . ( intloc 0 )) by A1, A2, Th20;

      end;

    end

    theorem :: SCMFSA7B:22

    

     Th21: for a be Int-Location, k be Integer holds ( rng ( aSeq (a,k))) c= {(a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))}

    proof

      let a be Int-Location;

      let k be Integer;

      let x be object;

      assume

       A1: x in ( rng ( aSeq (a,k)));

      per cases ;

        suppose

         A2: k > 0 & k = ( 0 + 1);

        then ex k1 be Nat st (k1 + 1) = k & ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) by SCMFSA_7:def 2;

        

        then ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ {} ) by A2

        .= <%(a := ( intloc 0 ))%>;

        then ( rng ( aSeq (a,k))) = {(a := ( intloc 0 ))} by AFINSQ_1: 33;

        then x = (a := ( intloc 0 )) by A1, TARSKI:def 1;

        hence x in {(a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by ENUMSET1:def 1;

      end;

        suppose

         A3: k > 0 & k <> 1;

        then

        consider k1 be Nat such that

         A4: (k1 + 1) = k and

         A5: ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) by SCMFSA_7:def 2;

        

         A6: k1 <> 0 by A3, A4;

        ( rng ( aSeq (a,k))) = (( rng <%(a := ( intloc 0 ))%>) \/ ( rng (k1 --> ( AddTo (a,( intloc 0 )))))) by A5, AFINSQ_1: 26

        .= ( {(a := ( intloc 0 ))} \/ ( rng (k1 --> ( AddTo (a,( intloc 0 )))))) by AFINSQ_1: 33

        .= ( {(a := ( intloc 0 ))} \/ {( AddTo (a,( intloc 0 )))}) by A6, FUNCOP_1: 8;

        then x in {(a := ( intloc 0 ))} or x in {( AddTo (a,( intloc 0 )))} by A1, XBOOLE_0:def 3;

        then x = (a := ( intloc 0 )) or x = ( AddTo (a,( intloc 0 ))) by TARSKI:def 1;

        hence x in {(a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by ENUMSET1:def 1;

      end;

        suppose

         A7: not k > 0 ;

        then

        consider k1 be Nat such that

         A8: (k1 + k) = 1 and

         A9: ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) by SCMFSA_7:def 2;

        

         A10: k1 <> 0 by A7, A8;

        ( rng ( aSeq (a,k))) = (( rng <%(a := ( intloc 0 ))%>) \/ ( rng (k1 --> ( SubFrom (a,( intloc 0 )))))) by A9, AFINSQ_1: 26

        .= ( {(a := ( intloc 0 ))} \/ ( rng (k1 --> ( SubFrom (a,( intloc 0 )))))) by AFINSQ_1: 33

        .= ( {(a := ( intloc 0 ))} \/ {( SubFrom (a,( intloc 0 )))}) by A10, FUNCOP_1: 8;

        then x in {(a := ( intloc 0 ))} or x in {( SubFrom (a,( intloc 0 )))} by A1, XBOOLE_0:def 3;

        then x = (a := ( intloc 0 )) or x = ( SubFrom (a,( intloc 0 ))) by TARSKI:def 1;

        hence x in {(a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by ENUMSET1:def 1;

      end;

    end;

    theorem :: SCMFSA7B:23

    

     Th22: for a be Int-Location, k be Integer holds ( rng (a := k)) c= {( halt SCM+FSA ), (a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))}

    proof

      let a be Int-Location;

      let k be Integer;

      let x be object;

      

       A1: ( rng ( aSeq (a,k))) c= {(a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by Th21;

      

       A2: ( rng (a := k)) = ( rng (( aSeq (a,k)) ^ ( Stop SCM+FSA ))) by SCMFSA_7: 1

      .= (( rng ( aSeq (a,k))) \/ ( rng ( Stop SCM+FSA ))) by AFINSQ_1: 26

      .= (( rng ( aSeq (a,k))) \/ {( halt SCM+FSA )}) by AFINSQ_1: 33;

      assume x in ( rng (a := k));

      then x in ( rng ( aSeq (a,k))) or x in {( halt SCM+FSA )} by A2, XBOOLE_0:def 3;

      then x = (a := ( intloc 0 )) or x = ( AddTo (a,( intloc 0 ))) or x = ( SubFrom (a,( intloc 0 ))) or x = ( halt SCM+FSA ) by A1, ENUMSET1:def 1, TARSKI:def 1;

      hence x in {( halt SCM+FSA ), (a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by ENUMSET1:def 2;

    end;

    registration

      let a be read-write Int-Location, k be Integer;

      cluster (a := k) -> good;

      correctness

      proof

        now

          let i be Instruction of SCM+FSA ;

          

           A1: ( rng (a := k)) c= {( halt SCM+FSA ), (a := ( intloc 0 )), ( AddTo (a,( intloc 0 ))), ( SubFrom (a,( intloc 0 )))} by Th22;

          assume

           A2: i in ( rng (a := k));

          per cases by A2, A1, ENUMSET1:def 2;

            suppose i = ( halt SCM+FSA );

            hence not i destroys ( intloc 0 );

          end;

            suppose i = (a := ( intloc 0 ));

            hence not i destroys ( intloc 0 ) by Th6;

          end;

            suppose i = ( AddTo (a,( intloc 0 )));

            hence not i destroys ( intloc 0 ) by Th7;

          end;

            suppose i = ( SubFrom (a,( intloc 0 )));

            hence not i destroys ( intloc 0 ) by Th8;

          end;

        end;

        then not (a := k) destroys ( intloc 0 );

        hence thesis;

      end;

    end

    reserve n for Nat;

    registration

      let a be read-write Int-Location, k be Integer;

      cluster (a := k) -> really-closed;

      correctness

      proof

        per cases ;

          suppose k > 0 ;

          then

          consider k1 be Nat such that (k1 + 1) = k and

           A1: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by SCMFSA_7:def 1;

          defpred P[ Nat] means (( <%(a := ( intloc 0 ))%> ^ ($1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

          (( <%(a := ( intloc 0 ))%> ^ ( 0 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) = (( <%(a := ( intloc 0 ))%> ^ {} ) ^ ( Stop SCM+FSA ))

          .= ( <%(a := ( intloc 0 ))%> ^ ( Stop SCM+FSA ))

          .= ( Macro (a := ( intloc 0 )));

          then (( <%(a := ( intloc 0 ))%> ^ ( 0 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

          then

           A2: P[ 0 ];

          

           A3: for n st P[n] holds P[(n + 1)]

          proof

            let n;

            assume

             A4: P[n];

            set p1 = (n --> ( AddTo (a,( intloc 0 ))));

            now

              per cases ;

                suppose n is empty;

                then p1 is empty;

                then ( <%(a := ( intloc 0 ))%> ^ p1) = <%(a := ( intloc 0 ))%>;

                hence ( <%(a := ( intloc 0 ))%> ^ p1) is halt-free;

              end;

                suppose

                 A5: n is non empty;

                then p1 is non empty;

                then

                reconsider pp = p1 as Program of SCM+FSA ;

                ( rng pp) = {( AddTo (a,( intloc 0 )))} by A5, FUNCOP_1: 8;

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

                then pp is halt-free by COMPOS_1:def 11;

                hence ( <%(a := ( intloc 0 ))%> ^ p1) is halt-free;

              end;

            end;

            then

            reconsider p = ( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) as halt-free Program of SCM+FSA ;

            set m = (( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ));

            m = ( stop p);

            then

            reconsider m as really-closed MacroInstruction of SCM+FSA by A4;

            

             A7: ( CutLastLoc m) = ( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) by AFINSQ_2: 83;

            

             A8: ( card ( CutLastLoc m)) = (( card m) -' 1) by VALUED_1: 65;

            (( <%(a := ( intloc 0 ))%> ^ (( Segm (n + 1)) --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) = (( <%(a := ( intloc 0 ))%> ^ ((( Segm n) --> ( AddTo (a,( intloc 0 )))) ^ <%( AddTo (a,( intloc 0 )))%>)) ^ ( Stop SCM+FSA )) by AFINSQ_1: 87

            .= ((( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) ^ <%( AddTo (a,( intloc 0 )))%>) ^ ( Stop SCM+FSA )) by AFINSQ_1: 27

            .= (( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) ^ ( <%( AddTo (a,( intloc 0 )))%> ^ ( Stop SCM+FSA ))) by AFINSQ_1: 27

            .= (( <%(a := ( intloc 0 ))%> ^ (n --> ( AddTo (a,( intloc 0 ))))) ^ ( Macro ( AddTo (a,( intloc 0 )))))

            .= (( CutLastLoc m) +* ( Shift (( Macro ( AddTo (a,( intloc 0 )))),(( card m) -' 1)))) by A7, A8, AFINSQ_1: 77

            .= (( CutLastLoc m) +* ( Shift (( Macro ( IncAddr (( AddTo (a,( intloc 0 ))),(( card m) -' 1)))),(( card m) -' 1)))) by COMPOS_0: 4

            .= (( CutLastLoc m) +* ( Shift (( IncAddr (( Macro ( AddTo (a,( intloc 0 )))),(( card m) -' 1))),(( card m) -' 1)))) by COMPOS_1: 74

            .= (( CutLastLoc m) +* ( Reloc (( Macro ( AddTo (a,( intloc 0 )))),(( card m) -' 1))))

            .= (m ';' ( Macro ( AddTo (a,( intloc 0 )))))

            .= (m ';' ( AddTo (a,( intloc 0 ))));

            then (( <%(a := ( intloc 0 ))%> ^ ((n + 1) --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

            hence P[(n + 1)];

          end;

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

          hence thesis by A1;

        end;

          suppose k <= 0 ;

          then

          consider k1 be Nat such that (k1 + k) = 1 and

           A9: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by SCMFSA_7:def 1;

          defpred P[ Nat] means (( <%(a := ( intloc 0 ))%> ^ ($1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

          (( <%(a := ( intloc 0 ))%> ^ ( 0 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) = (( <%(a := ( intloc 0 ))%> ^ {} ) ^ ( Stop SCM+FSA ))

          .= ( <%(a := ( intloc 0 ))%> ^ ( Stop SCM+FSA ))

          .= ( Macro (a := ( intloc 0 )));

          then (( <%(a := ( intloc 0 ))%> ^ ( 0 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

          then

           A10: P[ 0 ];

          

           A11: for n st P[n] holds P[(n + 1)]

          proof

            let n;

            assume

             A12: P[n];

            set p1 = (n --> ( SubFrom (a,( intloc 0 ))));

            now

              per cases ;

                suppose n is empty;

                then p1 is empty;

                then ( <%(a := ( intloc 0 ))%> ^ p1) = <%(a := ( intloc 0 ))%>;

                hence ( <%(a := ( intloc 0 ))%> ^ p1) is halt-free;

              end;

                suppose

                 A13: n is non empty;

                then p1 is non empty;

                then

                reconsider pp = p1 as Program of SCM+FSA ;

                ( rng pp) = {( SubFrom (a,( intloc 0 )))} by A13, FUNCOP_1: 8;

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

                then pp is halt-free by COMPOS_1:def 11;

                hence ( <%(a := ( intloc 0 ))%> ^ p1) is halt-free;

              end;

            end;

            then

            reconsider p = ( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) as halt-free Program of SCM+FSA ;

            set m = (( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ));

            m = ( stop p);

            then

            reconsider m as really-closed MacroInstruction of SCM+FSA by A12;

            

             A15: ( CutLastLoc m) = ( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) by AFINSQ_2: 83;

            

             A16: ( card ( CutLastLoc m)) = (( card m) -' 1) by VALUED_1: 65;

            (( <%(a := ( intloc 0 ))%> ^ (( Segm (n + 1)) --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) = (( <%(a := ( intloc 0 ))%> ^ ((( Segm n) --> ( SubFrom (a,( intloc 0 )))) ^ <%( SubFrom (a,( intloc 0 )))%>)) ^ ( Stop SCM+FSA )) by AFINSQ_1: 87

            .= ((( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) ^ <%( SubFrom (a,( intloc 0 )))%>) ^ ( Stop SCM+FSA )) by AFINSQ_1: 27

            .= (( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) ^ ( <%( SubFrom (a,( intloc 0 )))%> ^ ( Stop SCM+FSA ))) by AFINSQ_1: 27

            .= (( <%(a := ( intloc 0 ))%> ^ (n --> ( SubFrom (a,( intloc 0 ))))) ^ ( Macro ( SubFrom (a,( intloc 0 )))))

            .= (( CutLastLoc m) +* ( Shift (( Macro ( SubFrom (a,( intloc 0 )))),(( card m) -' 1)))) by A15, A16, AFINSQ_1: 77

            .= (( CutLastLoc m) +* ( Shift (( Macro ( IncAddr (( SubFrom (a,( intloc 0 ))),(( card m) -' 1)))),(( card m) -' 1)))) by COMPOS_0: 4

            .= (( CutLastLoc m) +* ( Shift (( IncAddr (( Macro ( SubFrom (a,( intloc 0 )))),(( card m) -' 1))),(( card m) -' 1)))) by COMPOS_1: 74

            .= (( CutLastLoc m) +* ( Reloc (( Macro ( SubFrom (a,( intloc 0 )))),(( card m) -' 1))))

            .= (m ';' ( Macro ( SubFrom (a,( intloc 0 )))))

            .= (m ';' ( SubFrom (a,( intloc 0 ))));

            then (( <%(a := ( intloc 0 ))%> ^ ((n + 1) --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) is really-closed;

            hence P[(n + 1)];

          end;

          for n holds P[n] from NAT_1:sch 2( A10, A11);

          hence thesis by A9;

        end;

      end;

    end

    registration

      let a be read-write Int-Location, k be Integer;

      cluster (a := k) -> keeping_0;

      correctness ;

    end