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))
A2: dom (ProgramPart (Relocated p,k)) c= NAT by RELAT_1:def 18;
NAT misses dom (DataPart p) by Lm1, RELAT_1:87, SCMFSA_2:127, XBOOLE_1:63;
then dom (DataPart p) misses dom (ProgramPart (Relocated p,k)) by A2, XBOOLE_1:63;
then A3: (dom (DataPart p)) /\ (dom (ProgramPart (Relocated p,k))) = {} by XBOOLE_0:def 7;
dom (DataPart p) misses {(IC SCM+FSA )} by AMI_1:100, ZFMISC_1:56;
then dom (DataPart p) misses dom (Start-At ((IC p) + k),SCM+FSA ) by FUNCOP_1:19;
then ((dom (DataPart p)) /\ (dom (Start-At ((IC p) + k),SCM+FSA ))) \/ ((dom (DataPart p)) /\ (dom (ProgramPart (Relocated p,k)))) = {} by A3, XBOOLE_0:def 7;
then (dom (DataPart p)) /\ ((dom (Start-At ((IC p) + k),SCM+FSA )) \/ (dom (ProgramPart (Relocated p,k)))) = {} by XBOOLE_1:23;
then dom (DataPart p) misses (dom (Start-At ((IC p) + k),SCM+FSA )) \/ (dom (ProgramPart (Relocated p,k))) by XBOOLE_0:def 7;
then dom (DataPart p) misses dom ((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))) by FUNCT_4:def 1;
then A4: ((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))) +* (DataPart p) = (DataPart p) +* ((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))) by FUNCT_4:36;
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 AMI_1:101;
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, AMI_1:109;
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 SCMFSA_4:def 6;
A13: pi (ProgramPart p),ii = (ProgramPart p) . (IC (Comput (ProgramPart s),s,i)) by A11, AMI_1:def 47
.= (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 AMI_1:150;
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 AMI_1:150;
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, Th4;
then (IC (Comput (ProgramPart s),s,i)) + k in dom (ProgramPart (Relocated p,k)) by AMI_1:106;
then A14: 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 A7, A9, FUNCT_4:14, Y
.= (IncAddr (Shift (ProgramPart p),k),k) . ((IC (Comput (ProgramPart s),s,i)) + k) by Th2
.= (Shift (IncAddr (ProgramPart p),k),k) . ((IC (Comput (ProgramPart s),s,i)) + k) by SCMFSA_4:35
.= (IncAddr (ProgramPart p),k) . ii by A12, VALUED_1:def 12
.= IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),k by A11, A13, SCMFSA_4:24, Z ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i) by AMI_1:144;
A15: Comput (ProgramPart s),s,(i + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,i) by AMI_1:14;
A16: 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+FSA )) = (Following (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i))) + k),SCM+FSA ) by SCMFSA_4:28;
S: ProgramPart (s +* (Relocated p,k)) = ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) by AMI_1:144;
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
.= ((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, SCMFSA_3:10, T, S ; :: thesis: verum

end;

A17: Comput (ProgramPart s),s,0 = s by AMI_1:13;
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 +* (((Start-At ((IC p) + k),SCM+FSA ) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p)) by AMI_1:13
.= s +* (((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))) +* (DataPart p)) by Th2
.= (s +* (DataPart p)) +* ((Start-At ((IC p) + k),SCM+FSA ) +* (ProgramPart (Relocated p,k))) by A4, 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