let k be Element of NAT ; :: 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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (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 Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (ProgramPart (Relocated p,k))
A4: IC p = IC s by A2, A3, GRFUNC_1:8;
defpred S₁[ Element of NAT ] means Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),$1 = ((Comput (ProgramPart s),s,$1) +* (Start-At ((IC (Comput (ProgramPart s),s,$1)) + k),(SCM R))) +* (ProgramPart (Relocated p,k));
A5: 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 A6: Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (ProgramPart (Relocated p,k)) ; :: thesis: S₁[i + 1]
reconsider ii = IC (Comput (ProgramPart s),s,i) as Element of NAT ;
dom (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R)) = {(IC (SCM R))} by FUNCOP_1:19;
then A7: IC (SCM R) in dom (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R)) by TARSKI:def 1;
not IC (SCM R) in dom (ProgramPart (Relocated p,k)) by COMPOS_1:12;
then A8: IC (((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (ProgramPart (Relocated p,k))) = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) . (IC (SCM R)) by FUNCT_4:12
.= (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R)) . (IC (SCM R)) by A7, FUNCT_4:14
.= (IC (Comput (ProgramPart s),s,i)) + k by FUNCOP_1:87 ;
A9: ProgramPart p c= Comput (ProgramPart s),s,i by A3, AMI_1:99;
not p is NAT -defined by A2, COMPOS_1:19;
then A10: IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p) by A1, A3, Th27;
then A11: IC (Comput (ProgramPart s),s,i) in dom (IncAddr (ProgramPart p),k) by AMISTD_2:def 15;
A12: (ProgramPart p) /. ii = (ProgramPart p) . ii by A10, PARTFUN1:def 8
.= (Comput (ProgramPart s),s,i) . (IC (Comput (ProgramPart s),s,i)) by A10, A9, GRFUNC_1:8 ;
Y: (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) /. (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) = (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart s),s,i)) /. (IC (Comput (ProgramPart s),s,i)) = (Comput (ProgramPart s),s,i) . (IC (Comput (ProgramPart s),s,i)) by COMPOS_1:38;
ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then (IC (Comput (ProgramPart s),s,i)) + k in dom (Relocated p,k) by A10, AMISTD_2:71;
then (IC (Comput (ProgramPart s),s,i)) + k in dom (ProgramPart (Relocated p,k)) by COMPOS_1:16;
then A13: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) = (ProgramPart (Relocated p,k)) . ((IC (Comput (ProgramPart s),s,i)) + k) by A6, A8, Y, FUNCT_4:14
.= (IncAddr (Shift (ProgramPart p),k),k) . ((IC (Comput (ProgramPart s),s,i)) + k) by AMISTD_2:69
.= (Shift (IncAddr (ProgramPart p),k),k) . ((IC (Comput (ProgramPart s),s,i)) + k) by AMISTD_2:75
.= (IncAddr (ProgramPart p),k) . (IC (Comput (ProgramPart s),s,i)) by A11, VALUED_1:def 12
.= IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),k by A10, A12, Z, AMISTD_2:def 15 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i) by AMI_1:123;
A14: Comput (ProgramPart s),s,(i + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,i) by AMI_1:14;
S: ProgramPart (s +* (Relocated p,k)) = ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) by AMI_1:123;
thus Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),(i + 1) = Following (ProgramPart (s +* (Relocated p,k))),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) by AMI_1:14
.= (Exec (IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),k),((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R)))) +* (ProgramPart (Relocated p,k)) by A6, A13, S, AMISTD_2:67
.= ((Comput (ProgramPart s),s,(i + 1)) +* (Start-At ((IC (Comput (ProgramPart s),s,(i + 1))) + k),(SCM R))) +* (ProgramPart (Relocated p,k)) by A14, Th22, T ; :: thesis: verum

end;

A15: Comput (ProgramPart s),s,0 = s by AMI_1:13;
DataPart p c= p by RELAT_1:88;
then A18: DataPart p c= s by A3, XBOOLE_1:1;
Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 = s +* ((IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k)) by AMI_1:13
.= s +* ((IncrIC (NPP p),k) +* (ProgramPart (Relocated p,k))) by AMISTD_2:69
.= s +* (((DataPart p) +* (Start-At ((IC p) + k),(SCM R))) +* (ProgramPart (Relocated p,k))) by A2, COMPOS_1:75
.= s +* ((DataPart p) +* ((Start-At ((IC p) + k),(SCM R)) +* (ProgramPart (Relocated p,k)))) by FUNCT_4:15
.= (s +* (DataPart p)) +* ((Start-At ((IC p) + k),(SCM R)) +* (ProgramPart (Relocated p,k))) by FUNCT_4:15
.= ((s +* (DataPart p)) +* (Start-At ((IC p) + k),(SCM R))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= ((Comput (ProgramPart s),s,0 ) +* (Start-At ((IC (Comput (ProgramPart s),s,0 )) + k),(SCM R))) +* (ProgramPart (Relocated p,k)) by A18, A4, A15, FUNCT_4:79 ;
then A19: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A19, A5);
hence for i being Element of NAT holds Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),(SCM R))) +* (ProgramPart (Relocated p,k)) ; :: thesis: verum