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 p being FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic )
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 p being FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic ) )
assume A1:
S is CurIns-recognized
; for p being FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic )
let p be FinPartState of S; ( IC in dom p implies for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic ) )
assume A2:
IC 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 )
RE:
Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k))
by COMPOS_1:116;
hereby ( Relocated (p,k) is autonomic implies p is autonomic )
assume A4:
p is
autonomic
;
Relocated (p,k) is autonomic thus
Relocated (
p,
k) is
autonomic
verumproof
let P,
Q be the
Instructions of
S -valued ManySortedSet of
NAT ;
EXTPRO_1:def 9 ( not ProgramPart (Relocated (p,k)) c= P or not ProgramPart (Relocated (p,k)) c= Q or for b1, b2 being set holds
( not Relocated (p,k) c= b1 or not Relocated (p,k) c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP (Relocated (p,k)))) = (Comput (Q,b2,b3)) | (proj1 (NPP (Relocated (p,k)))) ) )
assume that A5:
ProgramPart (Relocated (p,k)) c= P
and A6:
ProgramPart (Relocated (p,k)) c= Q
;
for b1, b2 being set holds
( not Relocated (p,k) c= b1 or not Relocated (p,k) c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP (Relocated (p,k)))) = (Comput (Q,b2,b3)) | (proj1 (NPP (Relocated (p,k)))) )
let s1,
s2 be
State of
S;
( not Relocated (p,k) c= s1 or not Relocated (p,k) c= s2 or for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP (Relocated (p,k)))) = (Comput (Q,s2,b1)) | (proj1 (NPP (Relocated (p,k)))) )
assume that A7:
Relocated (
p,
k)
c= s1
and A8:
Relocated (
p,
k)
c= s2
;
for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP (Relocated (p,k)))) = (Comput (Q,s2,b1)) | (proj1 (NPP (Relocated (p,k))))
let i be
Element of
NAT ;
(Comput (P,s1,i)) | (proj1 (NPP (Relocated (p,k)))) = (Comput (Q,s2,i)) | (proj1 (NPP (Relocated (p,k))))
A9:
Comput (
P,
s1,
i)
= ((IncIC ((Comput ((P +* (ProgramPart p)),(s1 +* p),i)),k)) +* (s1 | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A2, A4, A7, Th9, A1, A5, RE;
dom (ProgramPart p) c= the
carrier of
S
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s2
by PARTFUN1:def 4;
then A10:
dom (s2 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
dom (ProgramPart p) c= the
carrier of
S
by RELAT_1:def 18;
then
dom (ProgramPart p) c= dom s1
by PARTFUN1:def 4;
then A11:
dom (s1 | (dom (ProgramPart p))) = dom (ProgramPart p)
by RELAT_1:91;
A12:
dom (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S)) = {(IC )}
by FUNCOP_1:19;
then A13:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S))
by COMPOS_1:13;
A14:
dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S)) = {(IC )}
by FUNCOP_1:19;
then A15:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S))
by COMPOS_1:13;
A16:
Comput (
Q,
s2,
i)
= ((IncIC ((Comput ((Q +* (ProgramPart p)),(s2 +* p),i)),k)) +* (s2 | (dom (ProgramPart p)))) +* (Reloc ((ProgramPart p),k))
by A2, A4, A8, Th9, A1, A6, RE;
A17:
(
ProgramPart p c= P +* (ProgramPart p) &
ProgramPart p c= Q +* (ProgramPart p) )
by FUNCT_4:26;
(
p c= s1 +* p &
p c= s2 +* p )
by FUNCT_4:26;
then A18:
(Comput ((P +* (ProgramPart p)),(s1 +* p),i)) | (dom (NPP p)) = (Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) | (dom (NPP p))
by A4, EXTPRO_1:def 9, A17;
A19:
DataPart p c= NPP p
by COMPOS_1:169;
A20:
dom (DataPart p) misses dom (Reloc ((ProgramPart p),k))
by COMPOS_1:15, RE;
then A21:
(Comput (P,s1,i)) | (dom (DataPart p)) =
(((Comput ((P +* (ProgramPart p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S))) +* (s1 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A9, FUNCT_4:76
.=
((Comput ((P +* (ProgramPart p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S))) | (dom (DataPart p))
by A11, COMPOS_1:15, FUNCT_4:76
.=
(Comput ((P +* (ProgramPart p)),(s1 +* p),i)) | (dom (DataPart p))
by A15, FUNCT_4:76
.=
(Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) | (dom (DataPart p))
by A18, RELAT_1:188, A19, RELAT_1:25
.=
((Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S))) | (dom (DataPart p))
by A13, FUNCT_4:76
.=
(((Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S))) +* (s2 | (dom (ProgramPart p)))) | (dom (DataPart p))
by A10, COMPOS_1:15, FUNCT_4:76
.=
(Comput (Q,s2,i)) | (dom (DataPart p))
by A16, A20, FUNCT_4:76
;
IC in dom (NPP p)
by A2, COMPOS_1:179;
then A22:
{(IC )} c= dom (NPP p)
by ZFMISC_1:37;
A23:
Start-At (
(IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))),
S) =
(Comput ((P +* (ProgramPart p)),(s1 +* p),i)) | {(IC )}
by COMPOS_1:10
.=
(Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) | {(IC )}
by A18, A22, RELAT_1:188
.=
Start-At (
(IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))),
S)
by COMPOS_1:10
;
A24:
dom (Start-At (((IC p) + k),S)) = {(IC )}
by FUNCOP_1:19;
then A25:
dom (Start-At (((IC p) + k),S)) misses dom (Reloc ((ProgramPart p),k))
by COMPOS_1:14, RE;
then A26:
(Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S))) =
(((Comput ((P +* (ProgramPart p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S))) +* (s1 | (dom (ProgramPart p)))) | (dom (Start-At (((IC p) + k),S)))
by A9, FUNCT_4:76
.=
((Comput ((P +* (ProgramPart p)),(s1 +* p),i)) +* (Start-At (((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),S))) | (dom (Start-At (((IC p) + k),S)))
by A24, A11, COMPOS_1:14, FUNCT_4:76
.=
Start-At (
((IC (Comput ((P +* (ProgramPart p)),(s1 +* p),i))) + k),
S)
by A24, A14, FUNCT_4:24
.=
Start-At (
((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),
S)
by A23, COMPOS_1:43
.=
((Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S))) | (dom (Start-At (((IC p) + k),S)))
by A24, A12, FUNCT_4:24
.=
(((Comput ((Q +* (ProgramPart p)),(s2 +* p),i)) +* (Start-At (((IC (Comput ((Q +* (ProgramPart p)),(s2 +* p),i))) + k),S))) +* (s2 | (dom (ProgramPart p)))) | (dom (Start-At (((IC p) + k),S)))
by A24, A10, COMPOS_1:14, FUNCT_4:76
.=
(Comput (Q,s2,i)) | (dom (Start-At (((IC p) + k),S)))
by A16, A25, FUNCT_4:76
;
A27:
dom (Start-At (((IC p) + k),S)) = {(IC )}
by FUNCOP_1:19;
A28:
dom (NPP p) = {(IC )} \/ (dom (DataPart p))
by A2, COMPOS_1:70;
A29:
(Comput (P,s1,i)) | (dom (NPP p)) =
((Comput (P,s1,i)) | {(IC )}) \/ ((Comput (P,s1,i)) | (dom (DataPart p)))
by A28, RELAT_1:107
.=
(Comput (Q,s2,i)) | (dom (NPP p))
by A28, A27, A21, RELAT_1:107, A26
;
A30:
dom (IncIC ((NPP p),k)) =
(dom (NPP p)) \/ (dom (Start-At (((IC (NPP p)) + k),S)))
by FUNCT_4:def 1
.=
(dom (NPP p)) \/ (dom (Start-At (((IC p) + k),S)))
by A2, COMPOS_1:72
;
A31:
(Comput (P,s1,i)) | (dom (IncIC ((NPP p),k))) =
((Comput (P,s1,i)) | (dom (NPP p))) \/ ((Comput (P,s1,i)) | (dom (Start-At (((IC p) + k),S))))
by A30, RELAT_1:107
.=
(Comput (Q,s2,i)) | (dom (IncIC ((NPP p),k)))
by A30, RELAT_1:107, A26, A29
;
thus (Comput (P,s1,i)) | (dom (NPP (Relocated (p,k)))) =
(Comput (P,s1,i)) | (dom (IncIC ((NPP p),k)))
by COMPOS_1:180
.=
(Comput (Q,s2,i)) | (dom (NPP (Relocated (p,k))))
by A31, COMPOS_1:180
;
verum
end;
end;
assume A32:
Relocated (p,k) is autonomic
; p is autonomic
DataPart (Relocated (p,k)) c= NPP (Relocated (p,k))
by COMPOS_1:169;
then
DataPart p c= NPP (Relocated (p,k))
by COMPOS_1:115;
then A33:
dom (DataPart p) c= dom (NPP (Relocated (p,k)))
by GRFUNC_1:8;
let P, Q be the Instructions of S -valued ManySortedSet of NAT ; EXTPRO_1:def 9 ( not ProgramPart p c= P or not ProgramPart p c= Q or for b1, b2 being set holds
( not p c= b1 or not p c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP p)) = (Comput (Q,b2,b3)) | (proj1 (NPP p)) ) )
assume that
A34:
ProgramPart p c= P
and
A35:
ProgramPart p c= Q
; for b1, b2 being set holds
( not p c= b1 or not p c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP p)) = (Comput (Q,b2,b3)) | (proj1 (NPP p)) )
A36:
( Reloc ((ProgramPart p),k) c= P +* (Reloc ((ProgramPart p),k)) & Reloc ((ProgramPart p),k) c= Q +* (Reloc ((ProgramPart p),k)) )
by FUNCT_4:26;
let s1, s2 be State of S; ( not p c= s1 or not p c= s2 or for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP p)) = (Comput (Q,s2,b1)) | (proj1 (NPP p)) )
assume that
A37:
p c= s1
and
A38:
p c= s2
; for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP p)) = (Comput (Q,s2,b1)) | (proj1 (NPP p))
let i be Element of NAT ; (Comput (P,s1,i)) | (proj1 (NPP p)) = (Comput (Q,s2,i)) | (proj1 (NPP p))
A39:
Comput (Q,s2,i) = ((DecIC ((Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)),k)) +* (s2 | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A2, A32, A38, Th10, A1, A35;
dom (Reloc ((ProgramPart p),k)) c= the carrier of S
by RELAT_1:def 18;
then
dom (Reloc ((ProgramPart p),k)) c= dom s2
by PARTFUN1:def 4;
then A40:
dom (s2 | (dom (Reloc ((ProgramPart p),k)))) = dom (Reloc ((ProgramPart p),k))
by RELAT_1:91;
dom (Reloc ((ProgramPart p),k)) c= the carrier of S
by RELAT_1:def 18;
then
dom (Reloc ((ProgramPart p),k)) c= dom s1
by PARTFUN1:def 4;
then A41:
dom (s1 | (dom (Reloc ((ProgramPart p),k)))) = dom (Reloc ((ProgramPart p),k))
by RELAT_1:91;
A42:
Comput (P,s1,i) = ((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)),k)) +* (s1 | (dom (Reloc ((ProgramPart p),k))))) +* (ProgramPart p)
by A2, A32, A37, Th10, A1, A34;
( Relocated (p,k) c= s1 +* (Relocated (p,k)) & Relocated (p,k) c= s2 +* (Relocated (p,k)) )
by FUNCT_4:26;
then A43:
(Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)) | (dom (NPP (Relocated (p,k)))) = (Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)) | (dom (NPP (Relocated (p,k))))
by A32, EXTPRO_1:def 9, A36, RE;
A44:
dom (Start-At (((IC (Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i))) -' k),S)) = {(IC )}
by FUNCOP_1:19;
then A45:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i))) -' k),S))
by COMPOS_1:13;
A46:
dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i))) -' k),S)) = {(IC )}
by FUNCOP_1:19;
then A47:
dom (DataPart p) misses dom (Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i))) -' k),S))
by COMPOS_1:13;
A48:
dom (DataPart p) misses dom (ProgramPart p)
by COMPOS_1:15;
then A49: (Comput (P,s1,i)) | (dom (DataPart p)) =
((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)),k)) +* (s1 | (dom (Reloc ((ProgramPart p),k))))) | (dom (DataPart p))
by A42, FUNCT_4:76
.=
(DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)),k)) | (dom (DataPart p))
by A41, COMPOS_1:15, FUNCT_4:76, RE
.=
(Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)) | (dom (DataPart p))
by A47, FUNCT_4:76
.=
(Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)) | (dom (DataPart p))
by A43, A33, RELAT_1:188
.=
(DecIC ((Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)),k)) | (dom (DataPart p))
by A45, FUNCT_4:76
.=
((DecIC ((Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)),k)) +* (s2 | (dom (Reloc ((ProgramPart p),k))))) | (dom (DataPart p))
by A40, COMPOS_1:15, FUNCT_4:76, RE
.=
(Comput (Q,s2,i)) | (dom (DataPart p))
by A39, A48, FUNCT_4:76
;
IC in dom (Relocated (p,k))
by COMPOS_1:119;
then
IC in dom (NPP (Relocated (p,k)))
by COMPOS_1:179;
then A50:
{(IC )} c= dom (NPP (Relocated (p,k)))
by ZFMISC_1:37;
A51: Start-At ((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i))),S) =
(Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)) | {(IC )}
by COMPOS_1:10
.=
(Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)) | {(IC )}
by A43, A50, RELAT_1:188
.=
Start-At ((IC (Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i))),S)
by COMPOS_1:10
;
A52:
dom (Start-At ((IC p),S)) = {(IC )}
by FUNCOP_1:19;
then A53:
dom (Start-At ((IC p),S)) misses dom (ProgramPart p)
by COMPOS_1:14;
then A54: (Comput (P,s1,i)) | (dom (Start-At ((IC p),S))) =
((DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)),k)) +* (s1 | (dom (Reloc ((ProgramPart p),k))))) | (dom (Start-At ((IC p),S)))
by A42, FUNCT_4:76
.=
(DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i)),k)) | (dom (Start-At ((IC p),S)))
by A52, A41, COMPOS_1:14, FUNCT_4:76, RE
.=
Start-At (((IC (Comput ((P +* (Reloc ((ProgramPart p),k))),(s1 +* (Relocated (p,k))),i))) -' k),S)
by A52, A46, FUNCT_4:24
.=
Start-At (((IC (Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i))) -' k),S)
by A51, COMPOS_1:44
.=
(DecIC ((Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)),k)) | (dom (Start-At ((IC p),S)))
by A52, A44, FUNCT_4:24
.=
((DecIC ((Comput ((Q +* (Reloc ((ProgramPart p),k))),(s2 +* (Relocated (p,k))),i)),k)) +* (s2 | (dom (Reloc ((ProgramPart p),k))))) | (dom (Start-At ((IC p),S)))
by A52, A40, COMPOS_1:14, FUNCT_4:76, RE
.=
(Comput (Q,s2,i)) | (dom (Start-At ((IC p),S)))
by A39, A53, FUNCT_4:76
;
thus (Comput (P,s1,i)) | (dom (NPP p)) =
(Comput (P,s1,i)) | (dom ((Start-At ((IC p),S)) +* (DataPart p)))
by A2, COMPOS_1:181
.=
(Comput (P,s1,i)) | ((dom (Start-At ((IC p),S))) \/ (dom (DataPart p)))
by FUNCT_4:def 1
.=
((Comput (Q,s2,i)) | (dom (Start-At ((IC p),S)))) \/ ((Comput (Q,s2,i)) | (dom (DataPart p)))
by A49, A54, RELAT_1:107
.=
(Comput (Q,s2,i)) | ((dom (Start-At ((IC p),S))) \/ (dom (DataPart p)))
by RELAT_1:107
.=
(Comput (Q,s2,i)) | (dom ((Start-At ((IC p),S)) +* (DataPart p)))
by FUNCT_4:def 1
.=
(Comput (Q,s2,i)) | (dom (NPP p))
by A2, COMPOS_1:181
; verum