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

proof

set DPp = DataPart p;
let i be Element of NAT ; :: thesis:
assume that
A9: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A10: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
A11: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and
A12: DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; :: thesis:
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A13: dom (Comput (P1,s1,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
A14: dom (Comput (P1,s1,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set Cs2i1 = Comput (P2,s2,(i + 1));
A15: dom (Comput (P2,s2,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
A16: dom (Comput (P2,s2,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A17: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;

A18: now :: thesis:

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

end;

A19: now :: thesis:

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

end;

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

A23: now :: thesis:

reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A24: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis:
reconsider ii = loc as Element of NAT ;
A25: ii in dom q by A6, A1, AMISTD_5:def 4;
A26: loc + k in dom (Reloc (q,k)) by A25, COMPOS_1:46;
A27: dom P2 = NAT by PARTFUN1:def 2;
dom P1 = NAT by PARTFUN1:def 2;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 6
.= q . loc by A25, A4, GRFUNC_1:2
.= q . loc ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A25, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A24, A26, A5, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A27, PARTFUN1:def 6 ;
:: thesis:

end;

A28: now :: thesis:

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

end;

A29: now :: thesis:

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

end;

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

A35: now :: thesis:

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

end;

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

A39: now :: thesis:

let x be set ; :: thesis:
assume that
A40: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A41: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x and
A42: (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 A38, A22, A40, FUNCT_1:47;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A12, A21, A22, A35, A40, A41, A42, FUNCT_1:47; :: thesis:

end;

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

A45: now :: thesis:

let x, d be set ; :: thesis:
assume that
A46: d = x and
A47: d in dom (DataPart p) and
A48: (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 A33, A46, A47, A48, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A46, A47, FUNCT_1:47 ; :: thesis:

end;

A49: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A14, A31, XBOOLE_1:28 ;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A50: 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))) ;
A51: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A16, A31, XBOOLE_1:28 ;

A52: now :: thesis:

let x, d be set ; :: thesis:
assume that
A53: d = x and
A54: d in dom (DataPart p) and
A55: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d and
A56: (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ; :: thesis:
A57: ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d by A49, A54, FUNCT_1:47;
((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d by A51, A54, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A11, A33, A53, A54, A55, A56, A57, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A53, A54, FUNCT_1:47 ;
:: thesis:

end;

A58: 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 A32, NAT_1:36;

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

then A59: 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 A50, A59, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A9, A17, A59, A10, EXTPRO_1:def 3 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A23; :: thesis:
A60: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A17, A59, A10, EXTPRO_1:def 3;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A11, A50, A59, EXTPRO_1:def 3; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A12, A43, A59, A60, 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
A61: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMFSA_2:30;
A62: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A61, COMPOS_0:4;
A63: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A61, SCMFSA_2:63;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A62, SCMFSA_2:63; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A62, A63, SCMFSA_2:63; :: thesis:
A64: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

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

per cases by A33, A66, A65, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A67: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A61, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A66, A67; :: thesis:

end;

suppose A68: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A69: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db by A1, A7, A33, A61, A66, A68, A4, SCMFSA_3:5;
A70: (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db by A50, A61, A68, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db by A10, A17, A62, A68, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A64, A66, A70, A69; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A72: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A61, A71, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, A71, SCMFSA_2:63;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A66, A72; :: thesis:

end;

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

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

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

end;

suppose A75: da = x ; :: thesis:

A76: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . db by A43, A61, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A10, A17, A62, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A29, A35, A73, A75, A76; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A78: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A61, A77, SCMFSA_2:63;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, A77, SCMFSA_2:63;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A73, A78; :: thesis:

end;

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

end;

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

then consider da, db being Int-Location such that
A79: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMFSA_2:31;
A80: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A81: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A79, COMPOS_0:4;
A82: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A79, SCMFSA_2:64;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A81, SCMFSA_2:64; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A81, A82, SCMFSA_2:64; :: thesis:
A83: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

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

per cases by A33, A85, A84, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A86: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A79, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A85, A86; :: thesis:

end;

suppose A87: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A88: dom (DataPart p) c= dom p by GRFUNC_1:2;
A89: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A50, A79, A87, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A81, A87, SCMFSA_2:64;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A79, A83, A80, A85, A87, A89, A88, A4, SCMFSA_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A85; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A91: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A79, A90, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, A90, SCMFSA_2:64;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A85, A91; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A93: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A79, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A92, A93; :: thesis:

end;

suppose A94: da = x ; :: thesis:

then A95: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A79, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A81, A94, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A83, A80, A92, A95; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A97: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A79, A96, SCMFSA_2:64;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, A96, SCMFSA_2:64;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A92, A97; :: thesis:

end;

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

then consider da, db being Int-Location such that
A98: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMFSA_2:32;
A99: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A100: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A98, COMPOS_0:4;
A101: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A98, SCMFSA_2:65;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A100, SCMFSA_2:65; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A100, A101, SCMFSA_2:65; :: thesis:
A102: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

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

per cases by A33, A104, A103, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A105: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A98, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A104, A105; :: thesis:

end;

suppose A106: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A107: dom (DataPart p) c= dom p by GRFUNC_1:2;
A108: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A50, A98, A106, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A100, A106, SCMFSA_2:65;
then ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A98, A102, A99, A104, A106, A107, A4, SCMFSA_3:7;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A104, A108; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A110: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A98, A109, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, A109, SCMFSA_2:65;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A104, A110; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A112: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A98, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A111, A112; :: thesis:

end;

suppose A113: da = x ; :: thesis:

then A114: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A98, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A100, A113, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A102, A99, A111, A114; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A116: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A98, A115, SCMFSA_2:65;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, A115, SCMFSA_2:65;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A111, A116; :: thesis:

end;

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

then consider da, db being Int-Location such that
A117: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMFSA_2:33;
A118: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;
A119: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A117, COMPOS_0:4;
A120: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A117, SCMFSA_2:66;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A119, SCMFSA_2:66; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A119, A120, SCMFSA_2:66; :: thesis:
A121: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

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

per cases by A33, A123, A122, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A124: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A117, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A123, A124; :: thesis:

end;

suppose A125: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A126: dom (DataPart p) c= dom p by GRFUNC_1:2;
A127: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A50, A117, A125, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A119, A125, SCMFSA_2:66;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A117, A121, A118, A123, A125, A127, A126, A4, SCMFSA_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A123; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A129: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A117, A128, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, A128, SCMFSA_2:66;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A123, A129; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A131: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A117, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A130, A131; :: thesis:

end;

suppose A132: da = x ; :: thesis:

then A133: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A117, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A119, A132, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A121, A118, A130, A133; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A135: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A117, A134, SCMFSA_2:66;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, A134, SCMFSA_2:66;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A130, A135; :: thesis:

end;

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

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

per cases ;

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

A141: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A136, SCMFSA_2:67;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A138, SCMFSA_2:67; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A138, A141, SCMFSA_2:67; :: thesis:

now :: thesis:

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

per cases by A33, A143, A142, SCMFSA_2:100, XBOOLE_0:def 3;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A144: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A143, A144; :: thesis:

end;

suppose A145: da = x ; :: thesis:

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

end;

suppose A148: db = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then A149: dom (DataPart p) c= dom p by GRFUNC_1:2;
A150: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A50, A136, A148, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A148, SCMFSA_2:67;
then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A136, A139, A137, A143, A148, A150, A149, A4, SCMFSA_3:10;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A143; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A152: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A151, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A151, SCMFSA_2:67;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A143, A152; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A154: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A153, A154; :: thesis:

end;

suppose A155: da = x ; :: thesis:

then A156: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, A140, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A10, A17, A138, A140, A155, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A153, A156; :: thesis:

end;

suppose A157: db = x ; :: thesis:

then A158: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A157, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A153, A158; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A160: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A159, SCMFSA_2:67;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A159, SCMFSA_2:67;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A153, A160; :: thesis:

end;

suppose A161: da = db ; :: thesis:

then A162: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A136, SCMFSA_2:68;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A138, A161, SCMFSA_2:68; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A138, A161, A162, SCMFSA_2:68; :: thesis:

now :: thesis:

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

per cases by A33, A164, A163, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A165: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A161, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A164, A165; :: thesis:

end;

suppose A166: da = x ; :: thesis:

A167: ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A33, A44, A164, FUNCT_1:47;
A168: ((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x by A33, A49, A164, FUNCT_1:47;
A169: ((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x by A33, A51, A164, FUNCT_1:47;
A170: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x by A164, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A161, A166, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A11, A50, A136, A161, A166, A168, A169, A170, A167, SCMFSA_2:68; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A172: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A161, A171, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, A171, SCMFSA_2:68;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A164, A172; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A174: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A161, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A173, A174; :: thesis:

end;

suppose A175: da = x ; :: thesis:

then A176: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, A161, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A161, A175, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A173, A176; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A178: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A161, A177, SCMFSA_2:68;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, A177, SCMFSA_2:68;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A173, A178; :: thesis:

end;

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

then consider loc being Element of NAT such that
A179: CurInstr (P1,(Comput (P1,s1,i))) = goto loc by SCMFSA_2:35;
A180: CurInstr (P2,(Comput (P2,s2,i))) = goto (loc + k) by A10, A179, SCMFSA_4:1;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A179, SCMFSA_2:69
.= IC (Comput (P2,s2,(i + 1))) by A17, A180, SCMFSA_2:69 ; :: thesis:
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A23; :: thesis:

now :: thesis:

let x be set ; :: thesis:
assume A181: 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 A33, A181, SCMFSA_2:100, XBOOLE_0:def 3;
then A182: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A183: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A180, SCMFSA_2:69;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A179, A182, SCMFSA_2:69;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A181, A183; :: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A184: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A185: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A186: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A180, SCMFSA_2:69;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A179, A185, SCMFSA_2:69;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A184, A186; :: 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
A187: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by SCMFSA_2:36;

A188: now :: thesis:

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

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A187, 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 A9, A50, A58, A187, SCMFSA_2:70; :: thesis:

end;

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

A190: now :: thesis:

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

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

hence IC (Comput (P2,s2,(i + 1))) = loc + k by A17, A189, 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 A17, A189, SCMFSA_2:70; :: thesis:

end;

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

A192: now :: thesis:

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 A1, A7, A187, A191, A188, A190, 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 A9, A58, A188, A190; :: thesis:

end;

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

now :: thesis:

let x be set ; :: thesis:
assume A193: 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 A33, A193, SCMFSA_2:100, XBOOLE_0:def 3;
then A194: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A195: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A189, SCMFSA_2:70;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A187, A194, SCMFSA_2:70;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A193, A195; :: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A196: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A197: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A198: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A189, SCMFSA_2:70;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A187, A197, SCMFSA_2:70;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A196, A198; :: 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
A199: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by SCMFSA_2:37;

A200: now :: thesis:

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

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

hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A199, 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 A9, A50, A58, A199, SCMFSA_2:71; :: thesis:

end;

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

A202: now :: thesis:

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

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

hence IC (Comput (P2,s2,(i + 1))) = loc + k by A17, A201, 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 A17, A201, SCMFSA_2:71; :: thesis:

end;

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

A204: now :: thesis:

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 A1, A7, A199, A203, A200, A202, 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 A9, A58, A200, A202; :: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A205: 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 A33, A205, SCMFSA_2:100, XBOOLE_0:def 3;
then A206: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A207: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A201, SCMFSA_2:71;
(Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A199, A206, SCMFSA_2:71;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A205, A207; :: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A208: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def 3;
then A209: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def 16, SCMFSA_2:def 5;
then A210: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A201, SCMFSA_2:71;
(Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A199, A209, SCMFSA_2:71;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A208, A210; :: 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
A211: CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) by SCMFSA_2:38;
A212: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;
A213: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := (f,db) by A211, COMPOS_0:4;
A214: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A211, SCMFSA_2:72;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A213, SCMFSA_2:72; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A213, A214, SCMFSA_2:72; :: thesis:
A215: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

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

per cases by A33, A217, A216, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A218: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A211, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A217, A218; :: thesis:

end;

suppose A219: da = x ; :: thesis:

then consider k1 being Element of NAT such that
A220: k1 = abs ((Comput (P1,s1,i)) . db) and
A221: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) /. k1 by A50, A211, SCMFSA_2:72;
consider k2 being Element of NAT such that
A222: k2 = abs ((Comput (P2,s2,i)) . db) and
A223: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 by A10, A17, A213, A219, SCMFSA_2:72;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k2 = ((Comput (P1,s1,i)) . f) /. k1 by A1, A7, A33, A211, A215, A217, A219, A220, A222, A4, SCMFSA_3:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A212, A217, A221, A223; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A225: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A211, A224, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, A224, SCMFSA_2:72;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A217, A225; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A227: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A211, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A213, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A226, A227; :: thesis:

end;

suppose A228: da = x ; :: thesis:

then A229: 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 A43, A211, 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 A10, A17, A213, A228, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A215, A212, A226, A229; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A231: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A211, A230, SCMFSA_2:72;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, A230, SCMFSA_2:72;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A226, A231; :: 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
A232: CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da by SCMFSA_2:39;
A233: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;
A234: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = (f,db) := da by A232, COMPOS_0:4;
A235: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A232, SCMFSA_2:73;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A234, SCMFSA_2:73; :: thesis:
A236: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A234, A235, SCMFSA_2:73; :: thesis:
A237: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29;

now :: thesis:

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

per cases by A33, A239, A238, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A240: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A232, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A239, A240; :: thesis:

end;

suppose A241: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A242: k1 = abs ((Comput (P1,s1,i)) . db) and
A243: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A50, A232, SCMFSA_2:73;
consider k2 being Element of NAT such that
A244: k2 = abs ((Comput (P2,s2,i)) . db) and
A245: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) by A10, A17, A234, A241, SCMFSA_2:73;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (k2,((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A1, A7, A33, A232, A237, A239, A241, A242, A244, A4, SCMFSA_3:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A236, A233, A239, A243, A245; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A247: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A232, A246, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, A246, SCMFSA_2:73;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A239, A247; :: thesis:

end;

now :: thesis:

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

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

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by AMI_2:def 16;
A249: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A232, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A234, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A248, A249; :: thesis:

end;

suppose A250: f = x ; :: thesis:

then A251: 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 A43, A232, 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 A10, A17, A234, A250, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A237, A236, A233, A248, A251; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A253: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A232, A252, SCMFSA_2:73;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, A252, SCMFSA_2:73;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A248, A253; :: thesis:

end;

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

then consider da being Int-Location, f being FinSeq-Location such that
A254: CurInstr (P1,(Comput (P1,s1,i))) = da :=len f by SCMFSA_2:40;
A255: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :=len f by A254, COMPOS_0:4;
A256: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A254, SCMFSA_2:74;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A255, SCMFSA_2:74; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A255, A256, SCMFSA_2:74; :: thesis:
A257: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19;

now :: thesis:

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

per cases by A33, A259, A258, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A260: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A254, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A259, A260; :: thesis:

end;

suppose A261: da = x ; :: thesis:

DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then A262: len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f) by A1, A7, A33, A254, A259, A261, A4, SCMFSA_3:15;
A263: (Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f) by A50, A254, A261, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A255, A261, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A257, A259, A263, A262; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A265: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A254, A264, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, A264, SCMFSA_2:74;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A259, A265; :: thesis:

end;

now :: thesis:

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

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

suppose x in FinSeq-Locations ; :: thesis:

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

end;

suppose A268: da = x ; :: thesis:

then A269: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) by A43, A254, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A255, A268, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A257, A266, A269; :: thesis:

end;

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

then reconsider d = x as Int-Location by AMI_2:def 16;
A271: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A254, A270, SCMFSA_2:74;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, A270, SCMFSA_2:74;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A266, A271; :: thesis:

end;

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

then consider da being Int-Location, f being FinSeq-Location such that
A272: CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da by SCMFSA_2:41;
A273: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = f :=<0,...,0> da by A272, COMPOS_0:4;
A274: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A272, SCMFSA_2:75;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A273, SCMFSA_2:75; :: thesis:
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A273, A274, SCMFSA_2:75; :: thesis:
A275: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29;

now :: thesis:

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

per cases by A33, A277, A276, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by AMI_2:def 16;
A278: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A272, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A277, A278; :: thesis:

end;

suppose A279: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A280: k1 = abs ((Comput (P1,s1,i)) . da) and
A281: (Comput (P1,s1,(i + 1))) . x = k1 |-> 0 by A50, A272, SCMFSA_2:75;
consider k2 being Element of NAT such that
A282: k2 = abs ((Comput (P2,s2,i)) . da) and
A283: (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 by A10, A17, A273, A279, SCMFSA_2:75;
DataPart p c= p by RELAT_1:59;
then dom (DataPart p) c= dom p by GRFUNC_1:2;
then k2 |-> 0 = k1 |-> 0 by A1, A7, A33, A272, A275, A277, A279, A280, A282, A4, SCMFSA_3:16;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A277, A281, A283; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A285: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A272, A284, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, A284, SCMFSA_2:75;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A277, A285; :: thesis:

end;

now :: thesis:

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

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

suppose x in Int-Locations ; :: thesis:

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

end;

suppose A288: f = x ; :: thesis:

then A289: 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 A43, A272, 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 A10, A17, A273, A288, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A275, A286, A289; :: thesis:

end;

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

then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A291: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A272, A290, SCMFSA_2:75;
(Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, A290, SCMFSA_2:75;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A286, A291; :: thesis:

end;

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

now :: thesis:

thus (IC (Comput (P1,s1,0))) + k = (IC s1) + k
.= (IC p) + k by A1, A3, GRFUNC_1:2
.= (IC p) + k
.= IC (IncIC (p,k)) by MEMSTR_0:53
.= IC s2 by A2, A292, GRFUNC_1:2
.= IC (Comput (P2,s2,0)) ; :: thesis:
reconsider loc = IC p as Element of NAT ;
A293: IC p = IC s1 by A1, A3, GRFUNC_1:2;
then IC p = IC (Comput (P1,s1,0)) ;
then A294: loc in dom q by A6, A1, AMISTD_5:def 4;
A295: (IC p) + k in dom (Reloc (q,k)) by A294, COMPOS_1:46;
A296: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A297: q . (IC p) = P1 . (IC s1) by A293, A294, A4, GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def 2;
then A298: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 6
.= P2 . (IC s2)
.= P2 . (IC (IncIC (p,k))) by A2, A296, GRFUNC_1:2
.= P2 . ((IC p) + k) by MEMSTR_0:53
.= P2 . ((IC p) + k)
.= (Reloc (q,k)) . ((IC p) + k) by A295, A4, GRFUNC_1:2 ;
A299: dom P1 = NAT by PARTFUN1:def 2;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1)
.= P1 . (IC s1) by A299, PARTFUN1:def 6 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A298, A294, A297, COMPOS_1:35; :: thesis:
A300: DataPart p c= p by RELAT_1:59;
A301: DataPart p c= s1 by A1, A300, XBOOLE_1:1;
A302: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51;
DataPart p c= IncIC (p,k) by A302, MEMSTR_0:12;
then A303: DataPart p c= s2 by A2, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p))
.= DataPart p by A301, GRFUNC_1:23
.= s2 | (dom (DataPart p)) by A303, GRFUNC_1:23
.= (Comput (P2,s2,0)) | (dom (DataPart p)) ; :: thesis:
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2))
.= DataPart s2 by PBOOLE:142
.= DataPart (Comput (P2,s2,0)) ; :: thesis:

end;

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