let k be natural number ; for R being good Ring
for p being FinPartState of (SCM R)
for s being State of (SCM R) st not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
let R be good Ring; for p being FinPartState of (SCM R)
for s being State of (SCM R) st not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
let p be FinPartState of (SCM R); for s being State of (SCM R) st not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
let s be State of (SCM R); ( not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic implies for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) )
assume that
A1:
not R is trivial
and
A2:
IC (SCM R) in dom p
and
A3:
p c= s
and
A4:
Relocated p,k is autonomic
; for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
A5:
IC (SCM R) in dom (Relocated p,k)
by AMISTD_2:72;
defpred S1[ Element of NAT ] means Comput (ProgramPart s),s,$1 = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),$1) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),$1)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p);
A6:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp =
ProgramPart p as
NAT -defined FinPartState of ;
set sdom =
s | (dom (ProgramPart (Relocated p,k)));
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A7:
S1[
i]
;
S1[i + 1]
reconsider ii =
IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) as
Element of
NAT ;
A8:
ProgramPart (Relocated p,k) c= Comput (ProgramPart (s +* (Relocated p,k))),
(s +* (Relocated p,k)),
i
by AMI_1:99, FUNCT_4:26;
dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R)) = {(IC (SCM R))}
by FUNCOP_1:19;
then A9:
IC (SCM R) in dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))
by TARSKI:def 1;
dom (ProgramPart (Relocated p,k)) c= the
carrier of
(SCM R)
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated p,k)) c= dom s
by PARTFUN1:def 4;
then A10:
dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k))))
by RELAT_1:91;
reconsider sdom =
s | (dom (ProgramPart (Relocated p,k))) as
FinPartState of
(SCM R) ;
dom (s | (dom (ProgramPart (Relocated p,k)))) c= NAT
by A10, RELAT_1:87;
then reconsider sdom =
sdom as
NAT -defined FinPartState of
by RELAT_1:def 18;
consider jk being
natural number such that A11:
IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) = il. (SCM R),
jk
by AMISTD_1:26;
IC (SCM R) in dom (Relocated p,k)
by AMISTD_2:72;
then
not
Relocated p,
k is
NAT -defined
by AMI_1:109;
then A12:
IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) in dom (ProgramPart (Relocated p,k))
by A1, A4, Th27, FUNCT_4:26;
then A13:
il. (SCM R),
jk in { (il. (SCM R),(j + k)) where j is Element of NAT : il. (SCM R),j in dom (ProgramPart p) }
by A11, AMISTD_2:70;
(
dom sdom = (dom s) /\ (dom (ProgramPart (Relocated p,k))) & not
IC (SCM R) in dom (ProgramPart (Relocated p,k)) )
by AMI_1:101, RELAT_1:90;
then A14:
not
IC (SCM R) in dom sdom
by XBOOLE_0:def 4;
consider j being
Element of
NAT such that A15:
il. (SCM R),
jk = il. (SCM R),
(j + k)
and A16:
il. (SCM R),
j in dom (ProgramPart p)
by A13;
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;
dom (Shift pp,k) = { (il. (SCM R),(m + k)) where m is Element of NAT : il. (SCM R),m in dom pp }
by AMISTD_2:def 16;
then A17:
il. (SCM R),
(j + k) in dom (Shift (ProgramPart p),k)
by A16;
then A18:
IncAddr (pi (Shift (ProgramPart p),k),ii),
k =
(IncAddr (Shift (ProgramPart p),k),k) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))
by A11, A15, AMISTD_2:74
.=
(ProgramPart (Relocated p,k)) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))
by AMISTD_2:69
.=
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),
(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)
by A12, A8, GRFUNC_1:8, Y
;
A19:
((il. (SCM R),(j + k)) -' k,(SCM R)) + k,
(SCM R) =
(((il. (SCM R),j) + k,(SCM R)) -' k,(SCM R)) + k,
(SCM R)
by AMISTD_1:def 13
.=
(il. (SCM R),j) + k,
(SCM R)
by AMISTD_1:61
.=
il. (SCM R),
(j + k)
by AMISTD_1:def 13
;
Y:
(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;
A20:
(il. (SCM R),(j + k)) -' k,
(SCM R) =
((il. (SCM R),j) + k,(SCM R)) -' k,
(SCM R)
by AMISTD_1:def 13
.=
il. (SCM R),
j
by AMISTD_1:61
;
T:
ProgramPart (s +* (Relocated p,k)) = ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)
by AMI_1:144;
S:
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,i)
by AMI_1:144;
not
IC (SCM R) in dom (ProgramPart p)
by AMI_1:101;
then IC ((((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* sdom) +* (ProgramPart p)) =
(((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* sdom) . (IC (SCM R))
by FUNCT_4:12
.=
((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) . (IC (SCM R))
by A14, FUNCT_4:12
.=
(Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R)) . (IC (SCM R))
by A9, FUNCT_4:14
.=
(IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,
(SCM R)
by FUNCOP_1:87
;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),
(Comput (ProgramPart s),s,i) =
(ProgramPart p) . ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R))
by A7, A11, A15, A16, A20, FUNCT_4:14, Y
.=
(Shift (ProgramPart p),k) . (IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))
by A11, A15, A16, A19, A20, AMISTD_2:65
.=
pi (Shift (ProgramPart p),k),
ii
by A11, A15, A17, AMI_1:def 47
;
then A21:
(
Comput (ProgramPart (s +* (Relocated p,k))),
(s +* (Relocated p,k)),
(i + 1) = Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),
(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) &
Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),
((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) = (Following (ProgramPart (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (ProgramPart (s +* (Relocated p,k))),(Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i))) -' k,(SCM R)),(SCM R)) )
by A11, A15, A18, Th23, AMI_1:14, T;
thus Comput (ProgramPart s),
s,
(i + 1) =
Following (ProgramPart s),
(Comput (ProgramPart s),s,i)
by AMI_1:14
.=
(Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i)),(((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* sdom)) +* (ProgramPart p)
by A7, AMISTD_2:67, S
.=
(((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),(i + 1)) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),(i + 1))) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A21, AMISTD_2:67, T
;
verum
end;
set PR = ProgramPart (Relocated p,k);
set IP = Start-At ((IC p) + k,(SCM R)),(SCM R);
set IS = Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R);
set SD = s | (dom (ProgramPart (Relocated p,k)));
A22:
dom (Start-At ((IC p) + k,(SCM R)),(SCM R)) = {(IC (SCM R))}
by FUNCOP_1:19;
A23: IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 ) =
(s +* (Relocated p,k)) . (IC (SCM R))
by AMI_1:13
.=
(Relocated p,k) . (IC (SCM R))
by A5, FUNCT_4:14
.=
IC (Relocated p,k)
;
set PP = ProgramPart p;
ProgramPart p c= p
by RELAT_1:88;
then A24:
ProgramPart p c= s
by A3, XBOOLE_1:1;
Start-At (IC p),(SCM R) c= p
by A2, AMI_1:110;
then A25:
Start-At (IC p),(SCM R) c= s
by A3, XBOOLE_1:1;
set DP = DataPart p;
DataPart p c= p
by RELAT_1:88;
then A26:
DataPart p c= s
by A3, XBOOLE_1:1;
A27:
{(IC (SCM R))} misses dom (DataPart p)
by AMI_1:102;
A28:
{(IC (SCM R))} misses dom (ProgramPart (Relocated p,k))
by AMI_1:103;
(dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) /\ (dom (s | (dom (ProgramPart (Relocated p,k))))) =
(dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) /\ ((dom s) /\ (dom (ProgramPart (Relocated p,k))))
by RELAT_1:90
.=
{(IC (SCM R))} /\ ((dom s) /\ (dom (ProgramPart (Relocated p,k))))
by FUNCOP_1:19
.=
({(IC (SCM R))} /\ (dom (ProgramPart (Relocated p,k)))) /\ (dom s)
by XBOOLE_1:16
.=
{} /\ (dom s)
by A28, XBOOLE_0:def 7
.=
{}
;
then A29:
dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R)) misses dom (s | (dom (ProgramPart (Relocated p,k))))
by XBOOLE_0:def 7;
dom (ProgramPart (Relocated p,k)) c= the carrier of (SCM R)
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated p,k)) c= dom s
by PARTFUN1:def 4;
then A30:
dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k))))
by RELAT_1:91;
dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R)) = {(IC (SCM R))}
by FUNCOP_1:19;
then A31:
dom (Start-At ((IC p) + k,(SCM R)),(SCM R)) = dom (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))
by FUNCOP_1:19;
A32:
dom (DataPart p) misses dom (ProgramPart (Relocated p,k))
by AMI_1:104;
Comput (ProgramPart s),s,0 =
s
by AMI_1:13
.=
s +* (ProgramPart p)
by A24, FUNCT_4:79
.=
(s +* (Start-At (IC p),(SCM R))) +* (ProgramPart p)
by A25, FUNCT_4:79
.=
(s +* (Start-At (((IC p) + k,(SCM R)) -' k,(SCM R)),(SCM R))) +* (ProgramPart p)
by AMISTD_1:61
.=
(s +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (ProgramPart p)
by A23, AMISTD_2:73
.=
((s +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (ProgramPart p)
by FUNCT_4:80
.=
(((s +* (ProgramPart (Relocated p,k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (ProgramPart p)
by A30, FUNCT_4:78
.=
((s +* (ProgramPart (Relocated p,k))) +* ((s | (dom (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R)))) +* (ProgramPart p)
by FUNCT_4:15
.=
((s +* (ProgramPart (Relocated p,k))) +* ((Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R)) +* (s | (dom (ProgramPart (Relocated p,k)))))) +* (ProgramPart p)
by A29, FUNCT_4:36
.=
(((s +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A26, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* (DataPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A32, FUNCT_4:36
.=
((((s +* (ProgramPart (Relocated p,k))) +* (DataPart p)) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((((s +* (ProgramPart (Relocated p,k))) +* (DataPart p)) +* (Start-At ((IC p) + k,(SCM R)),(SCM R))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A31, FUNCT_4:78
.=
((((s +* ((ProgramPart (Relocated p,k)) +* (DataPart p))) +* (Start-At ((IC p) + k,(SCM R)),(SCM R))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (((ProgramPart (Relocated p,k)) +* (DataPart p)) +* (Start-At ((IC p) + k,(SCM R)),(SCM R)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* ((DataPart p) +* (Start-At ((IC p) + k,(SCM R)),(SCM R))))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* ((Start-At ((IC p) + k,(SCM R)),(SCM R)) +* (DataPart p)))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A22, A27, FUNCT_4:36
.=
(((s +* (((ProgramPart (Relocated p,k)) +* (Start-At ((IC p) + k,(SCM R)),(SCM R))) +* (DataPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (((Start-At ((IC p) + k,(SCM R)),(SCM R)) +* (ProgramPart (Relocated p,k))) +* (DataPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A22, AMI_1:103, FUNCT_4:36
.=
(((s +* (Relocated p,k)) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by AMISTD_2:69
.=
(((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 ) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),0 )) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by AMI_1:13
;
then A33:
S1[ 0 ]
;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A33, A6);
hence
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
; verum