let k be Nat; :: thesis:
let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; :: thesis:
let p be non empty q -autonomic FinPartState of SCM+FSA; :: thesis:
let s1, s2 be State of SCM+FSA; :: thesis:
assume that
A1: p c= s1 and
A2: IncIC (p,k) c= s2 ; :: thesis:
A3: IC in dom p by AMISTD_5:6;
let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis:
assume A4: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis:
A5: Reloc (q,k) c= P2 by A4;
A6: q c= P1 by A4;
set s3 = s1 +* (DataPart s2);
defpred S₁[ 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,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) );
A7: p c= s1 +* (DataPart s2) by A1, A2, MEMSTR_0:61;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

set DPp = DataPart p;
let i be Nat; :: thesis:
assume 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,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; :: thesis:
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A13: dom (Comput (P1,s1,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
A14: dom (Comput (P1,s1,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set Cs2i1 = Comput (P2,s2,(i + 1));
A15: dom (Comput (P2,s2,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
A16: dom (Comput (P2,s2,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A17: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;

A18: now :: thesis:

let s be State of SCM+FSA; :: thesis:
let d be FinSeq-Location ; :: thesis:
d in FinSeq-Locations by SCMFSA_2:def 5;
then d in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence d in dom (DataPart s) by MEMSTR_0:9; :: thesis:

end;

A19: now :: thesis:

let d be FinSeq-Location ; :: thesis:
A20: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A18;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:47
.= (Comput (P2,s2,i)) . d by A12, A20, FUNCT_1:47 ;
:: thesis:

end;

set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
A21: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9;
A22: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9;

A23: now :: thesis:

reconsider loc = IC (Comput (P1,s1,(i + 1))) as Nat ;
assume A24: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis:
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,(Comput (P1,s1,(i + 1)))) = 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 ;
:: thesis:

end;

A28: now :: thesis:

let s be State of SCM+FSA; :: thesis:
let d be Int-Location; :: thesis:
d in Int-Locations by AMI_2:def 16;
then d in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence d in dom (DataPart s) by MEMSTR_0:9; :: thesis:

end;

A29: now :: thesis:

let d be Int-Location; :: thesis:
A30: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A28;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:47
.= (Comput (P2,s2,i)) . d by A12, A30, FUNCT_1:47 ;
:: thesis:

end;

dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61;
then A31: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17;
A32: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A13, A31, XBOOLE_1:28 ;
A33: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9;

A34: now :: thesis:

let x be object ; :: thesis:
assume that
A35: x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) and
A36: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x ; :: thesis:
thus (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (Comput (P2,s2,(i + 1))) . x by A35, A36, FUNCT_1:47
.= (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A33, A35, FUNCT_1:47 ; :: thesis:

end;

A37: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9;

A38: now :: thesis:

let x be set ; :: thesis:
assume that
A39: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A40: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x and
A41: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x ; :: thesis:
(DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A37, A22, A39, FUNCT_1:47;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A12, A21, A22, A34, A39, A40, A41, FUNCT_1:47; :: thesis:

end;

A42: Comput (P1,(s1 +* (DataPart s2)),(i + 1)) = Following (P1,(Comput (P1,(s1 +* (DataPart s2)),i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,(s1 +* (DataPart s2)),i))) by A1, A7, A4, AMISTD_5:7 ;
A43: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A15, A31, XBOOLE_1:28 ;

A44: now :: thesis:

let x, d be set ; :: thesis:
assume that
A45: d = x and
A46: d in dom (DataPart p) and
A47: (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d ; :: thesis:
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A32, A45, A46, A47, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A45, A46, FUNCT_1:47 ; :: thesis:

end;

A48: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A14, A31, XBOOLE_1:28 ;
reconsider j = IC (Comput (P1,s1,i)) as Nat ;
A49: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A50: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A16, A31, XBOOLE_1:28 ;

A51: now :: thesis:

let x, d be set ; :: thesis:
assume that
A52: d = x and
A53: d in dom (DataPart p) and
A54: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d and
A55: (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ; :: thesis:
A56: ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d by A48, A53, FUNCT_1:47;
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d by A50, A53, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A11, A32, A52, A53, A54, A55, A56, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A52, A53, FUNCT_1:47 ;
:: thesis:

end;

A57: ((IC (Comput (P1,s1,i))) + k) + 1 = (j + k) + 1
.= (j + 1) + k
.= ((IC (Comput (P1,s1,i))) + 1) + k ;
not not InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 & ... & not InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12 by SCMFSA_2:16;

per cases ;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; :: thesis:

then A58: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM+FSA by SCMFSA_2:95;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A49, A58, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A9, A17, A58, A10, EXTPRO_1:def 3 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A23; :: thesis:
A59: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) 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; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A12, A42, A58, A59, EXTPRO_1:def 3; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 ; :: thesis:

then consider da, db being Int-Location such that
A60: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMFSA_2:30;
A61: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A60, COMPOS_0:4;
A62: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A63: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

let x be object ; :: thesis:
A64: dom (DataPart p) c= Data-Locations by RELAT_1:58;
assume A65: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A66: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A61, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A65, A66; :: thesis:

end;

suppose A67: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A68: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db by A1, A7, A32, A60, A65, A67, A4, SCMFSA_3:5;
A69: (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db by A49, A60, A67, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db by A10, A17, A61, A67, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A63, A65, A69, A68; :: thesis:

end;

suppose A70: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A71: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A60, A70, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A61, A70, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A65, A71; :: thesis:

end;

then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) 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; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A72: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A73: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A42, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A61, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A72, A73; :: thesis:

end;

suppose A74: da = x ; :: thesis:

A75: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . db by A42, A60, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A10, A17, A61, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A29, A34, A72, A74, A75; :: thesis:

end;

suppose A76: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A77: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A60, A76, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A61, A76, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A72, A77; :: thesis:

end;

then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A33, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A33, GRFUNC_1:3; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 ; :: thesis:

then consider da, db being Int-Location such that
A78: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMFSA_2:31;
A79: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A80: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A78, COMPOS_0:4;
A81: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A82: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

A83: dom (DataPart p) c= Data-Locations by RELAT_1:58;
let x be object ; :: thesis:
assume A84: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A85: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A80, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A84, A85; :: thesis:

end;

suppose A86: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A87: dom (DataPart p) c= dom p by GRFUNC_1:2;
A88: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A49, A78, A86, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A80, A86, SCMFSA_2:64;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A32, A78, A82, A79, A84, A86, A88, A87, A4, SCMFSA_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A84; :: thesis:

end;

suppose A89: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A90: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A78, A89, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A80, A89, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A84, A90; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A91: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A92: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A80, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A91, A92; :: thesis:

end;

suppose A93: da = x ; :: thesis:

then A94: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A78, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A80, A93, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A82, A79, A91, A94; :: thesis:

end;

suppose A95: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A96: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A78, A95, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A80, A95, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A91, A96; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 ; :: thesis:

then consider da, db being Int-Location such that
A97: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMFSA_2:32;
A98: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A99: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A97, COMPOS_0:4;
A100: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A101: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

A102: dom (DataPart p) c= Data-Locations by RELAT_1:58;
let x be object ; :: thesis:
assume A103: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A104: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A99, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A103, A104; :: thesis:

end;

suppose A105: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A106: dom (DataPart p) c= dom p by GRFUNC_1:2;
A107: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A49, A97, A105, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A99, A105, SCMFSA_2:65;
then ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x by A1, A7, A32, A97, A101, A98, A103, A105, A106, A4, SCMFSA_3:7;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A103, A107; :: thesis:

end;

suppose A108: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A109: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A97, A108, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A99, A108, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A103, A109; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A110: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A111: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A99, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A110, A111; :: thesis:

end;

suppose A112: da = x ; :: thesis:

then A113: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A97, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A99, A112, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A101, A98, A110, A113; :: thesis:

end;

suppose A114: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A115: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A97, A114, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A99, A114, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A110, A115; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 ; :: thesis:

then consider da, db being Int-Location such that
A116: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMFSA_2:33;
A117: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A118: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A116, COMPOS_0:4;
A119: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A120: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

A121: dom (DataPart p) c= Data-Locations by RELAT_1:58;
let x be object ; :: thesis:
assume A122: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A123: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A118, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A122, A123; :: thesis:

end;

suppose A124: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A125: dom (DataPart p) c= dom p by GRFUNC_1:2;
A126: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A49, A116, A124, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A118, A124, SCMFSA_2:66;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A32, A116, A120, A117, A122, A124, A126, A125, A4, SCMFSA_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A122; :: thesis:

end;

suppose A127: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A128: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A116, A127, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A118, A127, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A122, A128; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A129: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A130: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A118, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A129, A130; :: thesis:

end;

suppose A131: da = x ; :: thesis:

then A132: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A116, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A118, A131, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A120, A117, A129, A132; :: thesis:

end;

suppose A133: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A134: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A116, A133, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A118, A133, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A129, A134; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; :: thesis:

then consider da, db being Int-Location such that
A135: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by SCMFSA_2:34;
A136: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A137: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A135, COMPOS_0:4;
A138: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

per cases ;

suppose A139: da <> db ; :: thesis:

A140: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:

now :: thesis:

A141: dom (DataPart p) c= Data-Locations by RELAT_1:58;
let x be object ; :: thesis:
assume A142: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose ( db <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A143: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A142, A143; :: thesis:

end;

suppose A144: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A145: ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A1, A7, A32, A135, A139, A142, A144, A4, SCMFSA_3:9;
A146: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A49, A135, A139, A144, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A10, A17, A137, A139, A144, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A138, A136, A142, A146, A145, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A43, A142, FUNCT_1:47 ;
:: thesis:

end;

suppose A147: db = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A148: dom (DataPart p) c= dom p by GRFUNC_1:2;
A149: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A49, A135, A147, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A137, A147, SCMFSA_2:67;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A32, A135, A138, A136, A142, A147, A149, A148, A4, SCMFSA_3:10;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A142; :: thesis:

end;

suppose A150: ( da <> x & db <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A151: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A135, A150, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A150, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A142, A151; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A152: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A153: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A152, A153; :: thesis:

end;

suppose A154: da = x ; :: thesis:

then A155: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A135, A139, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A10, A17, A137, A139, A154, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A138, A136, A152, A155; :: thesis:

end;

suppose A156: db = x ; :: thesis:

then A157: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A135, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A137, A156, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A138, A136, A152, A157; :: thesis:

end;

suppose A158: ( da <> x & db <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A159: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A135, A158, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A158, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A152, A159; :: thesis:

end;

suppose A160: da = db ; :: thesis:

then A161: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:

now :: thesis:

A162: dom (DataPart p) c= Data-Locations by RELAT_1:58;
let x be object ; :: thesis:
assume A163: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A164: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A160, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A163, A164; :: thesis:

end;

suppose A165: da = x ; :: thesis:

A166: ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A32, A43, A163, FUNCT_1:47;
A167: ((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x by A32, A48, A163, FUNCT_1:47;
A168: ((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x by A32, A50, A163, FUNCT_1:47;
A169: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x by A163, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A137, A160, A165, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A11, A49, A135, A160, A165, A167, A168, A169, A166, SCMFSA_2:68; :: thesis:

end;

suppose A170: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A171: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A135, A160, A170, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A160, A170, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A163, A171; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A172: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A173: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A160, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A172, A173; :: thesis:

end;

suppose A174: da = x ; :: thesis:

then A175: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A42, A135, A160, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A137, A160, A174, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A138, A136, A172, A175; :: thesis:

end;

suppose A176: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A177: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A135, A160, A176, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A137, A160, A176, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A172, A177; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 ; :: thesis:

then consider loc being Nat such that
A178: CurInstr (P1,(Comput (P1,s1,i))) = goto loc by SCMFSA_2:35;
A179: CurInstr (P2,(Comput (P2,s2,i))) = 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 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A23; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A180: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Data-Locations 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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A179, SCMFSA_2:69;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A49, A178, A181, SCMFSA_2:69;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A180, A182; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A183: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A179, SCMFSA_2:69;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A42, A178, A184, SCMFSA_2:69;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A183, A185; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ; :: thesis:

then consider loc being Nat, da being Int-Location such that
A186: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by SCMFSA_2:36;

A187: now :: thesis:

per cases ) . da = 0 or (Comput (P1,s1,i)) . da <> 0 ) ;

case (Comput (P1,s1,i)) . da = 0 ; :: thesis:

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

end;

case (Comput (P1,s1,i)) . da <> 0 ; :: thesis:

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

end;

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

A189: now :: thesis:

per cases ) . da = 0 or (Comput (P2,s2,i)) . da <> 0 ) ;

case (Comput (P2,s2,i)) . da = 0 ; :: thesis:

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

end;

case (Comput (P2,s2,i)) . da <> 0 ; :: thesis:

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

end;

A190: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

A191: now :: thesis:

per cases ;

suppose loc <> (IC (Comput (P1,s1,i))) + 1 ; :: thesis:

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; :: thesis:

end;

suppose loc = (IC (Comput (P1,s1,i))) + 1 ; :: thesis:

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

end;

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

now :: thesis:

let x be object ; :: thesis:
assume A192: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Data-Locations 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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A188, SCMFSA_2:70;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A49, A186, A193, SCMFSA_2:70;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A192, A194; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A195: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A188, SCMFSA_2:70;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A42, A186, A196, SCMFSA_2:70;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A195, A197; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 ; :: thesis:

then consider loc being Nat, da being Int-Location such that
A198: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by SCMFSA_2:37;

A199: now :: thesis:

per cases ) . da > 0 or (Comput (P1,s1,i)) . da <= 0 ) ;

case (Comput (P1,s1,i)) . da > 0 ; :: thesis:

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

end;

case (Comput (P1,s1,i)) . da <= 0 ; :: thesis:

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

end;

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

A201: now :: thesis:

per cases ) . da > 0 or (Comput (P2,s2,i)) . da <= 0 ) ;

case (Comput (P2,s2,i)) . da > 0 ; :: thesis:

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

end;

case (Comput (P2,s2,i)) . da <= 0 ; :: thesis:

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

end;

A202: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

A203: now :: thesis:

per cases ;

suppose loc <> (IC (Comput (P1,s1,i))) + 1 ; :: thesis:

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; :: thesis:

end;

suppose loc = (IC (Comput (P1,s1,i))) + 1 ; :: thesis:

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

end;

now :: thesis:

let x be object ; :: thesis:
assume A204: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Data-Locations 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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A200, SCMFSA_2:71;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A49, A198, A205, SCMFSA_2:71;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A204, A206; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A207: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
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: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A200, SCMFSA_2:71;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A42, A198, A208, SCMFSA_2:71;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A207, A209; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 9 ; :: thesis:

then consider db, da being Int-Location, f being FinSeq-Location such that
A210: CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) by SCMFSA_2:38;
A211: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;
A212: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := (f,db) by A210, COMPOS_0:4;
A213: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A214: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

let x be object ; :: thesis:
A215: dom (DataPart p) c= Data-Locations by RELAT_1:58;
assume A216: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A217: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A210, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A212, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A216, A217; :: thesis:

end;

suppose A218: da = x ; :: thesis:

then consider k1 being Nat such that
A219: k1 = |.((Comput (P1,s1,i)) . db).| and
A220: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) /. k1 by A49, A210, SCMFSA_2:72;
consider k2 being Nat such that
A221: k2 = |.((Comput (P2,s2,i)) . db).| and
A222: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 by A10, A17, A212, A218, SCMFSA_2:72;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k2 = ((Comput (P1,s1,i)) . f) /. k1 by A1, A7, A32, A210, A214, A216, A218, A219, A221, A4, SCMFSA_3:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A211, A216, A220, A222; :: thesis:

end;

suppose A223: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A224: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A210, A223, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A212, A223, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A216, A224; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A225: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A226: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A42, A210, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A212, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A225, A226; :: thesis:

end;

suppose A227: da = x ; :: thesis:

then A228: ex k1 being Nat st
( k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . db).| & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k1 ) by A42, A210, SCMFSA_2:72;
ex k2 being Nat st
( k2 = |.((Comput (P2,s2,i)) . db).| & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 ) by A10, A17, A212, A227, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A214, A211, A225, A228; :: thesis:

end;

suppose A229: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A230: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A210, A229, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A212, A229, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A225, A230; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 10 ; :: thesis:

then consider db, da being Int-Location, f being FinSeq-Location such that
A231: CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da by SCMFSA_2:39;
A232: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;
A233: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = (f,db) := da by A231, COMPOS_0:4;
A234: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
A235: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . 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; :: thesis:
A236: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

let x be object ; :: thesis:
A237: dom (DataPart p) c= Data-Locations by RELAT_1:58;
assume A238: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A239: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A231, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A233, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A238, A239; :: thesis:

end;

suppose A240: f = x ; :: thesis:

then consider k1 being Nat such that
A241: k1 = |.((Comput (P1,s1,i)) . db).| and
A242: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A49, A231, SCMFSA_2:73;
consider k2 being Nat such that
A243: k2 = |.((Comput (P2,s2,i)) . db).| and
A244: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) by A10, A17, A233, A240, SCMFSA_2:73;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (k2,((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A1, A7, A32, A231, A236, A238, A240, A241, A243, A4, SCMFSA_3:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A235, A232, A238, A242, A244; :: thesis:

end;

suppose A245: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A246: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A231, A245, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A233, A245, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A238, A246; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A247: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by AMI_2:def 16;
A248: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A42, A231, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A233, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A247, A248; :: thesis:

end;

suppose A249: f = x ; :: thesis:

then A250: ex k1 being Nat st
( k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . db).| & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (k1,((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) ) by A42, A231, SCMFSA_2:73;
ex k2 being Nat st
( k2 = |.((Comput (P2,s2,i)) . db).| & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) ) by A10, A17, A233, A249, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A236, A235, A232, A247, A250; :: thesis:

end;

suppose A251: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A252: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A231, A251, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A233, A251, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A247, A252; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 11 ; :: thesis:

then consider da being Int-Location, f being FinSeq-Location such that
A253: CurInstr (P1,(Comput (P1,s1,i))) = da :=len f by SCMFSA_2:40;
A254: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :=len f by A253, COMPOS_0:4;
A255: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A256: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;

now :: thesis:

let x be object ; :: thesis:
A257: dom (DataPart p) c= Data-Locations by RELAT_1:58;
assume A258: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A259: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A254, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A258, A259; :: thesis:

end;

suppose A260: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A261: len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f) by A1, A7, A32, A253, A258, A260, A4, SCMFSA_3:15;
A262: (Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f) by A49, A253, A260, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A254, A260, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A256, A258, A262, A261; :: thesis:

end;

suppose A263: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A264: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A253, A263, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A254, A263, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A258, A264; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A265: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A266: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A42, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A254, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A265, A266; :: thesis:

end;

suppose A267: da = x ; :: thesis:

then A268: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) by A42, A253, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A254, A267, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A256, A265, A268; :: thesis:

end;

suppose A269: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A270: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A253, A269, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A254, A269, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A265, A270; :: thesis:

end;

suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12 ; :: thesis:

then consider da being Int-Location, f being FinSeq-Location such that
A271: CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da by SCMFSA_2:41;
A272: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = f :=<0,...,0> da by A271, COMPOS_0:4;
A273: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 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; :: thesis:
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; :: thesis:
A274: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

let x be object ; :: thesis:
A275: dom (DataPart p) c= Data-Locations by RELAT_1:58;
assume A276: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A277: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A271, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A272, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A276, A277; :: thesis:

end;

suppose A278: f = x ; :: thesis:

then consider k1 being Nat such that
A279: k1 = |.((Comput (P1,s1,i)) . da).| and
A280: (Comput (P1,s1,(i + 1))) . x = k1 |-> 0 by A49, A271, SCMFSA_2:75;
consider k2 being Nat such that
A281: k2 = |.((Comput (P2,s2,i)) . da).| and
A282: (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 by A10, A17, A272, A278, SCMFSA_2:75;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) 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 ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A44, A276, A280, A282; :: thesis:

end;

suppose A283: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A284: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A49, A271, A283, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A272, A283, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A32, A51, A276, A284; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A285: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by AMI_2:def 16;
A286: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A42, A271, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A272, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A285, A286; :: thesis:

end;

suppose A287: f = x ; :: thesis:

then A288: ex k1 being Nat st
( k1 = |.((Comput (P1,(s1 +* (DataPart s2)),i)) . da).| & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = k1 |-> 0 ) by A42, A271, SCMFSA_2:75;
ex k2 being Nat st
( k2 = |.((Comput (P2,s2,i)) . da).| & (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 ) by A10, A17, A272, A287, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A34, A274, A285, A288; :: thesis:

end;

suppose A289: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A290: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A42, A271, A289, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A272, A289, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A38, A285, A290; :: thesis:

end;

reconsider ii = IC p as Nat ;
A291: IC in dom (IncIC (p,k)) by MEMSTR_0:52;

now :: thesis:

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)) ; :: thesis:
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 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; :: thesis:
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)) ; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2))
.= DataPart s2 by PBOOLE:142
.= DataPart (Comput (P2,s2,0)) ; :: thesis:

end;

then A303: S₁[ 0 ] ;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A303, A8); :: thesis: