let k be Element of NAT ; for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st 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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
let p be autonomic FinPartState of SCM ; ( IC SCM in dom p implies for s being State of SCM st 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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) )
assume A1:
IC SCM in dom p
; for s being State of SCM st 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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
let s be State of SCM ; ( 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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k)) )
assume A2:
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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k));
A3:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set sdom =
s | (dom (ProgramPart p));
dom (ProgramPart p) c= the
carrier of
SCM
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s
by PARTFUN1:def 4;
then
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 COMPOS_1:32, RELAT_1:87;
then reconsider sdom =
s | (dom (ProgramPart p)) as
NAT -defined finite FinPartState of
by RELSET_1:11;
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A5:
Comput (ProgramPart s),
s,
i = (((Comput (ProgramPart (s +* p)),(s +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
;
S1[i + 1]
reconsider kk =
IC (Comput (ProgramPart (s +* p)),(s +* p),i) as
Element of
NAT ;
A6:
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 ) = {(IC SCM )}
by FUNCOP_1:19;
then A7:
IC SCM in dom (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM )
by TARSKI:def 1;
(
dom sdom = (dom s) /\ (dom (ProgramPart p)) & not
IC SCM in dom (ProgramPart p) )
by COMPOS_1:12, RELAT_1:90;
then A8:
not
IC SCM in dom sdom
by XBOOLE_0:def 4;
not
p is
NAT -defined
by A1, COMPOS_1:19;
then A9:
IC (Comput (ProgramPart (s +* p)),(s +* p),i) in dom (ProgramPart p)
by AMI_5:86, FUNCT_4:26;
then A10:
IC (Comput (ProgramPart (s +* p)),(s +* p),i) in dom (IncAddr (ProgramPart p),k)
by AMISTD_2:def 15;
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 A9, AMISTD_2:71;
then A11:
(IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k in dom (ProgramPart (Relocated p,k))
by COMPOS_1:16;
A12:
(ProgramPart p) /. kk =
(ProgramPart p) . kk
by A9, PARTFUN1:def 8
.=
(Comput (ProgramPart (s +* p)),(s +* p),i) . (IC (Comput (ProgramPart (s +* p)),(s +* p),i))
by A9, A6, GRFUNC_1:8
;
reconsider kk =
IC (Comput (ProgramPart (s +* p)),(s +* p),i) as
Element of
NAT ;
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;
T:
ProgramPart (s +* p) = ProgramPart (Comput (ProgramPart (s +* p)),(s +* p),i)
by AMI_1:123;
not
IC SCM 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 )) +* sdom) +* (ProgramPart (Relocated p,k))) =
(((Comput (ProgramPart (s +* p)),(s +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM )) +* sdom) . (IC SCM )
by FUNCT_4:12
.=
((Comput (ProgramPart (s +* p)),(s +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM )) . (IC SCM )
by A8, FUNCT_4:12
.=
(Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM ) . (IC SCM )
by A7, FUNCT_4:14
.=
(IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k
by FUNCOP_1:87
;
then A13:
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 A5, A11, Y, FUNCT_4:14
.=
(Reloc (ProgramPart p),k) . ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k)
by AMISTD_2:69
.=
(Shift (IncAddr (ProgramPart p),k),k) . ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k)
by Th19
.=
(IncAddr (ProgramPart p),k) . kk
by A10, VALUED_1:def 12
.=
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart (s +* p)),(s +* p),i)),(Comput (ProgramPart (s +* p)),(s +* p),i)),
k
by A9, A12, Z, AMISTD_2:def 15
;
A14:
Comput (ProgramPart (s +* p)),
(s +* p),
(i + 1) = Following (ProgramPart (s +* p)),
(Comput (ProgramPart (s +* p)),(s +* p),i)
by AMI_1:14;
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 AMI_1:14
.=
(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 )) +* sdom)) +* (ProgramPart (Relocated p,k))
by A5, A13, S, AMI_5:77
.=
((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 ))) +* sdom) +* (ProgramPart (Relocated p,k))
by AMI_5:77
.=
(((Comput (ProgramPart (s +* p)),(s +* p),(i + 1)) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),(i + 1))) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A14, Th31, T
;
verum
end;
set IP = Start-At (IC p),SCM ;
A15:
dom (Start-At (IC p),SCM ) = {(IC SCM )}
by FUNCOP_1:19;
A16:
Start-At ((IC p) + k),SCM c= Relocated p,k
by A1, Th28;
IC (Comput (ProgramPart (s +* p)),(s +* p),0 ) =
(s +* p) . (IC SCM )
by AMI_1:13
.=
p . (IC SCM )
by A1, FUNCT_4:14
.=
IC p
;
then A17:
Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM c= s
by A2, A16, XBOOLE_1:1;
set DP = DataPart p;
A18:
{(IC SCM )} misses dom (DataPart p)
by COMPOS_1:13;
set PP = ProgramPart p;
A19:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
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 RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s
by PARTFUN1:def 4;
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 AMISTD_2:68;
set PR = ProgramPart (Relocated p,k);
set IS = Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM ;
A24:
dom (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM ) = {(IC SCM )}
by FUNCOP_1:19;
Comput (ProgramPart s),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 (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A17, FUNCT_4:79
.=
((s +* ((Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM ) +* (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 ))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A24, COMPOS_1:14, FUNCT_4:36
.=
(((s +* (ProgramPart p)) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A23, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (ProgramPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (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 )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A19, FUNCT_4:36
.=
((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by FUNCT_4:15
.=
(((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At (IC p),SCM )) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A24, A15, FUNCT_4:78
.=
((((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At (IC p),SCM )) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by FUNCT_4:15
.=
(((s +* (((ProgramPart p) +* (DataPart p)) +* (Start-At (IC p),SCM ))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((DataPart p) +* (Start-At (IC p),SCM )))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((Start-At (IC p),SCM ) +* (DataPart p)))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A15, A18, FUNCT_4:36
.=
(((s +* (((ProgramPart p) +* (Start-At (IC p),SCM )) +* (DataPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by FUNCT_4:15
.=
(((s +* (((Start-At (IC p),SCM ) +* (ProgramPart p)) +* (DataPart p))) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A15, COMPOS_1:14, FUNCT_4:36
.=
(((s +* p) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A1, COMPOS_1:18
.=
(((Comput (ProgramPart (s +* p)),(s +* p),0 ) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),0 )) + k),SCM )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by AMI_1:13
;
then A25:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A25, A3); verum