let k be Element of NAT ; :: thesis:
let p be autonomic FinPartState of SCM+FSA; :: thesis:
let s1, s2 be State of SCM+FSA; :: thesis:
assume that
A1: IC in dom p and
A2: NPP p c= s1 and
A3: NPP (Relocated (p,k)) c= s2 ; :: thesis:
B1: IC in dom (NPP p) by A1, COMPOS_1:179;
B2: NPP p c= s1 by A2;
let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
assume A4: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 ) ; :: thesis:
A5: Reloc ((ProgramPart p),k) c= P2 by A4;
A6: ProgramPart p 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)) );
A9: not p is NAT -defined by A1, COMPOS_1:19;
A10: NPP p c= s1 +* (DataPart s2) by A2, A3, COMPOS_1:203;
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 SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
A17: dom (Comput (P1,s1,i)) = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
set Cs2i1 = Comput (P2,s2,(i + 1));
A18: dom (Comput (P2,s2,(i + 1))) = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
A19: dom (Comput (P2,s2,i)) = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A20: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:4
.= 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:10;
then d in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence d in dom (DataPart s) by COMPOS_1:50; :: 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:70
.= (Comput (P2,s2,i)) . d by A15, A23, FUNCT_1:70 ;
:: thesis:

end;

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

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 (ProgramPart p) by A9, AMISTD_5:def 4, A6, B2;
A29: loc + k in dom (Reloc ((ProgramPart p),k)) by A28, COMPOS_1:158;
A30: dom P2 = NAT by PARTFUN1:def 4;
dom P1 = NAT by PARTFUN1:def 4;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 8
.= (ProgramPart p) . loc by A28, GRFUNC_1:8, A4
.= (ProgramPart p) . loc ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc ((ProgramPart p),k)) . (loc + k) by A28, COMPOS_1:122
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A27, A29, A5, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A30, PARTFUN1:def 8 ;
:: 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:9;
then d in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence d in dom (DataPart s) by COMPOS_1:50; :: 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:70
.= (Comput (P2,s2,i)) . d by A15, A33, FUNCT_1:70 ;
:: thesis:

end;

dom (DataPart p) = (dom p) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A34: dom (DataPart p) c= {(IC )} \/ (Data-Locations SCM+FSA) by XBOOLE_1:10, XBOOLE_1:17;
A37: InsCode (CurInstr (P1,(Comput (P1,s1,i)))) <= 13 by SCMFSA_2:35;
A38: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A16, A34, XBOOLE_1:10, XBOOLE_1:28 ;
A39: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations SCM+FSA by COMPOS_1:50;

A40: now

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

end;

A43: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations SCM+FSA by COMPOS_1:50;

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

end;

A48: Comput (P1,(s1 +* (DataPart s2)),(i + 1)) = Following (P1,(Comput (P1,(s1 +* (DataPart s2)),i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,(s1 +* (DataPart s2)),i))) by A2, A9, A10, AMISTD_5:7, A4 ;
A49: dom (DataPart p) = dom (DataPart (Relocated (p,k))) by COMPOS_1:115;
then A50: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A18, A34, XBOOLE_1:10, 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:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A49, A50, A52, A53, FUNCT_1:70 ; :: thesis:

end;

A55: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A17, A34, XBOOLE_1:10, 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:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A57: dom ((Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by A49, RELAT_1:90
.= dom (DataPart p) by A19, A34, XBOOLE_1:10, 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:70;
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d by A49, A57, A60, FUNCT_1:70;
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:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A49, A50, A59, A60, FUNCT_1:70 ;
:: thesis:

end;

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

per cases by A37, NAT_1:38;

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

then A65: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM+FSA by SCMFSA_2:122;
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:54;
A68: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A67, COMPOS_1:92;
A69: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A67, SCMFSA_2:89;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A68, SCMFSA_2:89; :: 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:89; :: 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 SCM+FSA by RELAT_1:87;
assume A72: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A73: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A67, SCMFSA_2:89;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, SCMFSA_2:89;
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:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then A75: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db by A2, A9, A10, A38, A67, A72, A74, SCMFSA_3:19, A4;
A76: (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db by A56, A67, A74, SCMFSA_2:89;
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db by A13, A20, A68, A74, SCMFSA_2:89;
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:11;
A78: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A67, A77, SCMFSA_2:89;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, A77, SCMFSA_2:89;
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 A49, A38, A50, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A49, A38, A50, GRFUNC_1:9; :: 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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A80: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A67, SCMFSA_2:89;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A68, SCMFSA_2:89;
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:89;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A13, A20, A68, SCMFSA_2:89;
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:11;
A84: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A67, A83, SCMFSA_2:89;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A68, A83, SCMFSA_2:89;
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:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A25, A39, GRFUNC_1:9; :: 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:55;
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:92;
A88: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A85, SCMFSA_2:90;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A87, SCMFSA_2:90; :: 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:90; :: thesis:
A89: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

A90: dom (DataPart p) c= Data-Locations SCM+FSA by RELAT_1:87;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A92: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A85, SCMFSA_2:90;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, SCMFSA_2:90;
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:88;
then A94: dom (DataPart p) c= dom p by GRFUNC_1:8;
A95: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A56, A85, A93, SCMFSA_2:90;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A13, A20, A87, A93, SCMFSA_2:90;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A9, A10, A38, A85, A89, A86, A91, A93, A95, A94, SCMFSA_3:20, A4;
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:11;
A97: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A85, A96, SCMFSA_2:90;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, A96, SCMFSA_2:90;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A99: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A85, SCMFSA_2:90;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, SCMFSA_2:90;
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:90;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A13, A20, A87, A100, SCMFSA_2:90;
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:11;
A103: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A85, A102, SCMFSA_2:90;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A87, A102, SCMFSA_2:90;
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:56;
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:92;
A107: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A104, SCMFSA_2:91;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A106, SCMFSA_2:91; :: 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:91; :: thesis:
A108: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

A109: dom (DataPart p) c= Data-Locations SCM+FSA by RELAT_1:87;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A111: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A104, SCMFSA_2:91;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, SCMFSA_2:91;
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:88;
then A113: dom (DataPart p) c= dom p by GRFUNC_1:8;
A114: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A56, A104, A112, SCMFSA_2:91;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A13, A20, A106, A112, SCMFSA_2:91;
then ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x by A2, A9, A10, A38, A104, A108, A105, A110, A112, A113, SCMFSA_3:21, A4;
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:11;
A116: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A104, A115, SCMFSA_2:91;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, A115, SCMFSA_2:91;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A118: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A104, SCMFSA_2:91;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, SCMFSA_2:91;
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:91;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A13, A20, A106, A119, SCMFSA_2:91;
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:11;
A122: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A104, A121, SCMFSA_2:91;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A106, A121, SCMFSA_2:91;
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:57;
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:92;
A126: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A123, SCMFSA_2:92;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A125, SCMFSA_2:92; :: 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:92; :: thesis:
A127: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A32;

now

A128: dom (DataPart p) c= Data-Locations SCM+FSA by RELAT_1:87;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A130: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A123, SCMFSA_2:92;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, SCMFSA_2:92;
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:88;
then A132: dom (DataPart p) c= dom p by GRFUNC_1:8;
A133: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A56, A123, A131, SCMFSA_2:92;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A13, A20, A125, A131, SCMFSA_2:92;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A9, A10, A38, A123, A127, A124, A129, A131, A133, A132, SCMFSA_3:22, A4;
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:11;
A135: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A123, A134, SCMFSA_2:92;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, A134, SCMFSA_2:92;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A137: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A123, SCMFSA_2:92;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, SCMFSA_2:92;
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:92;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A13, A20, A125, A138, SCMFSA_2:92;
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:11;
A141: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A123, A140, SCMFSA_2:92;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A125, A140, SCMFSA_2:92;
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:58;
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:92;
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:93;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A144, SCMFSA_2:93; :: 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:93; :: thesis:

now

A148: dom (DataPart p) c= Data-Locations SCM+FSA by RELAT_1:87;
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, XBOOLE_0:def 3, SCMFSA_2:127;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A150: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, SCMFSA_2:93;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, SCMFSA_2:93;
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:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
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, A9, A10, A38, A142, A146, A149, A151, SCMFSA_3:23, A4;
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:93;
(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:93;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A145, A143, A149, A153, A152, FUNCT_1:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A49, A38, A50, A149, FUNCT_1:70 ;
:: thesis:

end;

suppose A154: db = x ; :: thesis:

DataPart p c= p by RELAT_1:88;
then A155: dom (DataPart p) c= dom p by GRFUNC_1:8;
A156: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A56, A142, A154, SCMFSA_2:93;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A154, SCMFSA_2:93;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A2, A9, A10, A38, A142, A145, A143, A149, A154, A156, A155, SCMFSA_3:24, A4;
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:11;
A158: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A157, SCMFSA_2:93;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A157, SCMFSA_2:93;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A160: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, SCMFSA_2:93;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, SCMFSA_2:93;
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:93;
(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:93;
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:93;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A13, A20, A144, A163, SCMFSA_2:93;
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:11;
A166: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A165, SCMFSA_2:93;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A165, SCMFSA_2:93;
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:94;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A144, A167, SCMFSA_2:94; :: 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:94; :: thesis:

now

A169: dom (DataPart p) c= Data-Locations SCM+FSA by RELAT_1:87;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A171: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A167, SCMFSA_2:94;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, SCMFSA_2:94;
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 A49, A38, A50, A170, FUNCT_1:70;
A174: ((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x by A38, A55, A170, FUNCT_1:70;
A175: ((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x by A49, A38, A57, A170, FUNCT_1:70;
A176: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x by A170, FUNCT_1:70;
(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:94;
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:94; :: thesis:

end;

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

then reconsider d = x as Int-Location by SCMFSA_2:11;
A178: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A142, A167, A177, SCMFSA_2:94;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, A177, SCMFSA_2:94;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A180: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A167, SCMFSA_2:94;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, SCMFSA_2:94;
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:94;
(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:94;
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:11;
A184: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A142, A167, A183, SCMFSA_2:94;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A144, A167, A183, SCMFSA_2:94;
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:59;
A186: CurInstr (P2,(Comput (P2,s2,i))) = goto (loc + k) by A13, A185, SCMFSA_4:14;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A56, A185, SCMFSA_2:95
.= IC (Comput (P2,s2,(i + 1))) by A20, A186, SCMFSA_2:95 ; :: 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 SCM+FSA by RELAT_1:87;
then ( x in Int-Locations or x in FinSeq-Locations ) by A38, A187, XBOOLE_0:def 3, SCMFSA_2:127;
then A188: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A189: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A186, SCMFSA_2:95;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A185, A188, SCMFSA_2:95;
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, XBOOLE_0:def 3, SCMFSA_2:127;
then A191: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A192: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A186, SCMFSA_2:95;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A185, A191, SCMFSA_2:95;
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:60;

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

end;

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

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:96; :: 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:96; :: 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, A9, A10, A193, A197, A194, A196, SCMFSA_3:25, A4; :: 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 SCM+FSA by RELAT_1:87;
then ( x in Int-Locations or x in FinSeq-Locations ) by A38, A199, XBOOLE_0:def 3, SCMFSA_2:127;
then A200: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A201: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A195, SCMFSA_2:96;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A193, A200, SCMFSA_2:96;
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, XBOOLE_0:def 3, SCMFSA_2:127;
then A203: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A204: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A195, SCMFSA_2:96;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A193, A203, SCMFSA_2:96;
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:61;

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

end;

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

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:97; :: 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:97; :: 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, A9, A10, A205, A209, A206, A208, SCMFSA_3:26, A4; :: 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 SCM+FSA by RELAT_1:87;
then ( x in Int-Locations or x in FinSeq-Locations ) by A38, A211, XBOOLE_0:def 3, SCMFSA_2:127;
then A212: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A213: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A207, SCMFSA_2:97;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A56, A205, A212, SCMFSA_2:97;
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, XBOOLE_0:def 3, SCMFSA_2:127;
then A215: ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then A216: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A20, A207, SCMFSA_2:97;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A48, A205, A215, SCMFSA_2:97;
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:62;
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:92;
A220: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A217, SCMFSA_2:98;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A219, SCMFSA_2:98; :: 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:98; :: 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 SCM+FSA by RELAT_1:87;
assume A223: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A224: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A217, SCMFSA_2:98;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, SCMFSA_2:98;
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:98;
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:98;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k2 = ((Comput (P1,s1,i)) . f) /. k1 by A2, A9, A10, A38, A217, A221, A223, A225, A226, A228, SCMFSA_3:27, A4;
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:11;
A231: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A217, A230, SCMFSA_2:98;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, A230, SCMFSA_2:98;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A233: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A217, SCMFSA_2:98;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A219, SCMFSA_2:98;
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:98;
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:98;
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:11;
A237: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A217, A236, SCMFSA_2:98;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A219, A236, SCMFSA_2:98;
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:63;
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:92;
A241: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A238, SCMFSA_2:99;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A240, SCMFSA_2:99; :: 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:99; :: 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 SCM+FSA by RELAT_1:87;
assume A245: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A246: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A238, SCMFSA_2:99;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, SCMFSA_2:99;
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:99;
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:99;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
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, A9, A10, A38, A238, A243, A245, A247, A248, A250, SCMFSA_3:28, A4;
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:12;
A253: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A238, A252, SCMFSA_2:99;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, A252, SCMFSA_2:99;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:11;
A255: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A238, SCMFSA_2:99;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A240, SCMFSA_2:99;
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:99;
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:99;
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:12;
A259: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A238, A258, SCMFSA_2:99;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A240, A258, SCMFSA_2:99;
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:64;
A261: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :=len f by A260, COMPOS_1:92;
A262: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A260, SCMFSA_2:100;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A261, SCMFSA_2:100; :: 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:100; :: 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 SCM+FSA by RELAT_1:87;
assume A265: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A266: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A260, SCMFSA_2:100;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, SCMFSA_2:100;
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:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then A268: len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f) by A2, A9, A10, A38, A260, A265, A267, SCMFSA_3:29, A4;
A269: (Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f) by A56, A260, A267, SCMFSA_2:100;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A13, A20, A261, A267, SCMFSA_2:100;
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:11;
A271: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A260, A270, SCMFSA_2:100;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, A270, SCMFSA_2:100;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A273: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A260, SCMFSA_2:100;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A261, SCMFSA_2:100;
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:100;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A13, A20, A261, A274, SCMFSA_2:100;
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:11;
A277: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A260, A276, SCMFSA_2:100;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A261, A276, SCMFSA_2:100;
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:65;
A279: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = f :=<0,...,0> da by A278, COMPOS_1:92;
A280: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A278, SCMFSA_2:101;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A279, SCMFSA_2:101; :: 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:101; :: 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 SCM+FSA by RELAT_1:87;
assume A283: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis:

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

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A284: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, SCMFSA_2:101;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, SCMFSA_2:101;
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:101;
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:101;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then k2 |-> 0 = k1 |-> 0 by A2, A9, A10, A38, A278, A281, A283, A285, A286, A288, SCMFSA_3:30, A4;
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:12;
A291: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, A290, SCMFSA_2:101;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, A290, SCMFSA_2:101;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:11;
A293: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A48, A278, SCMFSA_2:101;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A13, A20, A279, SCMFSA_2:101;
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:101;
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:101;
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:12;
A297: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A48, A278, A296, SCMFSA_2:101;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, A296, SCMFSA_2:101;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A44, A292, A297; :: thesis:

end;

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

then consider da being Int-Location such that
A278: CurInstr (P1,(Comput (P1,s1,i))) = da :==1 by SCMFSA_2:134;
A279: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :==1 by A278, COMPOS_1:92;
A280: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A278, SCMFSA_2:136;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A12, A13, A56, A20, A64, A279, SCMFSA_2:136; :: 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:136; :: thesis:

now

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A284: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, SCMFSA_2:136;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, SCMFSA_2:136;
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: da = x ; :: thesis:

then A287: (Comput (P1,s1,(i + 1))) . x = 1 by A56, A278, SCMFSA_2:136;
A289: (Comput (P2,s2,(i + 1))) . x = 1 by A13, A20, A279, A285, SCMFSA_2:136;
thus ((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: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A291: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A56, A278, A290, SCMFSA_2:136;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A13, A20, A279, A290, SCMFSA_2:136;
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, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider da = x as FinSeq-Location by SCMFSA_2:12;
A293: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . da by A48, A278, SCMFSA_2:136;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . da by A13, A20, A279, SCMFSA_2:136;
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: da = x ; :: thesis:

then A295: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = 1 by A48, A278, SCMFSA_2:136;
(Comput (P2,s2,(i + 1))) . x = 1 by A13, A20, A279, A294, SCMFSA_2:136;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A40, A292, A295; :: thesis:

end;

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

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

end;

A298: DataPart p = DataPart (Relocated (p,k)) by COMPOS_1:115;
reconsider ii = IC p as Element of NAT ;
A301: IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B301: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;

now

thus (IC (Comput (P1,s1,0))) + k = (IC s1) + k by EXTPRO_1:3
.= (IC (NPP p)) + k by A2, GRFUNC_1:8, B1
.= (IC p) + k by A1, COMPOS_1:72
.= IC (Relocated (p,k)) by A1, COMPOS_1:120
.= IC (NPP (Relocated (p,k))) by A301, COMPOS_1:72
.= IC s2 by A3, B301, GRFUNC_1:8
.= IC (Comput (P2,s2,0)) by EXTPRO_1:3 ; :: thesis:
reconsider loc = IC (NPP p) as Element of NAT ;
A302: IC (NPP p) = IC s1 by A2, GRFUNC_1:8, B1;
then IC (NPP p) = IC (Comput (P1,s1,0)) by EXTPRO_1:3;
then A303: loc in dom (ProgramPart p) by A9, AMISTD_5:def 4, A6, B2;
A304: (IC (NPP p)) + k in dom (Reloc ((ProgramPart p),k)) by A303, COMPOS_1:158;
IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B305: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;
A306: (ProgramPart p) . (IC (NPP p)) = P1 . (IC s1) by A302, A303, GRFUNC_1:8, A4;
dom P2 = NAT by PARTFUN1:def 4;
then A307: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 8
.= P2 . (IC s2) by EXTPRO_1:3
.= P2 . (IC (NPP (Relocated (p,k)))) by A3, GRFUNC_1:8, B305
.= P2 . (IC (Relocated (p,k))) by GRFUNC_1:8, B305
.= P2 . ((IC p) + k) by A1, COMPOS_1:120
.= P2 . ((IC (NPP p)) + k) by A1, COMPOS_1:72
.= (Reloc ((ProgramPart p),k)) . ((IC (NPP p)) + k) by A304, GRFUNC_1:8, A4 ;
A308: dom P1 = NAT by PARTFUN1:def 4;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:3
.= P1 . (IC s1) by A308, PARTFUN1:def 8 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A307, A303, A306, COMPOS_1:122; :: thesis:
B127: DataPart (NPP p) c= NPP p by RELAT_1:88;
DataPart p = DataPart (NPP p) by COMPOS_1:73;
then X1: DataPart p c= s1 by A2, B127, XBOOLE_1:1;
DataPart (Relocated (p,k)) c= NPP (Relocated (p,k)) by COMPOS_1:169;
then X2: DataPart p c= s2 by A3, A298, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by EXTPRO_1:3
.= DataPart p by GRFUNC_1:64, X1
.= s2 | (dom (DataPart p)) by GRFUNC_1:64, X2
.= (Comput (P2,s2,0)) | (dom (DataPart p)) by EXTPRO_1:3 ; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2)) by EXTPRO_1:3
.= DataPart s2 by PBOOLE:157
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:3 ; :: thesis:

end;

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