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 FinPartState of S st IC in dom p holds
for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of b1 -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
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 FinPartState of S st IC in dom p holds
for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p) )
assume A1:
S is CurIns-recognized
; for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
let k be Element of NAT ; for p being FinPartState of S st IC in dom p holds
for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
let p be FinPartState of S; ( IC in dom p implies for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p) )
RE:
Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k))
by COMPOS_1:116;
assume A3:
IC in dom p
; for s being State of S st p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
then A4:
Start-At ((IC p),S) c= p
by FUNCOP_1:99;
let s be State of S; ( p c= s & Relocated (p,k) is autonomic implies for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p) )
assume that
A5:
p c= s
and
A6:
Relocated (p,k) is autonomic
; for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
let P be the Instructions of S -valued ManySortedSet of NAT ; ( ProgramPart p c= P implies for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p) )
assume A7:
ProgramPart p c= P
; for i being Element of NAT holds Comput (P,s,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
A8:
Start-At ((IC p),S) c= s
by A5, A4, XBOOLE_1:1;
defpred S1[ Element of NAT ] means Comput (P,s,$1) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),$1)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p);
A9:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp =
ProgramPart p as
preProgram of
S ;
set sdom =
s | (dom (Reloc ((ProgramPart p),k)));
dom (Reloc ((ProgramPart p),k)) c= the
carrier of
S
by RELAT_1:def 18;
then
dom (Reloc ((ProgramPart p),k)) c= dom s
by PARTFUN1:def 4;
then
dom (Reloc ((ProgramPart p),k)) = dom (s | (dom (Reloc ((ProgramPart p),k))))
by RELAT_1:91;
then
(
rng (s | (dom (Reloc ((ProgramPart p),k)))) c= the
Instructions of
S &
dom (s | (dom (Reloc ((ProgramPart p),k)))) c= NAT )
by COMPOS_1:32, RELAT_1:87, RE;
then reconsider sdom =
s | (dom (Reloc ((ProgramPart p),k))) as
NAT -defined FinPartState of
by RELSET_1:11;
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A10:
Comput (
P,
s,
i)
= ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
;
S1[i + 1]
reconsider kk =
IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)) as
Element of
NAT ;
reconsider jk =
IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)) as
Element of
NAT ;
A11:
Relocated (
p,
k)
c= s +* (Relocated (p,k))
by FUNCT_4:26;
A12:
Reloc (
(ProgramPart p),
k)
c= P +* (Reloc ((ProgramPart p),k))
by FUNCT_4:26;
IC in dom (Relocated (p,k))
by COMPOS_1:119;
then
not
Relocated (
p,
k) is
NAT -defined
by COMPOS_1:19;
then A13:
IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)) in dom (Reloc ((ProgramPart p),k))
by A6, A1, Def4, A11, A12, RE;
then A14:
jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
by COMPOS_1:117;
(
dom sdom = (dom s) /\ (dom (Reloc ((ProgramPart p),k))) & not
IC in dom (Reloc ((ProgramPart p),k)) )
by COMPOS_1:12, RELAT_1:90, RE;
then A15:
not
IC in dom sdom
by XBOOLE_0:def 4;
dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i))) -' k),S)) = {(IC )}
by FUNCOP_1:19;
then A16:
IC in dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i))) -' k),S))
by TARSKI:def 1;
consider j being
Element of
NAT such that A17:
jk = j + k
and A18:
j in dom (ProgramPart p)
by A14;
A19:
dom (P +* (Reloc ((ProgramPart p),k))) = NAT
by PARTFUN1:def 4;
A20:
Reloc (
(ProgramPart p),
k)
c= P +* (Reloc ((ProgramPart p),k))
by FUNCT_4:26;
dom (Shift (pp,k)) = { (m + k) where m is Element of NAT : m in dom pp }
by VALUED_1:def 12;
then A21:
j + k in dom (Shift ((ProgramPart p),k))
by A18;
then A22:
IncAddr (
((Shift ((ProgramPart p),k)) /. kk),
k) =
(Reloc ((ProgramPart p),k)) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)))
by A17, COMPOS_1:def 40
.=
(P +* (Reloc ((ProgramPart p),k))) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)))
by A13, GRFUNC_1:8, A20
.=
CurInstr (
(P +* (Reloc ((ProgramPart p),k))),
(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)))
by PARTFUN1:def 8, A19
;
A23:
(j + k) -' k = j
by NAT_D:34;
A24:
dom P = NAT
by PARTFUN1:def 4;
not
IC in dom (ProgramPart p)
by COMPOS_1:12;
then A25:
IC (((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* sdom) +* (ProgramPart p)) =
((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* sdom) . (IC )
by FUNCT_4:12
.=
(DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) . (IC )
by A15, FUNCT_4:12
.=
(Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i))) -' k),S)) . (IC )
by A16, FUNCT_4:14
.=
(IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i))) -' k
by FUNCOP_1:87
;
CurInstr (
P,
(Comput (P,s,i))) =
P . (IC (Comput (P,s,i)))
by PARTFUN1:def 8, A24
.=
(ProgramPart p) . (IC (Comput (P,s,i)))
by A10, A17, A18, A23, GRFUNC_1:8, A7, A25
.=
(Shift ((ProgramPart p),k)) . (IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)))
by A17, A18, A23, VALUED_1:def 12, A10, A25
.=
(Shift ((ProgramPart p),k)) /. kk
by A17, A21, PARTFUN1:def 8
;
then A26:
(
Comput (
(P +* (Reloc ((ProgramPart p),k))),
(s +* (Relocated (p,k))),
(i + 1))
= Following (
(P +* (Reloc ((ProgramPart p),k))),
(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i))) &
Exec (
(CurInstr (P,(Comput (P,s,i)))),
(DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)))
= DecIC (
(Following ((P +* (Reloc ((ProgramPart p),k))),(Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)))),
k) )
by A17, A22, Th5, EXTPRO_1:4;
thus Comput (
P,
s,
(i + 1)) =
Following (
P,
(Comput (P,s,i)))
by EXTPRO_1:4
.=
(Exec ((CurInstr (P,(Comput (P,s,i)))),((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),i)),k)) +* sdom))) +* (ProgramPart p)
by A10, AMI_1:127
.=
((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),(i + 1))),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A26, AMI_1:127
;
verum
end;
A27:
IC in dom (Relocated (p,k))
by COMPOS_1:119;
A28: IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0)) =
(s +* (Relocated (p,k))) . (IC )
by EXTPRO_1:3
.=
IC (Relocated (p,k))
by A27, FUNCT_4:14
;
DataPart p c= p
by RELAT_1:88;
then A29:
DataPart p c= s
by A5, XBOOLE_1:1;
ProgramPart p c= p
by RELAT_1:88;
then A30:
ProgramPart p c= s
by A5, XBOOLE_1:1;
set DP = DataPart p;
set IP = Start-At (((IC p) + k),S);
A31:
dom (DataPart p) misses dom (Reloc ((ProgramPart p),k))
by COMPOS_1:15, RE;
set PP = ProgramPart p;
set IS = Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S);
A32:
dom (Start-At (((IC p) + k),S)) = {(IC )}
by FUNCOP_1:19;
set PR = Reloc ((ProgramPart p),k);
set SD = s | (dom (Reloc ((ProgramPart p),k)));
A33:
{(IC )} misses dom (DataPart p)
by COMPOS_1:13;
dom (Reloc ((ProgramPart p),k)) c= the carrier of S
by RELAT_1:def 18;
then
dom (Reloc ((ProgramPart p),k)) c= dom s
by PARTFUN1:def 4;
then A34:
dom (Reloc ((ProgramPart p),k)) = dom (s | (dom (Reloc ((ProgramPart p),k))))
by RELAT_1:91;
{(IC )} misses dom (Reloc ((ProgramPart p),k))
by COMPOS_1:14, RE;
then A35:
{(IC )} /\ (dom (Reloc ((ProgramPart p),k))) = {}
by XBOOLE_0:def 7;
A36:
dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S)) = {(IC )}
by FUNCOP_1:19;
then (dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) /\ (dom (s | (dom (Reloc ((ProgramPart p),k))))) =
{(IC )} /\ ((dom s) /\ (dom (Reloc ((ProgramPart p),k))))
by RELAT_1:90
.=
({(IC )} /\ (dom (Reloc ((ProgramPart p),k)))) /\ (dom s)
by XBOOLE_1:16
.=
{}
by A35
;
then A37:
dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S)) misses dom (s | (dom (Reloc ((ProgramPart p),k))))
by XBOOLE_0:def 7;
A38:
dom ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k))) = (dom (Start-At (((IC p) + k),S))) \/ (dom (Reloc ((ProgramPart p),k)))
by FUNCT_4:def 1;
dom (Reloc ((ProgramPart p),k)) c= NAT
by RELAT_1:def 18;
then A39:
dom (Reloc ((ProgramPart p),k)) misses Data-Locations S
by COMPOS_1:51, XBOOLE_1:63;
A40:
dom (Start-At (((IC p) + k),S)) misses dom (DataPart p)
by A33, FUNCOP_1:19;
dom (Reloc ((ProgramPart p),k)) misses dom (DataPart p)
by A39, XBOOLE_1:63, RELAT_1:87;
then A41:
dom ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k))) misses dom (DataPart p)
by A40, A38, XBOOLE_1:70;
A42: ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k))) +* (DataPart p) =
(DataPart p) +* ((Start-At (((IC p) + k),S)) +* (Reloc ((ProgramPart p),k)))
by A41, FUNCT_4:36
.=
((DataPart p) +* (Start-At (((IC p) + k),S))) +* (Reloc ((ProgramPart p),k))
by FUNCT_4:15
.=
Relocated (p,k)
by A3, COMPOS_1:75
;
Comput (P,s,0) =
s
by EXTPRO_1:3
.=
s +* (ProgramPart p)
by A30, FUNCT_4:79
.=
(s +* (Start-At ((IC p),S))) +* (ProgramPart p)
by A8, FUNCT_4:79
.=
(s +* (Start-At ((((IC p) + k) -' k),S))) +* (ProgramPart p)
by NAT_D:34
.=
(s +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (ProgramPart p)
by A28, A3, COMPOS_1:120
.=
((s +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (ProgramPart p)
by FUNCT_4:80
.=
(((s +* (Reloc ((ProgramPart p),k))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (ProgramPart p)
by A34, FUNCT_4:78
.=
((s +* (Reloc ((ProgramPart p),k))) +* ((s | (dom (Reloc ((ProgramPart p),k)))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S)))) +* (ProgramPart p)
by FUNCT_4:15
.=
((s +* (Reloc ((ProgramPart p),k))) +* ((Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S)) +* (s | (dom (Reloc ((ProgramPart p),k)))))) +* (ProgramPart p)
by A37, FUNCT_4:36
.=
(((s +* (Reloc ((ProgramPart p),k))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (Reloc ((ProgramPart p),k))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A29, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (Reloc ((ProgramPart p),k)))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((Reloc ((ProgramPart p),k)) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A31, FUNCT_4:36
.=
((((s +* (Reloc ((ProgramPart p),k))) +* (DataPart p)) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((((s +* (Reloc ((ProgramPart p),k))) +* (DataPart p)) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A36, A32, FUNCT_4:78
.=
((((s +* ((Reloc ((ProgramPart p),k)) +* (DataPart p))) +* (Start-At (((IC p) + k),S))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (((Reloc ((ProgramPart p),k)) +* (DataPart p)) +* (Start-At (((IC p) + k),S)))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((Reloc ((ProgramPart p),k)) +* ((DataPart p) +* (Start-At (((IC p) + k),S))))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((Reloc ((ProgramPart p),k)) +* ((Start-At (((IC p) + k),S)) +* (DataPart p)))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A32, A33, FUNCT_4:36
.=
(((s +* (((Reloc ((ProgramPart p),k)) +* (Start-At (((IC p) + k),S))) +* (DataPart p))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (Relocated (p,k))) +* (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0))) -' k),S))) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A42, A32, COMPOS_1:14, FUNCT_4:36, RE
.=
((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (Relocated (p,k))),0)),k)) +* (s | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by EXTPRO_1:3
;
then A43:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A43, A9); verum