let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving steady-programmed relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of b1 -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving steady-programmed relocable IC-recognized AMI-Struct of N; ( S is CurIns-recognized implies for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k)) )
assume A1:
S is CurIns-recognized
; for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
let k be Element of NAT ; for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
let p be autonomic FinPartState of S; ( IC in dom p implies for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k)) )
assume A2:
IC in dom p
; for s being State of S st Relocated (p,k) c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
RE:
Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k))
by COMPOS_1:116;
let s be State of S; ( Relocated (p,k) c= s implies for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k)) )
assume A4:
Relocated (p,k) c= s
; for P being the Instructions of S -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
let P be the Instructions of S -valued ManySortedSet of NAT ; ( Reloc ((ProgramPart p),k) c= P implies for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k)) )
assume A5:
Reloc ((ProgramPart p),k) c= P
; for i being Element of NAT holds Comput (P,s,i) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
defpred S1[ Element of NAT ] means Comput (P,s,$1) = ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),$1)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k));
A6:
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
S
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
S &
dom (s | (dom (ProgramPart p))) c= NAT )
by COMPOS_1:32, RELAT_1:87;
then reconsider sdom =
s | (dom (ProgramPart p)) as
NAT -defined FinPartState of
by RELSET_1:11;
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A7:
Comput (
P,
s,
i)
= ((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
;
S1[i + 1]
reconsider kk =
IC (Comput ((P +* (ProgramPart p)),(s +* p),i)) as
Element of
NAT ;
dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k),S)) = {(IC )}
by FUNCOP_1:19;
then A8:
IC in dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k),S))
by TARSKI:def 1;
(
dom sdom = (dom s) /\ (dom (ProgramPart p)) & not
IC in dom (ProgramPart p) )
by COMPOS_1:12, RELAT_1:90;
then A9:
not
IC in dom sdom
by XBOOLE_0:def 4;
A10:
p c= s +* p
by FUNCT_4:26;
A11:
ProgramPart p c= P +* (ProgramPart p)
by FUNCT_4:26;
not
p is
NAT -defined
by A2, COMPOS_1:19;
then A12:
IC (Comput ((P +* (ProgramPart p)),(s +* p),i)) in dom (ProgramPart p)
by A1, Def4, A10, A11;
then A13:
IC (Comput ((P +* (ProgramPart p)),(s +* p),i)) in dom (IncAddr ((ProgramPart p),k))
by COMPOS_1:def 40;
A14:
(IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k in dom (Reloc ((ProgramPart p),k))
by A12, COMPOS_1:158;
reconsider kk =
IC (Comput ((P +* (ProgramPart p)),(s +* p),i)) as
Element of
NAT ;
Reloc (
(ProgramPart p),
k)
= ProgramPart (Relocated (p,k))
by COMPOS_1:116;
then
not
IC in dom (Reloc ((ProgramPart p),k))
by COMPOS_1:12;
then A15:
IC (Comput (P,s,i)) =
(((Comput ((P +* (ProgramPart p)),(s +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k),S))) +* sdom) . (IC )
by FUNCT_4:12, A7
.=
((Comput ((P +* (ProgramPart p)),(s +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k),S))) . (IC )
by A9, FUNCT_4:12
.=
(Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k),S)) . (IC )
by A8, FUNCT_4:14
.=
(IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k
by FUNCOP_1:87
;
A16:
ProgramPart p c= P +* (ProgramPart p)
by FUNCT_4:26;
A17:
(ProgramPart p) /. kk = (ProgramPart p) . kk
by A12, PARTFUN1:def 8;
A18:
dom (P +* (ProgramPart p)) = NAT
by PARTFUN1:def 4;
dom P = NAT
by PARTFUN1:def 4;
then A19:
CurInstr (
P,
(Comput (P,s,i))) =
P . (IC (Comput (P,s,i)))
by PARTFUN1:def 8
.=
(Reloc ((ProgramPart p),k)) . (IC (Comput (P,s,i)))
by A5, A14, GRFUNC_1:8, A15
.=
(Shift ((IncAddr ((ProgramPart p),k)),k)) . ((IC (Comput ((P +* (ProgramPart p)),(s +* p),i))) + k)
by COMPOS_1:159, A15
.=
(IncAddr ((ProgramPart p),k)) . kk
by A13, VALUED_1:def 12
.=
IncAddr (
((ProgramPart p) /. kk),
k)
by A12, COMPOS_1:def 40
.=
IncAddr (
((P +* (ProgramPart p)) . (IC (Comput ((P +* (ProgramPart p)),(s +* p),i)))),
k)
by A12, GRFUNC_1:8, A17, A16
.=
IncAddr (
(CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* p),i)))),
k)
by PARTFUN1:def 8, A18
;
A20:
Comput (
(P +* (ProgramPart p)),
(s +* p),
(i + 1))
= Following (
(P +* (ProgramPart p)),
(Comput ((P +* (ProgramPart p)),(s +* p),i)))
by EXTPRO_1:4;
thus Comput (
P,
s,
(i + 1)) =
Following (
P,
(Comput (P,s,i)))
by EXTPRO_1:4
.=
(Exec ((IncAddr ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* p),i)))),k)),((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)) +* sdom))) +* (Reloc ((ProgramPart p),k))
by A7, A19, AMI_1:127
.=
((Exec ((IncAddr ((CurInstr ((P +* (ProgramPart p)),(Comput ((P +* (ProgramPart p)),(s +* p),i)))),k)),(IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),i)),k)))) +* sdom) +* (Reloc ((ProgramPart p),k))
by AMI_1:127
.=
((IncIC ((Comput ((P +* (ProgramPart p)),(s +* p),(i + 1))),k)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A20, Th4
;
verum
end;
set IP = Start-At ((IC p),S);
A21:
dom (Start-At ((IC p),S)) = {(IC )}
by FUNCOP_1:19;
A22:
Start-At (((IC p) + k),S) c= Relocated (p,k)
by A2, COMPOS_1:123;
IC (Comput ((P +* (ProgramPart p)),(s +* p),0)) =
(s +* p) . (IC )
by EXTPRO_1:3
.=
IC p
by A2, FUNCT_4:14
;
then A23:
Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S) c= s
by A4, A22, XBOOLE_1:1;
set DP = DataPart p;
A24:
{(IC )} misses dom (DataPart p)
by COMPOS_1:13;
set PP = ProgramPart p;
A25:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
set SD = s | (dom (ProgramPart p));
A26:
s | (dom (ProgramPart p)) c= s
by RELAT_1:88;
Reloc ((ProgramPart p),k) c= Relocated (p,k)
by RELAT_1:88, RE;
then A27:
Reloc ((ProgramPart p),k) c= s
by A4, XBOOLE_1:1;
dom (ProgramPart p) c= the carrier of S
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s
by PARTFUN1:def 4;
then A28:
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 A4, XBOOLE_1:1;
then A29:
DataPart p c= s
by COMPOS_1:115;
set PR = Reloc ((ProgramPart p),k);
set IS = Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S);
A30:
dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S)) = {(IC )}
by FUNCOP_1:19;
Comput (P,s,0) =
s
by EXTPRO_1:3
.=
s +* (Reloc ((ProgramPart p),k))
by A27, FUNCT_4:79
.=
(s +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A26, FUNCT_4:79
.=
((s +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A28, FUNCT_4:78
.=
(((s +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (ProgramPart p)) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A23, FUNCT_4:79
.=
((s +* ((Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S)) +* (ProgramPart p))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
((s +* ((ProgramPart p) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S)))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A30, COMPOS_1:14, FUNCT_4:36
.=
(((s +* (ProgramPart p)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (ProgramPart p)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A29, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (ProgramPart p))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A25, FUNCT_4:36
.=
((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((((s +* (ProgramPart p)) +* (DataPart p)) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A30, A21, FUNCT_4:78
.=
((((s +* ((ProgramPart p) +* (DataPart p))) +* (Start-At ((IC p),S))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((s +* (((ProgramPart p) +* (DataPart p)) +* (Start-At ((IC p),S)))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((DataPart p) +* (Start-At ((IC p),S))))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((s +* ((ProgramPart p) +* ((Start-At ((IC p),S)) +* (DataPart p)))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A21, A24, FUNCT_4:36
.=
(((s +* (((ProgramPart p) +* (Start-At ((IC p),S))) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
(((s +* (((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A21, COMPOS_1:14, FUNCT_4:36
.=
(((s +* p) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A2, COMPOS_1:18
.=
(((Comput ((P +* (ProgramPart p)),(s +* p),0)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s +* p),0))) + k),S))) +* (s | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by EXTPRO_1:3
;
then A31:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A31, A6); verum