let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N; :: thesis:
let F be data-only PartFunc of (FinPartSt S),(FinPartSt S); :: thesis:
let l be Nat; :: thesis:
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis:
let p be non empty q -autonomic q -halted FinPartState of S; :: thesis:
assume A1: IC in dom p ; :: thesis:
let k be Nat; :: thesis:

hereby :: thesis:

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

proof

let x be set ; :: according to EXTPRO_1:def 14 :: thesis:
assume A3: x in dom F ; :: thesis:
then consider d1 being FinPartState of S such that
A4: x = d1 and
A5: p +* d1 is Autonomy of q and
A6: F . d1 c= Result (q,(p +* d1)) by A2;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A3, MEMSTR_0:76;
reconsider d = d as data-only FinPartState of S by A3, MEMSTR_0:def 17;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A7: IC in dom (p +* d) by A1, XBOOLE_0:def 3;
A8: p +* d is q -autonomic by A4, A5, EXTPRO_1:def 12;
then A9: IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A7, Th11;
A10: p +* d is q -halted by A4, A5, EXTPRO_1:def 12;
reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A4, A5, EXTPRO_1:def 12;
A11: DataPart (Result (q,pd)) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A7, Th13
.= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by MEMSTR_0:54 ;
reconsider Fs1 = F . d1 as FinPartState of S by A6;
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 A8, A10, A9, EXTPRO_1:def 12; :: thesis:
A12: Fs1 is data-only by A3, A4, MEMSTR_0:def 17;
F . d1 c= DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d))) by A6, A12, A4, A11, MEMSTR_0:5;
hence F . d c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d)) by A4, A12, MEMSTR_0:5; :: thesis:

end;

assume A13: Reloc (q,k), IncIC (p,k) computes F ; :: thesis:
let x be set ; :: according to EXTPRO_1:def 14 :: thesis:
assume A14: x in dom F ; :: thesis:
then consider d1 being FinPartState of S such that
A15: x = d1 and
A16: (IncIC (p,k)) +* d1 is Autonomy of Reloc (q,k) and
A17: F . d1 c= Result ((Reloc (q,k)),((IncIC (p,k)) +* d1)) by A13;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A14, MEMSTR_0:76;
reconsider d = d as data-only FinPartState of S by A14, MEMSTR_0:def 17;
A18: dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A19: IC in dom (p +* d) by A1, XBOOLE_0:def 3;
A20: (IncIC (p,k)) +* d = IncIC ((p +* d),k) by MEMSTR_0:54;
IncIC ((p +* d),k) is Reloc (q,k) -autonomic by A15, A16, A20, EXTPRO_1:def 12;
then A21: p +* d is q -autonomic by A19, Th11;
A22: IncIC ((p +* d),k) is Reloc (q,k) -halted by A15, A16, A20, EXTPRO_1:def 12;
A23: p +* d is q -halted by A19, Th12, A21, A22;
reconsider pd = p +* d as non empty q -autonomic q -halted FinPartState of S by A19, Th12, A21, A22;
A24: IC in dom pd by A18, A1, XBOOLE_0:def 3;
A25: DataPart (Result ((Reloc (q,k)),((IncIC (p,k)) +* d1))) = DataPart (Result ((Reloc (q,k)),(IncIC ((p +* d),k)))) by A15, MEMSTR_0:54
.= DataPart (Result (q,(p +* d))) by Th13, A24 ;
take d ; :: thesis:
thus x = d ; :: thesis:
thus p +* d is Autonomy of q by A21, A23, EXTPRO_1:def 12; :: thesis:
reconsider Fs1 = F . d1 as FinPartState of S by A17;
A26: Fs1 is data-only by A14, A15, MEMSTR_0:def 17;
then F . d1 c= DataPart (Result (q,(p +* d))) by A25, A17, MEMSTR_0:5;
hence F . d c= Result (q,(p +* d)) by A15, A26, MEMSTR_0:5; :: thesis: