let k be Element of NAT ; :: thesis: for R being good Ring
for s1, s2, s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated (p,k) c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let R be good Ring; :: thesis: for s1, s2, s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated (p,k) c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let s1, s2, s be State of (SCM R); :: thesis: ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated (p,k) c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume A1: not R is trivial ; :: thesis: for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s1 & Relocated (p,k) c= s2 & s = s1 +* (DataPart s2) holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let p be autonomic FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p & p c= s1 & Relocated (p,k) c= s2 & s = s1 +* (DataPart s2) implies for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
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: for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
defpred S₁[ Element of NAT ] means ( (IC (Comput ((ProgramPart s1),s1,$1))) + k = IC (Comput ((ProgramPart s2),s2,$1)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,$1))),(Comput ((ProgramPart s1),s1,$1)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,$1))),(Comput ((ProgramPart s2),s2,$1))) & (Comput ((ProgramPart s1),s1,$1)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,$1)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) );
A6: not p is NAT -defined by A2, COMPOS_1:19;
A7: IC p = IC s1 by A2, A3, GRFUNC_1:8;
then IC p = IC (Comput ((ProgramPart s1),s1,0)) by EXTPRO_1:3;
then A8: IC p in dom (ProgramPart p) by A1, A3, A6, Th27;
A9: p c= s by A3, A4, A5, Th34;
A10: 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: ( S₁[i] implies S₁[i + 1] )
assume that
A11: (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) and
A12: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) and
A13: (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) and
A14: DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ; :: thesis: S₁[i + 1]
set Cs2i1 = Comput ((ProgramPart s2),s2,(i + 1));
set Cs3i = Comput ((ProgramPart s),s,i);
set Cs2i = Comput ((ProgramPart s2),s2,i);
A15: Comput ((ProgramPart s2),s2,(i + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i)))),(Comput ((ProgramPart s2),s2,i))) by AMI_1:123 ;

A16: now

let s be State of (SCM R); :: thesis: for d being Data-Location of R holds d in dom (DataPart s)
let d be Data-Location of R; :: thesis: d in dom (DataPart s)
d in Data-Locations SCM by SCMRING2:1;
hence d in dom (DataPart s) by Th9; :: thesis: verum

end;

A17: now

let d be Data-Location of R; :: thesis: (Comput ((ProgramPart s),s,i)) . d = (Comput ((ProgramPart s2),s2,i)) . d
A18: d in dom (DataPart (Comput ((ProgramPart s),s,i))) by A16;
hence (Comput ((ProgramPart s),s,i)) . d = (DataPart (Comput ((ProgramPart s),s,i))) . d by FUNCT_1:70
.= (Comput ((ProgramPart s2),s2,i)) . d by A14, A18, FUNCT_1:70 ;
:: thesis: verum

end;

set Cs1i1 = Comput ((ProgramPart s1),s1,(i + 1));
set Cs1i = Comput ((ProgramPart s1),s1,i);
dom (Comput ((ProgramPart s1),s1,(i + 1))) = the carrier of (SCM R) by PARTFUN1:def 4;
then A19: dom (Comput ((ProgramPart s1),s1,(i + 1))) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by Th1;
consider j being natural number ;
A21: succ ((IC (Comput ((ProgramPart s1),s1,i))) + k) = (succ (IC (Comput ((ProgramPart s1),s1,i)))) + k ;

A22: now

reconsider loc = IC (Comput ((ProgramPart s1),s1,(i + 1))) as Element of NAT ;
assume A23: (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) ; :: thesis: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1))))
A24: loc in dom (ProgramPart p) by A1, A3, A6, Th27;
ProgramPart p c= p by RELAT_1:88;
then A25: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then loc + k in dom (Relocated (p,k)) by A24, COMPOS_1:118;
then A26: (Relocated (p,k)) . (loc + k) = s2 . (loc + k) by A4, GRFUNC_1:8
.= (Comput ((ProgramPart s2),s2,(i + 1))) . (loc + k) by AMI_1:54 ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))) /. loc = (Comput ((ProgramPart s1),s1,(i + 1))) . loc by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))) /. (IC (Comput ((ProgramPart s2),s2,(i + 1)))) = (Comput ((ProgramPart s2),s2,(i + 1))) . (IC (Comput ((ProgramPart s2),s2,(i + 1)))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1)))) = s1 . loc by Y, AMI_1:54
.= p . loc by A3, A24, A25, GRFUNC_1:8 ;
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A23, A24, A26, Z, COMPOS_1:122; :: thesis: verum

end;

dom (Comput ((ProgramPart s2),s2,i)) = the carrier of (SCM R) by PARTFUN1:def 4;
then A27: dom (Comput ((ProgramPart s2),s2,i)) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by Th1;
Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
then dom (DataPart p) = (dom p) /\ (Data-Locations SCM) by RELAT_1:90;
then A28: dom (DataPart p) c= {(IC (SCM R))} \/ (Data-Locations SCM) by XBOOLE_1:10, XBOOLE_1:17;
set Cs3i1 = Comput ((ProgramPart s),s,(i + 1));
A29: dom (DataPart (Comput ((ProgramPart s2),s2,i))) = Data-Locations SCM by Th9;
A30: dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) = Data-Locations SCM by Th9;
then A31: dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) c= dom (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) by Th9;
A32: dom (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) = Data-Locations SCM by Th9;

A33: now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) & (Comput ((ProgramPart s),s,(i + 1))) . x = (Comput ((ProgramPart s2),s2,(i + 1))) . x implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x )
assume that
A34: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) and
A35: (Comput ((ProgramPart s),s,(i + 1))) . x = (Comput ((ProgramPart s2),s2,(i + 1))) . x ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x
thus (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (Comput ((ProgramPart s2),s2,(i + 1))) . x by A34, A35, FUNCT_1:70
.= (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A30, A32, A34, FUNCT_1:70 ; :: thesis: verum

end;

A36: dom (DataPart (Comput ((ProgramPart s),s,i))) = Data-Locations SCM by Th9;

A37: now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) & (Comput ((ProgramPart s),s,(i + 1))) . x = (Comput ((ProgramPart s),s,i)) . x & (Comput ((ProgramPart s2),s2,(i + 1))) . x = (Comput ((ProgramPart s2),s2,i)) . x implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x )
assume that
A38: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) and
A39: ( (Comput ((ProgramPart s),s,(i + 1))) . x = (Comput ((ProgramPart s),s,i)) . x & (Comput ((ProgramPart s2),s2,(i + 1))) . x = (Comput ((ProgramPart s2),s2,i)) . x ) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x
(DataPart (Comput ((ProgramPart s),s,i))) . x = (Comput ((ProgramPart s),s,i)) . x by A36, A30, A38, FUNCT_1:70;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A14, A29, A30, A33, A38, A39, FUNCT_1:70; :: thesis: verum

end;

dom (Comput ((ProgramPart s1),s1,i)) = the carrier of (SCM R) by PARTFUN1:def 4;
then A40: dom (Comput ((ProgramPart s1),s1,i)) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by Th1;
dom (Comput ((ProgramPart s2),s2,(i + 1))) = the carrier of (SCM R) by PARTFUN1:def 4;
then A41: dom (Comput ((ProgramPart s2),s2,(i + 1))) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by Th1;
set I = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)));
A42: Comput ((ProgramPart s1),s1,(i + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i))) by AMI_1:123 ;
A43: dom ((Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p))) = (dom (Comput ((ProgramPart s1),s1,i))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A40, A28, XBOOLE_1:10, XBOOLE_1:28 ;
A44: dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput ((ProgramPart s1),s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A19, A28, XBOOLE_1:10, XBOOLE_1:28 ;
A45: dom (DataPart p) = dom (DataPart (Relocated (p,k))) by COMPOS_1:115;
then A46: dom ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput ((ProgramPart s2),s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A41, A28, XBOOLE_1:10, XBOOLE_1:28 ;
then A47: dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) c= dom ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) by A44, COMPOS_1:115;
A48: dom ((Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput ((ProgramPart s2),s2,i))) /\ (dom (DataPart p)) by A45, RELAT_1:90
.= dom (DataPart p) by A27, A28, XBOOLE_1:10, XBOOLE_1:28 ;

A49: now

let x be set ; :: thesis: for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d holds
((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location of R; :: thesis: ( d = x & d in dom (DataPart p) & (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A50: d = x and
A51: d in dom (DataPart p) and
A52: ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
A53: ( ((Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p))) . d = (Comput ((ProgramPart s1),s1,i)) . d & ((Comput ((ProgramPart s2),s2,i)) | (dom (DataPart p))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A45, A43, A48, A51, FUNCT_1:70;
thus ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = (Comput ((ProgramPart s1),s1,(i + 1))) . d by A44, A50, A51, FUNCT_1:70
.= ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A13, A45, A46, A50, A51, A52, A53, FUNCT_1:70 ; :: thesis: verum

end;

A54: now

let x be set ; :: thesis: for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s2),s2,(i + 1))) . d holds
((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location of R; :: thesis: ( d = x & d in dom (DataPart p) & (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s2),s2,(i + 1))) . d implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A55: ( d = x & d in dom (DataPart p) ) and
A56: (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s2),s2,(i + 1))) . d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
thus ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = (Comput ((ProgramPart s2),s2,(i + 1))) . d by A44, A55, A56, FUNCT_1:70
.= ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A45, A46, A55, FUNCT_1:70 ; :: thesis: verum

end;

T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i)) by AMI_1:123;
A57: Comput ((ProgramPart s),s,(i + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s),s,i))) by A1, A3, A6, A9, Th28, T ;

per cases ( InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 0 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 1 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 2 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 3 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 4 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 5 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 6 or InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 7 ) by NAT_1:32, SCMRING3:71;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 0 ; :: thesis: S₁[i + 1]

then A58: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = halt (SCM R) by SCMRING3:16;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = (IC (Comput ((ProgramPart s1),s1,i))) + k by A42, EXTPRO_1:def 3
.= IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A15, A58, EXTPRO_1:def 3 ;
:: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A22; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
A59: Comput ((ProgramPart s2),s2,(i + 1)) = Comput ((ProgramPart s2),s2,i) by A12, A15, A58, EXTPRO_1:def 3;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A13, A42, A58, EXTPRO_1:def 3; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))
thus DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A14, A57, A58, A59, EXTPRO_1:def 3; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 1 ; :: thesis: S₁[i + 1]

then consider da, db being Data-Location of R such that
A60: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = da := db by SCMRING3:17;
A61: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = da := db by A60, COMPOS_1:92;
A62: (Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i)))) . (IC (SCM R)) = succ (IC (Comput ((ProgramPart s1),s1,i))) by A60, SCMRING2:13;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A42, A15, A21, A61, SCMRING2:13; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A11, A12, A22, A42, A15, A21, A61, A62, SCMRING2:13; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
A63: (Comput ((ProgramPart s),s,i)) . db = (Comput ((ProgramPart s2),s2,i)) . db by A17;

now

DataPart p c= p by RELAT_1:88;
then A64: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁ )
assume A65: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A65, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose A66: da = d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . db & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . db ) by A12, A42, A15, A60, A61, SCMRING2:13;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A1, A3, A6, A9, A44, A54, A60, A63, A65, A64, A66, Th29; :: thesis: verum

end;

suppose da <> d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A42, A15, A60, A61, SCMRING2:13;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A65; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁ )
assume A67: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose da = d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . db & (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . db ) by A12, A15, A57, A60, A61, SCMRING2:13;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A17, A33, A67; :: thesis: verum

end;

suppose da <> d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A15, A57, A60, A61, SCMRING2:13;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A67; :: thesis: verum

end;

end;

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 2 ; :: thesis: S₁[i + 1]

then consider da, db being Data-Location of R such that
A68: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = AddTo (da,db) by SCMRING3:18;
A69: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = AddTo (da,db) by A68, COMPOS_1:92;
A70: (Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i)))) . (IC (SCM R)) = succ (IC (Comput ((ProgramPart s1),s1,i))) by A68, SCMRING2:14;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A42, A15, A21, A69, SCMRING2:14; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A11, A12, A22, A42, A15, A21, A69, A70, SCMRING2:14; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
A71: ( (Comput ((ProgramPart s),s,i)) . da = (Comput ((ProgramPart s2),s2,i)) . da & (Comput ((ProgramPart s),s,i)) . db = (Comput ((ProgramPart s2),s2,i)) . db ) by A17;

now

DataPart p c= p by RELAT_1:88;
then A72: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁ )
assume A73: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A73, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose A74: da = d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = ((Comput ((ProgramPart s1),s1,i)) . da) + ((Comput ((ProgramPart s1),s1,i)) . db) & (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) + ((Comput ((ProgramPart s2),s2,i)) . db) ) by A12, A42, A15, A68, A69, SCMRING2:14;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A1, A3, A6, A9, A44, A54, A68, A71, A73, A72, A74, Th30; :: thesis: verum

end;

suppose da <> d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A42, A15, A68, A69, SCMRING2:14;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A73; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁ )
assume A75: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose da = d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) + ((Comput ((ProgramPart s2),s2,i)) . db) & (Comput ((ProgramPart s),s,(i + 1))) . d = ((Comput ((ProgramPart s),s,i)) . da) + ((Comput ((ProgramPart s),s,i)) . db) ) by A12, A15, A57, A68, A69, SCMRING2:14;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A33, A71, A75; :: thesis: verum

end;

suppose da <> d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A15, A57, A68, A69, SCMRING2:14;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A75; :: thesis: verum

end;

end;

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 3 ; :: thesis: S₁[i + 1]

then consider da, db being Data-Location of R such that
A76: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = SubFrom (da,db) by SCMRING3:19;
A77: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = SubFrom (da,db) by A76, COMPOS_1:92;
A78: (Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i)))) . (IC (SCM R)) = succ (IC (Comput ((ProgramPart s1),s1,i))) by A76, SCMRING2:15;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A42, A15, A21, A77, SCMRING2:15; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A11, A12, A22, A42, A15, A21, A77, A78, SCMRING2:15; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
A79: ( (Comput ((ProgramPart s),s,i)) . da = (Comput ((ProgramPart s2),s2,i)) . da & (Comput ((ProgramPart s),s,i)) . db = (Comput ((ProgramPart s2),s2,i)) . db ) by A17;

now

DataPart p c= p by RELAT_1:88;
then A80: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁ )
assume A81: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A81, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose A82: da = d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = ((Comput ((ProgramPart s1),s1,i)) . da) - ((Comput ((ProgramPart s1),s1,i)) . db) & (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) - ((Comput ((ProgramPart s2),s2,i)) . db) ) by A12, A42, A15, A76, A77, SCMRING2:15;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A1, A3, A6, A9, A44, A54, A76, A79, A81, A80, A82, Th31; :: thesis: verum

end;

suppose da <> d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A42, A15, A76, A77, SCMRING2:15;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A81; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁ )
assume A83: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose da = d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) - ((Comput ((ProgramPart s2),s2,i)) . db) & (Comput ((ProgramPart s),s,(i + 1))) . d = ((Comput ((ProgramPart s),s,i)) . da) - ((Comput ((ProgramPart s),s,i)) . db) ) by A12, A15, A57, A76, A77, SCMRING2:15;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A33, A79, A83; :: thesis: verum

end;

suppose da <> d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A15, A57, A76, A77, SCMRING2:15;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A83; :: thesis: verum

end;

end;

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 4 ; :: thesis: S₁[i + 1]

then consider da, db being Data-Location of R such that
A84: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = MultBy (da,db) by SCMRING3:20;
A85: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = MultBy (da,db) by A84, COMPOS_1:92;
A86: (Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i)))) . (IC (SCM R)) = succ (IC (Comput ((ProgramPart s1),s1,i))) by A84, SCMRING2:16;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A42, A15, A21, A85, SCMRING2:16; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A11, A12, A22, A42, A15, A21, A85, A86, SCMRING2:16; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
A87: ( (Comput ((ProgramPart s),s,i)) . da = (Comput ((ProgramPart s2),s2,i)) . da & (Comput ((ProgramPart s),s,i)) . db = (Comput ((ProgramPart s2),s2,i)) . db ) by A17;

now

DataPart p c= p by RELAT_1:88;
then A88: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁ )
assume A89: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A89, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose A90: da = d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = ((Comput ((ProgramPart s1),s1,i)) . da) * ((Comput ((ProgramPart s1),s1,i)) . db) & (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) * ((Comput ((ProgramPart s2),s2,i)) . db) ) by A12, A42, A15, A84, A85, SCMRING2:16;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A1, A3, A6, A9, A44, A54, A84, A87, A89, A88, A90, Th32; :: thesis: verum

end;

suppose da <> d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A42, A15, A84, A85, SCMRING2:16;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A89; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁ )
assume A91: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose da = d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s2),s2,(i + 1))) . d = ((Comput ((ProgramPart s2),s2,i)) . da) * ((Comput ((ProgramPart s2),s2,i)) . db) & (Comput ((ProgramPart s),s,(i + 1))) . d = ((Comput ((ProgramPart s),s,i)) . da) * ((Comput ((ProgramPart s),s,i)) . db) ) by A12, A15, A57, A84, A85, SCMRING2:16;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A33, A87, A91; :: thesis: verum

end;

suppose da <> d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A15, A57, A84, A85, SCMRING2:16;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A91; :: thesis: verum

end;

end;

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 5 ; :: thesis: S₁[i + 1]

then consider da being Data-Location of R, r being Element of R such that
A92: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = da := r by SCMRING3:21;
A93: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = da := r by A92, COMPOS_1:92;
A94: (Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i)))) . (IC (SCM R)) = succ (IC (Comput ((ProgramPart s1),s1,i))) by A92, SCMRING2:19;
hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A12, A42, A15, A21, A93, SCMRING2:19; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A11, A12, A22, A42, A15, A21, A93, A94, SCMRING2:19; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )

now

let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁ )
assume A95: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A95, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose A96: da = d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

thus ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = (Comput ((ProgramPart s1),s1,(i + 1))) . d by A44, A95, FUNCT_1:72
.= r by A42, A92, A96, SCMRING2:19
.= (Comput ((ProgramPart s2),s2,(i + 1))) . d by A12, A15, A93, A96, SCMRING2:19
.= ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A95, FUNCT_1:72 ; :: thesis: verum

end;

suppose da <> d ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . b₁ = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . b₁

then ( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A42, A15, A92, A93, SCMRING2:19;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A95; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁ )
assume A97: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;

per cases ( da = d or da <> d ) ;

suppose da = d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s2),s2,(i + 1))) . d = r & (Comput ((ProgramPart s),s,(i + 1))) . d = r ) by A12, A15, A57, A92, A93, SCMRING2:19;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A33, A97; :: thesis: verum

end;

suppose da <> d ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . b₁ = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . b₁

then ( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A12, A15, A57, A92, A93, SCMRING2:19;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A97; :: thesis: verum

end;

end;

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 6 ; :: thesis: S₁[i + 1]

then consider loc being Element of NAT such that
A98: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = goto (loc,R) by SCMRING3:22;
A99: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) = goto ((loc + k),R) by A12, A98, SCMRING3:69;
thus (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = loc + k by A42, A98, SCMRING2:17
.= IC (Comput ((ProgramPart s2),s2,(i + 1))) by A15, A99, SCMRING2:17 ; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) & (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) by A22; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )

now

let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x )
assume A100: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A100, SCMRING2:1;
( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A42, A15, A98, A99, SCMRING2:17;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A100; :: thesis: verum

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x )
assume A101: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;
( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A15, A57, A98, A99, SCMRING2:17;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A101; :: thesis: verum

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

suppose InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))) = 7 ; :: thesis: S₁[i + 1]

then consider da being Data-Location of R, loc being Element of NAT such that
A102: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = da =0_goto loc by SCMRING3:23;

A103: now

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

case (Comput ((ProgramPart s1),s1,i)) . da = 0. R ; :: thesis: (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = loc + k

hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = loc + k by A42, A102, SCMRING2:18; :: thesis: verum

end;

case (Comput ((ProgramPart s1),s1,i)) . da <> 0. R ; :: thesis: (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = succ (IC (Comput ((ProgramPart s2),s2,i)))

hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = succ (IC (Comput ((ProgramPart s2),s2,i))) by A11, A42, A21, A102, SCMRING2:18; :: thesis: verum

end;

end;

end;

A104: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) = da =0_goto (loc + k) by A12, A102, SCMRING3:70;

A105: now

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

case (Comput ((ProgramPart s2),s2,i)) . da = 0. R ; :: thesis: IC (Comput ((ProgramPart s2),s2,(i + 1))) = loc + k

hence IC (Comput ((ProgramPart s2),s2,(i + 1))) = loc + k by A15, A104, SCMRING2:18; :: thesis: verum

end;

case (Comput ((ProgramPart s2),s2,i)) . da <> 0. R ; :: thesis: IC (Comput ((ProgramPart s2),s2,(i + 1))) = succ (IC (Comput ((ProgramPart s2),s2,i)))

hence IC (Comput ((ProgramPart s2),s2,(i + 1))) = succ (IC (Comput ((ProgramPart s2),s2,i))) by A15, A104, SCMRING2:18; :: thesis: verum

end;

end;

end;

A106: (Comput ((ProgramPart s),s,i)) . da = (Comput ((ProgramPart s2),s2,i)) . da by A17;

now

per cases ( loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) or loc = succ (IC (Comput ((ProgramPart s1),s1,i))) ) ;

suppose loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) ; :: thesis: (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1)))

hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A1, A3, A6, A9, A102, A106, A103, A105, Th33; :: thesis: verum

end;

suppose loc = succ (IC (Comput ((ProgramPart s1),s1,i))) ; :: thesis: (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1)))

hence (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) by A11, A103, A105; :: thesis: verum

end;

end;

end;

hence ( (IC (Comput ((ProgramPart s1),s1,(i + 1)))) + k = IC (Comput ((ProgramPart s2),s2,(i + 1))) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(i + 1)))),(Comput ((ProgramPart s1),s1,(i + 1))))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(i + 1)))),(Comput ((ProgramPart s2),s2,(i + 1)))) ) by A22; :: thesis: ( (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) )

now

let x be set ; :: thesis: ( x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) implies ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x )
assume A107: x in dom ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations SCM by Th13;
then reconsider d = x as Data-Location of R by A44, A107, SCMRING2:1;
( (Comput ((ProgramPart s1),s1,(i + 1))) . d = (Comput ((ProgramPart s1),s1,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A42, A15, A102, A104, SCMRING2:18;
hence ((Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p))) . x by A44, A49, A107; :: thesis: verum

end;

then (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) c= (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart p)) by A47, GRFUNC_1:8;
hence (Comput ((ProgramPart s1),s1,(i + 1))) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) by A45, A44, A46, GRFUNC_1:9; :: thesis: DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1)))

now

let x be set ; :: thesis: ( x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) implies (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x )
assume A108: x in dom (DataPart (Comput ((ProgramPart s),s,(i + 1)))) ; :: thesis: (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x
then reconsider d = x as Data-Location of R by A30, SCMRING2:1;
( (Comput ((ProgramPart s),s,(i + 1))) . d = (Comput ((ProgramPart s),s,i)) . d & (Comput ((ProgramPart s2),s2,(i + 1))) . d = (Comput ((ProgramPart s2),s2,i)) . d ) by A15, A57, A102, A104, SCMRING2:18;
hence (DataPart (Comput ((ProgramPart s),s,(i + 1)))) . x = (DataPart (Comput ((ProgramPart s2),s2,(i + 1)))) . x by A37, A108; :: thesis: verum

end;

then DataPart (Comput ((ProgramPart s),s,(i + 1))) c= DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A31, GRFUNC_1:8;
hence DataPart (Comput ((ProgramPart s),s,(i + 1))) = DataPart (Comput ((ProgramPart s2),s2,(i + 1))) by A30, A32, GRFUNC_1:9; :: thesis: verum

end;

end;

end;

Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
then A109: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0)))),k) = IncAddr ((s1 . (IC s1)),k) by COMPOS_1:38;
A110: DataPart (Relocated (p,k)) c= Relocated (p,k) by RELAT_1:88;
A111: DataPart p c= p by RELAT_1:88;
A112: DataPart p = DataPart (Relocated (p,k)) by COMPOS_1:115;
A113: (Comput ((ProgramPart s1),s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by EXTPRO_1:3
.= DataPart p by A3, A111, GRFUNC_1:64, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A4, A112, A110, GRFUNC_1:64, XBOOLE_1:1
.= (Comput ((ProgramPart s2),s2,0)) | (dom (DataPart (Relocated (p,k)))) by A112, EXTPRO_1:3 ;
A114: DataPart (Comput ((ProgramPart s),s,0)) = DataPart (s1 +* (DataPart s2)) by A5, EXTPRO_1:3
.= DataPart s2 by PBOOLE:157
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ;
A115: IC (SCM R) in dom (Relocated (p,k)) by COMPOS_1:119;
A116: (IC (Comput ((ProgramPart s1),s1,0))) + k = (IC s1) + k by EXTPRO_1:3
.= (IC p) + k by A2, A3, GRFUNC_1:8
.= IC (Relocated (p,k)) by A2, COMPOS_1:120
.= IC s2 by A4, A115, GRFUNC_1:8
.= IC (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ;
A117: IC (SCM R) in dom (Relocated (p,k)) by COMPOS_1:119;
ProgramPart p c= p by RELAT_1:88;
then A118: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then A119: (IC p) + k in dom (Relocated (p,k)) by A8, COMPOS_1:118;
Y: (ProgramPart s2) /. (IC (Relocated (p,k))) = s2 . (IC (Relocated (p,k))) by COMPOS_1:38;
Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
then A120: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) = s2 . (IC (Relocated (p,k))) by A4, A117, Y, GRFUNC_1:8
.= s2 . ((IC p) + k) by A2, COMPOS_1:120
.= (Relocated (p,k)) . ((IC p) + k) by A4, A119, GRFUNC_1:8 ;
p . (IC p) = s1 . (IC s1) by A3, A7, A8, A118, GRFUNC_1:8;
then A121: S₁[ 0 ] by A116, A8, A109, A120, A113, A114, COMPOS_1:122;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A121, A10);
hence for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput ((ProgramPart s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ; :: thesis: verum