let F be PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA); :: thesis: for l being Element of NAT
for p being b₁ -started non program-free autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom p & F is data-only holds
for k being Element of NAT holds
( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F )
let l be Element of NAT ; :: thesis: for p being l -started non program-free autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom p & F is data-only holds
for k being Element of NAT holds
( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F )
let p be l -started non program-free autonomic halting FinPartState of SCM+FSA; :: thesis: ( IC SCM+FSA in dom p & F is data-only implies for k being Element of NAT holds
( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F ) )
assume that
A1: IC SCM+FSA in dom p and
A2: F is data-only ; :: thesis: for k being Element of NAT holds
( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F )
let k be Element of NAT ; :: thesis: ( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F )

hereby :: thesis: ( ProgramPart (Relocated (p,k)), Relocated (p,k) computes F implies ProgramPart p,p computes F )

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

proof

let x be set ; :: according to EXTPRO_1:def 13 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & (Relocated (p,k)) +* b₁ is Autonomy of ProgramPart (Relocated (p,k)) & F . b₁ c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* b₁)) ) )
assume A4: x in dom F ; :: thesis: ex b₁ being set st
( x = b₁ & (Relocated (p,k)) +* b₁ is Autonomy of ProgramPart (Relocated (p,k)) & F . b₁ c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* b₁)) )
then consider d1 being FinPartState of SCM+FSA such that
A5: x = d1 and
A6: p +* d1 is Autonomy of ProgramPart p and
A7: F . d1 c= Result ((ProgramPart p),(p +* d1)) by A3, EXTPRO_1:def 13;
dom F c= FinPartSt SCM+FSA by RELAT_1:def 18;
then reconsider d = x as FinPartState of SCM+FSA by A4, COMPOS_1:25;
reconsider d = d as data-only FinPartState of SCM+FSA by A2, A4, COMPOS_1:def 24;
dom d misses NAT by COMPOS_1:40;
then XX: 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 XX, FUNCT_4:36
.= (p +* (ProgramPart p)) +* d by FUNCT_4:15
.= p +* d by FUNCT_4:80 ;
then B6: ( p +* d1 is halting & p +* d1 is autonomic ) by A6, EXTPRO_1:def 11, A5;
xx: dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
X: (Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
y: ProgramPart ((Relocated (p,k)) +* d) = ProgramPart (Relocated (p,k)) by xx, FUNCT_4:76;
XX: dom d misses dom (ProgramPart (Relocated (p,k))) by xx, XBOOLE_1:63, RELAT_1:87;
BB: ((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,k)) +* d by FUNCT_4:80 ;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A8: IC SCM+FSA in dom (p +* d) by A1, XBOOLE_0:def 3;
then A9: DataPart (Result ((ProgramPart p),(p +* d1))) = DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d))) by A5, Th17, x, X, y, B6;
reconsider Fs1 = F . d1 as FinPartState of SCM+FSA by A7;
take d ; :: thesis: ( x = d & (Relocated (p,k)) +* d is Autonomy of ProgramPart (Relocated (p,k)) & F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d)) )
thus x = d ; :: thesis: ( (Relocated (p,k)) +* d is Autonomy of ProgramPart (Relocated (p,k)) & F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d)) )
(Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
then ( (Relocated (p,k)) +* d is autonomic & (Relocated (p,k)) +* d is halting ) by A5, A8, Th16, B6;
hence (Relocated (p,k)) +* d is Autonomy of ProgramPart (Relocated (p,k)) by EXTPRO_1:def 11, BB; :: thesis: F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d))
A10: Fs1 is data-only by A2, A4, A5, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((ProgramPart p),(p +* d1))) by A7, COMPOS_1:17;
hence F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d)) by A5, A10, A9, COMPOS_1:17; :: thesis: verum

end;

end;

assume A11: ProgramPart (Relocated (p,k)), Relocated (p,k) computes F ; :: thesis: ProgramPart p,p computes F
let x be set ; :: according to EXTPRO_1:def 13 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & p +* b₁ is Autonomy of ProgramPart p & F . b₁ c= Result ((ProgramPart p),(p +* b₁)) ) )
assume A12: x in dom F ; :: thesis: ex b₁ being set st
( x = b₁ & p +* b₁ is Autonomy of ProgramPart p & F . b₁ c= Result ((ProgramPart p),(p +* b₁)) )
then consider d1 being FinPartState of SCM+FSA such that
A13: x = d1 and
A14: (Relocated (p,k)) +* d1 is Autonomy of ProgramPart (Relocated (p,k)) and
A15: F . d1 c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1)) by A11, EXTPRO_1:def 13;
dom F c= FinPartSt SCM+FSA by RELAT_1:def 18;
then reconsider d = x as FinPartState of SCM+FSA by A12, COMPOS_1:25;
reconsider d = d as data-only FinPartState of SCM+FSA by A2, A12, COMPOS_1:def 24;
X: (Relocated (p,k)) +* d = Relocated ((p +* d),k) 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 (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A16: IC SCM+FSA in dom (p +* d) by A1, XBOOLE_0:def 3;
A17: (Relocated (p,k)) +* d = Relocated ((p +* d),k) by COMPOS_1:124;
XX: dom d misses dom (ProgramPart (Relocated (p,k))) by xx, XBOOLE_1:63, RELAT_1:87;
BB: ((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,k)) +* d by FUNCT_4:80 ;
Relocated ((p +* d),k) is autonomic by A14, EXTPRO_1:def 11, BB, A17, A13;
then A18: p +* d is autonomic by A16, Th16;
Relocated ((p +* d),k) is halting by A14, EXTPRO_1:def 11, BB, A17, A13;
then A19: p +* d is halting by A16, Th13, A18;
A20: DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1))) = DataPart (Result ((ProgramPart p),(p +* d))) by A16, A18, A19, Th17, x, y, X, A13;
take d ; :: thesis: ( x = d & p +* d is Autonomy of ProgramPart p & F . d c= Result ((ProgramPart p),(p +* d)) )
thus x = d ; :: thesis: ( p +* d is Autonomy of ProgramPart p & F . d c= Result ((ProgramPart p),(p +* d)) )
XX: dom d misses dom (ProgramPart p) by xx, XBOOLE_1:63, RELAT_1:87;
(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 ;
hence p +* d is Autonomy of ProgramPart p by A18, A19, EXTPRO_1:def 11; :: thesis: F . d c= Result ((ProgramPart p),(p +* d))
reconsider Fs1 = F . d1 as FinPartState of SCM+FSA by A15;
A21: Fs1 is data-only by A2, A12, A13, COMPOS_1:def 24;
then F . d1 c= DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1))) by A15, COMPOS_1:17;
hence F . d c= Result ((ProgramPart p),(p +* d)) by A13, A21, A20, COMPOS_1:17; :: thesis: verum