let k be Element of NAT ; :: thesis:
let q be NAT -defined the Instructions 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: IC in dom p and
A2: p c= s1 and
A3: IncIC (p,k) c= s2 ; :: thesis:
B1: IC in dom p by A1;
B2: p c= s1 by A2;
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)) );
A10: p c= s1 +* (DataPart s2) by A2, A3, MEMSTR_0:61;
A11: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

set DPp = DataPart p;
let i be Element of NAT ; :: thesis:
assume that
A12: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A13: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
A14: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and
A15: 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);
A16: 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);
A17: dom (Comput (P1,s1,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set Cs2i1 = Comput (P2,s2,(i + 1));
A18: dom (Comput (P2,s2,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
A19: dom (Comput (P2,s2,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A20: 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))) ;

A21: now

let s be State of SCM+FSA; :: thesis:
let d be FinSeq-Location ; :: thesis:
d in FinSeq-Locations by SCMFSA_2:3;
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;

A22: now

let d be FinSeq-Location ; :: thesis:
A23: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A21;
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 A15, A23, FUNCT_1:47 ;
:: thesis:

end;

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

A26: now

reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A27: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis:
reconsider ii = loc as Element of NAT ;
A28: ii in dom q by A6, B2, AMISTD_5:def 4;
A29: loc + k in dom (Reloc (q,k)) by A28, COMPOS_1:46;
A30: 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 A28, A4, GRFUNC_1:2
.= q . loc ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A28, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A27, A29, A5, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A30, PARTFUN1:def 6 ;
:: thesis:

end;

A31: now

let s be State of SCM+FSA; :: thesis:
let d be Int-Location ; :: thesis:
d in Int-Locations by SCMFSA_2:2;
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;

A32: now

let d be Int-Location ; :: thesis:
A33: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A31;
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 A15, A33, FUNCT_1:47 ;
:: thesis:

end;

dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61;
then A34: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17;
A37: InsCode (CurInstr (P1,(Comput (P1,s1,i)))) <= 12 by SCMFSA_2:16;
A38: 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 A16, A34, XBOOLE_1:28 ;
A39: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9;

A40: now

let x be set ; :: thesis:
assume that
A41: x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) and
A42: (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 A41, A42, FUNCT_1:47
.= (DataPart (Comput (P2,s2,(i + 1)))) . x by A25, A39, A41, FUNCT_1:47 ; :: thesis:

end;

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

A44: now

let x be set ; :: thesis:
assume that
A45: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A46: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x and
A47: (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 A43, A25, A45, FUNCT_1:47;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A15, A24, A25, A40, A45, A46, A47, FUNCT_1:47; :: thesis:

end;

A48: 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 A2, A10, A4, AMISTD_5:7 ;
A50: 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 A18, A34, XBOOLE_1:28 ;

A51: now

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 (P2,s2,(i + 1))) . d ; :: thesis:
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A38, A52, A53, A54, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A50, A52, A53, FUNCT_1:47 ; :: thesis:

end;

A55: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A17, A34, XBOOLE_1:28 ;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A56: 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))) ;
A57: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A19, A34, XBOOLE_1:28 ;

A58: now

let x, d be set ; :: thesis:
assume that
A59: d = x and
A60: d in dom (DataPart p) and
A61: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d and
A62: (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ; :: thesis:
A63: ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d by A55, A60, FUNCT_1:47;
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d by A57, A60, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A14, A38, A59, A60, A61, A62, A63, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A50, A59, A60, FUNCT_1:47 ;
:: thesis:

end;

A64: succ ((IC (Comput (P1,s1,i))) + k) = (j + k) + 1 by NAT_1:38
.= (j + 1) + k
.= (succ (IC (Comput (P1,s1,i)))) + k by NAT_1:38 ;

per cases by A37, NAT_1:36;

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

then A65: 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 A56, A65, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A12, A20, A65, A13, EXTPRO_1:def 3 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A26; :: thesis:
A66: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A20, A65, A13, EXTPRO_1:def 3;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A14, A56, A65, EXTPRO_1:def 3; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A15, A48, A65, A66, 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
A67: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMFSA_2:30;
A68: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A67, COMPOS_1:11;
A69: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A67, SCMFSA_2:63;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A68, SCMFSA_2:63; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A68, A69, SCMFSA_2:63; :: thesis:
A70: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A73: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A67, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A72, A73; :: thesis:

end;

suppose A74: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A75: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db by A2, A10, A38, A67, A72, A74, A4, SCMFSA_3:5;
A76: (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db by A56, A67, A74, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db by A13, A20, A68, A74, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A70, A72, A76, A75; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A78: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A67, A77, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, A77, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A72, A78; :: thesis:

end;

then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A38, A50, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A38, A50, GRFUNC_1:3; :: thesis:

now

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

per cases by A25, A79, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:5;
A80: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A67, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A68, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A79, A80; :: thesis:

end;

suppose A81: da = x ; :: thesis:

A82: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . db by A48, A67, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A13, A20, A68, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A40, A79, A81, A82; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A84: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A67, A83, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, A83, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A79, A84; :: thesis:

end;

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

end;

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

then consider da, db being Int-Location such that
A85: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMFSA_2:31;
A86: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;
A87: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A85, COMPOS_1:11;
A88: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A85, SCMFSA_2:64;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A87, SCMFSA_2:64; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A87, A88, SCMFSA_2:64; :: thesis:
A89: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A92: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A85, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A91, A92; :: thesis:

end;

suppose A93: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A94: dom (DataPart p) c= dom p by GRFUNC_1:2;
A95: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A56, A85, A93, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A13, A20, A87, A93, SCMFSA_2:64;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A10, A38, A85, A89, A86, A91, A93, A95, A94, A4, SCMFSA_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A91; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A97: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A85, A96, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, A96, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A91, A97; :: thesis:

end;

now

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

per cases by A25, A98, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A99: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A85, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A98, A99; :: thesis:

end;

suppose A100: da = x ; :: thesis:

then A101: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A85, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A13, A20, A87, A100, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A89, A86, A98, A101; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A103: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A85, A102, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, A102, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A98, A103; :: thesis:

end;

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

then consider da, db being Int-Location such that
A104: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMFSA_2:32;
A105: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;
A106: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A104, COMPOS_1:11;
A107: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A104, SCMFSA_2:65;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A106, SCMFSA_2:65; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A106, A107, SCMFSA_2:65; :: thesis:
A108: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A111: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A104, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A110, A111; :: thesis:

end;

suppose A112: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A113: dom (DataPart p) c= dom p by GRFUNC_1:2;
A114: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A56, A104, A112, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A13, A20, A106, A112, SCMFSA_2:65;
then ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x by A2, A10, A38, A104, A108, A105, A110, A112, A113, A4, SCMFSA_3:7;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A110, A114; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A116: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A104, A115, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, A115, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A110, A116; :: thesis:

end;

now

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

per cases by A25, A117, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A118: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A104, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A117, A118; :: thesis:

end;

suppose A119: da = x ; :: thesis:

then A120: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A104, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A13, A20, A106, A119, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A108, A105, A117, A120; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A122: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A104, A121, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, A121, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A117, A122; :: thesis:

end;

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

then consider da, db being Int-Location such that
A123: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMFSA_2:33;
A124: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;
A125: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A123, COMPOS_1:11;
A126: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A123, SCMFSA_2:66;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A125, SCMFSA_2:66; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A125, A126, SCMFSA_2:66; :: thesis:
A127: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A130: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A123, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A129, A130; :: thesis:

end;

suppose A131: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A132: dom (DataPart p) c= dom p by GRFUNC_1:2;
A133: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A56, A123, A131, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A13, A20, A125, A131, SCMFSA_2:66;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A10, A38, A123, A127, A124, A129, A131, A133, A132, A4, SCMFSA_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A129; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A135: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A123, A134, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, A134, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A129, A135; :: thesis:

end;

now

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

per cases by A25, A136, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A137: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A123, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A136, A137; :: thesis:

end;

suppose A138: da = x ; :: thesis:

then A139: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A123, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A13, A20, A125, A138, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A127, A124, A136, A139; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A141: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A123, A140, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, A140, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A136, A141; :: thesis:

end;

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

then consider da, db being Int-Location such that
A142: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by SCMFSA_2:34;
A143: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;
A144: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A142, COMPOS_1:11;
A145: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

per cases ;

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

A147: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A142, SCMFSA_2:67;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A144, SCMFSA_2:67; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A144, A147, SCMFSA_2:67; :: thesis:

now

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

per cases by A38, A149, A148, 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:5;
A150: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A149, A150; :: thesis:

end;

suppose A151: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A152: ((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 A2, A10, A38, A142, A146, A149, A151, A4, SCMFSA_3:9;
A153: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A56, A142, A146, A151, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A13, A20, A144, A146, A151, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A145, A143, A149, A153, A152, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A50, A149, FUNCT_1:47 ;
:: thesis:

end;

suppose A154: db = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A155: dom (DataPart p) c= dom p by GRFUNC_1:2;
A156: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A56, A142, A154, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A154, SCMFSA_2:67;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A10, A38, A142, A145, A143, A149, A154, A156, A155, A4, SCMFSA_3:10;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A149; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A158: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A157, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A157, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A149, A158; :: thesis:

end;

now

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

per cases by A25, A159, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A160: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A159, A160; :: thesis:

end;

suppose A161: da = x ; :: thesis:

then A162: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A142, A146, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A13, A20, A144, A146, A161, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A145, A143, A159, A162; :: thesis:

end;

suppose A163: db = x ; :: thesis:

then A164: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A142, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A163, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A145, A143, A159, A164; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A166: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A165, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A165, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A159, A166; :: thesis:

end;

suppose A167: da = db ; :: thesis:

then A168: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A142, SCMFSA_2:68;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A144, A167, SCMFSA_2:68; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A144, A167, A168, SCMFSA_2:68; :: thesis:

now

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

per cases by A38, A170, A169, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A171: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A167, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A170, A171; :: thesis:

end;

suppose A172: da = x ; :: thesis:

A173: ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A38, A50, A170, FUNCT_1:47;
A174: ((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x by A38, A55, A170, FUNCT_1:47;
A175: ((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x by A38, A57, A170, FUNCT_1:47;
A176: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x by A170, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A167, A172, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A14, A56, A142, A167, A172, A174, A175, A176, A173, SCMFSA_2:68; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A178: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A167, A177, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, A177, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A170, A178; :: thesis:

end;

now

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

per cases by A25, A179, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A180: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A167, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A179, A180; :: thesis:

end;

suppose A181: da = x ; :: thesis:

then A182: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A48, A142, A167, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A167, A181, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A145, A143, A179, A182; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A184: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A167, A183, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, A183, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A179, A184; :: thesis:

end;

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

then consider loc being Element of NAT such that
A185: CurInstr (P1,(Comput (P1,s1,i))) = goto loc by SCMFSA_2:35;
A186: CurInstr (P2,(Comput (P2,s2,i))) = goto (loc + k) by A13, A185, SCMFSA_4:1;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A56, A185, SCMFSA_2:69
.= IC (Comput (P2,s2,(i + 1))) by A20, A186, SCMFSA_2:69 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A26; :: thesis:

now

let x be set ; :: thesis:
assume A187: 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 A38, A187, SCMFSA_2:100, XBOOLE_0:def 3;
then A188: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A189: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A186, SCMFSA_2:69;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A185, A188, SCMFSA_2:69;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A187, A189; :: thesis:

end;

now

let x be set ; :: thesis:
assume A190: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A25, SCMFSA_2:100, XBOOLE_0:def 3;
then A191: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A192: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A186, SCMFSA_2:69;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A185, A191, SCMFSA_2:69;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A190, A192; :: thesis:

end;

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

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

A194: now

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 A56, A193, SCMFSA_2:70; :: thesis:

end;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A12, A56, A64, A193, SCMFSA_2:70; :: thesis:

end;

A195: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A13, A193, SCMFSA_4:2;

A196: now

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 A20, A195, SCMFSA_2:70; :: thesis:

end;

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

hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A20, A195, SCMFSA_2:70; :: thesis:

end;

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

A198: now

per cases ;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A2, A10, A193, A197, A194, A196, A4, SCMFSA_3:11; :: thesis:

end;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A64, A194, A196; :: 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 A26, A198; :: thesis:

now

let x be set ; :: thesis:
assume A199: 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 A38, A199, SCMFSA_2:100, XBOOLE_0:def 3;
then A200: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A201: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A195, SCMFSA_2:70;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A193, A200, SCMFSA_2:70;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A199, A201; :: thesis:

end;

now

let x be set ; :: thesis:
assume A202: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A25, SCMFSA_2:100, XBOOLE_0:def 3;
then A203: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A204: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A195, SCMFSA_2:70;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A193, A203, SCMFSA_2:70;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A202, A204; :: thesis:

end;

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

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

A206: now

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 A56, A205, SCMFSA_2:71; :: thesis:

end;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A12, A56, A64, A205, SCMFSA_2:71; :: thesis:

end;

A207: CurInstr (P2,(Comput (P2,s2,i))) = da >0_goto (loc + k) by A13, A205, SCMFSA_4:3;

A208: now

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 A20, A207, SCMFSA_2:71; :: thesis:

end;

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

hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A20, A207, SCMFSA_2:71; :: thesis:

end;

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

A210: now

per cases ;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A2, A10, A205, A209, A206, A208, A4, SCMFSA_3:12; :: thesis:

end;

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A64, A206, A208; :: thesis:

end;

now

let x be set ; :: thesis:
assume A211: 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 A38, A211, SCMFSA_2:100, XBOOLE_0:def 3;
then A212: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A213: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A207, SCMFSA_2:71;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A205, A212, SCMFSA_2:71;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A211, A213; :: thesis:

end;

now

let x be set ; :: thesis:
assume A214: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A25, SCMFSA_2:100, XBOOLE_0:def 3;
then A215: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:4, SCMFSA_2:5;
then A216: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A207, SCMFSA_2:71;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A205, A215, SCMFSA_2:71;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A214, A216; :: 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
A217: CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) by SCMFSA_2:38;
A218: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A22;
A219: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := (f,db) by A217, COMPOS_1:11;
A220: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A217, SCMFSA_2:72;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A219, SCMFSA_2:72; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A219, A220, SCMFSA_2:72; :: thesis:
A221: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;

now

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

per cases by A38, A223, A222, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A224: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A217, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A223, A224; :: thesis:

end;

suppose A225: da = x ; :: thesis:

then consider k1 being Element of NAT such that
A226: k1 = abs ((Comput (P1,s1,i)) . db) and
A227: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) /. k1 by A56, A217, SCMFSA_2:72;
consider k2 being Element of NAT such that
A228: k2 = abs ((Comput (P2,s2,i)) . db) and
A229: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 by A13, A20, A219, A225, 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 A2, A10, A38, A217, A221, A223, A225, A226, A228, A4, SCMFSA_3:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A218, A223, A227, A229; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A231: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A217, A230, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, A230, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A223, A231; :: thesis:

end;

now

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

per cases by A25, A232, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:5;
A233: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A217, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A219, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A232, A233; :: thesis:

end;

suppose A234: da = x ; :: thesis:

then A235: ex k1 being Element of NAT st
( k1 = abs ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k1 ) by A48, A217, SCMFSA_2:72;
ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . db) & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 ) by A13, A20, A219, A234, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A221, A218, A232, A235; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A237: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A217, A236, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, A236, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A232, A237; :: 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
A238: CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da by SCMFSA_2:39;
A239: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A22;
A240: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = (f,db) := da by A238, COMPOS_1:11;
A241: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A238, SCMFSA_2:73;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A240, SCMFSA_2:73; :: thesis:
A242: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A240, A241, SCMFSA_2:73; :: thesis:
A243: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A32;

now

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

per cases by A38, A245, A244, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:4;
A246: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A238, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A245, A246; :: thesis:

end;

suppose A247: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A248: k1 = abs ((Comput (P1,s1,i)) . db) and
A249: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A56, A238, SCMFSA_2:73;
consider k2 being Element of NAT such that
A250: k2 = abs ((Comput (P2,s2,i)) . db) and
A251: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) by A13, A20, A240, A247, 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 A2, A10, A38, A238, A243, A245, A247, A248, A250, A4, SCMFSA_3:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A242, A239, A245, A249, A251; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A253: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A238, A252, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, A252, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A245, A253; :: thesis:

end;

now

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

per cases by A25, A254, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:4;
A255: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A238, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A240, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A254, A255; :: thesis:

end;

suppose A256: f = x ; :: thesis:

then A257: ex k1 being Element of NAT st
( k1 = abs ((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 A48, A238, SCMFSA_2:73;
ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . db) & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) ) by A13, A20, A240, A256, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A243, A242, A239, A254, A257; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A259: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A238, A258, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, A258, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A254, A259; :: thesis:

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A260: CurInstr (P1,(Comput (P1,s1,i))) = da :=len f by SCMFSA_2:40;
A261: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :=len f by A260, COMPOS_1:11;
A262: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A260, SCMFSA_2:74;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A261, SCMFSA_2:74; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A261, A262, SCMFSA_2:74; :: thesis:
A263: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A22;

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A266: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A260, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A265, A266; :: thesis:

end;

suppose A267: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A268: len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f) by A2, A10, A38, A260, A265, A267, A4, SCMFSA_3:15;
A269: (Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f) by A56, A260, A267, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A13, A20, A261, A267, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A263, A265, A269, A268; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A271: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A260, A270, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, A270, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A265, A271; :: thesis:

end;

now

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

per cases by A25, A272, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:5;
A273: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A260, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A261, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A272, A273; :: thesis:

end;

suppose A274: da = x ; :: thesis:

then A275: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) by A48, A260, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A13, A20, A261, A274, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A263, A272, A275; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:4;
A277: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A260, A276, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, A276, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A272, A277; :: thesis:

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A278: CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da by SCMFSA_2:41;
A279: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = f :=<0,...,0> da by A278, COMPOS_1:11;
A280: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A278, SCMFSA_2:75;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A279, SCMFSA_2:75; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, A13, A26, A56, A20, A64, A279, A280, SCMFSA_2:75; :: thesis:
A281: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

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

per cases by A38, A283, A282, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:4;
A284: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A283, A284; :: thesis:

end;

suppose A285: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A286: k1 = abs ((Comput (P1,s1,i)) . da) and
A287: (Comput (P1,s1,(i + 1))) . x = k1 |-> 0 by A56, A278, SCMFSA_2:75;
consider k2 being Element of NAT such that
A288: k2 = abs ((Comput (P2,s2,i)) . da) and
A289: (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 by A13, A20, A279, A285, 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 A2, A10, A38, A278, A281, A283, A285, A286, A288, A4, SCMFSA_3:16;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A51, A283, A287, A289; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A291: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, A290, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, A290, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A38, A58, A283, A291; :: thesis:

end;

now

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

per cases by A25, A292, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:4;
A293: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A278, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A279, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A292, A293; :: thesis:

end;

suppose A294: f = x ; :: thesis:

then A295: ex k1 being Element of NAT st
( k1 = abs ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = k1 |-> 0 ) by A48, A278, SCMFSA_2:75;
ex k2 being Element of NAT st
( k2 = abs ((Comput (P2,s2,i)) . da) & (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 ) by A13, A20, A279, A294, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A281, A292, A295; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:5;
A297: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A278, A296, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, A296, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A292, A297; :: thesis:

end;

reconsider ii = IC p as Element of NAT ;
B301: IC in dom (IncIC (p,k)) by MEMSTR_0:52;

now

thus (IC (Comput (P1,s1,0))) + k = (IC s1) + k by EXTPRO_1:2
.= (IC p) + k by A2, B1, GRFUNC_1:2
.= (IC p) + k
.= IC (IncIC (p,k)) by MEMSTR_0:53
.= IC s2 by A3, B301, GRFUNC_1:2
.= IC (Comput (P2,s2,0)) by EXTPRO_1:2 ; :: thesis:
reconsider loc = IC p as Element of NAT ;
A302: IC p = IC s1 by A2, B1, GRFUNC_1:2;
then IC p = IC (Comput (P1,s1,0)) by EXTPRO_1:2;
then A303: loc in dom q by A6, B2, AMISTD_5:def 4;
A304: (IC p) + k in dom (Reloc (q,k)) by A303, COMPOS_1:46;
B305: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A306: q . (IC p) = P1 . (IC s1) by A302, A303, A4, GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def 2;
then A307: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 6
.= P2 . (IC s2) by EXTPRO_1:2
.= P2 . (IC (IncIC (p,k))) by A3, B305, GRFUNC_1:2
.= P2 . ((IC p) + k) by MEMSTR_0:53
.= P2 . ((IC p) + k)
.= (Reloc (q,k)) . ((IC p) + k) by A304, A4, GRFUNC_1:2 ;
A308: dom P1 = NAT by PARTFUN1:def 2;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:2
.= P1 . (IC s1) by A308, PARTFUN1:def 6 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A307, A303, A306, COMPOS_1:35; :: thesis:
B127: DataPart p c= p by RELAT_1:59;
X1: DataPart p c= s1 by A2, B127, XBOOLE_1:1;
HH: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51;
DataPart p c= IncIC (p,k) by HH, MEMSTR_0:12;
then X2: DataPart p c= s2 by A3, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by EXTPRO_1:2
.= DataPart p by X1, GRFUNC_1:23
.= s2 | (dom (DataPart p)) by X2, GRFUNC_1:23
.= (Comput (P2,s2,0)) | (dom (DataPart p)) by EXTPRO_1:2 ; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2)) by EXTPRO_1:2
.= DataPart s2 by PBOOLE:142
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ; :: thesis:

end;

then A309: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A309, A11); :: thesis: