let k be Element of NAT ; :: thesis:
let R be non trivial good Ring; :: thesis:
let l be Element of NAT ; :: thesis:
let p be l -started non program-free autonomic halting FinPartState of (SCM R); :: thesis:
let F be PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)); :: thesis:
assume that
A2: IC (SCM R) in dom p and
A3: F is data-only ; :: thesis:

hereby :: thesis:

assume A4: ProgramPart p,p computes F ; :: thesis:
thus ProgramPart (Relocated (p,k)), Relocated (p,k) computes F :: thesis:

let x be set ; :: according to EXTPRO_1:def 13 :: thesis:
assume A5: x in dom F ; :: thesis:
then consider d1 being FinPartState of (SCM R) such that
A6: x = d1 and
A7: p +* d1 is Autonomy of ProgramPart p and
A8: F . d1 c= Result ((ProgramPart p),(p +* d1)) by A4, EXTPRO_1:def 13;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider d = x as FinPartState of (SCM R) by A5, COMPOS_1:25;
reconsider d = d as data-only FinPartState of (SCM R) by A3, A5, COMPOS_1:def 24;
X: Relocated ((p +* d),k) = (Relocated (p,k)) +* d by COMPOS_1:124;
xx: dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
y: ProgramPart ((Relocated (p,k)) +* d) = ProgramPart (Relocated (p,k)) by xx, FUNCT_4:76;
dom (ProgramPart p) c= NAT by RELAT_1:87;
then XX: dom d misses dom (ProgramPart p) by xx, XBOOLE_1:63;
(p +* d) +* (ProgramPart p) = p +* (d +* (ProgramPart p)) by FUNCT_4:15
.= p +* ((ProgramPart p) +* d) by XX, FUNCT_4:36
.= (p +* (ProgramPart p)) +* d by FUNCT_4:15
.= p +* d by FUNCT_4:80 ;
then B10: ( p +* d1 is halting & p +* d1 is autonomic ) by A6, A7, EXTPRO_1:def 11;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A9: IC (SCM R) in dom (p +* d) by A2, XBOOLE_0:def 3;
then A10: DataPart (Result ((ProgramPart p),(p +* d1))) = DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d))) by B10, A6, Th41, x, X, y;
reconsider Fd1 = F . d1 as FinPartState of (SCM R) by A8;
take d ; :: thesis:
thus x = d ; :: thesis:
dom (ProgramPart (Relocated (p,k))) c= NAT by RELAT_1:87;
then VV: dom d misses dom (ProgramPart (Relocated (p,k))) by xx, XBOOLE_1:63;
YY: ((Relocated (p,k)) +* d) +* (ProgramPart (Relocated (p,k))) = (Relocated (p,k)) +* (d +* (ProgramPart (Relocated (p,k)))) by FUNCT_4:15
.= (Relocated (p,k)) +* ((ProgramPart (Relocated (p,k))) +* d) by VV, FUNCT_4:36
.= ((Relocated (p,k)) +* (ProgramPart (Relocated (p,k)))) +* d by FUNCT_4:15
.= (Relocated (p,k)) +* d by FUNCT_4:80 ;
(Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
then ( (Relocated (p,k)) +* d is halting & (Relocated (p,k)) +* d is autonomic ) by B10, A6, A9, Th40;
hence (Relocated (p,k)) +* d is Autonomy of ProgramPart (Relocated (p,k)) by YY, EXTPRO_1:def 11; :: thesis:
A11: Fd1 is data-only by A3, A5, A6, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((ProgramPart p),(p +* d1))) by A8, COMPOS_1:17;
hence F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d)) by A6, A11, A10, COMPOS_1:17; :: thesis:

end;

end;

assume A12: ProgramPart (Relocated (p,k)), Relocated (p,k) computes F ; :: thesis:
let x be set ; :: according to EXTPRO_1:def 13 :: thesis:
assume A13: x in dom F ; :: thesis:
then consider d1 being FinPartState of (SCM R) such that
A14: x = d1 and
A15: (Relocated (p,k)) +* d1 is Autonomy of ProgramPart (Relocated (p,k)) and
A16: F . d1 c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1)) by A12, EXTPRO_1:def 13;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider d = x as FinPartState of (SCM R) by A13, COMPOS_1:25;
reconsider d = d as data-only FinPartState of (SCM R) by A3, A13, COMPOS_1:def 24;
xx: dom d misses NAT by COMPOS_1:40;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A17: IC (SCM R) in dom (p +* d) by A2, XBOOLE_0:def 3;
A18: (Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
dom (ProgramPart (Relocated (p,k))) c= NAT by RELAT_1:87;
then XX: dom d misses dom (ProgramPart (Relocated (p,k))) by xx, XBOOLE_1:63;
YY: ((Relocated (p,k)) +* d) +* (ProgramPart (Relocated (p,k))) = (Relocated (p,k)) +* (d +* (ProgramPart (Relocated (p,k)))) by FUNCT_4:15
.= (Relocated (p,k)) +* ((ProgramPart (Relocated (p,k))) +* d) by XX, FUNCT_4:36
.= ((Relocated (p,k)) +* (ProgramPart (Relocated (p,k)))) +* d by FUNCT_4:15
.= Relocated ((p +* d),k) by A18, FUNCT_4:80 ;
then Relocated ((p +* d),k) is autonomic by A14, A15, EXTPRO_1:def 11;
then A19: p +* d is autonomic by A17, Th40;
B19: Relocated ((p +* d),k) is halting by A14, A15, EXTPRO_1:def 11, YY;
then A20: p +* d is halting by A17, Th36, A19;
X: Relocated ((p +* d),k) = (Relocated (p,k)) +* d by COMPOS_1:124;
xx: dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
y: ProgramPart ((Relocated (p,k)) +* d) = ProgramPart (Relocated (p,k)) by xx, FUNCT_4:76;
A21: DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1))) = DataPart (Result ((ProgramPart p),(p +* d))) by A17, A19, A20, Th41, x, y, X, A14;
take d ; :: thesis:
thus x = d ; :: thesis:
dom (ProgramPart p) c= NAT by RELAT_1:87;
then XX: dom d misses dom (ProgramPart p) by xx, XBOOLE_1:63;
AA: (p +* d) +* (ProgramPart p) = p +* (d +* (ProgramPart p)) by FUNCT_4:15
.= p +* ((ProgramPart p) +* d) by XX, FUNCT_4:36
.= (p +* (ProgramPart p)) +* d by FUNCT_4:15
.= p +* d by FUNCT_4:80 ;
p +* d is halting by A17, A19, Th36, B19;
hence p +* d is Autonomy of ProgramPart p by A19, EXTPRO_1:def 11, AA; :: thesis:
reconsider Fd1 = F . d1 as FinPartState of (SCM R) by A16;
A22: Fd1 is data-only by A3, A13, A14, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1))) by A16, COMPOS_1:17;
hence F . d c= Result ((ProgramPart p),(p +* d)) by A14, A22, A21, COMPOS_1:17; :: thesis: