:: 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;

registration

let l be Element of NAT ;
let p be l -started autonomic halting FinPartState of SCM+FSA;
let k be Element of NAT ;
cluster Relocated (p,k) -> halting ;
coherence
Relocated (p,k) is halting

proof end;

end;

theorem Th17: :: SCMFSA_5:17

for l being Element of NAT
for p being b₁ -started non program-free 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 l being Element of NAT
for p being b₂ -started non program-free autonomic halting 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;