let k be natural number ; :: thesis: for R being good Ring
for 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= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))
let R be good Ring; :: thesis: for 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= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))
let 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= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k)) )
assume A1: not R is trivial ; :: thesis: for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & p c= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))
let p be autonomic FinPartState of (SCM R); :: thesis: ( IC (SCM R) in dom p & p c= s implies for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k)) )
assume that
A2: IC (SCM R) in dom p and
A3: p c= s ; :: thesis: for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))
A4: (dom (DataPart p)) /\ {(IC (SCM R))} = {} by Lm1, AMI_1:100;
A5: dom (DataPart p) misses dom ((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k)))

proof

NAT misses dom (DataPart p) by Th26, AMI_2:29, XBOOLE_1:63;
then dom (DataPart p) misses dom (ProgramPart (Relocated p,k)) by RELAT_1:87, XBOOLE_1:63;
then (dom (DataPart p)) /\ (dom (ProgramPart (Relocated p,k))) = {} by XBOOLE_0:def 7;
then ((dom (DataPart p)) /\ (dom (Start-At ((IC p) + k)))) \/ ((dom (DataPart p)) /\ (dom (ProgramPart (Relocated p,k)))) = {} by A4, FUNCOP_1:19;
then (dom (DataPart p)) /\ ((dom (Start-At ((IC p) + k))) \/ (dom (ProgramPart (Relocated p,k)))) = {} by XBOOLE_1:23;
hence (dom (DataPart p)) /\ (dom ((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k)))) = {} by FUNCT_4:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

A6: IC p = p . (IC (SCM R)) by A2, AMI_1:def 43
.= IC s by A2, A3, GRFUNC_1:8 ;
DataPart p c= p by RELAT_1:88;
then A7: DataPart p c= s by A3, XBOOLE_1:1;
A8: Computation s,0 = s by AMI_1:13;
defpred S₁[ Element of NAT ] means Computation (s +* (Relocated p,k)),$1 = ((Computation s,$1) +* (Start-At ((IC (Computation s,$1)) + k))) +* (ProgramPart (Relocated p,k));
Computation (s +* (Relocated p,k)),0 = s +* (((Start-At ((IC p) + k)) +* (IncAddr (Shift [(ProgramPart p)],k),k)) +* (DataPart p)) by AMI_1:13
.= s +* (((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k))) +* (DataPart p)) by AMISTD_2:69
.= s +* ((DataPart p) +* ((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k)))) by A5, FUNCT_4:36
.= (s +* (DataPart p)) +* ((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k))) by FUNCT_4:15
.= ((s +* (DataPart p)) +* (Start-At ((IC p) + k))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= ((Computation s,0 ) +* (Start-At ((IC (Computation s,0 )) + k))) +* (ProgramPart (Relocated p,k)) by A6, A7, A8, FUNCT_4:79 ;
then A9: S₁[ 0 ] ;
A10: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A11: Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k)) ; :: thesis: S₁[i + 1]
A12: Computation s,(i + 1) = Following (Computation s,i) by AMI_1:14;
dom (Start-At ((IC (Computation s,i)) + k)) = {(IC (SCM R))} by FUNCOP_1:19;
then A13: IC (SCM R) in dom (Start-At ((IC (Computation s,i)) + k)) by TARSKI:def 1;
not IC (SCM R) in dom (ProgramPart (Relocated p,k)) by AMI_1:101;
then A14: IC (((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* [(ProgramPart (Relocated p,k))]) = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) . (IC (SCM R)) by FUNCT_4:12
.= (Start-At ((IC (Computation s,i)) + k)) . (IC (SCM R)) by A13, FUNCT_4:14
.= (IC (Computation s,i)) + k by FUNCOP_1:87 ;
not p is NAT -defined by A2, AMI_1:109;
then A15: IC (Computation s,i) in dom (ProgramPart p) by A1, A3, Th40;
then A16: IC (Computation s,i) in dom (IncAddr [(ProgramPart p)],k) by AMISTD_2:def 15;
A17: [(ProgramPart p)] c= Computation s,i by A3, AMI_1:99;
reconsider ii = IC (Computation s,i) as Element of NAT by ORDINAL1:def 13;
A18: pi [(ProgramPart p)],ii = [(ProgramPart p)] . ii by A15, AMI_1:def 47
.= (Computation s,i) . (IC (Computation s,i)) by A15, A17, GRFUNC_1:8 ;
ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then (IC (Computation s,i)) + k in dom (Relocated p,k) by A15, AMISTD_2:71;
then (IC (Computation s,i)) + k in dom (ProgramPart (Relocated p,k)) by AMI_1:106;
then A19: CurInstr (Computation (s +* (Relocated p,k)),i) = (ProgramPart (Relocated p,k)) . ((IC (Computation s,i)) + k) by A11, A14, FUNCT_4:14
.= (IncAddr (Shift [(ProgramPart p)],k),k) . ((IC (Computation s,i)) + k) by AMISTD_2:69
.= (Shift (IncAddr [(ProgramPart p)],k),k) . ((IC (Computation s,i)) + k) by AMISTD_2:75
.= (IncAddr [(ProgramPart p)],k) . (IC (Computation s,i)) by A16, AMISTD_2:65
.= IncAddr (CurInstr (Computation s,i)),k by A15, A18, AMISTD_2:74 ;
thus Computation (s +* (Relocated p,k)),(i + 1) = Following (Computation (s +* (Relocated p,k)),i) by AMI_1:14
.= (Exec (IncAddr (CurInstr (Computation s,i)),k),((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k)))) +* [(ProgramPart (Relocated p,k))] by A11, A19, AMISTD_2:67
.= ((Computation s,(i + 1)) +* (Start-At ((IC (Computation s,(i + 1))) + k))) +* (ProgramPart (Relocated p,k)) by A12, Th35 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A9, A10);
hence for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k)) ; :: thesis: verum