:: Relocability for { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 22, 1996
:: Copyright (c) 1996 Association of Mizar Users

begin

Lm1: NAT misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;

theorem :: SCMFSA_5:1

canceled;

theorem :: SCMFSA_5:2

canceled;

theorem :: SCMFSA_5:3

canceled;

theorem :: SCMFSA_5:4

canceled;

theorem :: SCMFSA_5:5

canceled;

theorem :: SCMFSA_5:6

canceled;

theorem :: SCMFSA_5:7

canceled;

theorem :: SCMFSA_5:8

canceled;

theorem :: SCMFSA_5:9

canceled;

theorem Th10: :: SCMFSA_5:10

for k being Element of NAT
for p being autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)

proof end;

begin

theorem :: SCMFSA_5:11

for k being Element of NAT
for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s holds
for i being Element of NAT holds Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),SCM+FSA )) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th12: :: SCMFSA_5:12

for k being Element of NAT
for p being autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st IC SCM+FSA in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart (s1 +* (DataPart s2))),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )

proof end;

theorem Th13: :: SCMFSA_5:13

for p being autonomic FinPartState of SCM+FSA
for k being Element of NAT st IC SCM+FSA in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem Th14: :: SCMFSA_5:14

for k being Element of NAT
for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st Relocated p,k c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* p)),(s +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k),SCM+FSA )) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th15: :: SCMFSA_5:15

for k being Element of NAT
for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM+FSA )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th16: :: SCMFSA_5:16

for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th17: :: SCMFSA_5:17

for p being autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for k being Element of NAT holds DataPart (Result (ProgramPart p),p) = DataPart (Result (ProgramPart (Relocated p,k)),(Relocated p,k))

proof end;

theorem :: SCMFSA_5:18

for F being PartFunc of (FinPartSt SCM+FSA ),(FinPartSt SCM+FSA )
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 )

proof end;