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