let N be non empty with_non-empty_elements set ; :: thesis:
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N; :: thesis:
assume A1: ( S is CurIns-recognized & S is relocable2 ) ; :: thesis:
let F be PartFunc of (FinPartSt S),(FinPartSt S); :: thesis:
let l be Element of NAT ; :: thesis:
let p be l -started non program-free autonomic halting FinPartState of S; :: thesis:
assume that
A2: IC in dom p and
A3: F is data-only ; :: thesis:
let k be Element of NAT ; :: thesis:
RE: Reloc ((ProgramPart p),k) = ProgramPart (Relocated (p,k)) by COMPOS_1:116;

hereby :: thesis:

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

let x be set ; :: according to EXTPRO_1:def 13 :: thesis:
assume A6: x in dom F ; :: thesis:
then consider d1 being FinPartState of S such that
A7: x = d1 and
A8: p +* d1 is Autonomy of ProgramPart p and
A9: F . d1 c= Result ((ProgramPart p),(p +* d1)) by A5, EXTPRO_1:def 13;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A6, COMPOS_1:25;
reconsider d = d as data-only FinPartState of S by A3, A6, COMPOS_1:def 24;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A10: IC in dom (p +* d) by A2, XBOOLE_0:def 3;
dom d misses NAT by COMPOS_1:40;
then A11: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
A12: dom d misses NAT by COMPOS_1:40;
A13: dom d misses dom (Reloc ((ProgramPart p),k)) by A12, RE, RELAT_1:87, XBOOLE_1:63;
A14: ((Relocated (p,k)) +* d) +* (Reloc ((ProgramPart p),k)) = (Relocated (p,k)) +* (d +* (Reloc ((ProgramPart p),k))) by FUNCT_4:15
.= (Relocated (p,k)) +* ((Reloc ((ProgramPart p),k)) +* d) by A13, FUNCT_4:36
.= ((Relocated (p,k)) +* (Reloc ((ProgramPart p),k))) +* d by FUNCT_4:15
.= (Relocated (p,k)) +* d by RE, FUNCT_4:80 ;
dom d misses NAT by COMPOS_1:40;
then A15: dom d misses dom (ProgramPart p) by RELAT_1:87, XBOOLE_1:63;
A16: (p +* d) +* (ProgramPart p) = p +* (d +* (ProgramPart p)) by FUNCT_4:15
.= p +* ((ProgramPart p) +* d) by A15, FUNCT_4:36
.= (p +* (ProgramPart p)) +* d by FUNCT_4:15
.= p +* d by FUNCT_4:80 ;
then A17: p +* d is autonomic by A7, A8, EXTPRO_1:def 11;
then A18: Relocated ((p +* d),k) is autonomic by A10, Th11, A1;
A19: p +* d is halting by A7, A8, A16, EXTPRO_1:def 11;
then A20: DataPart (Result ((ProgramPart p),(p +* d1))) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated ((p +* d),k)))) by A7, Th13, A10, A11, A17, A1
.= DataPart (Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d))) by COMPOS_1:124 ;
reconsider Fs1 = F . d1 as FinPartState of S by A9;
take d ; :: thesis:
thus x = d ; :: thesis:
(Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
hence (Relocated (p,k)) +* d is Autonomy of Reloc ((ProgramPart p),k) by A17, A19, A18, A14, EXTPRO_1:def 11; :: thesis:
A21: Fs1 is data-only by A3, A6, A7, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d))) by A20, A9, COMPOS_1:17;
hence F . d c= Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d)) by A7, A21, COMPOS_1:17; :: thesis:

end;

end;

assume A22: Reloc ((ProgramPart p),k), Relocated (p,k) computes F ; :: thesis:
let x be set ; :: according to EXTPRO_1:def 13 :: thesis:
assume A23: x in dom F ; :: thesis:
then consider d1 being FinPartState of S such that
A24: x = d1 and
A25: (Relocated (p,k)) +* d1 is Autonomy of Reloc ((ProgramPart p),k) and
A26: F . d1 c= Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d1)) by A22, EXTPRO_1:def 13;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A23, COMPOS_1:25;
reconsider d = d as data-only FinPartState of S by A3, A23, COMPOS_1:def 24;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A27: IC in dom (p +* d) by A2, XBOOLE_0:def 3;
dom d misses NAT by COMPOS_1:40;
then A28: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
A29: dom d misses NAT by COMPOS_1:40;
A30: dom d misses dom (Reloc ((ProgramPart p),k)) by A29, RE, RELAT_1:87, XBOOLE_1:63;
A31: ((Relocated (p,k)) +* d) +* (Reloc ((ProgramPart p),k)) = (Relocated (p,k)) +* (d +* (Reloc ((ProgramPart p),k))) by FUNCT_4:15
.= (Relocated (p,k)) +* ((Reloc ((ProgramPart p),k)) +* d) by A30, FUNCT_4:36
.= ((Relocated (p,k)) +* (Reloc ((ProgramPart p),k))) +* d by FUNCT_4:15
.= (Relocated (p,k)) +* d by RE, FUNCT_4:80 ;
A32: (Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
Relocated ((p +* d),k) is autonomic by A24, A25, A31, A32, EXTPRO_1:def 11;
then A33: p +* d is autonomic by A27, Th11, A1;
Relocated ((p +* d),k) is halting by A24, A25, A31, A32, EXTPRO_1:def 11;
then A34: p +* d is halting by A27, Th12, A33;
A35: DataPart (Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d1))) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated ((p +* d),k)))) by A24, COMPOS_1:124
.= DataPart (Result ((ProgramPart p),(p +* d))) by A27, A33, A34, Th13, A28, A1 ;
take d ; :: thesis:
thus x = d ; :: thesis:
dom d misses NAT by COMPOS_1:40;
then A36: dom d misses dom (ProgramPart p) by RELAT_1:87, XBOOLE_1:63;
(p +* d) +* (ProgramPart p) = p +* (d +* (ProgramPart p)) by FUNCT_4:15
.= p +* ((ProgramPart p) +* d) by A36, FUNCT_4:36
.= (p +* (ProgramPart p)) +* d by FUNCT_4:15
.= p +* d by FUNCT_4:80 ;
hence p +* d is Autonomy of ProgramPart p by A33, A34, EXTPRO_1:def 11; :: thesis:
reconsider Fs1 = F . d1 as FinPartState of S by A26;
A37: Fs1 is data-only by A3, A23, A24, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((Reloc ((ProgramPart p),k)),((Relocated (p,k)) +* d1))) by A26, COMPOS_1:17;
hence F . d c= Result ((ProgramPart p),(p +* d)) by A24, A37, A35, COMPOS_1:17; :: thesis: