let F be PartFunc of (FinPartSt SCM ),(FinPartSt SCM ); :: thesis: for p being 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 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 )
F1: (ProgramPart p) +* p = p by FUNCT_4:119;
F2: (ProgramPart (Relocated p,k)) +* (Relocated p,k) = Relocated p,k by FUNCT_4:119;

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 AMI_1:def 30 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* b₁ is set & 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₁ & ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* b₁ is set & 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: ((ProgramPart p) +* p) +* d1 is pre-program of SCM and
A7: F . d1 c= Result (ProgramPart p),(p +* d1) by A3, AMI_1:def 30;
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;
A9: DataPart (Result (ProgramPart p),(p +* d1)) = DataPart (Result (Reloc (ProgramPart p),k),(Relocated (p +* d),k)) by A5, A6, Th42, A8, F1, x
.= DataPart (Result (ProgramPart (Relocated p,k)),(Relocated (p +* d),k)) by AMISTD_2:69
.= 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 & ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d is set & F . d c= Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d) )
thus x = d ; :: thesis: ( ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d is set & F . d c= Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d) )
(Relocated p,k) +* d = Relocated (p +* d),k by Th29;
hence ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d is pre-program of SCM by A5, A6, A8, Th38, Th41, F2, F1; :: 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;
then F . d1 c= DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d)) by A9;
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 AMI_1:def 30 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & ((ProgramPart p) +* p) +* b₁ is set & F . b₁ c= Result (ProgramPart p),(p +* b₁) ) )
assume A12: x in dom F ; :: thesis: ex b₁ being set st
( x = b₁ & ((ProgramPart p) +* p) +* b₁ is set & F . b₁ c= Result (ProgramPart p),(p +* b₁) )
then consider d1 being FinPartState of SCM such that
A13: x = d1 and
A14: ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d1 is pre-program of SCM and
A15: F . d1 c= Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1) by A11, AMI_1:def 30;
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;
A17: (Relocated p,k) +* d = Relocated (p +* d),k by Th29;
then A18: p +* d is autonomic by A13, A14, A16, Th41, F2;
then A19: p +* d is halting by A13, A14, A17, A16, Th38, F2;
then ( Relocated (p +* d1),k = (Relocated p,k) +* d1 & Relocated (p +* d),k = (Relocated p,k) +* d ) by A13, Th29;
then A20: DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1)) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated (p +* d),k)) by A13
.= DataPart (Result (Reloc (ProgramPart p),k),(Relocated (p +* d),k)) by AMISTD_2:69
.= DataPart (Result (ProgramPart p),(p +* d)) by A16, A18, A19, Th42, x ;
take d ; :: thesis: ( x = d & ((ProgramPart p) +* p) +* d is set & F . d c= Result (ProgramPart p),(p +* d) )
thus x = d ; :: thesis: ( ((ProgramPart p) +* p) +* d is set & F . d c= Result (ProgramPart p),(p +* d) )
p +* d is pre-program of SCM by A13, A14, A17, A16, A18, Th38, F2;
hence ((ProgramPart p) +* p) +* d is pre-program of SCM by F1; :: 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