let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA 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+FSA))) +* (ProgramPart (Relocated (p,k)))
let p be autonomic FinPartState of SCM+FSA; :: thesis: ( IC SCM+FSA in dom p implies for s being State of SCM+FSA 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+FSA))) +* (ProgramPart (Relocated (p,k))) )
assume A1: IC SCM+FSA in dom p ; :: thesis: for s being State of SCM+FSA 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+FSA))) +* (ProgramPart (Relocated (p,k)))
let s be State of SCM+FSA; :: 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+FSA))) +* (ProgramPart (Relocated (p,k))) )
assume A5: 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+FSA))) +* (ProgramPart (Relocated (p,k)))
defpred S₁[ 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+FSA))) +* (ProgramPart (Relocated (p,k)));
A6: 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 A7: 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+FSA))) +* (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+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;
then A8: IC SCM+FSA in dom (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM+FSA)) by TARSKI:def 1;
not IC SCM+FSA in dom (ProgramPart (Relocated (p,k))) by COMPOS_1:12;
then A9: IC (((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM+FSA))) +* (ProgramPart (Relocated (p,k)))) = ((Comput ((ProgramPart s),s,i)) +* (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM+FSA))) . (IC SCM+FSA) by FUNCT_4:12
.= (Start-At (((IC (Comput ((ProgramPart s),s,i))) + k),SCM+FSA)) . (IC SCM+FSA) by A8, FUNCT_4:14
.= (IC (Comput ((ProgramPart s),s,i))) + k by FUNCOP_1:87 ;
A10: ProgramPart p c= Comput ((ProgramPart s),s,i) by A5, AMI_1:99;
not p is NAT -defined by A1, COMPOS_1:19;
then A11: IC (Comput ((ProgramPart s),s,i)) in dom (ProgramPart p) by A5, SCMFSA_3:17;
then A12: IC (Comput ((ProgramPart s),s,i)) in dom (IncAddr ((ProgramPart p),k)) by COMPOS_1:def 40;
A13: (ProgramPart p) /. ii = (ProgramPart p) . (IC (Comput ((ProgramPart s),s,i))) by A11, PARTFUN1:def 8
.= (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by A11, A10, GRFUNC_1:8 ;
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;
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;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i)) by AMI_1:123;
TR: ProgramPart (s +* (Relocated (p,k))) = ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) by AMI_1:123;
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 A11, COMPOS_1:118;
then (IC (Comput ((ProgramPart s),s,i))) + k in dom (ProgramPart (Relocated (p,k))) by COMPOS_1:16;
then A14: 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 A7, A9, Y, TR, 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 COMPOS_1:121
.= (IncAddr ((ProgramPart p),k)) . ii by A12, VALUED_1:def 12
.= IncAddr ((CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,i)))),k) by A11, A13, Z, T, SCMFSA_4:24 ;
A15: Comput ((ProgramPart s),s,(i + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))) by EXTPRO_1:4;
A16: 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+FSA)))) = (Following ((ProgramPart s),(Comput ((ProgramPart s),s,i)))) +* (Start-At (((IC (Following ((ProgramPart s),(Comput ((ProgramPart s),s,i))))) + k),SCM+FSA)) by SCMFSA_4:28;
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+FSA))) +* (ProgramPart (Relocated (p,k))) by A7, A15, A14, A16, AMI_1:127 ; :: thesis: verum

end;

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