let k be natural number ; :: thesis:
let R be good Ring; :: thesis:
let s1, s2, s be State of (SCM R); :: thesis:
assume A1: not R is trivial ; :: thesis:
let p be autonomic FinPartState of (SCM R); :: thesis:
assume that
A2: IC (SCM R) in dom p and
A3: p c= s1 and
A4: Relocated p,k c= s2 and
A5: s = s1 +* (DataPart s2) ; :: thesis:
A6: IC (SCM R) in dom (Relocated p,k) by AMISTD_2:72;
A7: DataPart p = DataPart (Relocated p,k) by AMISTD_2:68;
A8: DataPart p c= p by RELAT_1:88;
A9: DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
A10: not p is NAT -defined by A2, AMI_1:109;
A11: p c= s by A3, A4, A5, Th58;
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 s,$1) = DataPart (Computation s2,$1) );
A12: S₁[ 0 ]

proof

thus (IC (Computation s1,0 )) + k = (IC s1) + k by AMI_1:13
.= (IC p) + k by A2, A3, AMI_1:97
.= IC (Relocated p,k) by AMISTD_2:73
.= IC s2 by A4, A6, AMI_1:97
.= IC (Computation s2,0 ) by AMI_1:13 ; :: thesis:
A13: IC p = IC s1 by A2, A3, AMI_1:97;
then IC p = IC (Computation s1,0 ) by AMI_1:13;
then A14: IC p in dom (ProgramPart p) by A1, A3, A10, Th40;
ProgramPart p c= p by RELAT_1:88;
then A15: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
A16: p . (IC p) = s1 . (IC s1) by A3, A13, A14, A15, GRFUNC_1:8;
A17: IncAddr (CurInstr (Computation s1,0 )),k = IncAddr (CurInstr s1),k by AMI_1:13
.= IncAddr (s1 . (IC s1)),k ;
A18: IC (SCM R) in dom (Relocated p,k) by AMISTD_2:72;
A19: (IC p) + k in dom (Relocated p,k) by A14, A15, AMISTD_2:71;
CurInstr (Computation s2,0 ) = CurInstr s2 by AMI_1:13
.= s2 . (IC (Relocated p,k)) by A4, A18, AMI_1:97
.= s2 . ((IC p) + k) by AMISTD_2:73
.= (Relocated p,k) . ((IC p) + k) by A4, A19, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,0 )),k = CurInstr (Computation s2,0 ) by A14, A16, A17, AMISTD_2:76; :: thesis:
thus (Computation s1,0 ) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by AMI_1:13
.= DataPart p by A3, A8, GRFUNC_1:64, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A4, A7, A9, GRFUNC_1:64, XBOOLE_1:1
.= (Computation s2,0 ) | (dom (DataPart (Relocated p,k))) by A7, AMI_1:13 ; :: thesis:
thus DataPart (Computation s,0 ) = DataPart (s1 +* (DataPart s2)) by A5, AMI_1:13
.= DataPart s2 by CARD_3:99
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

A21: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume that
A22: (IC (Computation s1,i)) + k = IC (Computation s2,i) and
A23: IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) and
A24: (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) and
A25: DataPart (Computation s,i) = DataPart (Computation s2,i) ; :: thesis:
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
set Cs3i = Computation s,i;
set Cs1i1 = Computation s1,(i + 1);
set Cs2i1 = Computation s2,(i + 1);
set Cs3i1 = Computation s,(i + 1);
set DPp = DataPart p;
A26: dom (DataPart p) = dom (DataPart (Relocated p,k)) by AMISTD_2:68;
dom (Computation s1,(i + 1)) = the carrier of (SCM R) by AMI_1:79;
then A27: dom (Computation s1,(i + 1)) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by Th14;
dom (Computation s2,(i + 1)) = the carrier of (SCM R) by AMI_1:79;
then A28: dom (Computation s2,(i + 1)) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by Th14;
dom (Computation s1,i) = the carrier of (SCM R) by AMI_1:79;
then A29: dom (Computation s1,i) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by Th14;
dom (Computation s2,i) = the carrier of (SCM R) by AMI_1:79;
then A30: dom (Computation s2,i) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by Th14;
Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
then dom (DataPart p) = (dom p) /\ SCM-Data-Loc by RELAT_1:90;
then A31: dom (DataPart p) c= {(IC (SCM R))} \/ SCM-Data-Loc by XBOOLE_1:10, XBOOLE_1:17;
A32: dom ((Computation s1,(i + 1)) | (dom (DataPart p))) = (dom (Computation s1,(i + 1))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A27, A31, XBOOLE_1:10, XBOOLE_1:28 ;
A33: dom ((Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,(i + 1))) /\ (dom (DataPart p)) by A26, RELAT_1:90
.= dom (DataPart p) by A28, A31, XBOOLE_1:10, XBOOLE_1:28 ;
A34: dom ((Computation s1,i) | (dom (DataPart p))) = (dom (Computation s1,i)) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A29, A31, XBOOLE_1:10, XBOOLE_1:28 ;
A35: dom ((Computation s2,i) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,i)) /\ (dom (DataPart p)) by A26, RELAT_1:90
.= dom (DataPart p) by A30, A31, XBOOLE_1:10, XBOOLE_1:28 ;
A36: dom (DataPart (Computation s,i)) = SCM-Data-Loc by Th22;
A37: dom (DataPart (Computation s2,i)) = SCM-Data-Loc by Th22;
A38: dom (DataPart (Computation s,(i + 1))) = SCM-Data-Loc by Th22;
A39: dom (DataPart (Computation s2,(i + 1))) = SCM-Data-Loc by Th22;
A40: dom ((Computation s1,(i + 1)) | (dom (DataPart p))) c= dom ((Computation s2,(i + 1)) | (dom (DataPart p))) by A32, A33, AMISTD_2:68;
A41: dom (DataPart (Computation s,(i + 1))) c= dom (DataPart (Computation s2,(i + 1))) by A38, Th22;

A42: now

let s be State of (SCM R); :: thesis:
let d be Data-Location of R; :: thesis:
d in SCM-Data-Loc by SCMRING2:1;
hence d in dom (DataPart s) by Th22; :: thesis:

end;

A43: now

let d be Data-Location of R; :: thesis:
A44: ( d in dom (DataPart (Computation s,i)) & d in dom (DataPart (Computation s,i)) ) by A42;
hence (Computation s,i) . d = (DataPart (Computation s,i)) . d by FUNCT_1:70
.= (Computation s2,i) . d by A25, A44, FUNCT_1:70 ;
:: thesis:

end;

A45: now

let x be set ; :: thesis:
let d be Data-Location of R; :: thesis:
assume that
A46: ( d = x & d in dom (DataPart p) ) and
A47: ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) ; :: thesis:
A48: ( ((Computation s1,i) | (dom (DataPart p))) . d = (Computation s1,i) . d & ((Computation s2,i) | (dom (DataPart p))) . d = (Computation s2,i) . d ) by A26, A34, A35, A46, FUNCT_1:70;
thus ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s1,(i + 1)) . d by A32, A46, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A24, A26, A33, A46, A47, A48, FUNCT_1:70 ; :: thesis:

end;

A49: now

let x be set ; :: thesis:
let d be Data-Location of R; :: thesis:
assume that
A50: ( d = x & d in dom (DataPart p) ) and
A51: (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 A32, A50, A51, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A33, A50, FUNCT_1:70 ; :: thesis:

end;

A52: now

let x be set ; :: thesis:
assume A53: ( x in dom (DataPart (Computation s,(i + 1))) & (Computation s,(i + 1)) . x = (Computation s2,(i + 1)) . x ) ; :: thesis:
hence (DataPart (Computation s,(i + 1))) . x = (Computation s2,(i + 1)) . x by FUNCT_1:70
.= (DataPart (Computation s2,(i + 1))) . x by A38, A39, A53, FUNCT_1:70 ;
:: thesis:

end;

A54: now

let x be set ; :: thesis:
assume A55: ( x in dom (DataPart (Computation s,(i + 1))) & (Computation s,(i + 1)) . x = (Computation s,i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) ; :: thesis:
then ( (DataPart (Computation s,i)) . x = (Computation s,i) . x & (DataPart (Computation s2,i)) . x = (Computation s2,i) . x ) by A36, A37, A38, FUNCT_1:70;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A25, A52, A55; :: thesis:

end;

A56: now

assume A57: (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
reconsider loc = IC (Computation s1,(i + 1)) as Instruction-Location of SCM R ;
A58: loc in dom (ProgramPart p) by A1, A3, A10, Th40;
ProgramPart p c= p by RELAT_1:88;
then A59: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
A60: CurInstr (Computation s1,(i + 1)) = s1 . loc by AMI_1:54
.= p . loc by A3, A58, A59, GRFUNC_1:8 ;
loc + k in dom (Relocated p,k) by A58, A59, AMISTD_2:71;
then (Relocated p,k) . (loc + k) = s2 . (loc + k) by A4, GRFUNC_1:8
.= (Computation s2,(i + 1)) . (loc + k) by AMI_1:54 ;
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A57, A58, A60, AMISTD_2:76; :: thesis:

end;

A61: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A62: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
A63: Computation s,(i + 1) = Following (Computation s,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s,i) by A1, A3, A10, A11, Th41 ;
consider j being natural number such that
A64: IC (Computation s1,i) = il. (SCM R),j by AMISTD_1:26;
A65: Next ((IC (Computation s1,i)) + k) = Next (il. (SCM R),(j + k)) by A64, AMISTD_1:def 13
.= il. (SCM R),((j + k) + 1) by SCMRING3:67
.= il. (SCM R),((j + 1) + k)
.= (il. (SCM R),(j + 1)) + k by AMISTD_1:def 13
.= (Next (IC (Computation s1,i))) + k by A64, SCMRING3:67 ;
set I = CurInstr (Computation s1,i);

per cases by NAT_1:32, SCMRING3:71;

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

then A66: CurInstr (Computation s1,i) = halt (SCM R) by SCMRING3:16;
then A67: CurInstr (Computation s2,i) = halt (SCM R) by A23, AMISTD_2:29;
thus (IC (Computation s1,(i + 1))) + k = (IC (Computation s1,i)) + k by A61, A66, AMI_1:def 8
.= IC (Computation s2,(i + 1)) by A22, A62, A67, AMI_1:def 8 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A56; :: thesis:
A68: ( Computation s2,(i + 1) = Computation s2,i & Computation s1,(i + 1) = Computation s1,i ) by A61, A62, A66, A67, AMI_1:def 8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A24; :: thesis:
thus DataPart (Computation s,(i + 1)) = DataPart (Computation s2,(i + 1)) by A25, A63, A66, A68, AMI_1:def 8; :: thesis:

end;

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

then consider da, db being Data-Location of R such that
A69: CurInstr (Computation s1,i) = da := db by SCMRING3:17;
A70: IncAddr (CurInstr (Computation s1,i)),k = da := db by A69, AMISTD_2:29;
A71: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC (SCM R)) = Next (IC (Computation s1,i)) by A69, SCMRING2:13;
A72: (Computation s,i) . db = (Computation s2,i) . db by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A23, A61, A62, A65, A70, A71, SCMRING2:13; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A22, A23, A56, A61, A62, A65, A70, A71, SCMRING2:13; :: thesis:

now

let x be set ; :: thesis:
assume A73: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A73, SCMRING2:1;
DataPart p c= p by RELAT_1:88;
then A74: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A75: da = d ; :: thesis:

then A76: (Computation s1,(i + 1)) . d = (Computation s1,i) . db by A61, A69, SCMRING2:13;
(Computation s2,(i + 1)) . d = (Computation s2,i) . db by A23, A62, A70, A75, SCMRING2:13;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A1, A3, A10, A11, A32, A49, A69, A72, A73, A74, A75, A76, Th42; :: 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 A23, A61, A62, A69, A70, SCMRING2:13;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A73; :: thesis:

end;

then (Computation s1,(i + 1)) | (dom (DataPart p)) c= (Computation s2,(i + 1)) | (dom (DataPart p)) by A40, GRFUNC_1:8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A26, A32, A33, GRFUNC_1:9; :: thesis:

now

let x be set ; :: thesis:
assume A77: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = (Computation s2,i) . db & (Computation s,(i + 1)) . d = (Computation s,i) . db ) by A23, A62, A63, A69, A70, SCMRING2:13;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A43, A52, A77; :: thesis:

end;

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

then A79: (Computation s,(i + 1)) . d = (Computation s,i) . d by A63, A69, SCMRING2:13;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A23, A62, A70, A78, SCMRING2:13;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A77, A79; :: thesis:

end;

then DataPart (Computation s,(i + 1)) c= DataPart (Computation s2,(i + 1)) by A41, GRFUNC_1:8;
hence DataPart (Computation s,(i + 1)) = DataPart (Computation s2,(i + 1)) by A38, A39, GRFUNC_1:9; :: thesis:

end;

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

then consider da, db being Data-Location of R such that
A80: CurInstr (Computation s1,i) = AddTo da,db by SCMRING3:18;
A81: IncAddr (CurInstr (Computation s1,i)),k = AddTo da,db by A80, AMISTD_2:29;
A82: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC (SCM R)) = Next (IC (Computation s1,i)) by A80, SCMRING2:14;
A83: (Computation s,i) . da = (Computation s2,i) . da by A43;
A84: (Computation s,i) . db = (Computation s2,i) . db by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A23, A61, A62, A65, A81, A82, SCMRING2:14; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A22, A23, A56, A61, A62, A65, A81, A82, SCMRING2:14; :: thesis:

now

let x be set ; :: thesis:
assume A85: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A85, SCMRING2:1;
DataPart p c= p by RELAT_1:88;
then A86: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A87: da = d ; :: thesis:

then A88: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) + ((Computation s1,i) . db) by A61, A80, SCMRING2:14;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A23, A62, A81, A87, SCMRING2:14;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A1, A3, A10, A11, A32, A49, A80, A83, A84, A85, A86, A87, A88, Th43; :: 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 A23, A61, A62, A80, A81, SCMRING2:14;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A85; :: thesis:

end;

now

let x be set ; :: thesis:
assume A89: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;

per cases ;

suppose A90: da = d ; :: thesis:

then A91: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A23, A62, A81, SCMRING2:14;
(Computation s,(i + 1)) . d = ((Computation s,i) . da) + ((Computation s,i) . db) by A63, A80, A90, SCMRING2:14;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A52, A83, A84, A89, A91; :: thesis:

end;

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

then A93: (Computation s,(i + 1)) . d = (Computation s,i) . d by A63, A80, SCMRING2:14;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A23, A62, A81, A92, SCMRING2:14;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A89, A93; :: thesis:

end;

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

then consider da, db being Data-Location of R such that
A94: CurInstr (Computation s1,i) = SubFrom da,db by SCMRING3:19;
A95: IncAddr (CurInstr (Computation s1,i)),k = SubFrom da,db by A94, AMISTD_2:29;
A96: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC (SCM R)) = Next (IC (Computation s1,i)) by A94, SCMRING2:15;
A97: (Computation s,i) . da = (Computation s2,i) . da by A43;
A98: (Computation s,i) . db = (Computation s2,i) . db by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A23, A61, A62, A65, A95, A96, SCMRING2:15; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A22, A23, A56, A61, A62, A65, A95, A96, SCMRING2:15; :: thesis:

now

let x be set ; :: thesis:
assume A99: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A99, SCMRING2:1;
DataPart p c= p by RELAT_1:88;
then A100: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A101: da = d ; :: thesis:

then A102: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) - ((Computation s1,i) . db) by A61, A94, SCMRING2:15;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A23, A62, A95, A101, SCMRING2:15;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A1, A3, A10, A11, A32, A49, A94, A97, A98, A99, A100, A101, A102, Th44; :: 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 A23, A61, A62, A94, A95, SCMRING2:15;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A99; :: thesis:

end;

now

let x be set ; :: thesis:
assume A103: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;

per cases ;

suppose A104: da = d ; :: thesis:

then A105: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A23, A62, A95, SCMRING2:15;
(Computation s,(i + 1)) . d = ((Computation s,i) . da) - ((Computation s,i) . db) by A63, A94, A104, SCMRING2:15;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A52, A97, A98, A103, A105; :: thesis:

end;

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

then A107: (Computation s,(i + 1)) . d = (Computation s,i) . d by A63, A94, SCMRING2:15;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A23, A62, A95, A106, SCMRING2:15;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A103, A107; :: thesis:

end;

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

then consider da, db being Data-Location of R such that
A108: CurInstr (Computation s1,i) = MultBy da,db by SCMRING3:20;
A109: IncAddr (CurInstr (Computation s1,i)),k = MultBy da,db by A108, AMISTD_2:29;
A110: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC (SCM R)) = Next (IC (Computation s1,i)) by A108, SCMRING2:16;
A111: (Computation s,i) . da = (Computation s2,i) . da by A43;
A112: (Computation s,i) . db = (Computation s2,i) . db by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A23, A61, A62, A65, A109, A110, SCMRING2:16; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A22, A23, A56, A61, A62, A65, A109, A110, SCMRING2:16; :: thesis:

now

let x be set ; :: thesis:
assume A113: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A113, SCMRING2:1;
DataPart p c= p by RELAT_1:88;
then A114: dom (DataPart p) c= dom p by GRFUNC_1:8;

per cases ;

suppose A115: da = d ; :: thesis:

then A116: (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) * ((Computation s1,i) . db) by A61, A108, SCMRING2:16;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A23, A62, A109, A115, SCMRING2:16;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A1, A3, A10, A11, A32, A49, A108, A111, A112, A113, A114, A115, A116, Th45; :: 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 A23, A61, A62, A108, A109, SCMRING2:16;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A113; :: thesis:

end;

now

let x be set ; :: thesis:
assume A117: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;

per cases ;

suppose A118: da = d ; :: thesis:

then A119: (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A23, A62, A109, SCMRING2:16;
(Computation s,(i + 1)) . d = ((Computation s,i) . da) * ((Computation s,i) . db) by A63, A108, A118, SCMRING2:16;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A52, A111, A112, A117, A119; :: thesis:

end;

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

then A121: (Computation s,(i + 1)) . d = (Computation s,i) . d by A63, A108, SCMRING2:16;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A23, A62, A109, A120, SCMRING2:16;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A117, A121; :: thesis:

end;

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

then consider da being Data-Location of R, r being Element of R such that
A122: CurInstr (Computation s1,i) = da := r by SCMRING3:21;
A123: IncAddr (CurInstr (Computation s1,i)),k = da := r by A122, AMISTD_2:29;
A124: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC (SCM R)) = Next (IC (Computation s1,i)) by A122, SCMRING2:19;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A23, A61, A62, A65, A123, SCMRING2:19; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A22, A23, A56, A61, A62, A65, A123, A124, SCMRING2:19; :: thesis:

now

let x be set ; :: thesis:
assume A125: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A125, SCMRING2:1;

per cases ;

suppose A126: da = d ; :: thesis:

thus ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s1,(i + 1)) . d by A32, A125, FUNCT_1:72
.= r by A61, A122, A126, SCMRING2:19
.= (Computation s2,(i + 1)) . d by A23, A62, A123, A126, SCMRING2:19
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A125, FUNCT_1:72 ; :: 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 A23, A61, A62, A122, A123, SCMRING2:19;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A125; :: thesis:

end;

now

let x be set ; :: thesis:
assume A127: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = r & (Computation s,(i + 1)) . d = r ) by A23, A62, A63, A122, A123, SCMRING2:19;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A52, A127; :: thesis:

end;

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

then A129: (Computation s,(i + 1)) . d = (Computation s,i) . d by A63, A122, SCMRING2:19;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A23, A62, A123, A128, SCMRING2:19;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A127, A129; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM R such that
A130: CurInstr (Computation s1,i) = goto loc by SCMRING3:22;
A131: CurInstr (Computation s2,i) = goto (loc + k) by A23, A130, SCMRING3:69;
thus (IC (Computation s1,(i + 1))) + k = loc + k by A61, A130, SCMRING2:17
.= IC (Computation s2,(i + 1)) by A62, A131, SCMRING2:17 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A56; :: thesis:

now

let x be set ; :: thesis:
assume A132: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by Th26;
then reconsider d = x as Data-Location of R by A32, A132, SCMRING2:1;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A61, A62, A130, A131, SCMRING2:17;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A132; :: thesis:

end;

now

let x be set ; :: thesis:
assume A133: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;
( (Computation s,(i + 1)) . d = (Computation s,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A62, A63, A130, A131, SCMRING2:17;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A133; :: thesis:

end;

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

then consider da being Data-Location of R, loc being Instruction-Location of SCM R such that
A134: CurInstr (Computation s1,i) = da =0_goto loc by SCMRING3:23;
A135: CurInstr (Computation s2,i) = da =0_goto (loc + k) by A23, A134, SCMRING3:70;
A136: (Computation s,i) . da = (Computation s2,i) . da by A43;

A137: now

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

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

hence (IC (Computation s1,(i + 1))) + k = loc + k by A61, A134, SCMRING2:18; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A22, A61, A65, A134, SCMRING2:18; :: thesis:

end;

A138: now

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

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

hence IC (Computation s2,(i + 1)) = loc + k by A62, A135, SCMRING2:18; :: thesis:

end;

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

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A62, A135, SCMRING2:18; :: thesis:

end;

now

per cases ;

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

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A1, A3, A10, A11, A134, A136, A137, A138, Th46; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A22, A65, A137, A138; :: 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)) ) by A56; :: 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 Th26;
then reconsider d = x as Data-Location of R by A32, A139, SCMRING2:1;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A61, A62, A134, A135, SCMRING2:18;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A32, A45, A139; :: thesis:

end;

now

let x be set ; :: thesis:
assume A140: x in dom (DataPart (Computation s,(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location of R by A38, SCMRING2:1;
( (Computation s,(i + 1)) . d = (Computation s,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A62, A63, A134, A135, SCMRING2:18;
hence (DataPart (Computation s,(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A54, A140; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A12, A21);
hence for i being Element of NAT holds
( (IC (Computation s1,i)) + k = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) & (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Computation s,i) = DataPart (Computation s2,i) ) ; :: thesis: