let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of st IC SCM in dom p holds
for s being State of st Relocated p,k c= s holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
let p be autonomic FinPartState of ; :: thesis: ( IC SCM in dom p implies for s being State of st Relocated p,k c= s holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) )
assume A1: IC SCM in dom p ; :: thesis: for s being State of st Relocated p,k c= s holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
let s be State of ; :: thesis: ( Relocated p,k c= s implies for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) )
assume A2: Relocated p,k c= s ; :: thesis: for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
defpred S₁[ Element of NAT ] means Computation s,$1 = (((Computation (s +* p),$1) +* (Start-At ((IC (Computation (s +* p),$1)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k));
A3: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

set sdom = s | (dom (ProgramPart p));
dom [(ProgramPart p)] c= the carrier of SCM by AMI_1:80;
then dom (ProgramPart p) c= dom s by AMI_1:79;
then A4: dom (ProgramPart p) = dom (s | (dom (ProgramPart p))) by RELAT_1:91;
then ( rng (s | (dom (ProgramPart p))) c= the Instructions of SCM & dom (s | (dom (ProgramPart p))) c= NAT ) by AMI_1:140, RELAT_1:87;
then reconsider sdom = s | (dom (ProgramPart p)) as NAT -defined the Instructions of SCM -valued finite Function by A4, FINSET_1:29, RELSET_1:11;
let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) ; :: thesis: S₁[i + 1]
reconsider kk = IC (Computation (s +* p),i) as Element of NAT by ORDINAL1:def 13;
A6: ProgramPart p c= Computation (s +* p),i by AMI_1:99, FUNCT_4:26;
dom (Start-At ((IC (Computation (s +* p),i)) + k)) = {(IC SCM )} by FUNCOP_1:19;
then A7: IC SCM in dom (Start-At ((IC (Computation (s +* p),i)) + k)) by TARSKI:def 1;
( dom sdom = (dom s) /\ (dom (ProgramPart p)) & not IC SCM in dom (ProgramPart p) ) by AMI_1:101, RELAT_1:90;
then A8: not IC SCM in dom sdom by XBOOLE_0:def 4;
not p is NAT -defined by A1, AMI_1:109;
then A9: IC (Computation (s +* p),i) in dom (ProgramPart p) by AMI_5:86, FUNCT_4:26;
then A10: IC (Computation (s +* p),i) in dom (IncAddr (ProgramPart p),k) by Def5;
ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then (IC (Computation (s +* p),i)) + k in dom (Relocated p,k) by A9, Th24;
then A11: (IC (Computation (s +* p),i)) + k in dom (ProgramPart (Relocated p,k)) by AMI_1:106;
A12: (ProgramPart p) /. kk = (ProgramPart p) . kk by A9, PARTFUN1:def 8
.= (Computation (s +* p),i) . (IC (Computation (s +* p),i)) by A9, A6, GRFUNC_1:8 ;
reconsider kk = IC (Computation (s +* p),i) as Element of NAT by ORDINAL1:def 13;
not IC SCM in dom (ProgramPart (Relocated p,k)) by AMI_1:101;
then IC ((((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* [sdom]) +* [(ProgramPart (Relocated p,k))]) = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* sdom) . (IC SCM ) by FUNCT_4:12
.= ((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) . (IC SCM ) by A8, FUNCT_4:12
.= (Start-At ((IC (Computation (s +* p),i)) + k)) . (IC SCM ) by A7, FUNCT_4:14
.= (IC (Computation (s +* p),i)) + k by FUNCOP_1:87 ;
then A13: CurInstr (Computation s,i) = (ProgramPart (Relocated p,k)) . ((IC (Computation (s +* p),i)) + k) by A5, A11, FUNCT_4:14
.= (IncAddr (Shift (ProgramPart p),k),k) . ((IC (Computation (s +* p),i)) + k) by Th22
.= (Shift (IncAddr (ProgramPart p),k),k) . ((IC (Computation (s +* p),i)) + k) by Th19
.= (IncAddr (ProgramPart p),k) . kk by A10, VALUED_1:def 12
.= IncAddr (CurInstr (Computation (s +* p),i)),k by A9, A12, Def5 ;
A14: Computation (s +* p),(i + 1) = Following (Computation (s +* p),i) by AMI_1:14;
thus Computation s,(i + 1) = Following (Computation s,i) by AMI_1:14
.= (Exec (IncAddr (CurInstr (Computation (s +* p),i)),k),(((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* [sdom])) +* [(ProgramPart (Relocated p,k))] by A5, A13, AMI_5:77
.= ((Exec (IncAddr (CurInstr (Computation (s +* p),i)),k),((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k)))) +* sdom) +* (ProgramPart (Relocated p,k)) by AMI_5:77
.= (((Computation (s +* p),(i + 1)) +* (Start-At ((IC (Computation (s +* p),(i + 1))) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A14, Th31 ; :: thesis: verum

end;

set IP = Start-At (IC p);
A15: dom (Start-At (IC p)) = {(IC SCM )} by FUNCOP_1:19;
A16: Start-At ((IC p) + k) c= Relocated p,k by Th28;
IC (Computation (s +* p),0 ) = (s +* p) . (IC SCM ) by AMI_1:13
.= p . (IC SCM ) by A1, FUNCT_4:14
.= IC p by A1, AMI_1:def 43 ;
then A17: Start-At ((IC (Computation (s +* p),0 )) + k) c= s by A2, A16, XBOOLE_1:1;
set DP = DataPart p;
A18: {(IC SCM )} misses dom (DataPart p) by AMI_1:102;
set PP = ProgramPart p;
A19: dom (DataPart p) misses dom (ProgramPart p) by AMI_1:104;
set SD = s | (dom (ProgramPart p));
A20: s | (dom (ProgramPart p)) c= s by RELAT_1:88;
ProgramPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
then A21: ProgramPart (Relocated p,k) c= s by A2, XBOOLE_1:1;
dom [(ProgramPart p)] c= the carrier of SCM by AMI_1:80;
then dom (ProgramPart p) c= dom s by AMI_1:79;
then A22: dom (ProgramPart p) = dom (s | (dom (ProgramPart p))) by RELAT_1:91;
DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
then DataPart (Relocated p,k) c= s by A2, XBOOLE_1:1;
then A23: DataPart p c= s by Th21;
set PR = ProgramPart (Relocated p,k);
set IS = Start-At ((IC (Computation (s +* p),0 )) + k);
A24: dom (Start-At ((IC (Computation (s +* p),0 )) + k)) = {(IC SCM )} by FUNCOP_1:19;
Computation s,0 = s by AMI_1:13
.= s +* (ProgramPart (Relocated p,k)) by A21, FUNCT_4:79
.= (s +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A20, FUNCT_4:79
.= ((s +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A22, FUNCT_4:78
.= (((s +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A17, FUNCT_4:79
.= ((s +* ((Start-At ((IC (Computation (s +* p),0 )) + k)) +* (ProgramPart p))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= ((s +* ((ProgramPart p) +* (Start-At ((IC (Computation (s +* p),0 )) + k)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A24, AMI_1:103, FUNCT_4:36
.= (((s +* (ProgramPart p)) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= ((((s +* (DataPart p)) +* (ProgramPart p)) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A23, FUNCT_4:79
.= (((s +* ((DataPart p) +* (ProgramPart p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A19, FUNCT_4:36
.= ((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At (IC p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A24, A15, FUNCT_4:78
.= ((((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At (IC p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((s +* (((ProgramPart p) +* (DataPart p)) +* (Start-At (IC p)))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((s +* ((ProgramPart p) +* ((DataPart p) +* (Start-At (IC p))))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((s +* ((ProgramPart p) +* ((Start-At (IC p)) +* (DataPart p)))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A15, A18, FUNCT_4:36
.= (((s +* (((ProgramPart p) +* (Start-At (IC p))) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by FUNCT_4:15
.= (((s +* (((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A15, AMI_1:103, FUNCT_4:36
.= (((s +* p) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by A1, AMI_1:108
.= (((Computation (s +* p),0 ) +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) by AMI_1:13 ;
then A25: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A25, A3); :: thesis: verum