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
( p computes F iff 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
( p computes F iff 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
( p computes F iff Relocated p,k computes F )
let k be Element of NAT ; :: thesis: ( p computes F iff Relocated p,k computes F )

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

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

proof

let x be set ; :: according to AMI_1:def 29 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & (Relocated p,k) +* b₁ is set & F . b₁ c= Result ((Relocated p,k) +* b₁) ) )
assume A4: x in dom F ; :: thesis: ex b₁ being set st
( x = b₁ & (Relocated p,k) +* b₁ is set & F . b₁ c= Result ((Relocated p,k) +* b₁) )
then consider s1 being FinPartState of SCM+FSA such that
A5: x = s1 and
A6: p +* s1 is pre-program of SCM+FSA and
A7: F . s1 c= Result (p +* s1) by A3, AMI_1:def 29;
dom F c= FinPartSt SCM+FSA by RELAT_1:def 18;
then reconsider s = x as FinPartState of SCM+FSA by A4, AMI_1:125;
reconsider s = s as data-only FinPartState of SCM+FSA by A2, A4, AMI_1:def 52;
dom (p +* s) = (dom p) \/ (dom s) by FUNCT_4:def 1;
then A8: IC SCM+FSA in dom (p +* s) by A1, XBOOLE_0:def 3;
then A9: DataPart (Result (p +* s1)) = DataPart (Result (Relocated (p +* s),k)) by A5, A6, Th17
.= DataPart (Result ((Relocated p,k) +* s)) by A1, Th9 ;
reconsider Fs1 = F . s1 as FinPartState of SCM+FSA by A7;
take s ; :: thesis: ( x = s & (Relocated p,k) +* s is set & F . s c= Result ((Relocated p,k) +* s) )
thus x = s ; :: thesis: ( (Relocated p,k) +* s is set & F . s c= Result ((Relocated p,k) +* s) )
(Relocated p,k) +* s = Relocated (p +* s),k by A1, Th9;
hence (Relocated p,k) +* s is pre-program of SCM+FSA by A5, A6, A8, Th13, Th16; :: thesis: F . s c= Result ((Relocated p,k) +* s)
A10: Fs1 is data-only by A2, A4, A5, AMI_1:def 52;
then F . s1 c= DataPart (Result (p +* s1)) by A7, AMI_1:107;
hence F . s c= Result ((Relocated p,k) +* s) by A5, A10, A9, AMI_1:107; :: thesis: verum

end;

end;

assume A11: Relocated p,k computes F ; :: thesis: p computes F
let x be set ; :: according to AMI_1:def 29 :: thesis: ( not x in proj1 F or ex b₁ being set st
( x = b₁ & p +* b₁ is set & F . b₁ c= Result (p +* b₁) ) )
assume A12: x in dom F ; :: thesis: ex b₁ being set st
( x = b₁ & p +* b₁ is set & F . b₁ c= Result (p +* b₁) )
then consider s1 being FinPartState of SCM+FSA such that
A13: x = s1 and
A14: (Relocated p,k) +* s1 is pre-program of SCM+FSA and
A15: F . s1 c= Result ((Relocated p,k) +* s1) by A11, AMI_1:def 29;
dom F c= FinPartSt SCM+FSA by RELAT_1:def 18;
then reconsider s = x as FinPartState of SCM+FSA by A12, AMI_1:125;
reconsider s = s as data-only FinPartState of SCM+FSA by A2, A12, AMI_1:def 52;
dom (p +* s) = (dom p) \/ (dom s) by FUNCT_4:def 1;
then A16: IC SCM+FSA in dom (p +* s) by A1, XBOOLE_0:def 3;
A17: (Relocated p,k) +* s = Relocated (p +* s),k by A1, Th9;
then A18: p +* s is autonomic by A13, A14, A16, Th16;
then A19: p +* s is halting by A13, A14, A17, A16, Th13;
A20: DataPart (Result ((Relocated p,k) +* s1)) = DataPart (Result (Relocated (p +* s),k)) by A1, A13, Th9
.= DataPart (Result (p +* s)) by A16, A18, A19, Th17 ;
take s ; :: thesis: ( x = s & p +* s is set & F . s c= Result (p +* s) )
thus x = s ; :: thesis: ( p +* s is set & F . s c= Result (p +* s) )
thus p +* s is pre-program of SCM+FSA by A13, A14, A17, A16, A18, Th13; :: thesis: F . s c= Result (p +* s)
reconsider Fs1 = F . s1 as FinPartState of SCM+FSA by A15;
A21: Fs1 is data-only by A2, A12, A13, AMI_1:def 52;
then F . s1 c= DataPart (Result ((Relocated p,k) +* s1)) by A15, AMI_1:107;
hence F . s c= Result (p +* s) by A13, A21, A20, AMI_1:107; :: thesis: verum