let p be FinPartState of SCM+FSA ; ( IC SCM+FSA in dom p implies for k being Element of NAT holds
( p is autonomic iff Relocated p,k is autonomic ) )
assume A1:
IC SCM+FSA in dom p
; for k being Element of NAT holds
( p is autonomic iff Relocated p,k is autonomic )
let k be Element of NAT ; ( p is autonomic iff Relocated p,k is autonomic )
hereby ( Relocated p,k is autonomic implies p is autonomic )
assume A2:
p is
autonomic
;
Relocated p,k is autonomic thus
Relocated p,
k is
autonomic
verumproof
let s1,
s2 be
State of
SCM+FSA ;
AMI_1:def 25 ( not Relocated p,k c= s1 or not Relocated p,k c= s2 or for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,b1) | (proj1 (Relocated p,k)) )
assume that A3:
Relocated p,
k c= s1
and A4:
Relocated p,
k c= s2
;
for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,b1) | (proj1 (Relocated p,k))
let i be
Element of
NAT ;
(Comput (ProgramPart s1),s1,i) | (proj1 (Relocated p,k)) = (Comput (ProgramPart s2),s2,i) | (proj1 (Relocated p,k))
A5:
Comput (ProgramPart s1),
s1,
i = (((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )) +* (s1 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A1, A2, A3, Th14;
A6:
p c= s2 +* p
by FUNCT_4:26;
p c= s1 +* p
by FUNCT_4:26;
then A7:
(Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | (dom p) = (Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | (dom p)
by A2, A6, AMI_1:def 25;
dom (ProgramPart p) c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s2
by PARTFUN1:def 4;
then A8:
dom (s2 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
A9:
dom (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A10:
dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )
by COMPOS_1:13;
A11:
dom (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A12:
dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )
by COMPOS_1:13;
A13:
Comput (ProgramPart s2),
s2,
i = (((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )) +* (s2 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
by A1, A2, A4, Th14;
A14:
(Comput (ProgramPart s1),s1,i) | (dom (Reloc (ProgramPart p),k)) =
(Comput (ProgramPart s1),s1,i) | (dom (ProgramPart (Relocated p,k)))
by AMISTD_2:69
.=
ProgramPart (Relocated p,k)
by A5, FUNCT_4:24
.=
(Comput (ProgramPart s2),s2,i) | (dom (ProgramPart (Relocated p,k)))
by A13, FUNCT_4:24
.=
(Comput (ProgramPart s2),s2,i) | (dom (Reloc (ProgramPart p),k))
by AMISTD_2:69
;
DataPart p c= p
by RELAT_1:88;
then A15:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
dom (ProgramPart p) c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s1
by PARTFUN1:def 4;
then A16:
dom (s1 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
A17:
dom (DataPart p) misses dom (ProgramPart (Relocated p,k))
by COMPOS_1:15;
then A18:
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) =
(((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )) +* (s1 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A5, FUNCT_4:76
.=
((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )) | (dom (DataPart p))
by A16, COMPOS_1:15, FUNCT_4:76
.=
(Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | (dom (DataPart p))
by A12, FUNCT_4:76
.=
(Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | (dom (DataPart p))
by A7, A15, RELAT_1:188
.=
((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )) | (dom (DataPart p))
by A10, FUNCT_4:76
.=
(((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )) +* (s2 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A8, COMPOS_1:15, FUNCT_4:76
.=
(Comput (ProgramPart s2),s2,i) | (dom (DataPart p))
by A13, A17, FUNCT_4:76
;
A19:
{(IC SCM+FSA )} c= dom p
by A1, ZFMISC_1:37;
A20:
Start-At (IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)),
SCM+FSA =
(Comput (ProgramPart (s1 +* p)),(s1 +* p),i) | {(IC SCM+FSA )}
by COMPOS_1:10
.=
(Comput (ProgramPart (s2 +* p)),(s2 +* p),i) | {(IC SCM+FSA )}
by A7, A19, RELAT_1:188
.=
Start-At (IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)),
SCM+FSA
by COMPOS_1:10
;
A21:
dom (Start-At ((IC p) + k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A22:
dom (Start-At ((IC p) + k),SCM+FSA ) misses dom (ProgramPart (Relocated p,k))
by COMPOS_1:14;
then A23:
(Comput (ProgramPart s1),s1,i) | (dom (Start-At ((IC p) + k),SCM+FSA )) =
(((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )) +* (s1 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k),SCM+FSA ))
by A5, FUNCT_4:76
.=
((Comput (ProgramPart (s1 +* p)),(s1 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),SCM+FSA )) | (dom (Start-At ((IC p) + k),SCM+FSA ))
by A21, A16, COMPOS_1:14, FUNCT_4:76
.=
Start-At ((IC (Comput (ProgramPart (s1 +* p)),(s1 +* p),i)) + k),
SCM+FSA
by A21, A11, FUNCT_4:24
.=
Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),
SCM+FSA
by A20, COMPOS_1:43
.=
((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )) | (dom (Start-At ((IC p) + k),SCM+FSA ))
by A21, A9, FUNCT_4:24
.=
(((Comput (ProgramPart (s2 +* p)),(s2 +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* p)),(s2 +* p),i)) + k),SCM+FSA )) +* (s2 | (dom (ProgramPart p)))) | (dom (Start-At ((IC p) + k),SCM+FSA ))
by A21, A8, COMPOS_1:14, FUNCT_4:76
.=
(Comput (ProgramPart s2),s2,i) | (dom (Start-At ((IC p) + k),SCM+FSA ))
by A13, A22, FUNCT_4:76
;
U2:
dom (Start-At ((IC p) + k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
U:
dom (NPP p) = {(IC SCM+FSA )} \/ (dom (DataPart p))
by A1, COMPOS_1:70;
Y1:
(Comput (ProgramPart s1),s1,i) | (dom (NPP p)) =
((Comput (ProgramPart s1),s1,i) | {(IC SCM+FSA )}) \/ ((Comput (ProgramPart s1),s1,i) | (dom (DataPart p)))
by U, RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | (dom (NPP p))
by U, U2, A23, A18, RELAT_1:107
;
Y:
dom (IncrIC (NPP p),k) =
(dom (NPP p)) \/ (dom (Start-At ((IC (NPP p)) + k),SCM+FSA ))
by FUNCT_4:def 1
.=
(dom (NPP p)) \/ (dom (Start-At ((IC p) + k),SCM+FSA ))
by A1, COMPOS_1:72
;
X1:
(Comput (ProgramPart s1),s1,i) | (dom (IncrIC (NPP p),k)) =
((Comput (ProgramPart s1),s1,i) | (dom (NPP p))) \/ ((Comput (ProgramPart s1),s1,i) | (dom (Start-At ((IC p) + k),SCM+FSA )))
by Y, RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | (dom (IncrIC (NPP p),k))
by Y, Y1, A23, RELAT_1:107
;
X:
dom (Relocated p,k) = (dom (IncrIC (NPP p),k)) \/ (dom (Reloc (ProgramPart p),k))
by FUNCT_4:def 1;
hence (Comput (ProgramPart s1),s1,i) | (dom (Relocated p,k)) =
((Comput (ProgramPart s1),s1,i) | (dom (IncrIC (NPP p),k))) \/ ((Comput (ProgramPart s1),s1,i) | (dom (Reloc (ProgramPart p),k)))
by RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | (dom (Relocated p,k))
by X1, A14, X, RELAT_1:107
;
verum
end;
end;
assume A25:
Relocated p,k is autonomic
; p is autonomic
thus
p is autonomic
verumproof
DataPart (Relocated p,k) c= Relocated p,
k
by RELAT_1:88;
then
DataPart p c= Relocated p,
k
by AMISTD_2:68;
then A26:
dom (DataPart p) c= dom (Relocated p,k)
by GRFUNC_1:8;
let s1,
s2 be
State of
SCM+FSA ;
AMI_1:def 25 ( not p c= s1 or not p c= s2 or for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 p) = (Comput (ProgramPart s2),s2,b1) | (proj1 p) )
assume that A27:
p c= s1
and A28:
p c= s2
;
for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 p) = (Comput (ProgramPart s2),s2,b1) | (proj1 p)
let i be
Element of
NAT ;
(Comput (ProgramPart s1),s1,i) | (proj1 p) = (Comput (ProgramPart s2),s2,i) | (proj1 p)
A29:
Comput (ProgramPart s2),
s2,
i = (((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s2 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A1, A25, A28, Th15;
A30:
Comput (ProgramPart s1),
s1,
i = (((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s1 | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
by A1, A25, A27, Th15;
then A31:
(Comput (ProgramPart s1),s1,i) | (dom (ProgramPart p)) =
ProgramPart p
by FUNCT_4:24
.=
(Comput (ProgramPart s2),s2,i) | (dom (ProgramPart p))
by A29, FUNCT_4:24
;
dom (ProgramPart (Relocated p,k)) c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated p,k)) c= dom s1
by PARTFUN1:def 4;
then A32:
dom (s1 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k))
by RELAT_1:91;
A33:
Relocated p,
k c= s2 +* (Relocated p,k)
by FUNCT_4:26;
Relocated p,
k c= s1 +* (Relocated p,k)
by FUNCT_4:26;
then A34:
(Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | (dom (Relocated p,k)) = (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | (dom (Relocated p,k))
by A25, A33, AMI_1:def 25;
dom (ProgramPart (Relocated p,k)) c= the
carrier of
SCM+FSA
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated p,k)) c= dom s2
by PARTFUN1:def 4;
then A35:
dom (s2 | (dom (ProgramPart (Relocated p,k)))) = dom (ProgramPart (Relocated p,k))
by RELAT_1:91;
A36:
dom (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A37:
dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )
by COMPOS_1:13;
A38:
dom (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A39:
dom (DataPart p) misses dom (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )
by COMPOS_1:13;
A40:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
then A41:
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) =
(((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p))
by A30, FUNCT_4:76
.=
((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )) | (dom (DataPart p))
by A32, COMPOS_1:15, FUNCT_4:76
.=
(Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | (dom (DataPart p))
by A39, FUNCT_4:76
.=
(Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | (dom (DataPart p))
by A34, A26, RELAT_1:188
.=
((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )) | (dom (DataPart p))
by A37, FUNCT_4:76
.=
(((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (DataPart p))
by A35, COMPOS_1:15, FUNCT_4:76
.=
(Comput (ProgramPart s2),s2,i) | (dom (DataPart p))
by A29, A40, FUNCT_4:76
;
IC SCM+FSA in dom (Relocated p,k)
by AMISTD_2:72;
then A42:
{(IC SCM+FSA )} c= dom (Relocated p,k)
by ZFMISC_1:37;
A43:
Start-At (IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)),
SCM+FSA =
(Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) | {(IC SCM+FSA )}
by COMPOS_1:10
.=
(Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) | {(IC SCM+FSA )}
by A34, A42, RELAT_1:188
.=
Start-At (IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)),
SCM+FSA
by COMPOS_1:10
;
A44:
dom (Start-At (IC p),SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A45:
dom (Start-At (IC p),SCM+FSA ) misses dom (ProgramPart p)
by COMPOS_1:14;
then A46:
(Comput (ProgramPart s1),s1,i) | (dom (Start-At (IC p),SCM+FSA )) =
(((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s1 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p),SCM+FSA ))
by A30, FUNCT_4:76
.=
((Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),SCM+FSA )) | (dom (Start-At (IC p),SCM+FSA ))
by A44, A32, COMPOS_1:14, FUNCT_4:76
.=
Start-At ((IC (Comput (ProgramPart (s1 +* (Relocated p,k))),(s1 +* (Relocated p,k)),i)) -' k),
SCM+FSA
by A44, A38, FUNCT_4:24
.=
Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),
SCM+FSA
by A43, COMPOS_1:44
.=
((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )) | (dom (Start-At (IC p),SCM+FSA ))
by A44, A36, FUNCT_4:24
.=
(((Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s2 +* (Relocated p,k))),(s2 +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s2 | (dom (ProgramPart (Relocated p,k))))) | (dom (Start-At (IC p),SCM+FSA ))
by A44, A35, COMPOS_1:14, FUNCT_4:76
.=
(Comput (ProgramPart s2),s2,i) | (dom (Start-At (IC p),SCM+FSA ))
by A29, A45, FUNCT_4:76
;
A47:
(Comput (ProgramPart s1),s1,i) | (dom ((Start-At (IC p),SCM+FSA ) +* (ProgramPart p))) =
(Comput (ProgramPart s1),s1,i) | ((dom (Start-At (IC p),SCM+FSA )) \/ (dom (ProgramPart p)))
by FUNCT_4:def 1
.=
((Comput (ProgramPart s2),s2,i) | (dom (Start-At (IC p),SCM+FSA ))) \/ ((Comput (ProgramPart s2),s2,i) | (dom (ProgramPart p)))
by A46, A31, RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | ((dom (Start-At (IC p),SCM+FSA )) \/ (dom (ProgramPart p)))
by RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | (dom ((Start-At (IC p),SCM+FSA ) +* (ProgramPart p)))
by FUNCT_4:def 1
;
thus (Comput (ProgramPart s1),s1,i) | (dom p) =
(Comput (ProgramPart s1),s1,i) | (dom (((Start-At (IC p),SCM+FSA ) +* (ProgramPart p)) +* (DataPart p)))
by A1, COMPOS_1:18
.=
(Comput (ProgramPart s1),s1,i) | ((dom ((Start-At (IC p),SCM+FSA ) +* (ProgramPart p))) \/ (dom (DataPart p)))
by FUNCT_4:def 1
.=
((Comput (ProgramPart s2),s2,i) | (dom ((Start-At (IC p),SCM+FSA ) +* (ProgramPart p)))) \/ ((Comput (ProgramPart s2),s2,i) | (dom (DataPart p)))
by A41, A47, RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | ((dom ((Start-At (IC p),SCM+FSA ) +* (ProgramPart p))) \/ (dom (DataPart p)))
by RELAT_1:107
.=
(Comput (ProgramPart s2),s2,i) | (dom (((Start-At (IC p),SCM+FSA ) +* (ProgramPart p)) +* (DataPart p)))
by FUNCT_4:def 1
.=
(Comput (ProgramPart s2),s2,i) | (dom p)
by A1, COMPOS_1:18
;
verum
end;