let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st 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))) +* (ProgramPart (Relocated (p,k)))
let p be autonomic FinPartState of SCM; :: thesis: ( IC SCM in dom p implies for s being State of SCM st 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))) +* (ProgramPart (Relocated (p,k))) )
assume A1: IC SCM in dom p ; :: thesis: for s being State of SCM st 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))) +* (ProgramPart (Relocated (p,k)))
let s be State of SCM; :: thesis: ( 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))) +* (ProgramPart (Relocated (p,k))) )
assume A4: 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))) +* (ProgramPart (Relocated (p,k)))
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))) +* (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))) +* (ProgramPart (Relocated (p,k))) ; :: thesis: S₁[i + 1]
reconsider kk = IC (Comput ((ProgramPart s),s,i)) as Element of NAT ;
dom (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM)) = {(IC SCM)} by FUNCOP_1:19;
then A7: IC SCM in dom (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM)) by TARSKI:def 1;
not IC SCM 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))) +* (ProgramPart (Relocated (p,k)))) = ((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM))) . (IC SCM) by FUNCT_4:12
.= (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM)) . (IC SCM) 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 A4, AMI_1:99;
not p is NAT -defined by A1, COMPOS_1:19;
then A10: IC (Comput ((ProgramPart s),s,i)) in dom (ProgramPart p) by A4, AMI_5:86;
then A11: IC (Comput ((ProgramPart s),s,i)) in dom (IncAddr ((ProgramPart p),k)) by COMPOS_1:def 40;
S: ProgramPart (s +* (Relocated (p,k))) = ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) by AMI_1:123;
Y: (ProgramPart (s +* (Relocated (p,k)))) /. (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 S, COMPOS_1:38;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i)) by AMI_1:123;
Z: (ProgramPart s) /. (IC (Comput ((ProgramPart s),s,i))) = (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by T, COMPOS_1:38;
A12: (ProgramPart p) /. kk = (ProgramPart p) . (IC (Comput ((ProgramPart s),s,i))) by A10, PARTFUN1:def 8
.= (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by A10, A9, GRFUNC_1:8 ;
reconsider kk = IC (Comput ((ProgramPart s),s,i)) as Element of NAT ;
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 (s +* (Relocated (p,k)))),(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
.= (Reloc ((ProgramPart p),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 Th19
.= (IncAddr ((ProgramPart p),k)) . kk by A11, VALUED_1:def 12
.= IncAddr ((CurInstr ((ProgramPart s),(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))) & Exec ((IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,i)))),k)),((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM)))) = (Following ((ProgramPart s),(Comput ((ProgramPart s),s,i)))) +* (Start-At (((IC (Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))))) + k),SCM)) ) by Th31, T, EXTPRO_1:4;
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
.= ((Comput ((ProgramPart s),s,(i + 1))) +* (Start-At (((IC (Comput ((ProgramPart s),s,(i + 1)))) + k),SCM))) +* (ProgramPart (Relocated (p,k))) by A6, A13, A14, AMI_1:127
.= ((Comput ((ProgramPart s),s,(i + 1))) +* (Start-At (((IC (Comput ((ProgramPart s),s,(i + 1)))) + k),SCM))) +* (ProgramPart (Relocated (p,k))) ; :: thesis: verum

end;

A15: Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3;
A16: IC p = p . (IC SCM)
.= IC s by A1, A4, GRFUNC_1:8 ;
DataPart p c= p by RELAT_1:88;
then A17: DataPart p c= s by A4, 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))) +* (ProgramPart (Relocated (p,k)))) by A1, COMPOS_1:75
.= s +* ((DataPart p) +* ((Start-At (((IC p) + k),SCM)) +* (ProgramPart (Relocated (p,k))))) by FUNCT_4:15
.= (s +* (DataPart p)) +* ((Start-At (((IC p) + k),SCM)) +* (ProgramPart (Relocated (p,k)))) by FUNCT_4:15
.= (s +* (DataPart p)) +* ((Start-At (((IC p) + k),SCM)) +* (ProgramPart (Relocated (p,k))))
.= ((s +* (DataPart p)) +* (Start-At (((IC p) + k),SCM))) +* (ProgramPart (Relocated (p,k))) by FUNCT_4:15
.= ((Comput ((ProgramPart s),s,0)) +* (Start-At (((IC (Comput ((ProgramPart s),s,0))) + k),SCM))) +* (ProgramPart (Relocated (p,k))) by A16, A17, A15, FUNCT_4:79 ;
then A18: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A18, A5); :: thesis: verum