let k be Element of NAT ; 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
let R be 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
let s be State of (SCM R); ( 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k))) )
assume A1:
not R is trivial
; 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
let p be autonomic FinPartState of (SCM R); ( IC (SCM R) in dom p & Relocated (p,k) c= s implies for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k))) )
assume that
A2:
IC (SCM R) in dom p
and
A3:
Relocated (p,k) c= s
; for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
A4:
Start-At (((IC p) + k),(SCM R)) c= Relocated (p,k)
by A2, COMPOS_1:123;
defpred S1[ Element of NAT ] means Comput ((ProgramPart s),s,$1) = (((Comput ((ProgramPart (s +* p)),(s +* p),$1)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),$1))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)));
A5:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set sdom =
s | (dom (ProgramPart p));
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A6:
Comput (
(ProgramPart s),
s,
i)
= (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
;
S1[i + 1]
dom (ProgramPart p) c= the
carrier of
(SCM R)
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s
by PARTFUN1:def 4;
then A7:
dom (ProgramPart p) = dom (s | (dom (ProgramPart p)))
by RELAT_1:91;
reconsider sdom =
s | (dom (ProgramPart p)) as
FinPartState of
(SCM R) ;
dom (s | (dom (ProgramPart p))) c= NAT
by A7, RELAT_1:87;
then reconsider sdom =
sdom as
NAT -defined FinPartState of
by RELAT_1:def 18;
reconsider ii =
IC (Comput ((ProgramPart (s +* p)),(s +* p),i)) as
Element of
NAT ;
A8:
ProgramPart p c= Comput (
(ProgramPart (s +* p)),
(s +* p),
i)
by AMI_1:99, FUNCT_4:26;
dom (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R))) = {(IC (SCM R))}
by FUNCOP_1:19;
then A9:
IC (SCM R) in dom (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))
by TARSKI:def 1;
(
dom sdom = (dom s) /\ (dom (ProgramPart p)) & not
IC (SCM R) in dom (ProgramPart p) )
by COMPOS_1:12, RELAT_1:90;
then A10:
not
IC (SCM R) in dom sdom
by XBOOLE_0:def 4;
not
p is
NAT -defined
by A2, COMPOS_1:19;
then A11:
IC (Comput ((ProgramPart (s +* p)),(s +* p),i)) in dom (ProgramPart p)
by A1, Th27, FUNCT_4:26;
then A12:
IC (Comput ((ProgramPart (s +* p)),(s +* p),i)) in dom (IncAddr ((ProgramPart p),k))
by COMPOS_1:def 40;
ProgramPart p c= p
by RELAT_1:88;
then
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
then
(IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k in dom (Relocated (p,k))
by A11, COMPOS_1:118;
then A13:
(IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k in dom (ProgramPart (Relocated (p,k)))
by COMPOS_1:16;
A14:
(ProgramPart p) /. ii =
(ProgramPart p) . (IC (Comput ((ProgramPart (s +* p)),(s +* p),i)))
by A11, PARTFUN1:def 8
.=
(Comput ((ProgramPart (s +* p)),(s +* p),i)) . (IC (Comput ((ProgramPart (s +* p)),(s +* p),i)))
by A11, A8, GRFUNC_1:8
;
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 COMPOS_1:38;
Z:
(ProgramPart (Comput ((ProgramPart (s +* p)),(s +* p),i))) /. (IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) = (Comput ((ProgramPart (s +* p)),(s +* p),i)) . (IC (Comput ((ProgramPart (s +* p)),(s +* p),i)))
by COMPOS_1:38;
not
IC (SCM R) in dom (ProgramPart (Relocated (p,k)))
by COMPOS_1:12;
then IC ((((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* sdom) +* (ProgramPart (Relocated (p,k)))) =
(((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* sdom) . (IC (SCM R))
by FUNCT_4:12
.=
((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) . (IC (SCM R))
by A10, FUNCT_4:12
.=
(Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R))) . (IC (SCM R))
by A9, FUNCT_4:14
.=
(IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k
by FUNCOP_1:87
;
then A15:
CurInstr (
(ProgramPart (Comput ((ProgramPart s),s,i))),
(Comput ((ProgramPart s),s,i))) =
(ProgramPart (Relocated (p,k))) . ((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k)
by A6, A13, Y, FUNCT_4:14
.=
(IncAddr ((Shift ((ProgramPart p),k)),k)) . ((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k)
by COMPOS_1:116
.=
(Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k)
by COMPOS_1:121
.=
(IncAddr ((ProgramPart p),k)) . (IC (Comput ((ProgramPart (s +* p)),(s +* p),i)))
by A12, VALUED_1:def 12
.=
IncAddr (
(CurInstr ((ProgramPart (Comput ((ProgramPart (s +* p)),(s +* p),i))),(Comput ((ProgramPart (s +* p)),(s +* p),i)))),
k)
by A11, A14, Z, COMPOS_1:def 40
;
T:
ProgramPart (s +* p) = ProgramPart (Comput ((ProgramPart (s +* p)),(s +* p),i))
by AMI_1:123;
A16:
Comput (
(ProgramPart (s +* p)),
(s +* p),
(i + 1))
= Following (
(ProgramPart (s +* p)),
(Comput ((ProgramPart (s +* p)),(s +* p),i)))
by EXTPRO_1:4;
S:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i))
by AMI_1:123;
thus Comput (
(ProgramPart s),
s,
(i + 1)) =
Following (
(ProgramPart s),
(Comput ((ProgramPart s),s,i)))
by EXTPRO_1:4
.=
(Exec ((IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* p)),(s +* p),i))),(Comput ((ProgramPart (s +* p)),(s +* p),i)))),k)),(((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* sdom))) +* (ProgramPart (Relocated (p,k)))
by A6, A15, S, AMI_1:127
.=
((Exec ((IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* p)),(s +* p),i))),(Comput ((ProgramPart (s +* p)),(s +* p),i)))),k)),((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))))) +* sdom) +* (ProgramPart (Relocated (p,k)))
by AMI_1:127
.=
(((Comput ((ProgramPart (s +* p)),(s +* p),(i + 1))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),(i + 1)))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A16, Th22, T
;
verum
end;
set SD = s | (dom (ProgramPart p));
A17:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
set PR = ProgramPart (Relocated (p,k));
set IP = Start-At ((IC p),(SCM R));
A18:
s | (dom (ProgramPart p)) c= s
by RELAT_1:88;
set PP = ProgramPart p;
A19:
{(IC (SCM R))} misses dom (DataPart p)
by COMPOS_1:13;
ProgramPart (Relocated (p,k)) c= Relocated (p,k)
by RELAT_1:88;
then A20:
ProgramPart (Relocated (p,k)) c= s
by A3, XBOOLE_1:1;
dom (ProgramPart p) c= the carrier of (SCM R)
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s
by PARTFUN1:def 4;
then A21:
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 A3, XBOOLE_1:1;
then A22:
DataPart p c= s
by COMPOS_1:115;
set DP = DataPart p;
set IS = Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R));
A23:
dom (Start-At ((IC p),(SCM R))) = {(IC (SCM R))}
by FUNCOP_1:19;
IC (Comput ((ProgramPart (s +* p)),(s +* p),0)) =
(s +* p) . (IC (SCM R))
by EXTPRO_1:3
.=
IC p
by A2, FUNCT_4:14
;
then A24:
Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)) c= s
by A3, A4, XBOOLE_1:1;
A25:
dom (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R))) = {(IC (SCM R))}
by FUNCOP_1:19;
then A26:
dom (Start-At ((IC p),(SCM R))) = dom (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))
by FUNCOP_1:19;
Comput ((ProgramPart s),s,0) =
s
by EXTPRO_1:3
.=
s +* (ProgramPart (Relocated (p,k)))
by A20, FUNCT_4:79
.=
(s +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A18, FUNCT_4:79
.=
((s +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A21, FUNCT_4:78
.=
(((s +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A24, FUNCT_4:79
.=
((s +* ((Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R))) +* (ProgramPart p))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
((s +* ((ProgramPart p) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R))))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A25, COMPOS_1:14, FUNCT_4:36
.=
(((s +* (ProgramPart p)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (ProgramPart p)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A22, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (ProgramPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A17, FUNCT_4:36
.=
((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At ((IC p),(SCM R)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A26, FUNCT_4:78
.=
((((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At ((IC p),(SCM R)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((s +* (((ProgramPart p) +* (DataPart p)) +* (Start-At ((IC p),(SCM R))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((DataPart p) +* (Start-At ((IC p),(SCM R)))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((Start-At ((IC p),(SCM R))) +* (DataPart p)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A23, A19, FUNCT_4:36
.=
(((s +* (((ProgramPart p) +* (Start-At ((IC p),(SCM R)))) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by FUNCT_4:15
.=
(((s +* (((Start-At ((IC p),(SCM R))) +* (ProgramPart p)) +* (DataPart p))) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A23, COMPOS_1:14, FUNCT_4:36
.=
(((s +* p) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A2, COMPOS_1:18
.=
(((Comput ((ProgramPart (s +* p)),(s +* p),0)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),0))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by EXTPRO_1:3
;
then A27:
S1[ 0 ]
;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A27, A5);
hence
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
; verum