let k be Element of NAT ; :: thesis: for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
let p be FinPartState of SCM+FSA ; :: thesis: ( IC SCM+FSA in dom p implies for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) )
assume
IC SCM+FSA in dom p
; :: thesis: for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
then A1:
Start-At (IC p) c= p
by AMI_1:110;
let s be State of SCM+FSA ; :: thesis: ( p c= s & Relocated p,k is autonomic implies for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p) )
assume that
A2:
p c= s
and
A3:
Relocated p,k is autonomic
; :: thesis: for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
A4:
Start-At (IC p) c= s
by A2, A1, XBOOLE_1:1;
defpred S1[ Element of NAT ] means Computation s,$1 = (((Computation (s +* (Relocated p,k)),$1) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),$1)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p);
A5:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
reconsider pp =
[(ProgramPart p)] as
preProgram of
SCM+FSA ;
reconsider sdom =
s | (dom (ProgramPart (Relocated p,k))) as
Element of
sproduct the
Object-Kind of
SCM+FSA ;
let i be
Element of
NAT ;
:: thesis: ( S1[i] implies S1[i + 1] )
assume A6:
Computation s,
i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
;
:: thesis: S1[i + 1]
dom [(ProgramPart (Relocated p,k))] c= the
carrier of
SCM+FSA
by AMI_1:80;
then
dom (ProgramPart (Relocated p,k)) c= dom s
by AMI_1:79;
then A7:
dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k))))
by RELAT_1:91;
then reconsider sdom =
sdom as
FinPartState of
SCM+FSA by FINSET_1:29;
dom (s | (dom [(ProgramPart (Relocated p,k))])) c= NAT
by A7, RELAT_1:def 18;
then reconsider sdom =
sdom as
preProgram of
SCM+FSA by RELAT_1:def 18;
reconsider ii =
IC (Computation (s +* (Relocated p,k)),i) as
Element of
NAT by ORDINAL1:def 13;
reconsider jk =
IC (Computation (s +* (Relocated p,k)),i) as
Element of
NAT by ORDINAL1:def 13;
A8:
ProgramPart (Relocated p,k) c= Computation (s +* (Relocated p,k)),
i
by AMI_1:99, FUNCT_4:26;
IC SCM+FSA in dom (Relocated p,k)
by Th5;
then
not
Relocated p,
k is
NAT -defined
by AMI_1:109;
then A9:
IC (Computation (s +* (Relocated p,k)),i) in dom (ProgramPart (Relocated p,k))
by A3, FUNCT_4:26, SCMFSA_3:17;
then A10:
jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
by Th3;
A11:
not
IC SCM+FSA in dom (ProgramPart (Relocated p,k))
by AMI_1:101;
dom sdom = (dom s) /\ (dom (ProgramPart (Relocated p,k)))
by RELAT_1:90;
then A12:
not
IC SCM+FSA in dom sdom
by A11, XBOOLE_0:def 4;
dom (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k)) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A13:
IC SCM+FSA in dom (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))
by TARSKI:def 1;
not
IC SCM+FSA in dom (ProgramPart p)
by AMI_1:101;
then A14:
IC ((((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom) +* [(ProgramPart p)]) =
(((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom) . (IC SCM+FSA )
by FUNCT_4:12
.=
((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) . (IC SCM+FSA )
by A12, FUNCT_4:12
.=
(Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k)) . (IC SCM+FSA )
by A13, FUNCT_4:14
.=
(IC (Computation (s +* (Relocated p,k)),i)) -' k
by FUNCOP_1:87
;
consider j being
Element of
NAT such that A15:
jk = j + k
and A16:
j in dom (ProgramPart p)
by A10;
dom (Shift pp,k) = { (m + k) where m is Element of NAT : m in dom pp }
by VALUED_1:def 12;
then A17:
insloc (j + k) in dom (Shift (ProgramPart p),k)
by A16;
then A18:
IncAddr (pi [(Shift (ProgramPart p),k)],ii),
k =
(IncAddr [(Shift (ProgramPart p),k)],k) . (IC (Computation (s +* (Relocated p,k)),i))
by A15, SCMFSA_4:24
.=
(ProgramPart (Relocated p,k)) . (IC (Computation (s +* (Relocated p,k)),i))
by Th2
.=
CurInstr (Computation (s +* (Relocated p,k)),i)
by A9, A8, GRFUNC_1:8
;
A19:
((insloc (j + k)) -' k) + k = insloc (j + k)
by NAT_D:34;
(insloc (j + k)) -' k = insloc j
by NAT_D:34;
then CurInstr (Computation s,i) =
(ProgramPart p) . ((IC (Computation (s +* (Relocated p,k)),i)) -' k)
by A6, A14, A15, A16, FUNCT_4:14
.=
(Shift (ProgramPart p),k) . (IC (Computation (s +* (Relocated p,k)),i))
by A15, A16, A19, VALUED_1:def 12
.=
pi [(Shift (ProgramPart p),k)],
ii
by A15, A17, AMI_1:def 47
;
then A20:
Exec (CurInstr (Computation s,i)),
((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) = (Following (Computation (s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (Computation (s +* (Relocated p,k)),i))) -' k))
by A15, A18, SCMFSA_4:29;
A21:
Computation (s +* (Relocated p,k)),
(i + 1) = Following (Computation (s +* (Relocated p,k)),i)
by AMI_1:14;
Computation s,
(i + 1) =
Following (Computation s,i)
by AMI_1:14
.=
(Exec (CurInstr (Computation s,i)),(((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* sdom)) +* [(ProgramPart p)]
by A6, SCMFSA_3:10
.=
(((Following (Computation (s +* (Relocated p,k)),i)) +* (Start-At ((IC (Following (Computation (s +* (Relocated p,k)),i))) -' k))) +* sdom) +* (ProgramPart p)
by A20, SCMFSA_3:10
;
hence
S1[
i + 1]
by A21;
:: thesis: verum
end;
A22:
IC SCM+FSA in dom (Relocated p,k)
by Th5;
A23: IC (Computation (s +* (Relocated p,k)),0 ) =
(s +* (Relocated p,k)) . (IC SCM+FSA )
by AMI_1:13
.=
(Relocated p,k) . (IC SCM+FSA )
by A22, FUNCT_4:14
.=
IC (Relocated p,k)
by A22, AMI_1:def 43
;
DataPart p c= p
by RELAT_1:88;
then A24:
DataPart p c= s
by A2, XBOOLE_1:1;
ProgramPart p c= p
by RELAT_1:88;
then A25:
ProgramPart p c= s
by A2, XBOOLE_1:1;
set DP = DataPart p;
set IP = Start-At ((IC p) + k);
A26:
dom (DataPart p) misses dom (ProgramPart (Relocated p,k))
by AMI_1:104;
set PP = ProgramPart p;
set IS = Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k);
A27:
dom (Start-At ((IC p) + k)) = {(IC SCM+FSA )}
by FUNCOP_1:19;
set PR = ProgramPart (Relocated p,k);
set SD = s | (dom (ProgramPart (Relocated p,k)));
A28:
{(IC SCM+FSA )} misses dom (DataPart p)
by AMI_1:102;
dom [(ProgramPart (Relocated p,k))] c= the carrier of SCM+FSA
by AMI_1:80;
then
dom (ProgramPart (Relocated p,k)) c= dom s
by AMI_1:79;
then A29:
dom (ProgramPart (Relocated p,k)) = dom (s | (dom (ProgramPart (Relocated p,k))))
by RELAT_1:91;
{(IC SCM+FSA )} misses dom (ProgramPart (Relocated p,k))
by AMI_1:103;
then A30:
{(IC SCM+FSA )} /\ (dom (ProgramPart (Relocated p,k))) = {}
by XBOOLE_0:def 7;
A31:
dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then (dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) /\ (dom (s | (dom (ProgramPart (Relocated p,k))))) =
{(IC SCM+FSA )} /\ ((dom s) /\ (dom (ProgramPart (Relocated p,k))))
by RELAT_1:90
.=
({(IC SCM+FSA )} /\ (dom (ProgramPart (Relocated p,k)))) /\ (dom s)
by XBOOLE_1:16
.=
{}
by A30
;
then A32:
dom (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) misses dom (s | (dom (ProgramPart (Relocated p,k))))
by XBOOLE_0:def 7;
Computation s,0 =
s
by AMI_1:13
.=
s +* (ProgramPart p)
by A25, FUNCT_4:79
.=
(s +* (Start-At (IC p))) +* (ProgramPart p)
by A4, FUNCT_4:79
.=
(s +* (Start-At (((IC p) + k) -' k))) +* (ProgramPart p)
by NAT_D:34
.=
(s +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p)
by A23, Th6
.=
((s +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p)
by FUNCT_4:80
.=
(((s +* (ProgramPart (Relocated p,k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (ProgramPart p)
by A29, FUNCT_4:78
.=
((s +* (ProgramPart (Relocated p,k))) +* ((s | (dom (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)))) +* (ProgramPart p)
by FUNCT_4:15
.=
((s +* (ProgramPart (Relocated p,k))) +* ((Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k)) +* (s | (dom (ProgramPart (Relocated p,k)))))) +* (ProgramPart p)
by A32, FUNCT_4:36
.=
(((s +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (ProgramPart (Relocated p,k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A24, FUNCT_4:79
.=
(((s +* ((DataPart p) +* (ProgramPart (Relocated p,k)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A26, FUNCT_4:36
.=
((((s +* (ProgramPart (Relocated p,k))) +* (DataPart p)) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((((s +* (ProgramPart (Relocated p,k))) +* (DataPart p)) +* (Start-At ((IC p) + k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A31, A27, FUNCT_4:78
.=
((((s +* ((ProgramPart (Relocated p,k)) +* (DataPart p))) +* (Start-At ((IC p) + k))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (((ProgramPart (Relocated p,k)) +* (DataPart p)) +* (Start-At ((IC p) + k)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* ((DataPart p) +* (Start-At ((IC p) + k))))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((ProgramPart (Relocated p,k)) +* ((Start-At ((IC p) + k)) +* (DataPart p)))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A27, A28, FUNCT_4:36
.=
(((s +* (((ProgramPart (Relocated p,k)) +* (Start-At ((IC p) + k))) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by FUNCT_4:15
;
then Computation s,0 =
(((s +* (((Start-At ((IC p) + k)) +* (ProgramPart (Relocated p,k))) +* (DataPart p))) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A27, AMI_1:103, FUNCT_4:36
.=
(((s +* (Relocated p,k)) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by Th2
.=
(((Computation (s +* (Relocated p,k)),0 ) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),0 )) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by AMI_1:13
;
then A33:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A33, A5); :: thesis: verum