let k be Element of NAT ; 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
let p be FinPartState of SCM+FSA; ( 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) )
assume Z:
IC SCM+FSA in dom p
; for s being State of SCM+FSA st p c= s & Relocated (p,k) is autonomic holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
then A1:
Start-At ((IC p),SCM+FSA) c= p
by FUNCOP_1:99;
let s be State of SCM+FSA; ( p c= s & Relocated (p,k) is autonomic implies for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p) )
assume that
A2:
p c= s
and
A3:
Relocated (p,k) is autonomic
; for i being Element of NAT holds Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
A4:
Start-At ((IC p),SCM+FSA) c= s
by A2, A1, XBOOLE_1:1;
defpred S1[ Nat] means Comput ((ProgramPart s),s,$1) = (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),$1)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),$1))) -' k),SCM+FSA))) +* (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 ;
set sdom =
s | (dom (ProgramPart (Relocated (p,k))));
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A6:
Comput (
(ProgramPart s),
s,
i)
= (((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
;
S1[i + 1]
dom (ProgramPart (Relocated (p,k))) c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated (p,k))) c= dom s
by PARTFUN1:def 4;
then A7:
dom (ProgramPart (Relocated (p,k))) = dom (s | (dom (ProgramPart (Relocated (p,k)))))
by RELAT_1:91;
reconsider sdom =
s | (dom (ProgramPart (Relocated (p,k)))) as
FinPartState of
SCM+FSA ;
X:
rng (ProgramPart s) c= the
Instructions of
SCM+FSA
by RELAT_1:def 19;
dom (ProgramPart (Relocated (p,k))) c= NAT
by RELAT_1:def 18;
then
s | (dom (ProgramPart (Relocated (p,k)))) c= ProgramPart s
by RELAT_1:104;
then
rng (s | (dom (ProgramPart (Relocated (p,k))))) c= rng (ProgramPart s)
by RELAT_1:25;
then B:
rng (s | (dom (ProgramPart (Relocated (p,k))))) c= the
Instructions of
SCM+FSA
by X, XBOOLE_1:1;
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 B, RELAT_1:def 18, RELAT_1:def 19;
reconsider ii =
IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) as
Element of
NAT ;
reconsider jk =
IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) as
Element of
NAT ;
A8:
ProgramPart (Relocated (p,k)) c= Comput (
(ProgramPart (s +* (Relocated (p,k)))),
(s +* (Relocated (p,k))),
i)
by AMI_1:99, FUNCT_4:26;
IC SCM+FSA in dom (Relocated (p,k))
by COMPOS_1:119;
then
not
Relocated (
p,
k) is
NAT -defined
by COMPOS_1:19;
then A9:
IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) in dom (ProgramPart (Relocated (p,k)))
by A3, FUNCT_4:26, SCMFSA_3:17;
then
IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) in dom (Reloc ((ProgramPart p),k))
by COMPOS_1:116;
then A10:
jk in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
by COMPOS_1:117;
A11:
not
IC SCM+FSA in dom (ProgramPart (Relocated (p,k)))
by COMPOS_1:12;
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 (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA)) = {(IC SCM+FSA)}
by FUNCOP_1:19;
then A13:
IC SCM+FSA in dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))
by TARSKI:def 1;
not
IC SCM+FSA in dom (ProgramPart p)
by COMPOS_1:12;
then A14:
IC ((((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* sdom) +* (ProgramPart p)) =
(((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* sdom) . (IC SCM+FSA)
by FUNCT_4:12
.=
((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) . (IC SCM+FSA)
by A12, FUNCT_4:12
.=
(Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA)) . (IC SCM+FSA)
by A13, FUNCT_4:14
.=
(IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(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;
Y:
(ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) /. (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) = (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by COMPOS_1:38;
dom (Shift (pp,k)) = { (m + k) where m is Element of NAT : m in dom pp }
by VALUED_1:def 12;
then A17:
j + k in dom (Shift ((ProgramPart p),k))
by A16;
then A18:
IncAddr (
((Shift ((ProgramPart p),k)) /. ii),
k) =
(Reloc ((ProgramPart p),k)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by A15, SCMFSA_4:24
.=
(ProgramPart (Relocated (p,k))) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by COMPOS_1:116
.=
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))),
(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by A9, A8, Y, 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;
A19:
((j + k) -' k) + k = j + k
by NAT_D:34;
(j + k) -' k = j
by NAT_D:34;
then CurInstr (
(ProgramPart (Comput ((ProgramPart s),s,i))),
(Comput ((ProgramPart s),s,i))) =
(ProgramPart p) . ((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k)
by A6, A14, A15, A16, Y, FUNCT_4:14
.=
(Shift ((ProgramPart p),k)) . (IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by A15, A16, A19, VALUED_1:def 12
.=
(Shift ((ProgramPart p),k)) /. ii
by A15, A17, PARTFUN1:def 8
;
then A20:
Exec (
(CurInstr ((ProgramPart (Comput ((ProgramPart s),s,i))),(Comput ((ProgramPart s),s,i)))),
((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))))
= (Following ((ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))))) -' k),SCM+FSA))
by A15, A18, SCMFSA_4:29;
T:
ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,i))
by AMI_1:123;
S:
ProgramPart (s +* (Relocated (p,k))) = ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))
by AMI_1:123;
A21:
Comput (
(ProgramPart (s +* (Relocated (p,k)))),
(s +* (Relocated (p,k))),
(i + 1))
= Following (
(ProgramPart (s +* (Relocated (p,k)))),
(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))
by EXTPRO_1:4;
Comput (
(ProgramPart s),
s,
(i + 1)) =
Following (
(ProgramPart s),
(Comput ((ProgramPart s),s,i)))
by EXTPRO_1:4
.=
(Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s),s,i))),(Comput ((ProgramPart s),s,i)))),(((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))) -' k),SCM+FSA))) +* sdom))) +* (ProgramPart p)
by A6, T, AMI_1:127
.=
(((Following ((ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))),(Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),i))))) -' k),SCM+FSA))) +* sdom) +* (ProgramPart p)
by A20, AMI_1:127
;
hence
S1[
i + 1]
by A21, S;
verum
end;
A22:
IC SCM+FSA in dom (Relocated (p,k))
by COMPOS_1:119;
A23: IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0)) =
(s +* (Relocated (p,k))) . (IC SCM+FSA)
by EXTPRO_1:3
.=
IC (Relocated (p,k))
by A22, FUNCT_4:14
;
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),SCM+FSA);
set PP = ProgramPart p;
set IS = Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA);
A27:
dom (Start-At (((IC p) + k),SCM+FSA)) = {(IC SCM+FSA)}
by FUNCOP_1:19;
set PR = ProgramPart (Relocated (p,k));
set SD = s | (dom (ProgramPart (Relocated (p,k))));
dom (ProgramPart (Relocated (p,k))) c= the carrier of SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated (p,k))) c= dom s
by PARTFUN1:def 4;
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 COMPOS_1:14;
then A30:
{(IC SCM+FSA)} /\ (dom (ProgramPart (Relocated (p,k)))) = {}
by XBOOLE_0:def 7;
A31:
dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA)) = {(IC SCM+FSA)}
by FUNCOP_1:19;
then (dom (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) /\ (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 (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA)) misses dom (s | (dom (ProgramPart (Relocated (p,k)))))
by XBOOLE_0:def 7;
reconsider k = k as Element of NAT ;
Comput ((ProgramPart s),s,0) =
s
by EXTPRO_1:3
.=
s +* (ProgramPart p)
by A25, FUNCT_4:79
.=
(s +* (Start-At ((IC p),SCM+FSA))) +* (ProgramPart p)
by A4, FUNCT_4:79
.=
(s +* (Start-At ((((IC p) + k) -' k),SCM+FSA))) +* (ProgramPart p)
by NAT_D:34
.=
(s +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (ProgramPart p)
by A23, Z, COMPOS_1:120
.=
((s +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (ProgramPart p)
by FUNCT_4:80
.=
(((s +* (ProgramPart (Relocated (p,k)))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (ProgramPart p)
by A29, FUNCT_4:78
.=
((s +* (ProgramPart (Relocated (p,k)))) +* ((s | (dom (ProgramPart (Relocated (p,k))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA)))) +* (ProgramPart p)
by FUNCT_4:15
.=
((s +* (ProgramPart (Relocated (p,k)))) +* ((Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA)) +* (s | (dom (ProgramPart (Relocated (p,k))))))) +* (ProgramPart p)
by A32, FUNCT_4:36
.=
(((s +* (ProgramPart (Relocated (p,k)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by FUNCT_4:15
.=
((((s +* (DataPart p)) +* (ProgramPart (Relocated (p,k)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by A24, FUNCT_4:79
.=
(((((s +* (DataPart p)) +* (ProgramPart (Relocated (p,k)))) +* (Start-At (((IC p) + k),SCM+FSA))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by A31, A27, FUNCT_4:78
.=
((((s +* ((DataPart p) +* (ProgramPart (Relocated (p,k))))) +* (Start-At (((IC p) + k),SCM+FSA))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* (((DataPart p) +* (ProgramPart (Relocated (p,k)))) +* (Start-At (((IC p) + k),SCM+FSA)))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((DataPart p) +* ((ProgramPart (Relocated (p,k))) +* (Start-At (((IC p) + k),SCM+FSA))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((DataPart p) +* ((Start-At (((IC p) + k),SCM+FSA)) +* (ProgramPart (Relocated (p,k)))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by A27, COMPOS_1:14, FUNCT_4:36
.=
(((s +* (((DataPart p) +* (Start-At (((IC p) + k),SCM+FSA))) +* (ProgramPart (Relocated (p,k))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by FUNCT_4:15
.=
(((s +* ((IncrIC ((NPP p),k)) +* (ProgramPart (Relocated (p,k))))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by Z, COMPOS_1:75
.=
(((s +* (Relocated (p,k))) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by COMPOS_1:116
.=
(((Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0)) +* (Start-At (((IC (Comput ((ProgramPart (s +* (Relocated (p,k)))),(s +* (Relocated (p,k))),0))) -' k),SCM+FSA))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by EXTPRO_1:3
;
then A33:
S1[ 0 ]
;
thus
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A33, A5); verum