let k be natural number ; :: thesis: for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & 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 R be good Ring; :: thesis: for s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & 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 (SCM R); :: thesis: ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & 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:
not R is trivial
; :: thesis: for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & 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 (SCM R); :: thesis: ( IC (SCM R) in dom p & 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 that
A2:
IC (SCM R) in dom p
and
A3:
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))
A4:
dom (Start-At ((IC (Computation (s +* p),0 )) + k)) = {(IC (SCM R))}
by FUNCOP_1:19;
A5:
dom (Start-At (IC p)) = {(IC (SCM R))}
by FUNCOP_1:19;
ProgramPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
then A6:
ProgramPart (Relocated p,k) c= s
by A3, XBOOLE_1:1;
A7:
s | (dom (ProgramPart p)) c= s
by RELAT_1:88;
dom [(ProgramPart p)] c= the carrier of (SCM R)
by AMI_1:80;
then
dom (ProgramPart p) c= dom s
by AMI_1:79;
then A8:
dom (ProgramPart p) = dom (s | (dom (ProgramPart p)))
by RELAT_1:91;
A9: IC (Computation (s +* p),0 ) =
(s +* p) . (IC (SCM R))
by AMI_1:13
.=
p . (IC (SCM R))
by A2, FUNCT_4:14
.=
IC p
by A2, AMI_1:def 43
;
Start-At ((IC p) + k) c= Relocated p,k
by AMISTD_2:77;
then A10:
Start-At ((IC (Computation (s +* p),0 )) + k) c= s
by A3, A9, XBOOLE_1:1;
DataPart (Relocated p,k) c= Relocated p,k
by RELAT_1:88;
then
DataPart (Relocated p,k) c= s
by A3, XBOOLE_1:1;
then A11:
DataPart p c= s
by AMISTD_2:68;
A12:
dom (DataPart p) misses dom (ProgramPart p)
by AMI_1:104;
A13:
dom (Start-At (IC p)) = dom (Start-At ((IC (Computation (s +* p),0 )) + k))
by A4, FUNCOP_1:19;
A14:
{(IC (SCM R))} misses dom (DataPart p)
by AMI_1:102;
set IS = Start-At ((IC (Computation (s +* p),0 )) + k);
set IP = Start-At (IC p);
set SD = s | (dom (ProgramPart p));
set PP = ProgramPart p;
set DP = DataPart p;
set PR = ProgramPart (Relocated p,k);
defpred S1[ 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));
Computation s,0 =
s
by AMI_1:13
.=
s +* (ProgramPart (Relocated p,k))
by A6, FUNCT_4:79
.=
(s +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A7, FUNCT_4:79
.=
((s +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A8, FUNCT_4:78
.=
(((s +* (Start-At ((IC (Computation (s +* p),0 )) + k))) +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A10, 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 A4, 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 A11, 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 A12, 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 A13, 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 A5, A14, 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 A5, 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 A2, 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 A15:
S1[ 0 ]
;
A16:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S1[i] implies S1[i + 1] )
assume A17:
Computation s,
i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
;
:: thesis: S1[i + 1]
reconsider sdom =
s | (dom (ProgramPart p)) as
Element of
sproduct the
Object-Kind of
(SCM R) ;
dom [(ProgramPart p)] c= the
carrier of
(SCM R)
by AMI_1:80;
then
dom (ProgramPart p) c= dom s
by AMI_1:79;
then A18:
dom (ProgramPart p) = dom (s | (dom (ProgramPart p)))
by RELAT_1:91;
then reconsider sdom =
sdom as
FinPartState of
(SCM R) by FINSET_1:29;
dom (s | (dom (ProgramPart p))) c= NAT
by A18, RELAT_1:87;
then reconsider sdom =
sdom as
NAT -defined FinPartState of
(SCM R) by RELAT_1:def 18;
A19:
Computation (s +* p),
(i + 1) = Following (Computation (s +* p),i)
by AMI_1:14;
dom (Start-At ((IC (Computation (s +* p),i)) + k)) = {(IC (SCM R))}
by FUNCOP_1:19;
then A20:
IC (SCM R) in dom (Start-At ((IC (Computation (s +* p),i)) + k))
by TARSKI:def 1;
A21:
not
IC (SCM R) in dom (ProgramPart (Relocated p,k))
by AMI_1:101;
A22:
dom sdom = (dom s) /\ (dom (ProgramPart p))
by RELAT_1:90;
not
IC (SCM R) in dom (ProgramPart p)
by AMI_1:101;
then A23:
not
IC (SCM R) in dom sdom
by A22, XBOOLE_0:def 4;
A24:
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 R))
by A21, FUNCT_4:12
.=
((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) . (IC (SCM R))
by A23, FUNCT_4:12
.=
(Start-At ((IC (Computation (s +* p),i)) + k)) . (IC (SCM R))
by A20, FUNCT_4:14
.=
(IC (Computation (s +* p),i)) + k
by FUNCOP_1:87
;
not
p is
NAT -defined
by A2, AMI_1:109;
then A25:
IC (Computation (s +* p),i) in dom [(ProgramPart p)]
by A1, Th40, FUNCT_4:26;
then A26:
IC (Computation (s +* p),i) in dom (IncAddr [(ProgramPart p)],k)
by AMISTD_2:def 15;
A27:
[(ProgramPart p)] c= Computation (s +* p),
i
by AMI_1:99, FUNCT_4:26;
reconsider ii =
IC (Computation (s +* p),i) as
Element of
NAT by ORDINAL1:def 13;
A28:
pi [(ProgramPart p)],
ii =
[(ProgramPart p)] . (IC (Computation (s +* p),i))
by A25, AMI_1:def 47
.=
(Computation (s +* p),i) . (IC (Computation (s +* p),i))
by A25, A27, GRFUNC_1:8
;
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 A25, AMISTD_2:71;
then
(IC (Computation (s +* p),i)) + k in dom (ProgramPart (Relocated p,k))
by AMI_1:106;
then A29:
CurInstr (Computation s,i) =
(ProgramPart (Relocated p,k)) . ((IC (Computation (s +* p),i)) + k)
by A17, A24, FUNCT_4:14
.=
(IncAddr (Shift [(ProgramPart p)],k),k) . ((IC (Computation (s +* p),i)) + k)
by AMISTD_2:69
.=
(Shift (IncAddr [(ProgramPart p)],k),k) . ((IC (Computation (s +* p),i)) + k)
by AMISTD_2:75
.=
(IncAddr [(ProgramPart p)],k) . (IC (Computation (s +* p),i))
by A26, AMISTD_2:65
.=
IncAddr (CurInstr (Computation (s +* p),i)),
k
by A25, A28, AMISTD_2:74
;
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 A17, A29, AMISTD_2:67
.=
((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 AMISTD_2:67
.=
(((Computation (s +* p),(i + 1)) +* (Start-At ((IC (Computation (s +* p),(i + 1))) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A19, Th35
;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A15, A16);
hence
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))
; :: thesis: verum