scmfsa_7.miz



    begin

    reserve m for Nat;

    reserve P for the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ;

    

     Lm1: for p1,p2,p3,p4 be XFinSequence holds (((p1 ^ p2) ^ p3) ^ p4) = ((p1 ^ p2) ^ (p3 ^ p4)) & (((p1 ^ p2) ^ p3) ^ p4) = (p1 ^ ((p2 ^ p3) ^ p4)) & (((p1 ^ p2) ^ p3) ^ p4) = (p1 ^ (p2 ^ (p3 ^ p4))) & (((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;

      

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

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

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

      thus thesis by AFINSQ_1: 27;

    end;

    

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

    proof

      let p1,p2,p3,p4,p5 be XFinSequence;

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

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = ((p1 ^ p2) ^ ((p3 ^ p4) ^ p5)) by Lm1;

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = ((p1 ^ p2) ^ (p3 ^ (p4 ^ p5))) by Lm1;

      

      thus

       A1: ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = ((p1 ^ ((p2 ^ p3) ^ p4)) ^ p5) by Lm1

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

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

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = (p1 ^ (p2 ^ ((p3 ^ p4) ^ p5))) by A1, Lm1;

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = (p1 ^ (p2 ^ (p3 ^ (p4 ^ p5)))) by A1, Lm1;

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = (((p1 ^ p2) ^ (p3 ^ p4)) ^ p5) by Lm1;

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = ((p1 ^ ((p2 ^ p3) ^ p4)) ^ p5) by Lm1;

      thus ((((p1 ^ p2) ^ p3) ^ p4) ^ p5) = ((p1 ^ (p2 ^ (p3 ^ p4))) ^ p5) by Lm1;

      thus thesis by A1, Lm1;

    end;

    deffunc U( Nat) = ($1 -' 1);

    definition

      let a be Int-Location;

      let k be Integer;

      :: SCMFSA_7:def1

      func a := k -> the InstructionsF of SCM+FSA -valued NAT -defined finite Function means

      : Def1: ex k1 be Nat st (k1 + 1) = k & it = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) if k > 0

      otherwise ex k1 be Nat st (k1 + k) = 1 & it = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ));

      existence

      proof

        thus k > 0 implies ex f be the InstructionsF of SCM+FSA -valued NAT -defined finite Function st ex k1 be Nat st (k1 + 1) = k & f = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA ))

        proof

          assume k > 0 ;

          then ( 0 + 1) <= k by INT_1: 7;

          then

          reconsider k1 = (k - 1) as Element of NAT by INT_1: 5;

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

          reconsider xx as the InstructionsF of SCM+FSA -valued NAT -defined finite Function;

          take xx, k1;

          thus (k1 + 1) = k;

          thus thesis;

        end;

        assume k <= 0 ;

        then

        reconsider k1 = (1 - k) as Element of NAT by INT_1: 5;

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

        reconsider xx as the InstructionsF of SCM+FSA -valued NAT -defined finite Function;

        take xx, k1;

        thus (k1 + k) = 1;

        thus thesis;

      end;

      uniqueness ;

      correctness ;

    end

    definition

      let a be Int-Location;

      let k be Integer;

      :: SCMFSA_7:def2

      func aSeq (a,k) -> XFinSequence of the InstructionsF of SCM+FSA means

      : Def2: ex k1 be Nat st (k1 + 1) = k & it = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) if k > 0

      otherwise ex k1 be Nat st (k1 + k) = 1 & it = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))));

      existence

      proof

        thus k > 0 implies ex s be XFinSequence of the InstructionsF of SCM+FSA , k1 be Nat st (k1 + 1) = k & s = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 )))))

        proof

          assume k > 0 ;

          then ( 0 + 1) <= k by INT_1: 7;

          then

          reconsider k1 = (k - 1) as Element of NAT by INT_1: 5;

          take ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))), k1;

          thus (k1 + 1) = k;

          thus thesis;

        end;

        assume k <= 0 ;

        then

        reconsider k1 = (1 - k) as Element of NAT by INT_1: 5;

        take ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))), k1;

        thus (k1 + k) = 1;

        thus thesis;

      end;

      uniqueness ;

      correctness ;

    end

    theorem :: SCMFSA_7:1

    for a be Int-Location, k be Integer holds (a := k) = (( aSeq (a,k)) ^ ( Stop SCM+FSA ))

    proof

      let a be Int-Location, k be Integer;

      per cases ;

        suppose k > 0 ;

        then ex k1 be Nat st (k1 + 1) = k & (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by Def1;

        hence thesis by Def2;

      end;

        suppose

         A1: k <= 0 ;

        then ex k1 be Nat st (k1 + k) = 1 & (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by Def1;

        hence thesis by A1, Def2;

      end;

    end;

    definition

      let f be FinSeq-Location;

      let p be FinSequence of INT ;

      :: SCMFSA_7:def3

      func aSeq (f,p) -> XFinSequence of the InstructionsF of SCM+FSA means

      : Def3: ex pp be XFinSequence of (the InstructionsF of SCM+FSA ^omega ) st ( 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 (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>)) & it = ( FlattenSeq pp);

      existence

      proof

        defpred P[ Integer, set] means ex i be Integer st (i = (p . ($1 + 1)) & $2 = ((( aSeq (( intloc 1),($1 + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>));

        set D = (the InstructionsF of SCM+FSA ^omega );

        

         A1: for k be Nat st k in ( Segm ( len p)) holds ex d be Element of D st P[k, d]

        proof

          let k be Nat;

          assume k in ( Segm ( len p));

          then k < ( len p) by NAT_1: 44;

          then 1 <= (k + 1) & (k + 1) <= ( len p) by NAT_1: 12, NAT_1: 13;

          then (k + 1) in ( dom p) by FINSEQ_3: 25;

          then (p . (k + 1)) in INT by FINSEQ_2: 11;

          then

          reconsider i = (p . (k + 1)) as Integer;

          reconsider d = ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>) as Element of D by AFINSQ_1:def 7;

          take d;

          thus thesis;

        end;

        consider pp be XFinSequence of D such that

         A2: ( dom pp) = ( Segm ( len p)) and

         A3: for k be Nat st k in ( Segm ( len p)) holds P[k, (pp . k)] from STIRL2_1:sch 5( A1);

        reconsider tt = ( FlattenSeq pp) as XFinSequence of the InstructionsF of SCM+FSA by AFINSQ_1:def 7;

        take tt, pp;

        thus ( len pp) = ( len p) by A2;

        thus for k be Nat st k < ( len pp) holds ex i be Integer st i = (p . (k + 1)) & ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>) = (pp . k) by A2, A3, NAT_1: 44;

        thus thesis;

      end;

      uniqueness

      proof

        reconsider i = ( len p) as Nat;

        let s1,s2 be XFinSequence of the InstructionsF of SCM+FSA such that

         A4: ex pp be XFinSequence of (the InstructionsF of SCM+FSA ^omega ) st ( 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 (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>)) & s1 = ( FlattenSeq pp) and

         A5: ex pp be XFinSequence of (the InstructionsF of SCM+FSA ^omega ) st ( 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 (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>)) & s2 = ( FlattenSeq pp);

        consider pp1 be XFinSequence of (the InstructionsF of SCM+FSA ^omega ) such that

         A6: ( len pp1) = ( len p) and

         A7: for k be Nat st k < ( len pp1) holds ex i be Integer st i = (p . (k + 1)) & (pp1 . k) = ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>) and

         A8: s1 = ( FlattenSeq pp1) by A4;

        consider pp2 be XFinSequence of (the InstructionsF of SCM+FSA ^omega ) such that

         A9: ( len pp2) = ( len p) and

         A10: for k be Nat st k < ( len pp2) holds ex i be Integer st i = (p . (k + 1)) & (pp2 . k) = ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i))) ^ <%((f,( intloc 1)) := ( intloc 2))%>) and

         A11: s2 = ( FlattenSeq pp2) by A5;

        for k be Nat st k < ( len pp1) holds (pp1 . k) = (pp2 . k)

        proof

          let k be Nat;

          assume

           A12: k < ( len pp1);

          (ex i1 be Integer st i1 = (p . (k + 1)) & (pp1 . k) = ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i1))) ^ <%((f,( intloc 1)) := ( intloc 2))%>)) & ex i2 be Integer st i2 = (p . (k + 1)) & (pp2 . k) = ((( aSeq (( intloc 1),(k + 1))) ^ ( aSeq (( intloc 2),i2))) ^ <%((f,( intloc 1)) := ( intloc 2))%>) by A7, A10, A12, A6, A9;

          hence (pp1 . k) = (pp2 . k);

        end;

        hence thesis by A8, A11, A6, A9, AFINSQ_1: 9;

      end;

      correctness ;

    end

    definition

      let f be FinSeq-Location;

      let p be FinSequence of INT ;

      :: SCMFSA_7:def4

      func f := p -> the InstructionsF of SCM+FSA -valued NAT -defined finite Function equals (((( aSeq (( intloc 1),( len p))) ^ <%(f :=<0,...,0> ( intloc 1))%>) ^ ( aSeq (f,p))) ^ ( Stop SCM+FSA ));

      correctness ;

    end

    theorem :: SCMFSA_7:2

    for a be Int-Location holds (a := 1) = ( <%(a := ( intloc 0 ))%> ^ ( Stop SCM+FSA ))

    proof

      let a be Int-Location;

      

       A1: ( 0 + 1) = 1;

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

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

      hence thesis by Def1, A1;

    end;

    theorem :: SCMFSA_7:3

    for a be Int-Location holds (a := 0 ) = (( <%(a := ( intloc 0 ))%> ^ <%( SubFrom (a,( intloc 0 )))%>) ^ ( Stop SCM+FSA ))

    proof

      let a be Int-Location;

      (1 + 0 ) = 1 & (( <%(a := ( intloc 0 ))%> ^ <%( SubFrom (a,( intloc 0 )))%>) ^ ( Stop SCM+FSA )) = (( <%(a := ( intloc 0 ))%> ^ (1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by CARD_1: 49;

      hence thesis by Def1;

    end;

    theorem :: SCMFSA_7:4

    

     Th4: for c0 be Nat holds for s be c0 -started State of SCM+FSA st (s . ( intloc 0 )) = 1 holds for a be Int-Location, k be Integer st a <> ( intloc 0 ) & (for c be Nat st c in ( dom ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . (c0 + c))) holds (for i be Nat st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i) & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f))) & (( Comput (P,s,( len ( aSeq (a,k))))) . a) = k

    proof

      let c0 be Nat;

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

      assume

       A1: (s . ( intloc 0 )) = 1;

      

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

      let a be Int-Location;

      let k be Integer;

      assume that

       A3: a <> ( intloc 0 ) and

       A4: for c be Nat st c in ( dom ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . (c0 + c));

      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, Def2;

        defpred Q[ Nat] means $1 <= k9 implies ( IC ( Comput (P,s,$1))) = (c0 + $1) & (1 <= $1 implies (( Comput (P,s,$1)) . a) = $1) & (for b be Int-Location st b <> a holds (( Comput (P,s,$1)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,$1)) . f) = (s . f));

        

         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: 33

        .= k9 by A6;

        

         A9: for i be Nat st i <= ( len ( aSeq (a,k9))) holds ( IC ( Comput (P,s,i))) = (c0 + i) & (1 <= i implies (( Comput (P,s,i)) . a) = i) & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f)

        proof

          

           A10: for i be Nat st i < k9 holds i in ( dom ( aSeq (a,k9))) by A8, AFINSQ_1: 86;

          

           A11: (P . (c0 + 0 )) = (( aSeq (a,k9)) . 0 ) by A5, A4, A10

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

           A12:

          now

            let n be Nat;

            assume n = 0 ;

            hence

             A13: ( Comput (P,s,n)) = s by EXTPRO_1: 2;

            hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A2, A11, PBOOLE: 143;

            

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

            .= ( Exec ((a := ( intloc 0 )),s)) by A2, A11, A13, PBOOLE: 143;

          end;

           A14:

          now

            let i be Nat;

            assume that

             A15: 1 <= i and

             A16: i < k9;

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

            i = (i1 + 1);

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

            then

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

            

             A18: ( 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 A15, A7, A18, A6, A16, AFINSQ_1: 18

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

          end;

           A19:

          now

            let i be Nat;

            assume that

             A20: 0 < i and

             A21: i < k9;

            

             A22: ( 0 + 1) <= i by A20, NAT_1: 13;

            

            thus (P . (c0 + i)) = (( aSeq (a,k9)) . i) by A4, A10, A21

            .= ( AddTo (a,( intloc 0 ))) by A14, A22, A21;

          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 A12

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

              hereby

                assume 1 <= (n + 1);

                

                thus (( Comput (P,s,(n + 1))) . a) = (( Exec ((a := ( intloc 0 )),s)) . a) by A12, A26

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

              end;

              hereby

                let b be Int-Location;

                assume

                 A27: b <> a;

                

                thus (( Comput (P,s,(n + 1))) . b) = (( Exec ((a := ( intloc 0 )),s)) . b) by A12, A26

                .= (s . b) by A27, SCMFSA_2: 63;

              end;

              let f be FinSeq-Location;

              

              thus (( Comput (P,s,(n + 1))) . f) = (( Exec ((a := ( intloc 0 )),s)) . f) by A12, A26

              .= (s . f) by SCMFSA_2: 63;

            end;

              suppose

               A28: n > 0 ;

              

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

              

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

              

              then

               A31: ( CurInstr (P,( Comput (P,s,n)))) = (P . (c0 + n)) by A24, A25, PBOOLE: 143, XXREAL_0: 2

              .= ( AddTo (a,( intloc 0 ))) by A19, A28, A29;

              

               A32: ( 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 A31;

              

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

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

              

               A33: ( 0 + 1) <= n by A28, INT_1: 7;

              hereby

                assume 1 <= (n + 1);

                

                thus (( Comput (P,s,(n + 1))) . a) = (n + (( Comput (P,s,n)) . ( intloc 0 ))) by A24, A25, A33, A30, A32, SCMFSA_2: 64, XXREAL_0: 2

                .= (n + 1) by A1, A3, A24, A25, A30, XXREAL_0: 2;

              end;

              hereby

                let b be Int-Location;

                assume

                 A34: b <> a;

                

                hence (( Comput (P,s,(n + 1))) . b) = (( Comput (P,s,n)) . b) by A32, SCMFSA_2: 64

                .= (s . b) by A24, A25, A30, A34, XXREAL_0: 2;

              end;

              let f be FinSeq-Location;

              

              thus (( Comput (P,s,(n + 1))) . f) = (( Comput (P,s,n)) . f) by A32, SCMFSA_2: 64

              .= (s . f) by A24, A25, A30, XXREAL_0: 2;

            end;

          end;

          

           A35: Q[ 0 ] by A2, EXTPRO_1: 2;

          

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

          let i be Nat;

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

          hence thesis by A8, A36;

        end;

        hence for i be Nat st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i) & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f);

        1 <= ( len ( aSeq (a,k))) by A6, A8, NAT_1: 11;

        hence thesis by A8, A9;

      end;

        suppose

         A37: 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) & (1 <= $1 implies (( Comput (P,s,$1)) . a) = ((( - $1) + 1) + 1)) & (for b be Int-Location st b <> a holds (( Comput (P,s,$1)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,$1)) . f) = (s . f));

        consider k1 be Nat such that

         A38: (k1 + k) = 1 and

         A39: ( aSeq (a,k)) = ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) by A37, Def2;

        

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

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

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

        

         A41: for i be Nat st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i) & (1 <= i implies (( Comput (P,s,i)) . a) = ((( - i) + 1) + 1)) & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f)

        proof

          

           A42: for i be Nat st i < ((mk + 1) + 1) holds i in ( dom ( aSeq (a,k))) by A40, AFINSQ_1: 86;

          

           A43: (P . (c0 + 0 )) = (( aSeq (a,k)) . 0 ) by A4, A42

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

          

           A44: for n be 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 Nat;

            assume n = 0 ;

            hence

             A45: ( Comput (P,s,n)) = s by EXTPRO_1: 2;

            hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A2, A43, PBOOLE: 143;

            

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

            .= ( Exec ((a := ( intloc 0 )),s)) by A2, A43, A45, PBOOLE: 143;

          end;

           A46:

          now

            let i be Nat;

            assume that

             A47: 1 <= i and

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

            

             A49: (i - 1) < (((mk + 1) + 1) - 1) by A48, XREAL_1: 9;

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

            

             A50: i1 in ( Segm k1) by A38, A49, NAT_1: 44;

            

             A51: ( 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 A39, A47, A51, A38, A48, AFINSQ_1: 18

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

          end;

           A52:

          now

            let i be Nat;

            assume that

             A53: 0 < i and

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

            

             A55: ( 0 + 1) <= i by A53, NAT_1: 13;

            

            thus (P . (c0 + i)) = (( aSeq (a,k)) . i) by A4, A42, A54

            .= ( SubFrom (a,( intloc 0 ))) by A46, A55, A54;

          end;

          

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

          proof

            let n be Nat;

            assume

             A57: Q[n];

            assume

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

            per cases ;

              suppose

               A59: n = 0 ;

              

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

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

              hereby

                assume 1 <= (n + 1);

                

                thus (( Comput (P,s,(n + 1))) . a) = (( Exec ((a := ( intloc 0 )),s)) . a) by A44, A59

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

              end;

              hereby

                let b be Int-Location;

                assume

                 A60: b <> a;

                

                thus (( Comput (P,s,(n + 1))) . b) = (( Exec ((a := ( intloc 0 )),s)) . b) by A44, A59

                .= (s . b) by A60, SCMFSA_2: 63;

              end;

              let f be FinSeq-Location;

              

              thus (( Comput (P,s,(n + 1))) . f) = (( Exec ((a := ( intloc 0 )),s)) . f) by A44, A59

              .= (s . f) by SCMFSA_2: 63;

            end;

              suppose

               A61: n > 0 ;

              

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

              

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

              

              then

               A64: ( CurInstr (P,( Comput (P,s,n)))) = (P . (c0 + n)) by A57, A58, PBOOLE: 143, XXREAL_0: 2

              .= ( SubFrom (a,( intloc 0 ))) by A52, A61, A62;

              

               A65: ( 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 A64;

              

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

              .= (c0 + (n + 1)) by A57, A58, A63, XXREAL_0: 2;

              

               A66: ( 0 + 1) < (n + 1) by A61, XREAL_1: 6;

              hereby

                assume 1 <= (n + 1);

                

                thus (( Comput (P,s,(n + 1))) . a) = (((( - n) + 1) + 1) - (( Comput (P,s,n)) . ( intloc 0 ))) by A57, A58, A66, A65, NAT_1: 13, SCMFSA_2: 65

                .= (((( - n) + 1) + 1) - (s . ( intloc 0 ))) by A3, A57, A58, A63, XXREAL_0: 2

                .= ((( - (n + 1)) + 1) + 1) by A1;

              end;

              hereby

                let b be Int-Location;

                assume

                 A67: b <> a;

                

                hence (( Comput (P,s,(n + 1))) . b) = (( Comput (P,s,n)) . b) by A65, SCMFSA_2: 65

                .= (s . b) by A57, A58, A63, A67, XXREAL_0: 2;

              end;

              let f be FinSeq-Location;

              

              thus (( Comput (P,s,(n + 1))) . f) = (( Comput (P,s,n)) . f) by A65, SCMFSA_2: 65

              .= (s . f) by A57, A58, A63, XXREAL_0: 2;

            end;

          end;

          

           A68: Q[ 0 ] by A2, EXTPRO_1: 2;

          

           A69: for i be Nat holds Q[i] from NAT_1:sch 2( A68, A56);

          let i be Nat;

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

          hence thesis by A40, A69;

        end;

        hence for i be Nat st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = (c0 + i) & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f);

        1 <= ( len ( aSeq (a,k))) by A40, NAT_1: 11;

        

        hence (( Comput (P,s,( len ( aSeq (a,k))))) . a) = ((( - (( - k) + (1 + 1))) + 1) + 1) by A40, A41

        .= k;

      end;

    end;

    theorem :: SCMFSA_7:5

    

     Th5: for s be 0 -started State of SCM+FSA st (s . ( intloc 0 )) = 1 holds for a be Int-Location holds for k be Integer st ( aSeq (a,k)) c= P & a <> ( intloc 0 ) holds (for i be Nat st i <= ( len ( aSeq (a,k))) holds ( IC ( Comput (P,s,i))) = i & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f))) & (( Comput (P,s,( len ( aSeq (a,k))))) . a) = k

    proof

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

      assume

       A1: (s . ( intloc 0 )) = 1;

      let a be Int-Location;

      let k be Integer;

      assume that

       A2: ( aSeq (a,k)) c= P and

       A3: a <> ( intloc 0 );

      

       A4: for c be Nat st c in ( dom ( aSeq (a,k))) holds (( aSeq (a,k)) . c) = (P . ( 0 + c)) by A2, GRFUNC_1: 2;

      hereby

        let i be Nat;

        assume

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

        then ( IC ( Comput (P,s,i))) = ( 0 + i) by A1, A3, A4, Th4;

        hence ( IC ( Comput (P,s,i))) = i & (for b be Int-Location st b <> a holds (( Comput (P,s,i)) . b) = (s . b)) & for f be FinSeq-Location holds (( Comput (P,s,i)) . f) = (s . f) by A1, A3, A4, A5, Th4;

      end;

      thus thesis by A1, A3, A4, Th4;

    end;

    theorem :: SCMFSA_7:6

    for s be 0 -started State of SCM+FSA st (s . ( intloc 0 )) = 1 holds for a be Int-Location, k be Integer st (a := k) c= P & a <> ( intloc 0 ) holds P halts_on s & (( Result (P,s)) . a) = k & (for b be Int-Location st b <> a holds (( Result (P,s)) . b) = (s . b)) & for f be FinSeq-Location holds (( Result (P,s)) . f) = (s . f)

    proof

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

      assume that

       A1: (s . ( intloc 0 )) = 1;

      

       A2: ( IC s) = 0 by MEMSTR_0:def 11;

      let a be Int-Location, k be Integer;

      assume that

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

       A4: a <> ( intloc 0 );

      per cases ;

        suppose

         A5: k > 0 ;

        then

        consider k1 be Nat such that

         A6: (k1 + 1) = k and

         A7: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by Def1;

        

         A8: ( 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: 33

        .= k by A6;

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

        defpred Q[ Nat] means $1 <= k implies (1 <= $1 implies (( Comput (P,s,$1)) . a) = $1) & (for b be Int-Location st b <> a holds (( Comput (P,s,$1)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,$1)) . f) = (s . f));

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

        

         A9: (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;

        

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

        .= (k + 1) by A8, AFINSQ_1: 33;

         A11:

        now

          let i be Nat;

          assume that

           A12: i <= k;

          i < ( len f) by A12, NAT_1: 13, A10;

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

        end;

        

         A13: for i be Nat st i <= k holds (P . i) = (f . i) by A3, A7, A11, GRFUNC_1: 2;

        then

         A14: (P . 0 ) = (a := ( intloc 0 )) by A9;

         A15:

        now

          let n be Nat;

          assume n = 0 ;

          hence

           A16: ( Comput (P,s,n)) = s by EXTPRO_1: 2;

          hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A2, A14, PBOOLE: 143;

          

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

          .= ( Exec ((a := ( intloc 0 )),s)) by A2, A14, A16, PBOOLE: 143;

        end;

         A17:

        now

          let i be Nat;

          assume that

           A18: 1 <= i and

           A19: i < k;

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

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

          then

           A20: i1 in ( Segm k1) by A6, NAT_1: 44;

          

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

          

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

          i in ( dom ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( AddTo (a,( intloc 0 )))))) by A19, A8, 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 A18, A19, A21, A22, A6, AFINSQ_1: 18

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

        end;

         A23:

        now

          let i be Nat;

          assume that

           A24: 0 < i and

           A25: i < k;

          

           A26: ( 0 + 1) <= i by A24, NAT_1: 13;

          

          thus (P . i) = (f . i) by A13, A25

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

        end;

        

         A27: for i be 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 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 A15

              .= (n + 1) by A2, 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, PBOOLE: 143, XXREAL_0: 2

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

              ( 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;

              hence ( IC ( Comput (P,s,(n + 1)))) = (n + 1) by A30, A31, NAT_1: 13, SCMFSA_2: 64;

            end;

          end;

          

           A36: P[ 0 ] by A2, EXTPRO_1: 2;

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

          hence thesis by A28;

        end;

        

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

        proof

          let n be Nat;

          assume

           A38: Q[n];

          assume

           A39: (n + 1) <= k;

          per cases ;

            suppose

             A40: n = 0 ;

            hereby

              assume 1 <= (n + 1);

              

              thus (( Comput (P,s,(n + 1))) . a) = (( Exec ((a := ( intloc 0 )),s)) . a) by A15, A40

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

            end;

            hereby

              let b be Int-Location;

              assume

               A41: b <> a;

              

              thus (( Comput (P,s,(n + 1))) . b) = (( Exec ((a := ( intloc 0 )),s)) . b) by A15, A40

              .= (s . b) by A41, SCMFSA_2: 63;

            end;

            let f be FinSeq-Location;

            

            thus (( Comput (P,s,(n + 1))) . f) = (( Exec ((a := ( intloc 0 )),s)) . f) by A15, A40

            .= (s . f) by SCMFSA_2: 63;

          end;

            suppose

             A42: n > 0 ;

            

             A43: n < k by A39, NAT_1: 13;

            

             A44: (P /. ( IC ( Comput (P,s,n)))) = (P . ( IC ( Comput (P,s,n)))) by PBOOLE: 143;

            

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

            

            then

             A46: ( CurInstr (P,( Comput (P,s,n)))) = (P . n) by A27, A39, A44, XXREAL_0: 2

            .= ( AddTo (a,( intloc 0 ))) by A23, A42, A43;

            

             A47: ( 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 A46;

            

             A48: ( 0 + 1) <= n by A42, INT_1: 7;

            hereby

              assume 1 <= (n + 1);

              

              thus (( Comput (P,s,(n + 1))) . a) = (n + (( Comput (P,s,n)) . ( intloc 0 ))) by A38, A39, A48, A45, A47, SCMFSA_2: 64, XXREAL_0: 2

              .= (n + 1) by A1, A4, A38, A39, A45, XXREAL_0: 2;

            end;

            hereby

              let b be Int-Location;

              assume

               A49: b <> a;

              

              hence (( Comput (P,s,(n + 1))) . b) = (( Comput (P,s,n)) . b) by A47, SCMFSA_2: 64

              .= (s . b) by A38, A39, A45, A49, XXREAL_0: 2;

            end;

            let f be FinSeq-Location;

            

            thus (( Comput (P,s,(n + 1))) . f) = (( Comput (P,s,n)) . f) by A47, SCMFSA_2: 64

            .= (s . f) by A38, A39, A45, XXREAL_0: 2;

          end;

        end;

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

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

        

        then

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

        .= ( halt SCM+FSA );

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

        then

         A51: 1 <= k by NAT_1: 13;

        

         A52: Q[ 0 ] by EXTPRO_1: 2;

        

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

        

         A54: (P /. ( IC ( Comput (P,s,k)))) = (P . ( IC ( Comput (P,s,k)))) by PBOOLE: 143;

        

         A55: ( CurInstr (P,( Comput (P,s,k)))) = (P . k) by A27, A54

        .= ( halt SCM+FSA ) by A50, A13;

        hence P halts_on s by EXTPRO_1: 29;

        then ( Comput (P,s,k)) = ( Result (P,s)) by A55, EXTPRO_1:def 9;

        hence thesis by A53, A51;

      end;

        suppose

         A56: k <= 0 ;

        then

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

        defpred Q[ Nat] means $1 <= ((mk + 1) + 1) implies (1 <= $1 implies (( Comput (P,s,$1)) . a) = ((( - $1) + 1) + 1)) & (for b be Int-Location st b <> a holds (( Comput (P,s,$1)) . b) = (s . b)) & (for f be FinSeq-Location holds (( Comput (P,s,$1)) . f) = (s . f));

        consider k1 be Nat such that

         A57: (k1 + k) = 1 and

         A58: (a := k) = (( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 ))))) ^ ( Stop SCM+FSA )) by A56, Def1;

        

         A59: ( 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: 33

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

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

        

         A60: (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;

        

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

        .= (((mk + 1) + 1) + 1) by A59, AFINSQ_1: 33;

         A62:

        now

          let i be Nat;

          assume that

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

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

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

        end;

        

         A64: for i be Nat st i <= ((mk + 1) + 1) holds (P . i) = (f . i) by A3, A58, GRFUNC_1: 2, A62;

        then

         A65: (P . 0 ) = (a := ( intloc 0 )) by A60;

         A66:

        now

          let n be Nat;

          assume n = 0 ;

          hence

           A67: ( Comput (P,s,n)) = s by EXTPRO_1: 2;

          hence ( CurInstr (P,( Comput (P,s,n)))) = (a := ( intloc 0 )) by A2, A65, PBOOLE: 143;

          

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

          .= ( Exec ((a := ( intloc 0 )),s)) by A2, A65, A67, PBOOLE: 143;

        end;

         A68:

        now

          

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

          let i be Nat;

          assume that

           A70: 1 <= i and

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

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

          (i - 1) < ((k1 + 1) - 1) by A71, A57, XREAL_1: 9;

          then

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

          

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

          i in ( dom ( <%(a := ( intloc 0 ))%> ^ (k1 --> ( SubFrom (a,( intloc 0 )))))) by A71, A59, 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 A57, A70, A71, A69, A73, AFINSQ_1: 18

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

        end;

         A74:

        now

          let i be Nat;

          assume that

           A75: 0 < i and

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

          

           A77: ( 0 + 1) <= i by A75, NAT_1: 13;

          

          thus (P . i) = (f . i) by A64, A76

          .= ( SubFrom (a,( intloc 0 ))) by A68, A77, A76;

        end;

        

         A78: 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

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

          

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

          proof

            let n be Nat;

            assume

             A81: P[n];

            assume

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

            then

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

            per cases ;

              suppose

               A84: n = 0 ;

              

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

              .= (n + 1) by A2, A84, SCMFSA_2: 63;

            end;

              suppose

               A85: n > 0 ;

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

              

              then

               A86: ( CurInstr (P,( Comput (P,s,n)))) = (P . n) by A81, A82, PBOOLE: 143, XXREAL_0: 2

              .= ( SubFrom (a,( intloc 0 ))) by A74, A83, A85;

              ( 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 A86;

              hence ( IC ( Comput (P,s,(n + 1)))) = (n + 1) by A81, A82, NAT_1: 13, SCMFSA_2: 65;

            end;

          end;

          

           A87: P[ 0 ] by A2, EXTPRO_1: 2;

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

          hence thesis by A79;

        end;

        

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

        proof

          let n be Nat;

          assume

           A89: Q[n];

          assume

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

          per cases ;

            suppose

             A91: n = 0 ;

            hereby

              assume 1 <= (n + 1);

              

              thus (( Comput (P,s,(n + 1))) . a) = (( Exec ((a := ( intloc 0 )),s)) . a) by A66, A91

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

            end;

            hereby

              let b be Int-Location;

              assume

               A92: b <> a;

              

              thus (( Comput (P,s,(n + 1))) . b) = (( Exec ((a := ( intloc 0 )),s)) . b) by A66, A91

              .= (s . b) by A92, SCMFSA_2: 63;

            end;

            let f be FinSeq-Location;

            

            thus (( Comput (P,s,(n + 1))) . f) = (( Exec ((a := ( intloc 0 )),s)) . f) by A66, A91

            .= (s . f) by SCMFSA_2: 63;

          end;

            suppose

             A93: n > 0 ;

            

             A94: n < ((mk + 1) + 1) by A90, NAT_1: 13;

            

             A95: (P /. ( IC ( Comput (P,s,n)))) = (P . ( IC ( Comput (P,s,n)))) by PBOOLE: 143;

            

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

            

            then

             A97: ( CurInstr (P,( Comput (P,s,n)))) = (P . n) by A78, A90, A95, XXREAL_0: 2

            .= ( SubFrom (a,( intloc 0 ))) by A74, A93, A94;

            

             A98: ( 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 A97;

            

             A99: ( 0 + 1) < (n + 1) by A93, XREAL_1: 6;

            hereby

              assume 1 <= (n + 1);

              

              thus (( Comput (P,s,(n + 1))) . a) = (((( - n) + 1) + 1) - (( Comput (P,s,n)) . ( intloc 0 ))) by A89, A90, A99, A98, NAT_1: 13, SCMFSA_2: 65

              .= (((( - n) + 1) + 1) - (s . ( intloc 0 ))) by A4, A89, A90, A96, XXREAL_0: 2

              .= ((( - (n + 1)) + 1) + 1) by A1;

            end;

            hereby

              let b be Int-Location;

              assume

               A100: b <> a;

              

              hence (( Comput (P,s,(n + 1))) . b) = (( Comput (P,s,n)) . b) by A98, SCMFSA_2: 65

              .= (s . b) by A89, A90, A96, A100, XXREAL_0: 2;

            end;

            let f be FinSeq-Location;

            

            thus (( Comput (P,s,(n + 1))) . f) = (( Comput (P,s,n)) . f) by A98, SCMFSA_2: 65

            .= (s . f) by A89, A90, A96, XXREAL_0: 2;

          end;

        end;

        

         A101: ( len ( Stop SCM+FSA )) = 1 by AFINSQ_1: 34;

        ( 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

         A102: (f . ((mk + 1) + 1)) = ( halt SCM+FSA ) by A59, XREAL_1: 29, A101;

        

         A103: (P /. ( IC ( Comput (P,s,((mk + 1) + 1))))) = (P . ( IC ( Comput (P,s,((mk + 1) + 1))))) by PBOOLE: 143;

        

         A104: ( CurInstr (P,( Comput (P,s,((mk + 1) + 1))))) = (P . ((mk + 1) + 1)) by A78, A103

        .= ( halt SCM+FSA ) by A102, A64;

        hence P halts_on s by EXTPRO_1: 29;

        then

         A105: ( Comput (P,s,((mk + 1) + 1))) = ( Result (P,s)) by A104, EXTPRO_1:def 9;

        

         A106: Q[ 0 ] by EXTPRO_1: 2;

        

         A107: for i be Nat holds Q[i] from NAT_1:sch 2( A106, A88);

        ((( - ((mk + 1) + 1)) + 1) + 1) = k & ( 0 + 1) <= (mk + (1 + 1)) by XREAL_1: 7;

        hence thesis by A107, A105;

      end;

    end;

    theorem :: SCMFSA_7:7

    for s be 0 -started State of SCM+FSA st (s . ( intloc 0 )) = 1 holds for f be FinSeq-Location, p be FinSequence of INT st (f := p) c= P holds P halts_on s & (( Result (P,s)) . f) = p & (for b be Int-Location st b <> ( intloc 1) & b <> ( intloc 2) holds (( Result (P,s)) . b) = (s . b)) & for g be FinSeq-Location st g <> f holds (( Result (P,s)) . g) = (s . g)

    proof

      set D = the InstructionsF of SCM+FSA ;

      set V = ( intloc 2);

      set I = ( intloc 1);

      set O = ( intloc 0 );

      

       A1: I <> O by AMI_3: 10;

      

       A2: I <> V by AMI_3: 10;

      let s be 0 -started State of SCM+FSA such that

       A3: (s . O) = 1;

      let f be FinSeq-Location, p be FinSequence of INT such that

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

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

      

       A5: for i,k be Nat st i < ( len q) holds (P . i) = (q . i) by A4, GRFUNC_1: 2, AFINSQ_1: 86;

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

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

       A6: ( len pp) = ( len p) and

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

       A8: ( aSeq (f,p)) = ( FlattenSeq pp) by Def3;

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

      then ( len q) = (( len (q0 ^ ( FlattenSeq pp))) + 1) by A8, AFINSQ_1: 17;

      then

       A9: ( 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 Nat st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i) & (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f) | ( len pp0)) = (p | ( len pp0))) & ( len (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f)) = ( len p) & (for b be Int-Location st b <> I & b <> V holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . b) = (s . b)) & (for g be FinSeq-Location st g <> f holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . g) = (s . g))));

      

       A10: V <> O by AMI_3: 10;

      

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

      proof

        let r be XFinSequence, x be object;

        assume

         A12: 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

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

        assume

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

        then

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

        then

         A16: r1 < ( len pp) by A13, AFINSQ_1: 86;

        then

        consider pr1 be Integer such that

         A17: pr1 = (p . (r1 + 1)) and

         A18: (pp . r1) = ((( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1))) ^ <%((f,I) := V)%>) by A7;

        1 <= (r1 + 1) & (r1 + 1) <= ( len pp) by A16, NAT_1: 11, NAT_1: 13;

        then

         A19: (r1 + 1) in ( Seg ( len pp));

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

        then

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

         A20: pp0 = r and

         A21: for i be Nat st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i and

         A22: ((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f) | ( len pp0)) = (p | ( len pp0)) and

         A23: ( len (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f)) = ( len p) and

         A24: for b be Int-Location st b <> I & b <> V holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . b) = (s . b) and

         A25: for h be FinSeq-Location st h <> f holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . h) = (s . h) by A12, A14, XBOOLE_1: 1;

        

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

        .= (pp . r1) by A14, A13, GRFUNC_1: 2;

        then x in (D ^omega ) by A13, A15, FUNCT_1: 102;

        then

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

        take pp1;

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

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

        

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

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

        

         A28: ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3;

        ( len pp1) <= ( len p) by A6, A14, A20, NAT_1: 43;

        then

         A29: ( Seg ( len pp1)) c= ( Seg ( len p)) by FINSEQ_1: 5;

        then

         A30: ( dom (p | ( Seg ( len pp1)))) = ( Seg ( len pp1)) by A28, RELAT_1: 62;

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

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

        set s1 = ( Comput (P,s,c1));

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

        

         A31: x = (( aSeq (I,(r1 + 1))) ^ (( aSeq (V,pr1)) ^ <%((f,I) := V)%>)) by A18, A26, AFINSQ_1: 27;

        

        then

         A32: (( len q0) + ( len ( FlattenSeq pp1))) = (( len q0) + ( len ((( FlattenSeq pp0) ^ ( aSeq (I,(r1 + 1)))) ^ (( aSeq (V,pr1)) ^ <%((f,I) := V)%>)))) by A27, AFINSQ_1: 27

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

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

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

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

        .= (c2 + (( len ( aSeq (V,pr1))) + 1)) by AFINSQ_1: 33

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

        then

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

        

         A34: ( FlattenSeq pp1) c= ( FlattenSeq pp) by A14, A20, AFINSQ_2: 82;

         A35:

        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 A34, A27, XBOOLE_1: 1;

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

          then

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

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

          hence ((q0 ^ ( FlattenSeq pp0)) ^ p) c= q by A36, XBOOLE_1: 1;

        end;

        ( IC s1) = c1 by A21;

        then

        reconsider s1 as c1 -started State of SCM+FSA by MEMSTR_0:def 12;

        

         A37: (s1 . O) = 1 by A1, A10, A3, A24;

        

         A38: for c be Nat st c in ( dom ( aSeq (I,(r1 + 1)))) holds (( aSeq (I,(r1 + 1))) . c) = (P . (c1 + c))

        proof

          let c be Nat;

          assume

           A39: c in ( dom ( aSeq (I,(r1 + 1))));

          then

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

          

           A41: ((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (I,(r1 + 1)))) c= q by A31, A35, AFINSQ_1: 74;

          then

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

          

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

          .= (q . (c1 + c)) by A41, A40, GRFUNC_1: 2

          .= (P . (c1 + c)) by A4, A42, A40, GRFUNC_1: 2;

        end;

        then

         A43: (( Comput (P,s1,( len ( aSeq (I,(r1 + 1)))))) . I) = (r1 + 1) by Th4, A37, A1;

        

         A44: (q0 ^ ( FlattenSeq pp1)) = ((q0 ^ ( FlattenSeq pp0)) ^ x) by A27, AFINSQ_1: 27;

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

        then

         A45: (c2 + ( len ( aSeq (V,pr1)))) < ( len q) by A33, NAT_1: 13;

         A46:

        now

          let i be Nat;

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

          

          hence (c1 + i) = ( IC ( Comput (P,s1,i))) by A38, Th4, A37, A1

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

        end;

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

        

         A47: c3 = (c2 + ( len ( aSeq (V,pr1)))) by AFINSQ_1: 17;

        

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

        then

         A49: s2 = ( Comput (P,( Comput (P,s,c1)),( len ( aSeq (I,(r1 + 1)))))) by EXTPRO_1: 4;

        ( IC s2) = c2 by A48, A49, A38, Th4, A37, A1;

        then

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

        

         A50: (s2 . O) = 1 by A49, A38, Th4, A37, A1;

        

         A51: for c be Nat st c in ( dom ( aSeq (V,pr1))) holds (( aSeq (V,pr1)) . c) = (P . (c2 + c))

        proof

          let c be Nat;

          assume

           A52: c in ( dom ( aSeq (V,pr1)));

          then

           A53: (c2 + c) in ( dom (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (I,(r1 + 1)))) ^ ( aSeq (V,pr1)))) by AFINSQ_1: 23;

          ((q0 ^ ( FlattenSeq pp0)) ^ (( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1)))) c= q by A18, A26, A35, AFINSQ_1: 74;

          then

           A54: (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (I,(r1 + 1)))) ^ ( aSeq (V,pr1))) c= q by AFINSQ_1: 27;

          then

           A55: ( dom (((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (I,(r1 + 1)))) ^ ( aSeq (V,pr1)))) c= ( dom q) by GRFUNC_1: 2;

          

          thus (( aSeq (V,pr1)) . c) = ((((q0 ^ ( FlattenSeq pp0)) ^ ( aSeq (I,(r1 + 1)))) ^ ( aSeq (V,pr1))) . (c2 + c)) by A52, AFINSQ_1:def 3

          .= (q . (c2 + c)) by A53, A54, GRFUNC_1: 2

          .= (P . (c2 + c)) by A4, A55, A53, GRFUNC_1: 2;

        end;

        then

         A56: (( Comput (P,s2,( len ( aSeq (V,pr1))))) . V) = pr1 by Th4, A50, A10;

        

         A57: (( Comput (P,s,c3)) . f) = (( Comput (P,s,(c2 + ( len ( aSeq (V,pr1)))))) . f) by AFINSQ_1: 17

        .= (( Comput (P,s2,( len ( aSeq (V,pr1))))) . f) by EXTPRO_1: 4

        .= (s2 . f) by A51, Th4, A50, A10

        .= (s1 . f) by A49, A38, Th4, A37, A1;

         A58:

        now

          let i be Nat;

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

          

          hence (c2 + i) = ( IC ( Comput (P,s2,i))) by A51, Th4, A50, A10

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

        end;

        

         A59: for i be Nat st i < ( len (q0 ^ ( FlattenSeq pp1))) holds ( IC ( Comput (P,s,i))) = i

        proof

          let i be Nat;

          assume

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

           A61:

          now

            

             A62: i < (( len q0) + ( len ( FlattenSeq pp1))) by A60, AFINSQ_1: 17;

            assume

             A63: not i <= c1;

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

            hence (c2 + 1) <= i & i <= (c2 + ( len ( aSeq (V,pr1)))) by A32, A63, A62, NAT_1: 13;

          end;

          per cases by A61;

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

            hence thesis by A21;

          end;

            suppose

             A64: (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 A64, XREAL_1: 9;

            

            hence i = ( IC ( Comput (P,s,(c1 + ii)))) by A48, A46

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

          end;

            suppose

             A65: (c2 + 1) <= i & i <= (c2 + ( len ( aSeq (V,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 (V,pr1)))) - c2) by A65, XREAL_1: 9;

            

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

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

          end;

        end;

        

         A66: c3 = ((c1 + ( len ( aSeq (I,(r1 + 1))))) + ( len ( aSeq (V,pr1)))) by A48, AFINSQ_1: 17;

        

         A67: (P /. ( IC ( Comput (P,s,c3)))) = (P . ( IC ( Comput (P,s,c3)))) by PBOOLE: 143;

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

        then

        consider rq be XFinSequence of D such that

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

        

         A69: ( len (q0 ^ ( FlattenSeq pp1))) = ((c2 + ( len ( aSeq (V,pr1)))) + 1) by A32, AFINSQ_1: 17;

        then

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

        then

         A71: c3 in ( dom ((q0 ^ ( FlattenSeq pp0)) ^ x)) by A44, A47, AFINSQ_1: 66;

        

         A72: 0 in ( dom <%((f,I) := V)%>) by TARSKI:def 1;

        ( len <%((f,I) := V)%>) = 1 by AFINSQ_1: 34;

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

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

        then

         A73: ( len (( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1)))) in ( dom ((( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1))) ^ <%((f,I) := V)%>)) by AFINSQ_1: 66;

        ( CurInstr (P,( Comput (P,s,c3)))) = (P . c3) by A47, A59, A67, A70

        .= (q . c3) by A5, A47, A45

        .= (((q0 ^ ( FlattenSeq pp0)) ^ x) . (c1 + (( len ( aSeq (I,(r1 + 1)))) + ( len ( aSeq (V,pr1)))))) by A66, A71, A68, AFINSQ_1:def 3

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

        

        then

         A74: ( CurInstr (P,( Comput (P,s,c3)))) = (((( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1))) ^ <%((f,I) := V)%>) . (( len (( aSeq (I,(r1 + 1))) ^ ( aSeq (V,pr1)))) + 0 )) by A73, A18, A26, AFINSQ_1:def 3

        .= ( <%((f,I) := V)%> . 0 ) by A72, AFINSQ_1:def 3

        .= ((f,I) := V);

        

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

        .= ( Exec (((f,I) := V),( Comput (P,s,c3)))) by A74;

        

        then

         A76: ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1)))))) = (( IC ( Comput (P,s,c3))) + 1) by A47, A33, SCMFSA_2: 73

        .= ( len (q0 ^ ( FlattenSeq pp1))) by A47, A69, A59, A70;

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

        proof

          let i be Nat;

          assume

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

          per cases by A77, XXREAL_0: 1;

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

            hence thesis by A59;

          end;

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

            hence thesis by A76;

          end;

        end;

        

         A78: (( Comput (P,s,c3)) . V) = (( Comput (P,s,(c2 + ( len ( aSeq (V,pr1)))))) . V) by AFINSQ_1: 17

        .= (p . (r1 + 1)) by A17, A56, EXTPRO_1: 4;

        consider ki be Nat such that

         A79: ki = |.(( Comput (P,s,c3)) . I).| and

         A80: (( Exec (((f,I) := V),( Comput (P,s,c3)))) . f) = ((( Comput (P,s,c3)) . f) +* (ki,(( Comput (P,s,c3)) . V))) by SCMFSA_2: 73;

        

         A81: ki = |.(( Comput (P,s,(c2 + ( len ( aSeq (V,pr1)))))) . I).| by A79, AFINSQ_1: 17

        .= |.(( Comput (P,s2,( len ( aSeq (V,pr1))))) . I).| by EXTPRO_1: 4

        .= |.(s2 . I).| by A2, A51, Th4, A50, A10

        .= (r1 + 1) by A49, A43, ABSVALUE:def 1;

        

         A82: ( dom (s1 . f)) = ( Seg ( len p)) by A23, FINSEQ_1:def 3;

        for i be Nat st i in ( Seg ( len pp1)) holds (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1))) . i) = ((p | ( Seg ( len pp1))) . i)

        proof

          let i be Nat;

          assume

           A83: i in ( Seg ( len pp1));

          then

           A84: i <= ( len pp1) by FINSEQ_1: 1;

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

          then

           A85: ( len pp1) = (( len pp0) + 1) by AFINSQ_1: 17;

          per cases ;

            suppose

             A86: i = ( len pp1);

            

            thus (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1))) . i) = (((s1 . f) +* ((r1 + 1),(p . (r1 + 1)))) . i) by A47, A69, A75, A80, A81, A78, A57, A86, A85, FINSEQ_1: 4, FUNCT_1: 49

            .= (p . i) by A20, A6, A82, A86, A19, A85, FUNCT_7: 31

            .= ((p | ( Seg ( len pp1))) . i) by A86, A85, FINSEQ_1: 4, FUNCT_1: 49;

          end;

            suppose

             A87: i <> ( len pp1);

            then i < (( len pp0) + 1) by A85, A84, XXREAL_0: 1;

            then

             A88: i <= ( len pp0) by NAT_1: 13;

            1 <= i by A83, FINSEQ_1: 1;

            then

             A89: i in ( Seg ( len pp0)) by A88;

            (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1))) . i) = (((s1 . f) +* ((r1 + 1),(p . (r1 + 1)))) . i) by A47, A69, A75, A80, A81, A78, A57, A83, FUNCT_1: 49

            .= ((s1 . f) . i) by A85, A20, A87, FUNCT_7: 32;

            

            hence (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1))) . i) = ((p | ( Seg ( len pp0))) . i) by A22, A89, FUNCT_1: 49

            .= (p . i) by A89, FUNCT_1: 49

            .= ((p | ( Seg ( len pp1))) . i) by A83, FUNCT_1: 49;

          end;

        end;

        then

         A90: for i be object st i in ( Seg ( len pp1)) holds (((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1))) . i) = ((p | ( Seg ( len pp1))) . i);

        

         A91: ( dom ((s1 . f) +* ((r1 + 1),(p . (r1 + 1))))) = ( dom (s1 . f)) by FUNCT_7: 30;

        ( dom (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f)) = ( dom ((s1 . f) +* ((r1 + 1),(p . (r1 + 1))))) by A33, A75, A80, A81, A78, A57, AFINSQ_1: 17

        .= ( Seg ( len p)) by A23, A91, FINSEQ_1:def 3;

        then ( dom ((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( Seg ( len pp1)))) = ( Seg ( len pp1)) by A29, RELAT_1: 62;

        hence ((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f) | ( len pp1)) = (p | ( len pp1)) by A30, A90, FUNCT_1: 2;

        ( len ((s1 . f) +* ((r1 + 1),(p . (r1 + 1))))) = ( len (s1 . f)) by A91, FINSEQ_3: 29;

        hence ( len (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . f)) = ( len p) by A23, A33, A75, A80, A81, A78, A57, AFINSQ_1: 17;

        hereby

          let b be Int-Location;

          assume that

           A92: b <> I and

           A93: b <> V;

          

          thus (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . b) = (( Comput (P,s,(c2 + ( len ( aSeq (V,pr1)))))) . b) by A47, A33, A75, SCMFSA_2: 73

          .= (( Comput (P,s2,( len ( aSeq (V,pr1))))) . b) by EXTPRO_1: 4

          .= (s2 . b) by A51, A93, Th4, A50, A10

          .= (s1 . b) by A49, A38, A92, Th4, A37, A1

          .= (s . b) by A24, A92, A93;

        end;

        hereby

          let h be FinSeq-Location;

          assume

           A94: h <> f;

          

          hence (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp1))))) . h) = (( Comput (P,s,(c2 + ( len ( aSeq (V,pr1)))))) . h) by A47, A33, A75, SCMFSA_2: 73

          .= (( Comput (P,s2,( len ( aSeq (V,pr1))))) . h) by EXTPRO_1: 4

          .= (s2 . h) by A51, Th4, A50, A10

          .= (s1 . h) by A49, A38, Th4, A37, A1

          .= (s . h) by A25, A94;

        end;

      end;

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

      ( len <%(f :=<0,...,0> I)%>) = 1 by AFINSQ_1: 34;

      then

       A95: ( len q0) = (k + 1) by AFINSQ_1: 17;

      

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

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

      then ( aSeq (I,( len p))) c= (f := p) by AFINSQ_1: 74;

      then

       A97: ( aSeq (I,( len p))) c= P by A4, XBOOLE_1: 1;

      then

       A98: (( Comput (P,s,( len ( aSeq (I,( len p)))))) . I) = ( len p) by A1, A3, Th5;

      

       A99: P[ {} ]

      proof

         A100:

        now

          let i be Nat such that

           A101: i < ( len q0);

          i < ( len q0) implies i <= ( len ( aSeq (I,( len p)))) by A95, NAT_1: 13;

          hence ( IC ( Comput (P,s,i))) = i by A1, A3, A97, A101, Th5;

        end;

        assume {} c= pp;

        reconsider sD = ( <%> (D ^omega )) as XFinSequence of (D ^omega );

        take sD;

        

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

        .= (q0 ^ {} )

        .= q0;

        

         A103: k < ( len q0) by A95, NAT_1: 13;

        then

         A104: ( IC ( Comput (P,s,k))) = k by A100;

        

         A105: (P /. ( IC ( Comput (P,s,k)))) = (P . ( IC ( Comput (P,s,k)))) by PBOOLE: 143;

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

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

        then

         A106: k < ( len q) by A95, NAT_1: 13;

        

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

        

         A108: k in ( dom q0) by A103, AFINSQ_1: 66;

        

         A109: ( CurInstr (P,( Comput (P,s,k)))) = (q . k) by A5, A104, A105, A106

        .= (q0 . k) by A107, A108, AFINSQ_1:def 3

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

        thus sD = {} ;

        

         A110: ( Comput (P,s,( len q0))) = ( Following (P,( Comput (P,s,k)))) by A95, EXTPRO_1: 3

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

        then

         A111: ( IC ( Comput (P,s,( len q0)))) = ( len q0) by A95, A104, SCMFSA_2: 75;

        now

          let i be 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 A100, A111;

        end;

        hence for i be Nat st i <= ( len (q0 ^ ( FlattenSeq sD))) holds ( IC ( Comput (P,s,i))) = i by A102;

        consider ki be Nat such that

         A112: ki = |.(( Comput (P,s,k)) . I).| and

         A113: (( Exec ((f :=<0,...,0> I),( Comput (P,s,k)))) . f) = (ki |-> 0 ) by SCMFSA_2: 75;

        ((( Comput (P,s,( len (q0 ^ ( FlattenSeq sD))))) . f) | 0 ) = (p | ( len sD));

        hence ((( Comput (P,s,( len (q0 ^ ( FlattenSeq sD))))) . f) | ( len sD)) = (p | ( len sD));

        ki = ( len p) by A98, A112, ABSVALUE:def 1;

        hence ( len (( Comput (P,s,( len (q0 ^ ( FlattenSeq sD))))) . f)) = ( len p) by A102, A110, A113, CARD_1:def 7;

        now

          let b be Int-Location such that

           A114: b <> I and b <> V;

          

          thus (( Comput (P,s,( len q0))) . b) = (( Comput (P,s,k)) . b) by A110, SCMFSA_2: 75

          .= (s . b) by A1, A3, A97, A114, Th5;

        end;

        hence for b be Int-Location st b <> I & b <> V holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq sD))))) . b) = (s . b) by A102;

        now

          let g be FinSeq-Location;

          assume g <> f;

          

          hence (( Comput (P,s,( len q0))) . g) = (( Comput (P,s,k)) . g) by A110, SCMFSA_2: 75

          .= (s . g) by A1, A3, A97, Th5;

        end;

        hence thesis by A102;

      end;

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

      then

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

       A115: pp0 = pp and

       A116: for i be Nat st i <= ( len (q0 ^ ( FlattenSeq pp0))) holds ( IC ( Comput (P,s,i))) = i and

       A117: ((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f) | ( len pp0)) = (p | ( len pp0)) and

       A118: ( len (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f)) = ( len p) and

       A119: (for b be Int-Location st b <> I & b <> V holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . b) = (s . b)) & for g be FinSeq-Location st g <> f holds (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . g) = (s . g);

      

       A120: (P /. ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp))))))) = (P . ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp))))))) by PBOOLE: 143;

      ( IC ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp)))))) = ( len (q0 ^ ( FlattenSeq pp))) by A115, A116;

      

      then

       A121: ( CurInstr (P,( Comput (P,s,( len (q0 ^ ( FlattenSeq pp))))))) = (q . ( len (q0 ^ ( FlattenSeq pp)))) by A5, A9, A120

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

      hence P halts_on s by EXTPRO_1: 29;

      then

       A122: ( Comput (P,s,( len (q0 ^ ( FlattenSeq pp))))) = ( Result (P,s)) by A121, EXTPRO_1:def 9;

      

       A123: ( Seg ( len pp0)) = ( dom p) by A6, A115, FINSEQ_1:def 3;

      (( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f) = ((( Comput (P,s,( len (q0 ^ ( FlattenSeq pp0))))) . f) | ( len pp0)) by A6, A115, A118, FINSEQ_3: 113;

      hence (( Result (P,s)) . f) = p by A123, A115, A122, A117;

      thus thesis by A115, A119, A122;

    end;