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 COMPOS_1:def 40;
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, COMPOS_1:118;
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 COMPOS_1:116
.= (Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput ((ProgramPart s),s,i))) + k) by COMPOS_1:121
.= (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, COMPOS_1:def 40 ;
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 EXTPRO_1:4;
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 EXTPRO_1:4
.= (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, AMI_1:127
.= ((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 EXTPRO_1:3;
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 EXTPRO_1:3
.= s +* ((IncrIC ((NPP p),k)) +* (ProgramPart (Relocated (p,k)))) by COMPOS_1:116
.= 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