let F be PartFunc of (FinPartSt SCM+FSA ),(FinPartSt SCM+FSA ); :: thesis: for p being 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 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 )
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+FSA such that
A5: x = d1 and
A6: ((ProgramPart p) +* p) +* d1 is pre-program of SCM+FSA and
A7: F . d1 c= Result (ProgramPart p),(p +* d1) by A3, AMI_1:def 30;
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;
X: (Relocated p,k) +* d = Relocated (p +* d),k by AMISTD_2:78;
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 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 +* d),k)) by A5, A6, F1, Th17, x, X, y
.= DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d)) by AMISTD_2:78 ;
reconsider Fs1 = F . d1 as FinPartState of SCM+FSA 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 AMISTD_2:78;
hence ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d is pre-program of SCM+FSA by A5, A6, A8, Th13, Th16, F1, F2; :: 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 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+FSA such that
A13: x = d1 and
A14: ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d1 is pre-program of SCM+FSA 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+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 AMISTD_2:78;
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 AMISTD_2:78;
then A18: p +* d is autonomic by A13, A14, A16, Th16, F2;
then A19: p +* d is halting by A13, A14, A17, A16, Th13, F2;
A20: DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1)) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated (p +* d),k)) by A13, A17, Th13, F2, A16, Th16
.= DataPart (Result (ProgramPart p),(p +* d)) by A16, A18, A19, Th17, x, y, 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) )
thus ((ProgramPart p) +* p) +* d is pre-program of SCM+FSA by A13, A14, A17, A16, A18, Th13, F1, F2; :: 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