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

begin

definition

let p be FinPartState of SCM+FSA ;
let k be Element of NAT ;
func Relocated p,k -> FinPartState of SCM+FSA equals :: SCMFSA_5:def 1
((Start-At ((IC p) + k),SCM+FSA ) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);
correctness
coherence
((Start-At ((IC p) + k),SCM+FSA ) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p) is FinPartState of SCM+FSA ;
;

end;

:: deftheorem defines Relocated SCMFSA_5:def 1 :

for p being FinPartState of SCM+FSA
for k being Element of NAT holds Relocated p,k = ((Start-At ((IC p) + k),SCM+FSA ) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);

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

theorem Th1: :: SCMFSA_5:1

for p being FinPartState of SCM+FSA
for k being Element of NAT holds DataPart (Relocated p,k) = DataPart p

proof end;

theorem Th2: :: SCMFSA_5:2

for p being FinPartState of SCM+FSA
for k being Element of NAT holds ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k

proof end;

theorem Th3: :: SCMFSA_5:3

for k being Element of NAT
for p being FinPartState of SCM+FSA holds dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }

proof end;

theorem Th4: :: SCMFSA_5:4

for p being FinPartState of SCM+FSA
for k, l being Element of NAT holds
( l in dom p iff l + k in dom (Relocated p,k) )

proof end;

theorem Th5: :: SCMFSA_5:5

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

proof end;

theorem Th6: :: SCMFSA_5:6

for p being FinPartState of SCM+FSA
for k being Element of NAT holds IC (Relocated p,k) = (IC p) + k

proof end;

theorem Th7: :: SCMFSA_5:7

for p being FinPartState of SCM+FSA
for k, loc being Element of NAT
for I being Instruction of SCM+FSA st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr I,k = (Relocated p,k) . (loc + k)

proof end;

theorem Th8: :: SCMFSA_5:8

for p being FinPartState of SCM+FSA
for k being Element of NAT holds Start-At ((IC p) + k),SCM+FSA c= Relocated p,k

proof end;

theorem Th9: :: SCMFSA_5:9

for s being data-only FinPartState of SCM+FSA
for p being FinPartState of SCM+FSA
for k being Element of NAT st IC SCM+FSA in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s

proof end;

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 (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(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 p) = DataPart (Result (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
( p computes F iff Relocated p,k computes F )

proof end;