let p be FinPartState of SCM+FSA; :: thesis: ( 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 ; :: thesis: for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic )
let k be Element of NAT ; :: thesis: ( p is autonomic iff Relocated (p,k) is autonomic )

hereby :: thesis: ( Relocated (p,k) is autonomic implies p is autonomic )

assume A2: p is autonomic ; :: thesis: Relocated (p,k) is autonomic
thus Relocated (p,k) is autonomic :: thesis: verum

proof

let s1, s2 be State of SCM+FSA; :: according to EXTPRO_1:def 9 :: thesis: ( not Relocated (p,k) c= s1 or not Relocated (p,k) c= s2 or for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 (Relocated (p,k))) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 (Relocated (p,k))) )
assume that
A3: Relocated (p,k) c= s1 and
A4: Relocated (p,k) c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 (Relocated (p,k))) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 (Relocated (p,k)))
let i be Element of NAT ; :: thesis: (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, EXTPRO_1:def 9;
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 COMPOS_1:116
.= 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 COMPOS_1:116 ;
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 ;
:: thesis: verum

end;

end;

assume A25: Relocated (p,k) is autonomic ; :: thesis: p is autonomic
thus p is autonomic :: thesis: verum

proof

DataPart (Relocated (p,k)) c= Relocated (p,k) by RELAT_1:88;
then DataPart p c= Relocated (p,k) by COMPOS_1:115;
then A26: dom (DataPart p) c= dom (Relocated (p,k)) by GRFUNC_1:8;
let s1, s2 be State of SCM+FSA; :: according to EXTPRO_1:def 9 :: thesis: ( not p c= s1 or not p c= s2 or for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 p) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 p) )
assume that
A27: p c= s1 and
A28: p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 p) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 p)
let i be Element of NAT ; :: thesis: (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, EXTPRO_1:def 9;
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 COMPOS_1:119;
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 ; :: thesis: verum

end;