let N be non empty with_non-empty_elements set ; :: thesis:
let S be standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized relocable1 AMI-Struct of N; :: thesis:
assume A1: ( S is CurIns-recognized & S is relocable1 & S is relocable2 & S is proper-halt ) ; :: thesis:
let F be data-only PartFunc of (FinPartSt S),(FinPartSt S); :: thesis:
let l be Element of NAT ; :: thesis:
let q be NAT -defined the Instructions of S -valued finite non halt-free Function; :: thesis:
let p be non empty q -autonomic q -halted FinPartState of S; :: thesis:
assume A2: IC in dom p ; :: thesis:
let k be Element of NAT ; :: thesis:

hereby :: thesis:

assume A5: q,p computes F ; :: thesis:
thus Reloc (q,k), IncIC (p,k) computes F :: thesis:

let x be set ; :: according to EXTPRO_1:def 14 :: 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 q and
A9: F . d1 c= Result (q,(p +* d1)) by A5, EXTPRO_1:def 14;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A6, MEMSTR_0:76;
reconsider d = d as data-only FinPartState of S by A6, MEMSTR_0:def 14;
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;
A17: p +* d is q -autonomic by A7, A8, EXTPRO_1:def 12;
then A18: IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A10, Th11, A1;
A19: p +* d is q -halted by A7, A8, EXTPRO_1:def 12;
reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A7, A8, EXTPRO_1:def 12;
A20: DataPart (Result (q,pd)) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A1, A10, Th13
.= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by MEMSTR_0:54 ;
reconsider Fs1 = F . d1 as FinPartState of S by A9;
take d ; :: thesis:
thus x = d ; :: thesis:
(IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;
hence (IncIC (p,k)) +* d is Autonomy of Reloc (q,k) by A17, A19, A18, EXTPRO_1:def 12; :: thesis:
SS: p +* d1 = pd by A7;
A21: Fs1 is data-only by A6, A7, MEMSTR_0:def 14;
F . d1 c= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by A9, A21, SS, A20, MEMSTR_0:5;
hence F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) by A7, A21, MEMSTR_0:5; :: thesis:

end;

end;

assume A22: Reloc (q,k), IncIC (p,k) computes F ; :: thesis:
let x be set ; :: according to EXTPRO_1:def 14 :: thesis:
assume A23: x in dom F ; :: thesis:
then consider d1 being FinPartState of S such that
A24: x = d1 and
A25: (IncIC (p,k)) +* d1 is Autonomy of Reloc (q,k) and
A26: F . d1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d1)) by A22, EXTPRO_1:def 14;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A23, MEMSTR_0:76;
reconsider d = d as data-only FinPartState of S by A23, MEMSTR_0:def 14;
B27: 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;
A32: (IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;
IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A24, A25, A32, EXTPRO_1:def 12;
then A33: p +* d is q -autonomic by A27, Th11, A1;
RR: IncIC ((p +* d),k) is Reloc (q,k) -halted by A24, A25, A32, EXTPRO_1:def 12;
A34: p +* d is q -halted by A27, Th12, A33, RR;
reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A27, Th12, A33, RR;
WR: IC in dom pd by B27, A2, XBOOLE_0:def 3;
A35: DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d1))) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A24, MEMSTR_0:54
.= DataPart (Result (q,(p +* d))) by Th13, A1, WR ;
take d ; :: thesis:
thus x = d ; :: thesis:
thus p +* d is Autonomy of q by A33, A34, EXTPRO_1:def 12; :: thesis:
reconsider Fs1 = F . d1 as FinPartState of S by A26;
A37: Fs1 is data-only by A23, A24, MEMSTR_0:def 14;
then F . d1 c= DataPart (Result (q,(p +* d))) by A35, A26, MEMSTR_0:5;
hence F . d c= Result (q,(p +* d)) by A24, A37, MEMSTR_0:5; :: thesis: