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

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)) +* (IncAddr [(Shift (ProgramPart p),k)],k)) +* (DataPart p);
correctness
coherence
((Start-At ((IC p) + k)) +* (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)) +* (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 being Element of NAT
for l being Instruction-Location of SCM+FSA 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) 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;

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 Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (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 (Computation s1,i)) + k = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) & (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation 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 Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (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 Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (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;