let k be Element of NAT ; :: thesis: for R being good Ring
for p being FinPartState of (SCM R) st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated (p,k) is autonomic )
let R be good Ring; :: thesis: for p being FinPartState of (SCM R) st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated (p,k) is autonomic )
let p be FinPartState of (SCM R); :: thesis: ( not R is trivial & IC (SCM R) in dom p implies ( p is autonomic iff Relocated (p,k) is autonomic ) )
assume that
A1: not R is trivial and
A2: IC (SCM R) in dom p ; :: thesis: ( p is autonomic iff Relocated (p,k) is autonomic )

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

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