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 Fthus
Relocated p,
k computes F
:: thesis: verumproof
let x be
set ;
:: according to AMI_1:def 29 :: thesis: ( not x in dom F or ex b1 being Element of sproduct the Object-Kind of (SCM R) st
( x = b1 & (Relocated p,k) +* b1 is Element of sproduct the Object-Kind of (SCM R) & F . b1 c= Result ((Relocated p,k) +* b1) ) )
assume A5:
x in dom F
;
:: thesis: ex b1 being Element of sproduct the Object-Kind of (SCM R) st
( x = b1 & (Relocated p,k) +* b1 is Element of sproduct the Object-Kind of (SCM R) & F . b1 c= Result ((Relocated p,k) +* b1) )
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 51;
take
s
;
:: thesis: ( x = s & (Relocated p,k) +* s is Element of sproduct the Object-Kind of (SCM R) & F . s c= Result ((Relocated p,k) +* s) )
thus
x = s
;
:: thesis: ( (Relocated p,k) +* s is Element of sproduct the Object-Kind of (SCM R) & F . s c= Result ((Relocated p,k) +* s) )
consider s1 being
FinPartState of
(SCM R) such that A6:
(
x = s1 &
p +* s1 is
pre-program of
(SCM R) &
F . s1 c= Result (p +* s1) )
by A4, A5, AMI_1:def 29;
reconsider Fs1 =
F . s1 as
FinPartState of
(SCM R) by A6, CARD_3:80;
A7:
Fs1 is
data-only
by A3, A5, A6, AMI_1:def 51;
then A8:
F . s1 c= DataPart (Result (p +* s1))
by A6, AMI_1:107;
A9:
(Relocated p,k) +* s = Relocated (p +* s),
k
by A2, AMISTD_2:78;
dom (p +* s) = (dom p) \/ (dom s)
by FUNCT_4:def 1;
then A10:
IC (SCM R) in dom (p +* s)
by A2, XBOOLE_0:def 3;
hence
(Relocated p,k) +* s is
pre-program of
(SCM R)
by A1, A6, A9, Th60, Th64;
:: thesis: F . s c= Result ((Relocated p,k) +* s)
DataPart (Result (p +* s1)) =
DataPart (Result (Relocated (p +* s),k))
by A1, A6, A10, Th65
.=
DataPart (Result ((Relocated p,k) +* s))
by A2, AMISTD_2:78
;
hence
F . s c= Result ((Relocated p,k) +* s)
by A6, A7, A8, 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 dom F or ex b1 being Element of sproduct the Object-Kind of (SCM R) st
( x = b1 & p +* b1 is Element of sproduct the Object-Kind of (SCM R) & F . b1 c= Result (p +* b1) ) )
assume A12:
x in dom F
; :: thesis: ex b1 being Element of sproduct the Object-Kind of (SCM R) st
( x = b1 & p +* b1 is Element of sproduct the Object-Kind of (SCM R) & F . b1 c= Result (p +* b1) )
dom F c= FinPartSt (SCM R)
by RELAT_1:def 18;
then reconsider s = x as FinPartState of (SCM R) by A12, AMI_1:125;
reconsider s = s as data-only FinPartState of (SCM R) by A3, A12, AMI_1:def 51;
take
s
; :: thesis: ( x = s & p +* s is Element of sproduct the Object-Kind of (SCM R) & F . s c= Result (p +* s) )
thus
x = s
; :: thesis: ( p +* s is Element of sproduct the Object-Kind of (SCM R) & F . s c= Result (p +* s) )
consider s1 being FinPartState of (SCM R) such that
A13:
( x = s1 & (Relocated p,k) +* s1 is pre-program of (SCM R) & F . s1 c= Result ((Relocated p,k) +* s1) )
by A11, A12, AMI_1:def 29;
reconsider Fs1 = F . s1 as FinPartState of (SCM R) by A13, CARD_3:80;
A14:
Fs1 is data-only
by A3, A12, A13, AMI_1:def 51;
then A15:
F . s1 c= DataPart (Result ((Relocated p,k) +* s1))
by A13, AMI_1:107;
A16:
(Relocated p,k) +* s = Relocated (p +* s),k
by A2, AMISTD_2:78;
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;
then A18:
p +* s is autonomic
by A1, A13, A16, Th64;
hence
p +* s is pre-program of (SCM R)
by A1, A13, A16, A17, Th60; :: thesis: F . s c= Result (p +* s)
A19:
p +* s is halting
by A1, A13, A16, A17, A18, Th60;
DataPart (Result ((Relocated p,k) +* s1)) =
DataPart (Result (Relocated (p +* s),k))
by A2, A13, AMISTD_2:78
.=
DataPart (Result (p +* s))
by A1, A17, A18, A19, Th65
;
hence
F . s c= Result (p +* s)
by A13, A14, A15, AMI_1:107; :: thesis: verum