let F be PartFunc of (FinPartSt SCM),(FinPartSt SCM); :: thesis: for l being Element of NAT
for p being b₁ -started non program-free autonomic halting FinPartState of SCM st IC SCM 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 st IC SCM 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; :: thesis: ( IC SCM 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 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 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 by RELAT_1:def 18;
then reconsider d = x as FinPartState of SCM by A4, COMPOS_1:25;
reconsider d = d as data-only FinPartState of SCM by A2, A4, COMPOS_1:def 24;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A8: IC SCM in dom (p +* d) by A1, XBOOLE_0:def 3;
X: Relocated ((p +* d),k) = (Relocated (p,k)) +* d by Th29;
dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
xx: dom d misses NAT by COMPOS_1:40;
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 d misses NAT by COMPOS_1:40;
then XX: dom d misses dom (ProgramPart p) by RELAT_1:87, 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 ;
then HH2: p +* d is autonomic by A5, A6, EXTPRO_1:def 11;
then HH1: Relocated ((p +* d),k) is autonomic by A8, Th41;
HH3: p +* d is halting by A5, A6, EXTPRO_1:def 11, AA;
then A9: DataPart (Result ((ProgramPart p),(p +* d1))) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated ((p +* d),k)))) by A5, Th42, A8, x, HH2
.= DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated ((p +* d),k)))) by COMPOS_1:116
.= DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d))) by X ;
reconsider Fs1 = F . d1 as FinPartState of SCM 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)) )
HH: Relocated ((p +* d),k) is halting by A8, HH2, HH3;
(Relocated (p,k)) +* d = Relocated ((p +* d),k) by Th29;
hence (Relocated (p,k)) +* d is Autonomy of ProgramPart (Relocated (p,k)) by HH, HH1, BB, EXTPRO_1:def 11; :: 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 (Relocated (p,k))),((Relocated (p,k)) +* d))) by A9, A7, COMPOS_1:17;
hence F . d c= Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d)) by A5, A10, 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 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 by RELAT_1:def 18;
then reconsider d = x as FinPartState of SCM by A12, COMPOS_1:25;
reconsider d = d as data-only FinPartState of SCM by A2, A12, COMPOS_1:def 24;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A16: IC SCM in dom (p +* d) by A1, XBOOLE_0:def 3;
dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
xx: dom d misses NAT by COMPOS_1:40;
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 ;
A17: (Relocated (p,k)) +* d = Relocated ((p +* d),k) by Th29;
Relocated ((p +* d),k) is autonomic by A13, A14, EXTPRO_1:def 11, BB, A17;
then A18: p +* d is autonomic by A16, Th41;
Relocated ((p +* d),k) is halting by A13, A14, EXTPRO_1:def 11, BB, A17;
then A19: p +* d is halting by A16, Th38, A18;
A20: DataPart (Result ((ProgramPart (Relocated (p,k))),((Relocated (p,k)) +* d1))) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated ((p +* d),k)))) by A13, Th29
.= DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated ((p +* d),k)))) by COMPOS_1:116
.= DataPart (Result ((ProgramPart p),(p +* d))) by A16, A18, A19, Th42, x ;
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)) )
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 ;
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 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