let p be FinPartState of SCM; ( IC SCM in dom p implies for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic ) )
assume A1:
IC SCM 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;
EXTPRO_1:def 9 ( 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))) +* (s1 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A1, A2, A3, Th39;
dom (ProgramPart p) c= the
carrier of
SCM
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s2
by PARTFUN1:def 4;
then A6:
dom (s2 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
dom (ProgramPart p) c= the
carrier of
SCM
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s1
by PARTFUN1:def 4;
then A7:
dom (s1 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
A8:
dom (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A9:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))
by COMPOS_1:13;
A10:
dom (Start-At (((IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))) + k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A11:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))) + k),SCM))
by COMPOS_1:13;
A12:
Comput (
(ProgramPart s2),
s2,
i)
= (((Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))) +* (s2 | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))
by A1, A2, A4, Th39;
A13:
(Comput ((ProgramPart s1),s1,i)) | (dom (Reloc ((ProgramPart p),k))) =
(Comput ((ProgramPart s1),s1,i)) | (dom (ProgramPart (Relocated (p,k))))
by COMPOS_1:116
.=
ProgramPart (Relocated (p,k))
by A5, FUNCT_4:24
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (ProgramPart (Relocated (p,k))))
by A12, FUNCT_4:24
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (Reloc ((ProgramPart p),k)))
by COMPOS_1:116
;
DataPart p c= p
by RELAT_1:88;
then A14:
dom (DataPart p) c= dom p
by GRFUNC_1:8;
(
p c= s1 +* p &
p c= s2 +* p )
by FUNCT_4:26;
then A15:
(Comput ((ProgramPart (s1 +* p)),(s1 +* p),i)) | (dom p) = (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) | (dom p)
by A2, EXTPRO_1:def 9;
A16:
dom (DataPart p) misses dom (ProgramPart (Relocated (p,k)))
by COMPOS_1:15;
then A17:
(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))) +* (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))) | (dom (DataPart p))
by A7, COMPOS_1:15, FUNCT_4:76
.=
(Comput ((ProgramPart (s1 +* p)),(s1 +* p),i)) | (dom (DataPart p))
by A11, FUNCT_4:76
.=
(Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) | (dom (DataPart p))
by A15, A14, RELAT_1:188
.=
((Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))) | (dom (DataPart p))
by A9, FUNCT_4:76
.=
(((Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))) +* (s2 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A6, COMPOS_1:15, FUNCT_4:76
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (DataPart p))
by A12, A16, FUNCT_4:76
;
A18:
{(IC SCM)} c= dom p
by A1, ZFMISC_1:37;
A19:
Start-At (
(IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))),
SCM) =
(Comput ((ProgramPart (s1 +* p)),(s1 +* p),i)) | {(IC SCM)}
by COMPOS_1:10
.=
(Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) | {(IC SCM)}
by A15, A18, RELAT_1:188
.=
Start-At (
(IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))),
SCM)
by COMPOS_1:10
;
A20:
dom (Start-At (((IC p) + k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A21:
dom (Start-At (((IC p) + k),SCM)) misses dom (ProgramPart (Relocated (p,k)))
by COMPOS_1:14;
then A22:
(Comput ((ProgramPart s1),s1,i)) | (dom (Start-At (((IC p) + k),SCM))) =
(((Comput ((ProgramPart (s1 +* p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))) + k),SCM))) +* (s1 | (dom (ProgramPart p)))) | (dom (Start-At (((IC p) + k),SCM)))
by A5, FUNCT_4:76
.=
((Comput ((ProgramPart (s1 +* p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))) + k),SCM))) | (dom (Start-At (((IC p) + k),SCM)))
by A20, A7, COMPOS_1:14, FUNCT_4:76
.=
Start-At (
((IC (Comput ((ProgramPart (s1 +* p)),(s1 +* p),i))) + k),
SCM)
by A20, A10, FUNCT_4:24
.=
Start-At (
((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),
SCM)
by A19, COMPOS_1:43
.=
((Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))) | (dom (Start-At (((IC p) + k),SCM)))
by A20, A8, FUNCT_4:24
.=
(((Comput ((ProgramPart (s2 +* p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s2 +* p)),(s2 +* p),i))) + k),SCM))) +* (s2 | (dom (ProgramPart p)))) | (dom (Start-At (((IC p) + k),SCM)))
by A20, A6, COMPOS_1:14, FUNCT_4:76
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (Start-At (((IC p) + k),SCM)))
by A12, A21, FUNCT_4:76
;
U1:
dom (Start-At (((IC p) + k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
U:
dom (NPP p) = {(IC SCM)} \/ (dom (DataPart p))
by A1, COMPOS_1:70;
Y1:
(Comput ((ProgramPart s1),s1,i)) | (dom (NPP p)) =
((Comput ((ProgramPart s1),s1,i)) | {(IC SCM)}) \/ ((Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)))
by U, RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (NPP p))
by U, U1, A17, RELAT_1:107, A22
;
Y:
dom (IncrIC ((NPP p),k)) =
(dom (NPP p)) \/ (dom (Start-At (((IC (NPP p)) + k),SCM)))
by FUNCT_4:def 1
.=
(dom (NPP p)) \/ (dom (Start-At (((IC p) + k),SCM)))
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))))
by Y, RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (IncrIC ((NPP p),k)))
by Y, Y1, A22, 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, A13, X, RELAT_1:107
;
verum
end;
end;
assume A24:
Relocated (p,k) is autonomic
; p is autonomic
DataPart (Relocated (p,k)) c= Relocated (p,k)
by RELAT_1:88;
then
DataPart p c= Relocated (p,k)
by COMPOS_1:115;
then A25:
dom (DataPart p) c= dom (Relocated (p,k))
by GRFUNC_1:8;
let s1, s2 be State of SCM; EXTPRO_1:def 9 ( 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
A26:
p c= s1
and
A27:
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)
A28:
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))) +* (s2 | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by A1, A24, A27, Th40;
dom (ProgramPart (Relocated (p,k))) c= the carrier of SCM
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated (p,k))) c= dom s2
by PARTFUN1:def 4;
then A29:
dom (s2 | (dom (ProgramPart (Relocated (p,k))))) = dom (ProgramPart (Relocated (p,k)))
by RELAT_1:91;
dom (ProgramPart (Relocated (p,k))) c= the carrier of SCM
by RELAT_1:def 18;
then
dom (ProgramPart (Relocated (p,k))) c= dom s1
by PARTFUN1:def 4;
then A30:
dom (s1 | (dom (ProgramPart (Relocated (p,k))))) = dom (ProgramPart (Relocated (p,k)))
by RELAT_1:91;
A31:
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))) +* (s1 | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)
by A1, A24, A26, Th40;
then A32: (Comput ((ProgramPart s1),s1,i)) | (dom (ProgramPart p)) =
ProgramPart p
by FUNCT_4:24
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (ProgramPart p))
by A28, FUNCT_4:24
;
( Relocated (p,k) c= s1 +* (Relocated (p,k)) & Relocated (p,k) c= s2 +* (Relocated (p,k)) )
by FUNCT_4:26;
then A33:
(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 A24, EXTPRO_1:def 9;
A34:
dom (Start-At (((IC (Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i))) -' k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A35:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i))) -' k),SCM))
by COMPOS_1:13;
A36:
dom (Start-At (((IC (Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i))) -' k),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A37:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i))) -' k),SCM))
by COMPOS_1:13;
A38:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
then A39: (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))) +* (s1 | (dom (ProgramPart (Relocated (p,k)))))) | (dom (DataPart p))
by A31, 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))) | (dom (DataPart p))
by A30, COMPOS_1:15, FUNCT_4:76
.=
(Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i)) | (dom (DataPart p))
by A37, FUNCT_4:76
.=
(Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i)) | (dom (DataPart p))
by A33, A25, 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))) | (dom (DataPart p))
by A35, 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))) +* (s2 | (dom (ProgramPart (Relocated (p,k)))))) | (dom (DataPart p))
by A29, COMPOS_1:15, FUNCT_4:76
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (DataPart p))
by A28, A38, FUNCT_4:76
;
IC SCM in dom (Relocated (p,k))
by COMPOS_1:119;
then A40:
{(IC SCM)} c= dom (Relocated (p,k))
by ZFMISC_1:37;
A41: Start-At ((IC (Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i))),SCM) =
(Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i)) | {(IC SCM)}
by COMPOS_1:10
.=
(Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i)) | {(IC SCM)}
by A33, A40, RELAT_1:188
.=
Start-At ((IC (Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i))),SCM)
by COMPOS_1:10
;
A42:
dom (Start-At ((IC p),SCM)) = {(IC SCM)}
by FUNCOP_1:19;
then A43:
dom (Start-At ((IC p),SCM)) misses dom (ProgramPart p)
by COMPOS_1:14;
then A44: (Comput ((ProgramPart s1),s1,i)) | (dom (Start-At ((IC p),SCM))) =
(((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))) +* (s1 | (dom (ProgramPart (Relocated (p,k)))))) | (dom (Start-At ((IC p),SCM)))
by A31, 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))) | (dom (Start-At ((IC p),SCM)))
by A42, A30, COMPOS_1:14, FUNCT_4:76
.=
Start-At (((IC (Comput ((ProgramPart (s1 +* (Relocated (p,k)))),(s1 +* (Relocated (p,k))),i))) -' k),SCM)
by A42, A36, FUNCT_4:24
.=
Start-At (((IC (Comput ((ProgramPart (s2 +* (Relocated (p,k)))),(s2 +* (Relocated (p,k))),i))) -' k),SCM)
by A41, 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))) | (dom (Start-At ((IC p),SCM)))
by A42, A34, 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))) +* (s2 | (dom (ProgramPart (Relocated (p,k)))))) | (dom (Start-At ((IC p),SCM)))
by A42, A29, COMPOS_1:14, FUNCT_4:76
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (Start-At ((IC p),SCM)))
by A28, A43, FUNCT_4:76
;
A45: (Comput ((ProgramPart s1),s1,i)) | (dom ((Start-At ((IC p),SCM)) +* (ProgramPart p))) =
(Comput ((ProgramPart s1),s1,i)) | ((dom (Start-At ((IC p),SCM))) \/ (dom (ProgramPart p)))
by FUNCT_4:def 1
.=
((Comput ((ProgramPart s2),s2,i)) | (dom (Start-At ((IC p),SCM)))) \/ ((Comput ((ProgramPart s2),s2,i)) | (dom (ProgramPart p)))
by A44, A32, RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | ((dom (Start-At ((IC p),SCM))) \/ (dom (ProgramPart p)))
by RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | (dom ((Start-At ((IC p),SCM)) +* (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)) +* (ProgramPart p)) +* (DataPart p)))
by A1, COMPOS_1:18
.=
(Comput ((ProgramPart s1),s1,i)) | ((dom ((Start-At ((IC p),SCM)) +* (ProgramPart p))) \/ (dom (DataPart p)))
by FUNCT_4:def 1
.=
((Comput ((ProgramPart s2),s2,i)) | (dom ((Start-At ((IC p),SCM)) +* (ProgramPart p)))) \/ ((Comput ((ProgramPart s2),s2,i)) | (dom (DataPart p)))
by A39, A45, RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | ((dom ((Start-At ((IC p),SCM)) +* (ProgramPart p))) \/ (dom (DataPart p)))
by RELAT_1:107
.=
(Comput ((ProgramPart s2),s2,i)) | (dom (((Start-At ((IC p),SCM)) +* (ProgramPart p)) +* (DataPart p)))
by FUNCT_4:def 1
.=
(Comput ((ProgramPart s2),s2,i)) | (dom p)
by A1, COMPOS_1:18
; verum