let k be Element of NAT ; :: thesis:
let p be autonomic FinPartState of SCM ; :: thesis:
let s1, s2 be State of SCM ; :: thesis:
assume that
A1: IC SCM in dom p and
A2: p c= s1 and
A3: Relocated p,k c= s2 ; :: thesis:
set s3 = s1 +* (DataPart s2);
A5: IC SCM in dom (Relocated p,k) by Th25;
A6: DataPart p = DataPart (Relocated p,k) by Th21;
A7: DataPart p c= p by RELAT_1:88;
A8: DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
A9: not p is programmed by A1, AMI_1:109;
A10: p c= s1 +* (DataPart s2) by A2, A3, Th30;
defpred S₁[ Element of NAT ] means ( (IC (Computation s1,$1)) + k = IC (Computation s2,$1) & IncAddr (CurInstr (Computation s1,$1)),k = CurInstr (Computation s2,$1) & (Computation s1,$1) | (dom (DataPart p)) = (Computation s2,$1) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),$1) = DataPart (Computation s2,$1) );

now

thus (IC (Computation s1,0 )) + k = (IC s1) + k by AMI_1:13
.= (IC p) + k by A1, A2, AMI_1:97
.= IC (Relocated p,k) by Th26
.= IC s2 by A3, A5, AMI_1:97
.= IC (Computation s2,0 ) by AMI_1:13 ; :: thesis:
reconsider loc = IC p as Element of NAT ;
A11: IC p = IC s1 by A1, A2, AMI_1:97;
then IC p = IC (Computation s1,0 ) by AMI_1:13;
then A12: loc in dom (ProgramPart p) by A2, A9, AMI_5:86;
ProgramPart p c= p by RELAT_1:88;
then A13: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then A14: p . (IC p) = s1 . (IC s1) by A2, A11, A12, GRFUNC_1:8;
A15: IncAddr (CurInstr (Computation s1,0 )),k = IncAddr (CurInstr s1),k by AMI_1:13
.= IncAddr (s1 . (IC s1)),k ;
A16: IC SCM in dom (Relocated p,k) by Th25;
A17: (IC p) + k in dom (Relocated p,k) by A12, A13, Th24;
CurInstr (Computation s2,0 ) = CurInstr s2 by AMI_1:13
.= s2 . (IC (Relocated p,k)) by A3, A16, AMI_1:97
.= s2 . ((IC p) + k) by Th26
.= (Relocated p,k) . ((IC p) + k) by A3, A17, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,0 )),k = CurInstr (Computation s2,0 ) by A12, A14, A15, Th27; :: thesis:
thus (Computation s1,0 ) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by AMI_1:13
.= DataPart p by A2, A7, GRFUNC_1:64, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A3, A6, A8, GRFUNC_1:64, XBOOLE_1:1
.= (Computation s2,0 ) | (dom (DataPart (Relocated p,k))) by A6, AMI_1:13 ; :: thesis:
A18: dom (DataPart s2) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
thus DataPart (Computation (s1 +* (DataPart s2)),0 ) = DataPart (s1 +* (DataPart s2)) by AMI_1:13
.= DataPart s2 by A18, AMI_3:72, FUNCT_4:24
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

then A19: S₁[ 0 ] ;

now

let i be Element of NAT ; :: thesis:
assume that
A20: (IC (Computation s1,i)) + k = IC (Computation s2,i) and
A21: IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) and
A22: (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) and
A23: DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) ; :: thesis:
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
set Cs3i = Computation (s1 +* (DataPart s2)),i;
set Cs1i1 = Computation s1,(i + 1);
set Cs2i1 = Computation s2,(i + 1);
set Cs3i1 = Computation (s1 +* (DataPart s2)),(i + 1);
set DPp = DataPart p;
A24: dom (DataPart p) = dom (DataPart (Relocated p,k)) by Th21;
A25: dom (Computation s1,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
A26: dom (Computation s2,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
A27: dom (Computation s1,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
A28: dom (Computation s2,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
dom (DataPart p) = (dom p) /\ SCM-Data-Loc by AMI_3:72, FUNCT_1:68;
then A29: dom (DataPart p) c= {(IC SCM )} \/ SCM-Data-Loc by XBOOLE_1:10, XBOOLE_1:17;
A30: dom ((Computation s1,(i + 1)) | (dom (DataPart p))) = (dom (Computation s1,(i + 1))) /\ (dom (DataPart p)) by FUNCT_1:68
.= dom (DataPart p) by A25, A29, XBOOLE_1:10, XBOOLE_1:28 ;
A31: dom ((Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,(i + 1))) /\ (dom (DataPart p)) by A24, FUNCT_1:68
.= dom (DataPart p) by A26, A29, XBOOLE_1:10, XBOOLE_1:28 ;
A32: dom ((Computation s1,i) | (dom (DataPart p))) = (dom (Computation s1,i)) /\ (dom (DataPart p)) by FUNCT_1:68
.= dom (DataPart p) by A27, A29, XBOOLE_1:10, XBOOLE_1:28 ;
A33: dom ((Computation s2,i) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,i)) /\ (dom (DataPart p)) by A24, FUNCT_1:68
.= dom (DataPart p) by A28, A29, XBOOLE_1:10, XBOOLE_1:28 ;
A34: dom (DataPart (Computation (s1 +* (DataPart s2)),i)) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
A35: dom (DataPart (Computation s2,i)) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
A36: dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
A37: dom (DataPart (Computation s2,(i + 1))) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;

A38: now

let s be State of SCM ; :: thesis:
let d be Data-Location ; :: thesis:
d in SCM-Data-Loc by AMI_3:def 2;
hence d in dom (DataPart s) by AMI_3:72, SCMNORM:14; :: thesis:

end;

A39: now

let d be Data-Location ; :: thesis:
A40: ( d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) & d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) ) by A38;
hence (Computation (s1 +* (DataPart s2)),i) . d = (DataPart (Computation (s1 +* (DataPart s2)),i)) . d by FUNCT_1:70
.= (Computation s2,i) . d by A23, A40, FUNCT_1:70 ;
:: thesis:

end;

A41: now

let x be set ; :: thesis:
let d be Data-Location ; :: thesis:
assume that
A42: ( d = x & d in dom (DataPart p) ) and
A43: ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) ; :: thesis:
( ((Computation s1,i) | (dom (DataPart p))) . d = (Computation s1,i) . d & ((Computation s2,i) | (dom (DataPart p))) . d = (Computation s2,i) . d ) by A24, A32, A33, A42, FUNCT_1:70;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A22, A24, A30, A42, A43, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A24, A31, A42, FUNCT_1:70 ;
:: thesis:

end;

A44: now

let x be set ; :: thesis:
let d be Data-Location ; :: thesis:
assume that
A45: ( d = x & d in dom (DataPart p) ) and
A46: (Computation s1,(i + 1)) . d = (Computation s2,(i + 1)) . d ; :: thesis:
thus ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A30, A45, A46, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A24, A31, A45, FUNCT_1:70 ; :: thesis:

end;

A47: now

let x be set ; :: thesis:
assume A48: ( x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation s2,(i + 1)) . x ) ; :: thesis:
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (Computation s2,(i + 1)) . x by FUNCT_1:70
.= (DataPart (Computation s2,(i + 1))) . x by A36, A37, A48, FUNCT_1:70 ;
:: thesis:

end;

A49: now

let x be set ; :: thesis:
assume A50: ( x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) ; :: thesis:
then ( (DataPart (Computation (s1 +* (DataPart s2)),i)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (DataPart (Computation s2,i)) . x = (Computation s2,i) . x ) by A34, A35, A36, FUNCT_1:70;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A23, A47, A50; :: thesis:

end;

A51: now

assume A52: (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
reconsider loc = IC (Computation s1,(i + 1)) as Instruction-Location of SCM ;
reconsider kk = loc as Element of NAT by ORDINAL1:def 13;
A53: loc in dom (ProgramPart p) by A2, A9, AMI_5:86;
ProgramPart p c= p by RELAT_1:88;
then A54: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
A55: CurInstr (Computation s1,(i + 1)) = s1 . loc by AMI_1:54
.= p . loc by A2, A53, A54, GRFUNC_1:8 ;
loc + k in dom (Relocated p,k) by A53, A54, Th24;
then (Relocated p,k) . (loc + k) = s2 . (loc + k) by A3, GRFUNC_1:8
.= (Computation s2,(i + 1)) . (kk + k) by AMI_1:54 ;
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A52, A53, A55, Th27; :: thesis:

end;

A56: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A57: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
A58: Computation (s1 +* (DataPart s2)),(i + 1) = Following (Computation (s1 +* (DataPart s2)),i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation (s1 +* (DataPart s2)),i) by A2, A9, A10, AMI_5:87 ;
reconsider j = IC (Computation s1,i) as Element of NAT by ORDINAL1:def 13;
A60: Next ((IC (Computation s1,i)) + k) = il. ((j + k) + 1) by NAT_1:39
.= (il. (j + 1)) + k
.= (Next (IC (Computation s1,i))) + k by NAT_1:39 ;
set I = CurInstr (Computation s1,i);

per cases by AMI_5:36, NAT_1:33;

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

then A61: CurInstr (Computation s1,i) = halt SCM by AMI_5:46;
then A62: CurInstr (Computation s2,i) = halt SCM by A21, Def3, AMI_5:37;
thus (IC (Computation s1,(i + 1))) + k = (IC (Computation s1,i)) + k by A56, A61, AMI_1:def 8
.= IC (Computation s2,(i + 1)) by A20, A57, A62, AMI_1:def 8 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A51; :: thesis:
A63: ( Computation s2,(i + 1) = Computation s2,i & Computation s1,(i + 1) = Computation s1,i ) by A56, A57, A61, A62, AMI_1:def 8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A22; :: thesis:
thus DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) by A23, A58, A61, A63, AMI_1:def 8; :: thesis:

end;

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

then consider da, db being Data-Location such that
A64: CurInstr (Computation s1,i) = da := db by AMI_5:47;
A65: IncAddr (CurInstr (Computation s1,i)),k = da := db by A64, Th5;
A66: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A64, AMI_3:8;
A67: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A39;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A65, A66, AMI_3:8; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A65, A66, AMI_3:8; :: thesis:

now

let x be set ; :: thesis:
assume A68: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A68;
then reconsider d = x as Data-Location by AMI_3:def 2;
DataPart p c= p by RELAT_1:88;
then A69: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A70: da = d ; :: thesis:

then A71: (Computation s1,(i + 1)) . d = (Computation s1,i) . db by A56, A64, AMI_3:8;
(Computation s2,(i + 1)) . d = (Computation s2,i) . db by A21, A57, A65, A70, AMI_3:8;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A9, A10, A30, A44, A64, A67, A68, A69, A70, A71, AMI_5:88; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A64, A65, AMI_3:8;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A68; :: thesis:

end;

then (Computation s1,(i + 1)) | (dom (DataPart p)) c= (Computation s2,(i + 1)) | (dom (DataPart p)) by A24, A30, A31, GRFUNC_1:8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A24, A30, A31, GRFUNC_1:9; :: thesis:

now

let x be set ; :: thesis:
assume A72: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = (Computation s2,i) . db & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . db ) by A21, A57, A58, A64, A65, AMI_3:8;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A39, A47, A72; :: thesis:

end;

suppose A73: da <> d ; :: thesis:

then A74: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A64, AMI_3:8;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A65, A73, AMI_3:8;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A72, A74; :: thesis:

end;

then DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) c= DataPart (Computation s2,(i + 1)) by A36, A37, GRFUNC_1:8;
hence DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) by A36, A37, GRFUNC_1:9; :: thesis:

end;

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

then consider da, db being Data-Location such that
A75: CurInstr (Computation s1,i) = AddTo da,db by AMI_5:48;
A76: IncAddr (CurInstr (Computation s1,i)),k = AddTo da,db by A75, Th6;
A77: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A75, AMI_3:9;
A78: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;
A79: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A39;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A76, A77, AMI_3:9; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A76, A77, AMI_3:9; :: thesis:

now

let x be set ; :: thesis:
assume A80: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A80;
then reconsider d = x as Data-Location by AMI_3:def 2;
DataPart p c= p by RELAT_1:88;
then A81: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A82: da = d ; :: thesis:

then A83: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) + ((Computation s1,i) . db) by A56, A75, AMI_3:9;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A21, A57, A76, A82, AMI_3:9;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A9, A10, A30, A44, A75, A78, A79, A80, A81, A82, A83, AMI_5:89; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A75, A76, AMI_3:9;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A80; :: thesis:

end;

now

let x be set ; :: thesis:
assume A84: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose A85: da = d ; :: thesis:

then A86: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A21, A57, A76, AMI_3:9;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) + ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A75, A85, AMI_3:9;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A78, A79, A84, A86; :: thesis:

end;

suppose A87: da <> d ; :: thesis:

then A88: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A75, AMI_3:9;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A76, A87, AMI_3:9;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A84, A88; :: thesis:

end;

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

then consider da, db being Data-Location such that
A89: CurInstr (Computation s1,i) = SubFrom da,db by AMI_5:49;
A90: IncAddr (CurInstr (Computation s1,i)),k = SubFrom da,db by A89, Th7;
A91: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A89, AMI_3:10;
A92: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;
A93: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A39;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A90, A91, AMI_3:10; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A90, A91, AMI_3:10; :: thesis:

now

let x be set ; :: thesis:
assume A94: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A94;
then reconsider d = x as Data-Location by AMI_3:def 2;
DataPart p c= p by RELAT_1:88;
then A95: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A96: da = d ; :: thesis:

then A97: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) - ((Computation s1,i) . db) by A56, A89, AMI_3:10;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A21, A57, A90, A96, AMI_3:10;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A9, A10, A30, A44, A89, A92, A93, A94, A95, A96, A97, AMI_5:90; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A89, A90, AMI_3:10;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A94; :: thesis:

end;

now

let x be set ; :: thesis:
assume A98: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose A99: da = d ; :: thesis:

then A100: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A21, A57, A90, AMI_3:10;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) - ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A89, A99, AMI_3:10;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A92, A93, A98, A100; :: thesis:

end;

suppose A101: da <> d ; :: thesis:

then A102: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A89, AMI_3:10;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A90, A101, AMI_3:10;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A98, A102; :: thesis:

end;

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

then consider da, db being Data-Location such that
A103: CurInstr (Computation s1,i) = MultBy da,db by AMI_5:50;
A104: IncAddr (CurInstr (Computation s1,i)),k = MultBy da,db by A103, Th8;
A105: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A103, AMI_3:11;
A106: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;
A107: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A39;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A104, A105, AMI_3:11; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A104, A105, AMI_3:11; :: thesis:

now

let x be set ; :: thesis:
assume A108: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A108;
then reconsider d = x as Data-Location by AMI_3:def 2;
DataPart p c= p by RELAT_1:88;
then A109: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A110: da = d ; :: thesis:

then A111: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) * ((Computation s1,i) . db) by A56, A103, AMI_3:11;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A21, A57, A104, A110, AMI_3:11;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A9, A10, A30, A44, A103, A106, A107, A108, A109, A110, A111, AMI_5:91; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A103, A104, AMI_3:11;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A108; :: thesis:

end;

now

let x be set ; :: thesis:
assume A112: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose A113: da = d ; :: thesis:

then A114: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A21, A57, A104, AMI_3:11;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) * ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A103, A113, AMI_3:11;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A106, A107, A112, A114; :: thesis:

end;

suppose A115: da <> d ; :: thesis:

then A116: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A103, AMI_3:11;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A104, A115, AMI_3:11;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A112, A116; :: thesis:

end;

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

then consider da, db being Data-Location such that
A117: CurInstr (Computation s1,i) = Divide da,db by AMI_5:51;
A118: IncAddr (CurInstr (Computation s1,i)),k = Divide da,db by A117, Th9;
A119: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;
A120: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A39;

now

per cases ;

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

A122: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A117, AMI_3:12;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A118, AMI_3:12; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A118, A122, AMI_3:12; :: thesis:

now

let x be set ; :: thesis:
assume A123: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A123;
then reconsider d = x as Data-Location by AMI_3:def 2;
DataPart p c= p by RELAT_1:88;
then A124: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A125: da = d ; :: thesis:

then A126: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) div ((Computation s1,i) . db) by A56, A117, A121, AMI_3:12;
A127: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) div ((Computation s2,i) . db) by A21, A57, A118, A121, A125, AMI_3:12;
((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) = ((Computation s1,i) . da) div ((Computation s1,i) . db) by A2, A9, A10, A30, A117, A121, A123, A124, A125, AMI_5:92;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A119, A120, A123, A126, A127, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A24, A30, A31, A123, FUNCT_1:70 ;
:: thesis:

end;

suppose A128: db = d ; :: thesis:

then A129: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) mod ((Computation s1,i) . db) by A56, A117, AMI_3:12;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A21, A57, A118, A128, AMI_3:12;
then (Computation s1,(i + 1)) . d = (Computation s2,(i + 1)) . d by A2, A9, A10, A30, A117, A119, A120, A121, A123, A124, A128, A129, AMI_5:93;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A44, A123; :: thesis:

end;

suppose ( da <> d & db <> d ) ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A117, A118, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A123; :: thesis:

end;

now

let x be set ; :: thesis:
assume A130: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose A131: da = d ; :: thesis:

then A132: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) div ((Computation s2,i) . db) by A21, A57, A118, A121, AMI_3:12;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A117, A121, A131, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A119, A120, A130, A132; :: thesis:

end;

suppose A133: db = d ; :: thesis:

then A134: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A21, A57, A118, AMI_3:12;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A117, A133, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A119, A120, A130, A134; :: thesis:

end;

suppose A135: ( da <> d & db <> d ) ; :: thesis:

then A136: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A117, AMI_3:12;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A118, A135, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A130, A136; :: thesis:

end;

suppose A137: da = db ; :: thesis:

A138: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A117, AMI_3:12;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A21, A56, A57, A60, A118, AMI_3:12; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A20, A21, A51, A56, A57, A60, A118, A138, AMI_3:12; :: thesis:

now

let x be set ; :: thesis:
assume A139: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A139;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A140: da = d ; :: thesis:

then A141: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A21, A57, A118, A137, AMI_3:12;
A142: ( ((Computation s1,i) | (dom (DataPart p))) . d = (Computation s1,i) . d & ((Computation s2,i) | (dom (DataPart p))) . d = (Computation s2,i) . d ) by A24, A30, A32, A33, A139, FUNCT_1:70;
( ((Computation s1,(i + 1)) | (dom (DataPart p))) . d = (Computation s1,(i + 1)) . d & ((Computation s2,(i + 1)) | (dom (DataPart p))) . d = (Computation s2,(i + 1)) . d ) by A24, A30, A31, A139, FUNCT_1:70;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A22, A24, A56, A117, A137, A140, A141, A142, AMI_3:12; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A21, A56, A57, A117, A118, A137, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A139; :: thesis:

end;

now

let x be set ; :: thesis:
assume A143: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;

per cases ;

suppose A144: da = d ; :: thesis:

then A145: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A21, A57, A118, A137, AMI_3:12;
(Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) by A58, A117, A137, A144, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A47, A119, A120, A143, A145; :: thesis:

end;

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

then A147: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A58, A117, A137, AMI_3:12;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A21, A57, A118, A137, A146, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A143, A147; :: thesis:

end;

hence ( (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) & IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) & (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) ) ; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM such that
A148: CurInstr (Computation s1,i) = goto loc by AMI_5:52;
A149: CurInstr (Computation s2,i) = goto (loc + k) by A21, A148, Th10;
thus (IC (Computation s1,(i + 1))) + k = loc + k by A56, A148, AMI_3:13
.= IC (Computation s2,(i + 1)) by A57, A149, AMI_3:13 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A51; :: thesis:

now

let x be set ; :: thesis:
assume A150: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A150;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A56, A57, A148, A149, AMI_3:13;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A150; :: thesis:

end;

now

let x be set ; :: thesis:
assume A151: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A57, A58, A148, A149, AMI_3:13;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A151; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A152: CurInstr (Computation s1,i) = da =0_goto loc by AMI_5:53;
A153: CurInstr (Computation s2,i) = da =0_goto (loc + k) by A21, A152, Th11;
A154: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;

A155: now

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

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

hence (IC (Computation s1,(i + 1))) + k = loc + k by A56, A152, AMI_3:14; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A20, A56, A60, A152, AMI_3:14; :: thesis:

end;

A156: now

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

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

hence IC (Computation s2,(i + 1)) = loc + k by A57, A153, AMI_3:14; :: thesis:

end;

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

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A57, A153, AMI_3:14; :: thesis:

end;

A157: now

per cases ;

suppose loc <> Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A2, A9, A10, A152, A154, A155, A156, AMI_5:94; :: thesis:

end;

suppose loc = Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A60, A155, A156; :: thesis:

end;

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A51, A157; :: thesis:

now

let x be set ; :: thesis:
assume A158: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A158;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A56, A57, A152, A153, AMI_3:14;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A158; :: thesis:

end;

now

let x be set ; :: thesis:
assume A159: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A57, A58, A152, A153, AMI_3:14;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A159; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A160: CurInstr (Computation s1,i) = da >0_goto loc by AMI_5:54;
A161: CurInstr (Computation s2,i) = da >0_goto (loc + k) by A21, A160, Th12;
A162: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A39;

A163: now

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

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

hence (IC (Computation s1,(i + 1))) + k = loc + k by A56, A160, AMI_3:15; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A20, A56, A60, A160, AMI_3:15; :: thesis:

end;

A164: now

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

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

hence IC (Computation s2,(i + 1)) = loc + k by A57, A161, AMI_3:15; :: thesis:

end;

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

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A57, A161, AMI_3:15; :: thesis:

end;

A165: now

per cases ;

suppose loc <> Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A2, A9, A10, A160, A162, A163, A164, AMI_5:95; :: thesis:

end;

suppose loc = Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A20, A60, A163, A164; :: thesis:

end;

now

let x be set ; :: thesis:
assume A166: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A30, A166;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A56, A57, A160, A161, AMI_3:15;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A30, A41, A166; :: thesis:

end;

now

let x be set ; :: thesis:
assume A167: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A36, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A57, A58, A160, A161, AMI_3:15;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A49, A167; :: thesis:

end;

then A168: for i being Element of NAT st S₁[i] holds
S₁[i + 1] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A19, A168); :: thesis: