scmfsa_5.miz



    begin

    reserve j,k,m for Nat;

    begin

    theorem :: SCMFSA_5:1

    

     Th1: for k be Nat holds for q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function, p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA st p c= s1 & ( IncIC (p,k)) c= s2 holds for P1,P2 be Instruction-Sequence of SCM+FSA st q c= P1 & ( Reloc (q,k)) c= P2 holds for i be Nat holds (( IC ( Comput (P1,s1,i))) + k) = ( IC ( Comput (P2,s2,i))) & ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),k)) = ( CurInstr (P2,( Comput (P2,s2,i)))) & (( Comput (P1,s1,i)) | ( dom ( DataPart p))) = (( Comput (P2,s2,i)) | ( dom ( DataPart p))) & ( DataPart ( Comput (P1,(s1 +* ( DataPart s2)),i))) = ( DataPart ( Comput (P2,s2,i)))

    proof

      let k be Nat;

      let q be non halt-free finitethe InstructionsF of SCM+FSA -valued NAT -defined Function, p be q -autonomic non empty FinPartState of SCM+FSA , s1,s2 be State of SCM+FSA such that

       A1: p c= s1 and

       A2: ( IncIC (p,k)) c= s2;

      

       A3: ( IC SCM+FSA ) in ( dom p) by AMISTD_5: 6;

      let P1,P2 be Instruction-Sequence of SCM+FSA such that

       A4: q c= P1 & ( Reloc (q,k)) c= P2;

      

       A5: ( Reloc (q,k)) c= P2 by A4;

      

       A6: q c= P1 by A4;

      set s3 = (s1 +* ( DataPart s2));

      defpred Y[ Nat] means (( IC ( Comput (P1,s1,$1))) + k) = ( IC ( Comput (P2,s2,$1))) & ( IncAddr (( CurInstr (P1,( Comput (P1,s1,$1)))),k)) = ( CurInstr (P2,( Comput (P2,s2,$1)))) & (( Comput (P1,s1,$1)) | ( dom ( DataPart p))) = (( Comput (P2,s2,$1)) | ( dom ( DataPart p))) & ( DataPart ( Comput (P1,s3,$1))) = ( DataPart ( Comput (P2,s2,$1)));

      

       A7: p c= s3 by A1, A2, MEMSTR_0: 61;

      

       A8: for i be Nat st Y[i] holds Y[(i + 1)]

      proof

        set DPp = ( DataPart p);

        let i be Nat such that

         A9: (( IC ( Comput (P1,s1,i))) + k) = ( IC ( Comput (P2,s2,i))) and

         A10: ( IncAddr (( CurInstr (P1,( Comput (P1,s1,i)))),k)) = ( CurInstr (P2,( Comput (P2,s2,i)))) and

         A11: (( Comput (P1,s1,i)) | ( dom ( DataPart p))) = (( Comput (P2,s2,i)) | ( dom ( DataPart p))) and

         A12: ( DataPart ( Comput (P1,s3,i))) = ( DataPart ( Comput (P2,s2,i)));

        set Cs1i1 = ( Comput (P1,s1,(i + 1)));

        set Cs1i = ( Comput (P1,s1,i));

        

         A13: ( dom Cs1i1) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

        set Cs3i = ( Comput (P1,s3,i));

        set Cs2i = ( Comput (P2,s2,i));

        

         A14: ( dom Cs1i) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

        set Cs2i1 = ( Comput (P2,s2,(i + 1)));

        

         A15: ( dom Cs2i1) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

        

         A16: ( dom Cs2i) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

        set I = ( CurInstr (P1,Cs1i));

        

         A17: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

         A18:

        now

          let s be State of SCM+FSA , d be FinSeq-Location;

          d in FinSeq-Locations by SCMFSA_2:def 5;

          then d in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

          hence d in ( dom ( DataPart s)) by MEMSTR_0: 9;

        end;

         A19:

        now

          let d be FinSeq-Location;

          

           A20: d in ( dom ( DataPart Cs3i)) by A18;

          

          hence (Cs3i . d) = (( DataPart Cs3i) . d) by FUNCT_1: 47

          .= (Cs2i . d) by A12, A20, FUNCT_1: 47;

        end;

        set Cs3i1 = ( Comput (P1,s3,(i + 1)));

        

         A21: ( dom ( DataPart Cs2i)) = ( Data-Locations SCM+FSA ) by MEMSTR_0: 9;

        

         A22: ( dom ( DataPart Cs3i1)) = ( Data-Locations SCM+FSA ) by MEMSTR_0: 9;

         A23:

        now

          reconsider loc = ( IC Cs1i1) as Nat;

          assume

           A24: (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1))));

          reconsider ii = loc as Nat;

          

           A25: ii in ( dom q) by A6, A1, AMISTD_5:def 4;

          

           A26: (loc + k) in ( dom ( Reloc (q,k))) by A25, COMPOS_1: 46;

          

           A27: ( dom P2) = NAT by PARTFUN1:def 2;

          ( dom P1) = NAT by PARTFUN1:def 2;

          

          then ( CurInstr (P1,Cs1i1)) = (P1 . loc) by PARTFUN1:def 6

          .= (q . loc) by A25, A4, GRFUNC_1: 2

          .= (q . loc);

          

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = (( Reloc (q,k)) . (loc + k)) by A25, COMPOS_1: 35

          .= (P2 . ( IC ( Comput (P2,s2,(i + 1))))) by A24, A26, A5, GRFUNC_1: 2

          .= ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A27, PARTFUN1:def 6;

        end;

         A28:

        now

          let s be State of SCM+FSA , d be Int-Location;

          d in Int-Locations by AMI_2:def 16;

          then d in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

          hence d in ( dom ( DataPart s)) by MEMSTR_0: 9;

        end;

         A29:

        now

          let d be Int-Location;

          

           A30: d in ( dom ( DataPart Cs3i)) by A28;

          

          hence (Cs3i . d) = (( DataPart Cs3i) . d) by FUNCT_1: 47

          .= (Cs2i . d) by A12, A30, FUNCT_1: 47;

        end;

        ( dom DPp) = (( dom p) /\ ( Data-Locations SCM+FSA )) by RELAT_1: 61;

        then

         A31: ( dom DPp) c= ( {( IC SCM+FSA )} \/ ( Data-Locations SCM+FSA )) by XBOOLE_1: 10, XBOOLE_1: 17;

        

         A32: ( dom (Cs1i1 | ( dom DPp))) = (( dom Cs1i1) /\ ( dom DPp)) by RELAT_1: 61

        .= ( dom DPp) by A13, A31, XBOOLE_1: 28;

        

         A33: ( dom ( DataPart Cs2i1)) = ( Data-Locations SCM+FSA ) by MEMSTR_0: 9;

         A34:

        now

          let x be object;

          assume that

           A35: x in ( dom (Cs3i1 | ( Data-Locations SCM+FSA ))) and

           A36: (Cs3i1 . x) = (Cs2i1 . x);

          

          thus (( DataPart Cs3i1) . x) = (Cs2i1 . x) by A35, A36, FUNCT_1: 47

          .= (( DataPart Cs2i1) . x) by A22, A33, A35, FUNCT_1: 47;

        end;

        

         A37: ( dom ( DataPart Cs3i)) = ( Data-Locations SCM+FSA ) by MEMSTR_0: 9;

         A38:

        now

          let x be set;

          assume that

           A39: x in ( dom ( DataPart Cs3i1)) and

           A40: (Cs3i1 . x) = (Cs3i . x) and

           A41: (Cs2i1 . x) = (Cs2i . x);

          (( DataPart Cs3i) . x) = (Cs3i . x) by A37, A22, A39, FUNCT_1: 47;

          hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A12, A21, A22, A34, A39, A40, A41, FUNCT_1: 47;

        end;

        

         A42: Cs3i1 = ( Following (P1,Cs3i)) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P1,Cs1i)),Cs3i)) by A1, A7, A4, AMISTD_5: 7;

        

         A43: ( dom (Cs2i1 | ( dom ( DataPart p)))) = (( dom Cs2i1) /\ ( dom DPp)) by RELAT_1: 61

        .= ( dom DPp) by A15, A31, XBOOLE_1: 28;

         A44:

        now

          let x,d be set such that

           A45: d = x and

           A46: d in ( dom DPp) and

           A47: (Cs1i1 . d) = (Cs2i1 . d);

          

          thus ((Cs1i1 | ( dom DPp)) . x) = (Cs2i1 . d) by A32, A45, A46, A47, FUNCT_1: 47

          .= ((Cs2i1 | ( dom DPp)) . x) by A43, A45, A46, FUNCT_1: 47;

        end;

        

         A48: ( dom (Cs1i | ( dom DPp))) = (( dom Cs1i) /\ ( dom DPp)) by RELAT_1: 61

        .= ( dom DPp) by A14, A31, XBOOLE_1: 28;

        reconsider j = ( IC Cs1i) as Nat;

        

         A49: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

        .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

        

         A50: ( dom (Cs2i | ( dom ( DataPart p)))) = (( dom Cs2i) /\ ( dom DPp)) by RELAT_1: 61

        .= ( dom DPp) by A16, A31, XBOOLE_1: 28;

         A51:

        now

          let x,d be set such that

           A52: d = x and

           A53: d in ( dom DPp) and

           A54: (Cs1i1 . d) = (Cs1i . d) and

           A55: (Cs2i1 . d) = (Cs2i . d);

          

           A56: ((Cs1i | ( dom DPp)) . d) = (Cs1i . d) by A48, A53, FUNCT_1: 47;

          ((Cs2i | ( dom DPp)) . d) = (Cs2i . d) by A50, A53, FUNCT_1: 47;

          

          hence ((Cs1i1 | ( dom DPp)) . x) = (Cs2i1 . d) by A11, A32, A52, A53, A54, A55, A56, FUNCT_1: 47

          .= ((Cs2i1 | ( dom DPp)) . x) by A43, A52, A53, FUNCT_1: 47;

        end;

        

         A57: ((( IC Cs1i) + k) + 1) = ((j + k) + 1)

        .= ((j + 1) + k)

        .= ((( IC Cs1i) + 1) + k);

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

        per cases ;

          suppose ( InsCode I) = 0 ;

          then

           A58: I = ( halt SCM+FSA ) by SCMFSA_2: 95;

          

          thus (( IC ( Comput (P1,s1,(i + 1)))) + k) = (( IC Cs1i) + k) by A49, A58, EXTPRO_1:def 3

          .= ( IC ( Comput (P2,s2,(i + 1)))) by A9, A17, A58, A10, EXTPRO_1:def 3;

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A23;

          

           A59: Cs2i1 = Cs2i by A17, A58, A10, EXTPRO_1:def 3;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A11, A49, A58, EXTPRO_1:def 3;

          thus thesis by A12, A42, A58, A59, EXTPRO_1:def 3;

        end;

          suppose ( InsCode I) = 1;

          then

          consider da,db be Int-Location such that

           A60: I = (da := db) by SCMFSA_2: 30;

          

           A61: ( IncAddr (I,k)) = (da := db) by A60, COMPOS_0: 4;

          

           A62: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A60, SCMFSA_2: 63;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A61, SCMFSA_2: 63;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A61, A62, SCMFSA_2: 63;

          

           A63: (Cs3i . db) = (Cs2i . db) by A29;

          now

            let x be object;

            

             A64: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            assume

             A65: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A65, A64, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A66: (Cs1i1 . d) = (Cs1i . d) by A49, A60, SCMFSA_2: 63;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A61, SCMFSA_2: 63;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A65, A66;

            end;

              suppose

               A67: da = x;

              DPp c= p by RELAT_1: 59;

              then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              then

               A68: (Cs3i . db) = (Cs1i . db) by A1, A7, A32, A60, A65, A67, A4, SCMFSA_3: 5;

              

               A69: (Cs1i1 . x) = (Cs1i . db) by A49, A60, A67, SCMFSA_2: 63;

              (Cs2i1 . x) = (Cs2i . db) by A10, A17, A61, A67, SCMFSA_2: 63;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A63, A65, A69, A68;

            end;

              suppose

               A70: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A71: (Cs1i1 . d) = (Cs1i . d) by A49, A60, A70, SCMFSA_2: 63;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A61, A70, SCMFSA_2: 63;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A65, A71;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A72: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A72, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A73: (Cs3i1 . f) = (Cs3i . f) by A42, A60, SCMFSA_2: 63;

              (Cs2i1 . f) = (Cs2i . f) by A10, A17, A61, SCMFSA_2: 63;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A72, A73;

            end;

              suppose

               A74: da = x;

              

               A75: (Cs3i1 . da) = (Cs3i . db) by A42, A60, SCMFSA_2: 63;

              (Cs2i1 . da) = (Cs2i . db) by A10, A17, A61, SCMFSA_2: 63;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A29, A34, A72, A74, A75;

            end;

              suppose

               A76: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A77: (Cs3i1 . d) = (Cs3i . d) by A42, A60, A76, SCMFSA_2: 63;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A61, A76, SCMFSA_2: 63;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A72, A77;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 2;

          then

          consider da,db be Int-Location such that

           A78: I = ( AddTo (da,db)) by SCMFSA_2: 31;

          

           A79: (Cs3i . db) = (Cs2i . db) by A29;

          

           A80: ( IncAddr (I,k)) = ( AddTo (da,db)) by A78, COMPOS_0: 4;

          

           A81: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A78, SCMFSA_2: 64;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A80, SCMFSA_2: 64;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A80, A81, SCMFSA_2: 64;

          

           A82: (Cs3i . da) = (Cs2i . da) by A29;

          now

            

             A83: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            let x be object such that

             A84: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A84, A83, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A85: (Cs1i1 . d) = (Cs1i . d) by A49, A78, SCMFSA_2: 64;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A80, SCMFSA_2: 64;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A84, A85;

            end;

              suppose

               A86: da = x;

              DPp c= p by RELAT_1: 59;

              then

               A87: ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              

               A88: (Cs1i1 . x) = ((Cs1i . da) + (Cs1i . db)) by A49, A78, A86, SCMFSA_2: 64;

              (Cs2i1 . x) = ((Cs2i . da) + (Cs2i . db)) by A10, A17, A80, A86, SCMFSA_2: 64;

              then (Cs1i1 . x) = (Cs2i1 . x) by A1, A7, A32, A78, A82, A79, A84, A86, A88, A87, A4, SCMFSA_3: 6;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A84;

            end;

              suppose

               A89: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A90: (Cs1i1 . d) = (Cs1i . d) by A49, A78, A89, SCMFSA_2: 64;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A80, A89, SCMFSA_2: 64;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A84, A90;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A91: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A91, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A92: (Cs3i1 . d) = (Cs3i . d) by A42, A78, SCMFSA_2: 64;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A80, SCMFSA_2: 64;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A91, A92;

            end;

              suppose

               A93: da = x;

              then

               A94: (Cs3i1 . x) = ((Cs3i . da) + (Cs3i . db)) by A42, A78, SCMFSA_2: 64;

              (Cs2i1 . x) = ((Cs2i . da) + (Cs2i . db)) by A10, A17, A80, A93, SCMFSA_2: 64;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A82, A79, A91, A94;

            end;

              suppose

               A95: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A96: (Cs3i1 . d) = (Cs3i . d) by A42, A78, A95, SCMFSA_2: 64;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A80, A95, SCMFSA_2: 64;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A91, A96;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 3;

          then

          consider da,db be Int-Location such that

           A97: I = ( SubFrom (da,db)) by SCMFSA_2: 32;

          

           A98: (Cs3i . db) = (Cs2i . db) by A29;

          

           A99: ( IncAddr (I,k)) = ( SubFrom (da,db)) by A97, COMPOS_0: 4;

          

           A100: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A97, SCMFSA_2: 65;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A99, SCMFSA_2: 65;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A99, A100, SCMFSA_2: 65;

          

           A101: (Cs3i . da) = (Cs2i . da) by A29;

          now

            

             A102: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            let x be object such that

             A103: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A103, A102, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A104: (Cs1i1 . d) = (Cs1i . d) by A49, A97, SCMFSA_2: 65;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A99, SCMFSA_2: 65;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A103, A104;

            end;

              suppose

               A105: da = x;

              DPp c= p by RELAT_1: 59;

              then

               A106: ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              

               A107: (Cs1i1 . x) = ((Cs1i . da) - (Cs1i . db)) by A49, A97, A105, SCMFSA_2: 65;

              (Cs2i1 . x) = ((Cs2i . da) - (Cs2i . db)) by A10, A17, A99, A105, SCMFSA_2: 65;

              then ((Cs1i . da) - (Cs1i . db)) = (Cs2i1 . x) by A1, A7, A32, A97, A101, A98, A103, A105, A106, A4, SCMFSA_3: 7;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A103, A107;

            end;

              suppose

               A108: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A109: (Cs1i1 . d) = (Cs1i . d) by A49, A97, A108, SCMFSA_2: 65;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A99, A108, SCMFSA_2: 65;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A103, A109;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A110: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A110, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A111: (Cs3i1 . d) = (Cs3i . d) by A42, A97, SCMFSA_2: 65;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A99, SCMFSA_2: 65;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A110, A111;

            end;

              suppose

               A112: da = x;

              then

               A113: (Cs3i1 . x) = ((Cs3i . da) - (Cs3i . db)) by A42, A97, SCMFSA_2: 65;

              (Cs2i1 . x) = ((Cs2i . da) - (Cs2i . db)) by A10, A17, A99, A112, SCMFSA_2: 65;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A101, A98, A110, A113;

            end;

              suppose

               A114: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A115: (Cs3i1 . d) = (Cs3i . d) by A42, A97, A114, SCMFSA_2: 65;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A99, A114, SCMFSA_2: 65;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A110, A115;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 4;

          then

          consider da,db be Int-Location such that

           A116: I = ( MultBy (da,db)) by SCMFSA_2: 33;

          

           A117: (Cs3i . db) = (Cs2i . db) by A29;

          

           A118: ( IncAddr (I,k)) = ( MultBy (da,db)) by A116, COMPOS_0: 4;

          

           A119: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A116, SCMFSA_2: 66;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A118, SCMFSA_2: 66;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A118, A119, SCMFSA_2: 66;

          

           A120: (Cs3i . da) = (Cs2i . da) by A29;

          now

            

             A121: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            let x be object such that

             A122: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A122, A121, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A123: (Cs1i1 . d) = (Cs1i . d) by A49, A116, SCMFSA_2: 66;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A118, SCMFSA_2: 66;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A122, A123;

            end;

              suppose

               A124: da = x;

              DPp c= p by RELAT_1: 59;

              then

               A125: ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              

               A126: (Cs1i1 . x) = ((Cs1i . da) * (Cs1i . db)) by A49, A116, A124, SCMFSA_2: 66;

              (Cs2i1 . x) = ((Cs2i . da) * (Cs2i . db)) by A10, A17, A118, A124, SCMFSA_2: 66;

              then (Cs1i1 . x) = (Cs2i1 . x) by A1, A7, A32, A116, A120, A117, A122, A124, A126, A125, A4, SCMFSA_3: 8;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A122;

            end;

              suppose

               A127: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A128: (Cs1i1 . d) = (Cs1i . d) by A49, A116, A127, SCMFSA_2: 66;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A118, A127, SCMFSA_2: 66;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A122, A128;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A129: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A129, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A130: (Cs3i1 . d) = (Cs3i . d) by A42, A116, SCMFSA_2: 66;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A118, SCMFSA_2: 66;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A129, A130;

            end;

              suppose

               A131: da = x;

              then

               A132: (Cs3i1 . x) = ((Cs3i . da) * (Cs3i . db)) by A42, A116, SCMFSA_2: 66;

              (Cs2i1 . x) = ((Cs2i . da) * (Cs2i . db)) by A10, A17, A118, A131, SCMFSA_2: 66;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A120, A117, A129, A132;

            end;

              suppose

               A133: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A134: (Cs3i1 . d) = (Cs3i . d) by A42, A116, A133, SCMFSA_2: 66;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A118, A133, SCMFSA_2: 66;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A129, A134;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 5;

          then

          consider da,db be Int-Location such that

           A135: I = ( Divide (da,db)) by SCMFSA_2: 34;

          

           A136: (Cs3i . db) = (Cs2i . db) by A29;

          

           A137: ( IncAddr (I,k)) = ( Divide (da,db)) by A135, COMPOS_0: 4;

          

           A138: (Cs3i . da) = (Cs2i . da) by A29;

          per cases ;

            suppose

             A139: da <> db;

            

             A140: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A135, SCMFSA_2: 67;

            hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A137, SCMFSA_2: 67;

            thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A137, A140, SCMFSA_2: 67;

            now

              

               A141: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

              let x be object such that

               A142: x in ( dom (Cs1i1 | ( dom DPp)));

              per cases by A32, A142, A141, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose db <> x & x in FinSeq-Locations ;

                then

                reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

                

                 A143: (Cs1i1 . d) = (Cs1i . d) by A49, A135, SCMFSA_2: 67;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, SCMFSA_2: 67;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A142, A143;

              end;

                suppose

                 A144: da = x;

                DPp c= p by RELAT_1: 59;

                then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

                then

                 A145: ((Cs3i . da) div (Cs3i . db)) = ((Cs1i . da) div (Cs1i . db)) by A1, A7, A32, A135, A139, A142, A144, A4, SCMFSA_3: 9;

                

                 A146: (Cs1i1 . x) = ((Cs1i . da) div (Cs1i . db)) by A49, A135, A139, A144, SCMFSA_2: 67;

                (Cs2i1 . x) = ((Cs2i . da) div (Cs2i . db)) by A10, A17, A137, A139, A144, SCMFSA_2: 67;

                

                hence ((Cs1i1 | ( dom DPp)) . x) = (Cs2i1 . x) by A138, A136, A142, A146, A145, FUNCT_1: 47

                .= ((Cs2i1 | ( dom DPp)) . x) by A32, A43, A142, FUNCT_1: 47;

              end;

                suppose

                 A147: db = x;

                DPp c= p by RELAT_1: 59;

                then

                 A148: ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

                

                 A149: (Cs1i1 . x) = ((Cs1i . da) mod (Cs1i . db)) by A49, A135, A147, SCMFSA_2: 67;

                (Cs2i1 . x) = ((Cs2i . da) mod (Cs2i . db)) by A10, A17, A137, A147, SCMFSA_2: 67;

                then (Cs1i1 . x) = (Cs2i1 . x) by A1, A7, A32, A135, A138, A136, A142, A147, A149, A148, A4, SCMFSA_3: 10;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A142;

              end;

                suppose

                 A150: da <> x & db <> x & x in Int-Locations ;

                then

                reconsider d = x as Int-Location by AMI_2:def 16;

                

                 A151: (Cs1i1 . d) = (Cs1i . d) by A49, A135, A150, SCMFSA_2: 67;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A150, SCMFSA_2: 67;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A142, A151;

              end;

            end;

            then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

            hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

            now

              let x be object;

              assume

               A152: x in ( dom ( DataPart Cs3i1));

              per cases by A22, A152, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose x in FinSeq-Locations ;

                then

                reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

                

                 A153: (Cs3i1 . d) = (Cs3i . d) by A42, A135, SCMFSA_2: 67;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, SCMFSA_2: 67;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A152, A153;

              end;

                suppose

                 A154: da = x;

                then

                 A155: (Cs3i1 . x) = ((Cs3i . da) div (Cs3i . db)) by A42, A135, A139, SCMFSA_2: 67;

                (Cs2i1 . x) = ((Cs2i . da) div (Cs2i . db)) by A10, A17, A137, A139, A154, SCMFSA_2: 67;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A138, A136, A152, A155;

              end;

                suppose

                 A156: db = x;

                then

                 A157: (Cs3i1 . x) = ((Cs3i . da) mod (Cs3i . db)) by A42, A135, SCMFSA_2: 67;

                (Cs2i1 . x) = ((Cs2i . da) mod (Cs2i . db)) by A10, A17, A137, A156, SCMFSA_2: 67;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A138, A136, A152, A157;

              end;

                suppose

                 A158: da <> x & db <> x & x in Int-Locations ;

                then

                reconsider d = x as Int-Location by AMI_2:def 16;

                

                 A159: (Cs3i1 . d) = (Cs3i . d) by A42, A135, A158, SCMFSA_2: 67;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A158, SCMFSA_2: 67;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A152, A159;

              end;

            end;

            then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

            hence ( DataPart Cs3i1) = ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 3;

          end;

            suppose

             A160: da = db;

            then

             A161: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A135, SCMFSA_2: 68;

            hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A137, A160, SCMFSA_2: 68;

            thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A137, A160, A161, SCMFSA_2: 68;

            now

              

               A162: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

              let x be object such that

               A163: x in ( dom (Cs1i1 | ( dom DPp)));

              per cases by A32, A163, A162, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose x in FinSeq-Locations ;

                then

                reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

                

                 A164: (Cs1i1 . d) = (Cs1i . d) by A49, A135, A160, SCMFSA_2: 68;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A160, SCMFSA_2: 68;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A163, A164;

              end;

                suppose

                 A165: da = x;

                

                 A166: ((Cs2i1 | ( dom DPp)) . x) = (Cs2i1 . x) by A32, A43, A163, FUNCT_1: 47;

                

                 A167: ((Cs1i | ( dom DPp)) . x) = (Cs1i . x) by A32, A48, A163, FUNCT_1: 47;

                

                 A168: ((Cs2i | ( dom DPp)) . x) = (Cs2i . x) by A32, A50, A163, FUNCT_1: 47;

                

                 A169: ((Cs1i1 | ( dom DPp)) . x) = (Cs1i1 . x) by A163, FUNCT_1: 47;

                (Cs2i1 . x) = ((Cs2i . da) mod (Cs2i . db)) by A10, A17, A137, A160, A165, SCMFSA_2: 68;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A11, A49, A135, A160, A165, A167, A168, A169, A166, SCMFSA_2: 68;

              end;

                suppose

                 A170: da <> x & x in Int-Locations ;

                then

                reconsider d = x as Int-Location by AMI_2:def 16;

                

                 A171: (Cs1i1 . d) = (Cs1i . d) by A49, A135, A160, A170, SCMFSA_2: 68;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A160, A170, SCMFSA_2: 68;

                hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A163, A171;

              end;

            end;

            then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

            hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

            now

              let x be object;

              assume

               A172: x in ( dom ( DataPart Cs3i1));

              per cases by A22, A172, SCMFSA_2: 100, XBOOLE_0:def 3;

                suppose x in FinSeq-Locations ;

                then

                reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

                

                 A173: (Cs3i1 . d) = (Cs3i . d) by A42, A135, A160, SCMFSA_2: 68;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A160, SCMFSA_2: 68;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A172, A173;

              end;

                suppose

                 A174: da = x;

                then

                 A175: (Cs3i1 . x) = ((Cs3i . da) mod (Cs3i . db)) by A42, A135, A160, SCMFSA_2: 68;

                (Cs2i1 . x) = ((Cs2i . da) mod (Cs2i . db)) by A10, A17, A137, A160, A174, SCMFSA_2: 68;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A138, A136, A172, A175;

              end;

                suppose

                 A176: da <> x & x in Int-Locations ;

                then

                reconsider d = x as Int-Location by AMI_2:def 16;

                

                 A177: (Cs3i1 . d) = (Cs3i . d) by A42, A135, A160, A176, SCMFSA_2: 68;

                (Cs2i1 . d) = (Cs2i . d) by A10, A17, A137, A160, A176, SCMFSA_2: 68;

                hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A172, A177;

              end;

            end;

            then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

            hence ( DataPart Cs3i1) = ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 3;

          end;

        end;

          suppose ( InsCode I) = 6;

          then

          consider loc be Nat such that

           A178: I = ( goto loc) by SCMFSA_2: 35;

          

           A179: ( CurInstr (P2,Cs2i)) = ( goto (loc + k)) by A10, A178, SCMFSA_4: 1;

          

          thus (( IC ( Comput (P1,s1,(i + 1)))) + k) = (loc + k) by A49, A178, SCMFSA_2: 69

          .= ( IC ( Comput (P2,s2,(i + 1)))) by A17, A179, SCMFSA_2: 69;

          hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A23;

          now

            let x be object;

            assume

             A180: x in ( dom (Cs1i1 | ( dom DPp)));

            ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            then x in Int-Locations or x in FinSeq-Locations by A32, A180, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A181: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A182: (Cs2i1 . x) = (Cs2i . x) by A17, A179, SCMFSA_2: 69;

            (Cs1i1 . x) = (Cs1i . x) by A49, A178, A181, SCMFSA_2: 69;

            hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A180, A182;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A183: x in ( dom ( DataPart Cs3i1));

            then x in Int-Locations or x in FinSeq-Locations by A22, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A184: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A185: (Cs2i1 . x) = (Cs2i . x) by A17, A179, SCMFSA_2: 69;

            (Cs3i1 . x) = (Cs3i . x) by A42, A178, A184, SCMFSA_2: 69;

            hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A183, A185;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 7;

          then

          consider loc be Nat, da be Int-Location such that

           A186: I = (da =0_goto loc) by SCMFSA_2: 36;

           A187:

          now

            per cases ;

              case (Cs1i . da) = 0 ;

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = (loc + k) by A49, A186, SCMFSA_2: 70;

            end;

              case (Cs1i . da) <> 0 ;

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = (( IC Cs2i) + 1) by A9, A49, A57, A186, SCMFSA_2: 70;

            end;

          end;

          

           A188: ( CurInstr (P2,Cs2i)) = (da =0_goto (loc + k)) by A10, A186, SCMFSA_4: 2;

           A189:

          now

            per cases ;

              case (Cs2i . da) = 0 ;

              hence ( IC ( Comput (P2,s2,(i + 1)))) = (loc + k) by A17, A188, SCMFSA_2: 70;

            end;

              case (Cs2i . da) <> 0 ;

              hence ( IC ( Comput (P2,s2,(i + 1)))) = (( IC Cs2i) + 1) by A17, A188, SCMFSA_2: 70;

            end;

          end;

          

           A190: (Cs3i . da) = (Cs2i . da) by A29;

           A191:

          now

            per cases ;

              suppose loc <> (( IC Cs1i) + 1);

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A1, A7, A186, A190, A187, A189, A4, SCMFSA_3: 11;

            end;

              suppose loc = (( IC Cs1i) + 1);

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A187, A189;

            end;

          end;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1))));

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A23, A191;

          now

            let x be object;

            assume

             A192: x in ( dom (Cs1i1 | ( dom DPp)));

            ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            then x in Int-Locations or x in FinSeq-Locations by A32, A192, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A193: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A194: (Cs2i1 . x) = (Cs2i . x) by A17, A188, SCMFSA_2: 70;

            (Cs1i1 . x) = (Cs1i . x) by A49, A186, A193, SCMFSA_2: 70;

            hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A192, A194;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A195: x in ( dom ( DataPart Cs3i1));

            then x in Int-Locations or x in FinSeq-Locations by A22, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A196: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A197: (Cs2i1 . x) = (Cs2i . x) by A17, A188, SCMFSA_2: 70;

            (Cs3i1 . x) = (Cs3i . x) by A42, A186, A196, SCMFSA_2: 70;

            hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A195, A197;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 8;

          then

          consider loc be Nat, da be Int-Location such that

           A198: I = (da >0_goto loc) by SCMFSA_2: 37;

           A199:

          now

            per cases ;

              case (Cs1i . da) > 0 ;

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = (loc + k) by A49, A198, SCMFSA_2: 71;

            end;

              case (Cs1i . da) <= 0 ;

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = (( IC Cs2i) + 1) by A9, A49, A57, A198, SCMFSA_2: 71;

            end;

          end;

          

           A200: ( CurInstr (P2,Cs2i)) = (da >0_goto (loc + k)) by A10, A198, SCMFSA_4: 3;

           A201:

          now

            per cases ;

              case (Cs2i . da) > 0 ;

              hence ( IC ( Comput (P2,s2,(i + 1)))) = (loc + k) by A17, A200, SCMFSA_2: 71;

            end;

              case (Cs2i . da) <= 0 ;

              hence ( IC ( Comput (P2,s2,(i + 1)))) = (( IC Cs2i) + 1) by A17, A200, SCMFSA_2: 71;

            end;

          end;

          

           A202: (Cs3i . da) = (Cs2i . da) by A29;

           A203:

          now

            per cases ;

              suppose loc <> (( IC Cs1i) + 1);

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A1, A7, A198, A202, A199, A201, A4, SCMFSA_3: 12;

            end;

              suppose loc = (( IC Cs1i) + 1);

              hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A199, A201;

            end;

          end;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1))));

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A23, A203;

          now

            let x be object;

            assume

             A204: x in ( dom (Cs1i1 | ( dom DPp)));

            ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            then x in Int-Locations or x in FinSeq-Locations by A32, A204, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A205: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A206: (Cs2i1 . x) = (Cs2i . x) by A17, A200, SCMFSA_2: 71;

            (Cs1i1 . x) = (Cs1i . x) by A49, A198, A205, SCMFSA_2: 71;

            hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A204, A206;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A207: x in ( dom ( DataPart Cs3i1));

            then x in Int-Locations or x in FinSeq-Locations by A22, SCMFSA_2: 100, XBOOLE_0:def 3;

            then

             A208: x is Int-Location or x is FinSeq-Location by AMI_2:def 16, SCMFSA_2:def 5;

            then

             A209: (Cs2i1 . x) = (Cs2i . x) by A17, A200, SCMFSA_2: 71;

            (Cs3i1 . x) = (Cs3i . x) by A42, A198, A208, SCMFSA_2: 71;

            hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A207, A209;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 9;

          then

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

           A210: I = (da := (f,db)) by SCMFSA_2: 38;

          

           A211: (Cs3i . f) = (Cs2i . f) by A19;

          

           A212: ( IncAddr (I,k)) = (da := (f,db)) by A210, COMPOS_0: 4;

          

           A213: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A210, SCMFSA_2: 72;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A212, SCMFSA_2: 72;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A212, A213, SCMFSA_2: 72;

          

           A214: (Cs3i . db) = (Cs2i . db) by A29;

          now

            let x be object;

            

             A215: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            assume

             A216: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A216, A215, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A217: (Cs1i1 . d) = (Cs1i . d) by A49, A210, SCMFSA_2: 72;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A212, SCMFSA_2: 72;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A216, A217;

            end;

              suppose

               A218: da = x;

              then

              consider k1 be Nat such that

               A219: k1 = |.(Cs1i . db).| and

               A220: (Cs1i1 . x) = ((Cs1i . f) /. k1) by A49, A210, SCMFSA_2: 72;

              consider k2 be Nat such that

               A221: k2 = |.(Cs2i . db).| and

               A222: (Cs2i1 . x) = ((Cs2i . f) /. k2) by A10, A17, A212, A218, SCMFSA_2: 72;

              DPp c= p by RELAT_1: 59;

              then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              then ((Cs3i . f) /. k2) = ((Cs1i . f) /. k1) by A1, A7, A32, A210, A214, A216, A218, A219, A221, A4, SCMFSA_3: 13;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A211, A216, A220, A222;

            end;

              suppose

               A223: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A224: (Cs1i1 . d) = (Cs1i . d) by A49, A210, A223, SCMFSA_2: 72;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A212, A223, SCMFSA_2: 72;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A216, A224;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A225: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A225, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A226: (Cs3i1 . f) = (Cs3i . f) by A42, A210, SCMFSA_2: 72;

              (Cs2i1 . f) = (Cs2i . f) by A10, A17, A212, SCMFSA_2: 72;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A225, A226;

            end;

              suppose

               A227: da = x;

              then

               A228: ex k1 be Nat st k1 = |.(Cs3i . db).| & (Cs3i1 . x) = ((Cs3i . f) /. k1) by A42, A210, SCMFSA_2: 72;

              ex k2 be Nat st k2 = |.(Cs2i . db).| & (Cs2i1 . x) = ((Cs2i . f) /. k2) by A10, A17, A212, A227, SCMFSA_2: 72;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A214, A211, A225, A228;

            end;

              suppose

               A229: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A230: (Cs3i1 . d) = (Cs3i . d) by A42, A210, A229, SCMFSA_2: 72;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A212, A229, SCMFSA_2: 72;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A225, A230;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 10;

          then

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

           A231: I = ((f,db) := da) by SCMFSA_2: 39;

          

           A232: (Cs3i . f) = (Cs2i . f) by A19;

          

           A233: ( IncAddr (I,k)) = ((f,db) := da) by A231, COMPOS_0: 4;

          

           A234: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A231, SCMFSA_2: 73;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A233, SCMFSA_2: 73;

          

           A235: (Cs3i . da) = (Cs2i . da) by A29;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A233, A234, SCMFSA_2: 73;

          

           A236: (Cs3i . db) = (Cs2i . db) by A29;

          now

            let x be object;

            

             A237: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            assume

             A238: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A238, A237, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A239: (Cs1i1 . d) = (Cs1i . d) by A49, A231, SCMFSA_2: 73;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A233, SCMFSA_2: 73;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A238, A239;

            end;

              suppose

               A240: f = x;

              then

              consider k1 be Nat such that

               A241: k1 = |.(Cs1i . db).| and

               A242: (Cs1i1 . x) = ((Cs1i . f) +* (k1,(Cs1i . da))) by A49, A231, SCMFSA_2: 73;

              consider k2 be Nat such that

               A243: k2 = |.(Cs2i . db).| and

               A244: (Cs2i1 . x) = ((Cs2i . f) +* (k2,(Cs2i . da))) by A10, A17, A233, A240, SCMFSA_2: 73;

              DPp c= p by RELAT_1: 59;

              then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              then ((Cs3i . f) +* (k2,(Cs3i . da))) = ((Cs1i . f) +* (k1,(Cs1i . da))) by A1, A7, A32, A231, A236, A238, A240, A241, A243, A4, SCMFSA_3: 14;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A235, A232, A238, A242, A244;

            end;

              suppose

               A245: f <> x & x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A246: (Cs1i1 . d) = (Cs1i . d) by A49, A231, A245, SCMFSA_2: 73;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A233, A245, SCMFSA_2: 73;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A238, A246;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A247: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A247, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in Int-Locations ;

              then

              reconsider f = x as Int-Location by AMI_2:def 16;

              

               A248: (Cs3i1 . f) = (Cs3i . f) by A42, A231, SCMFSA_2: 73;

              (Cs2i1 . f) = (Cs2i . f) by A10, A17, A233, SCMFSA_2: 73;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A247, A248;

            end;

              suppose

               A249: f = x;

              then

               A250: ex k1 be Nat st k1 = |.(Cs3i . db).| & (Cs3i1 . x) = ((Cs3i . f) +* (k1,(Cs3i . da))) by A42, A231, SCMFSA_2: 73;

              ex k2 be Nat st k2 = |.(Cs2i . db).| & (Cs2i1 . x) = ((Cs2i . f) +* (k2,(Cs2i . da))) by A10, A17, A233, A249, SCMFSA_2: 73;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A236, A235, A232, A247, A250;

            end;

              suppose

               A251: f <> x & x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A252: (Cs3i1 . d) = (Cs3i . d) by A42, A231, A251, SCMFSA_2: 73;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A233, A251, SCMFSA_2: 73;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A247, A252;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 11;

          then

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

           A253: I = (da :=len f) by SCMFSA_2: 40;

          

           A254: ( IncAddr (I,k)) = (da :=len f) by A253, COMPOS_0: 4;

          

           A255: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A253, SCMFSA_2: 74;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A254, SCMFSA_2: 74;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A254, A255, SCMFSA_2: 74;

          

           A256: (Cs3i . f) = (Cs2i . f) by A19;

          now

            let x be object;

            

             A257: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            assume

             A258: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A258, A257, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A259: (Cs1i1 . d) = (Cs1i . d) by A49, A253, SCMFSA_2: 74;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A254, SCMFSA_2: 74;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A258, A259;

            end;

              suppose

               A260: da = x;

              DPp c= p by RELAT_1: 59;

              then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              then

               A261: ( len (Cs3i . f)) = ( len (Cs1i . f)) by A1, A7, A32, A253, A258, A260, A4, SCMFSA_3: 15;

              

               A262: (Cs1i1 . x) = ( len (Cs1i . f)) by A49, A253, A260, SCMFSA_2: 74;

              (Cs2i1 . x) = ( len (Cs2i . f)) by A10, A17, A254, A260, SCMFSA_2: 74;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A256, A258, A262, A261;

            end;

              suppose

               A263: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A264: (Cs1i1 . d) = (Cs1i . d) by A49, A253, A263, SCMFSA_2: 74;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A254, A263, SCMFSA_2: 74;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A258, A264;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A265: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A265, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in FinSeq-Locations ;

              then

              reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A266: (Cs3i1 . f) = (Cs3i . f) by A42, A253, SCMFSA_2: 74;

              (Cs2i1 . f) = (Cs2i . f) by A10, A17, A254, SCMFSA_2: 74;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A265, A266;

            end;

              suppose

               A267: da = x;

              then

               A268: (Cs3i1 . x) = ( len (Cs3i . f)) by A42, A253, SCMFSA_2: 74;

              (Cs2i1 . x) = ( len (Cs2i . f)) by A10, A17, A254, A267, SCMFSA_2: 74;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A256, A265, A268;

            end;

              suppose

               A269: da <> x & x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A270: (Cs3i1 . d) = (Cs3i . d) by A42, A253, A269, SCMFSA_2: 74;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A254, A269, SCMFSA_2: 74;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A265, A270;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

          suppose ( InsCode I) = 12;

          then

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

           A271: I = (f :=<0,...,0> da) by SCMFSA_2: 41;

          

           A272: ( IncAddr (I,k)) = (f :=<0,...,0> da) by A271, COMPOS_0: 4;

          

           A273: (( Exec (I,Cs1i)) . ( IC SCM+FSA )) = (( IC Cs1i) + 1) by A271, SCMFSA_2: 75;

          hence (( IC ( Comput (P1,s1,(i + 1)))) + k) = ( IC ( Comput (P2,s2,(i + 1)))) by A9, A10, A49, A17, A57, A272, SCMFSA_2: 75;

          thus ( IncAddr (( CurInstr (P1,( Comput (P1,s1,(i + 1))))),k)) = ( CurInstr (P2,( Comput (P2,s2,(i + 1))))) by A9, A10, A23, A49, A17, A57, A272, A273, SCMFSA_2: 75;

          

           A274: (Cs3i . da) = (Cs2i . da) by A29;

          now

            let x be object;

            

             A275: ( dom DPp) c= ( Data-Locations SCM+FSA ) by RELAT_1: 58;

            assume

             A276: x in ( dom (Cs1i1 | ( dom DPp)));

            per cases by A32, A276, A275, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in Int-Locations ;

              then

              reconsider d = x as Int-Location by AMI_2:def 16;

              

               A277: (Cs1i1 . d) = (Cs1i . d) by A49, A271, SCMFSA_2: 75;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A272, SCMFSA_2: 75;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A276, A277;

            end;

              suppose

               A278: f = x;

              then

              consider k1 be Nat such that

               A279: k1 = |.(Cs1i . da).| and

               A280: (Cs1i1 . x) = (k1 |-> 0 ) by A49, A271, SCMFSA_2: 75;

              consider k2 be Nat such that

               A281: k2 = |.(Cs2i . da).| and

               A282: (Cs2i1 . x) = (k2 |-> 0 ) by A10, A17, A272, A278, SCMFSA_2: 75;

              DPp c= p by RELAT_1: 59;

              then ( dom DPp) c= ( dom p) by GRFUNC_1: 2;

              then (k2 |-> 0 ) = (k1 |-> 0 ) by A1, A7, A32, A271, A274, A276, A278, A279, A281, A4, SCMFSA_3: 16;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A44, A276, A280, A282;

            end;

              suppose

               A283: f <> x & x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A284: (Cs1i1 . d) = (Cs1i . d) by A49, A271, A283, SCMFSA_2: 75;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A272, A283, SCMFSA_2: 75;

              hence ((Cs1i1 | ( dom DPp)) . x) = ((Cs2i1 | ( dom DPp)) . x) by A32, A51, A276, A284;

            end;

          end;

          then (Cs1i1 | ( dom DPp)) c= (Cs2i1 | ( dom DPp)) by A32, A43, GRFUNC_1: 2;

          hence (( Comput (P1,s1,(i + 1))) | ( dom ( DataPart p))) = (( Comput (P2,s2,(i + 1))) | ( dom ( DataPart p))) by A32, A43, GRFUNC_1: 3;

          now

            let x be object;

            assume

             A285: x in ( dom ( DataPart Cs3i1));

            per cases by A22, A285, SCMFSA_2: 100, XBOOLE_0:def 3;

              suppose x in Int-Locations ;

              then

              reconsider f = x as Int-Location by AMI_2:def 16;

              

               A286: (Cs3i1 . f) = (Cs3i . f) by A42, A271, SCMFSA_2: 75;

              (Cs2i1 . f) = (Cs2i . f) by A10, A17, A272, SCMFSA_2: 75;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A285, A286;

            end;

              suppose

               A287: f = x;

              then

               A288: ex k1 be Nat st k1 = |.(Cs3i . da).| & (Cs3i1 . x) = (k1 |-> 0 ) by A42, A271, SCMFSA_2: 75;

              ex k2 be Nat st k2 = |.(Cs2i . da).| & (Cs2i1 . x) = (k2 |-> 0 ) by A10, A17, A272, A287, SCMFSA_2: 75;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A34, A274, A285, A288;

            end;

              suppose

               A289: f <> x & x in FinSeq-Locations ;

              then

              reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;

              

               A290: (Cs3i1 . d) = (Cs3i . d) by A42, A271, A289, SCMFSA_2: 75;

              (Cs2i1 . d) = (Cs2i . d) by A10, A17, A272, A289, SCMFSA_2: 75;

              hence (( DataPart Cs3i1) . x) = (( DataPart Cs2i1) . x) by A38, A285, A290;

            end;

          end;

          then ( DataPart Cs3i1) c= ( DataPart ( Comput (P2,s2,(i + 1)))) by A22, A33, GRFUNC_1: 2;

          hence thesis by A22, A33, GRFUNC_1: 3;

        end;

      end;

      reconsider ii = ( IC p) as Nat;

      

       A291: ( IC SCM+FSA ) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

      now

        

        thus (( IC ( Comput (P1,s1, 0 ))) + k) = (( IC s1) + k)

        .= (( IC p) + k) by A1, A3, GRFUNC_1: 2

        .= (( IC p) + k)

        .= ( IC ( IncIC (p,k))) by MEMSTR_0: 53

        .= ( IC s2) by A2, A291, GRFUNC_1: 2

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

        reconsider loc = ( IC p) as Nat;

        

         A292: ( IC p) = ( IC s1) by A1, A3, GRFUNC_1: 2;

        then ( IC p) = ( IC ( Comput (P1,s1, 0 )));

        then

         A293: loc in ( dom q) by A6, A1, AMISTD_5:def 4;

        

         A294: (( IC p) + k) in ( dom ( Reloc (q,k))) by A293, COMPOS_1: 46;

        

         A295: ( IC SCM+FSA ) in ( dom ( IncIC (p,k))) by MEMSTR_0: 52;

        

         A296: (q . ( IC p)) = (P1 . ( IC s1)) by A292, A293, A4, GRFUNC_1: 2;

        ( dom P2) = NAT by PARTFUN1:def 2;

        

        then

         A297: ( CurInstr (P2,( Comput (P2,s2, 0 )))) = (P2 . ( IC ( Comput (P2,s2, 0 )))) by PARTFUN1:def 6

        .= (P2 . ( IC s2))

        .= (P2 . ( IC ( IncIC (p,k)))) by A2, A295, GRFUNC_1: 2

        .= (P2 . (( IC p) + k)) by MEMSTR_0: 53

        .= (P2 . (( IC p) + k))

        .= (( Reloc (q,k)) . (( IC p) + k)) by A294, A4, GRFUNC_1: 2;

        

         A298: ( dom P1) = NAT by PARTFUN1:def 2;

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

        .= (P1 . ( IC s1)) by A298, PARTFUN1:def 6;

        hence ( IncAddr (( CurInstr (P1,( Comput (P1,s1, 0 )))),k)) = ( CurInstr (P2,( Comput (P2,s2, 0 )))) by A297, A293, A296, COMPOS_1: 35;

        

         A299: ( DataPart p) c= p by RELAT_1: 59;

        

         A300: ( DataPart p) c= s1 by A1, A299, XBOOLE_1: 1;

        

         A301: ( DataPart ( IncIC (p,k))) = ( DataPart p) by MEMSTR_0: 51;

        ( DataPart p) c= ( IncIC (p,k)) by A301, MEMSTR_0: 12;

        then

         A302: ( DataPart p) c= s2 by A2, XBOOLE_1: 1;

        

        thus (( Comput (P1,s1, 0 )) | ( dom ( DataPart p))) = (s1 | ( dom ( DataPart p)))

        .= ( DataPart p) by A300, GRFUNC_1: 23

        .= (s2 | ( dom ( DataPart p))) by A302, GRFUNC_1: 23

        .= (( Comput (P2,s2, 0 )) | ( dom ( DataPart p)));

        

        thus ( DataPart ( Comput (P1,s3, 0 ))) = ( DataPart (s1 +* ( DataPart s2)))

        .= ( DataPart s2) by PBOOLE: 142

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

      end;

      then

       A303: Y[ 0 ];

      thus for i be Nat holds Y[i] from NAT_1:sch 2( A303, A8);

    end;

    registration

      cluster SCM+FSA -> relocable1 relocable2;

      coherence by Th1;

    end