let k be natural number ; :: thesis: for R being good Ring
for p being FinPartState of (SCM R) st not R is trivial holds
for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F )
let R be good Ring; :: thesis: for p being FinPartState of (SCM R) st not R is trivial holds
for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F )
let p be FinPartState of (SCM R); :: thesis: ( not R is trivial implies for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F ) )
assume A1: not R is trivial ; :: thesis: for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F )
let F be PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)); :: thesis: ( IC (SCM R) in dom p & F is data-only implies ( p computes F iff Relocated p,k computes F ) )
assume that
A2: IC (SCM R) in dom p and
A3: F is data-only ; :: thesis: ( p computes F iff Relocated p,k computes F )

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

assume A4: 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 A5: 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 R) such that
A6: x = s1 and
A7: p +* s1 is pre-program of SCM R and
A8: F . s1 c= Result (p +* s1) by A4, AMI_1:def 29;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider s = x as FinPartState of (SCM R) by A5, AMI_1:125;
reconsider s = s as data-only FinPartState of (SCM R) by A3, A5, AMI_1:def 52;
dom (p +* s) = (dom p) \/ (dom s) by FUNCT_4:def 1;
then A9: IC (SCM R) in dom (p +* s) by A2, XBOOLE_0:def 3;
then A10: DataPart (Result (p +* s1)) = DataPart (Result (Relocated (p +* s),k)) by A1, A6, A7, Th41
.= DataPart (Result ((Relocated p,k) +* s)) by A2, AMISTD_2:78 ;
reconsider Fs1 = F . s1 as FinPartState of (SCM R) by A8;
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 A2, AMISTD_2:78;
hence (Relocated p,k) +* s is pre-program of SCM R by A1, A6, A7, A9, Th36, Th40; :: thesis: F . s c= Result ((Relocated p,k) +* s)
A11: Fs1 is data-only by A3, A5, A6, AMI_1:def 52;
then F . s1 c= DataPart (Result (p +* s1)) by A8, AMI_1:107;
hence F . s c= Result ((Relocated p,k) +* s) by A6, A11, A10, AMI_1:107; :: thesis: verum

end;

end;

assume A12: 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 A13: 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 R) such that
A14: x = s1 and
A15: (Relocated p,k) +* s1 is pre-program of SCM R and
A16: F . s1 c= Result ((Relocated p,k) +* s1) by A12, AMI_1:def 29;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider s = x as FinPartState of (SCM R) by A13, AMI_1:125;
reconsider s = s as data-only FinPartState of (SCM R) by A3, A13, AMI_1:def 52;
dom (p +* s) = (dom p) \/ (dom s) by FUNCT_4:def 1;
then A17: IC (SCM R) in dom (p +* s) by A2, XBOOLE_0:def 3;
A18: (Relocated p,k) +* s = Relocated (p +* s),k by A2, AMISTD_2:78;
then A19: p +* s is autonomic by A1, A14, A15, A17, Th40;
then A20: p +* s is halting by A1, A14, A15, A18, A17, Th36;
A21: DataPart (Result ((Relocated p,k) +* s1)) = DataPart (Result (Relocated (p +* s),k)) by A2, A14, AMISTD_2:78
.= DataPart (Result (p +* s)) by A1, A17, A19, A20, Th41 ;
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 R by A1, A14, A15, A18, A17, A19, Th36; :: thesis: F . s c= Result (p +* s)
reconsider Fs1 = F . s1 as FinPartState of (SCM R) by A16;
A22: Fs1 is data-only by A3, A13, A14, AMI_1:def 52;
then F . s1 c= DataPart (Result ((Relocated p,k) +* s1)) by A16, AMI_1:107;
hence F . s c= Result (p +* s) by A14, A22, A21, AMI_1:107; :: thesis: verum