:: Relocatability
:: by Yasushi Tanaka
::
:: Received June 16, 1994
:: Copyright (c) 1994 Association of Mizar Users

begin

theorem :: RELOC:1

canceled;

theorem :: RELOC:2

canceled;

theorem :: RELOC:3

canceled;

theorem :: RELOC:4

canceled;

registration

let a, b be Data-Location ;
cluster a := b -> ins-loc-free ;
coherence
a := b is ins-loc-free

proof end;

cluster AddTo (a,b) -> ins-loc-free ;
coherence
AddTo (a,b) is ins-loc-free

proof end;

cluster SubFrom (a,b) -> ins-loc-free ;
coherence
SubFrom (a,b) is ins-loc-free

proof end;

cluster MultBy (a,b) -> ins-loc-free ;
coherence
MultBy (a,b) is ins-loc-free

proof end;

cluster Divide (a,b) -> ins-loc-free ;
coherence
Divide (a,b) is ins-loc-free

proof end;

end;

theorem :: RELOC:5

canceled;

theorem :: RELOC:6

canceled;

theorem :: RELOC:7

canceled;

theorem :: RELOC:8

canceled;

theorem :: RELOC:9

canceled;

theorem Th10: :: RELOC:10

for k, loc being Element of NAT holds IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k)

proof end;

theorem Th11: :: RELOC:11

for k, loc being Element of NAT
for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)

proof end;

theorem Th12: :: RELOC:12

for k, loc being Element of NAT
for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)

proof end;

theorem Th13: :: RELOC:13

for I being Instruction of SCM
for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) holds
IncAddr (I,k) = I

proof end;

theorem Th14: :: RELOC:14

for II, I being Instruction of SCM
for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr (II,k) = I holds
II = I

proof end;

theorem :: RELOC:15

canceled;

theorem :: RELOC:16

canceled;

theorem :: RELOC:17

canceled;

theorem :: RELOC:18

canceled;

theorem Th19: :: RELOC:19

for i being Element of NAT
for p being NAT -defined the Instructions of SCM -valued finite Function holds Shift ((IncAddr (p,i)),i) = Reloc (p,i)

proof end;

theorem :: RELOC:20

canceled;

theorem :: RELOC:21

canceled;

theorem :: RELOC:22

canceled;

theorem :: RELOC:23

canceled;

theorem :: RELOC:24

canceled;

theorem :: RELOC:25

canceled;

theorem Th26: :: RELOC:26

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

proof end;

theorem Th27: :: RELOC:27

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

proof end;

theorem Th28: :: RELOC:28

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

proof end;

theorem Th29: :: RELOC:29

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

proof end;

theorem Th30: :: RELOC:30

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

proof end;

theorem Th31: :: RELOC:31

for k being Element of NAT
for s being State of SCM holds Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))

proof end;

theorem Th32: :: RELOC:32

for INS being Instruction of SCM
for s being State of SCM
for j, k being Element of NAT st IC s = j + k holds
Exec (INS,(s +* (Start-At (((IC s) -' k),SCM)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM))

proof end;

begin

theorem :: RELOC:33

for k being Element of NAT
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM 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))) +* (ProgramPart (Relocated (p,k)))

proof end;

Lm1: for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM 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),(s1 +* (DataPart s2)),i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )

proof end;

theorem :: RELOC:34

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM 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)) by Lm1;

theorem Th35: :: RELOC:35

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated (p,k) c= s2 holds
for i being Element of NAT holds IncAddr ((CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) by Lm1;

theorem :: RELOC:36

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated (p,k) c= s2 holds
for i being Element of NAT holds (Comput ((ProgramPart s1),s1,i)) | (dom (DataPart p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (DataPart (Relocated (p,k)))) by Lm1;

theorem :: RELOC:37

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2, s3 being State of SCM st IC SCM in dom p & p c= s1 & Relocated (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds
for i being Element of NAT holds DataPart (Comput ((ProgramPart s1),s3,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) by Lm1;

theorem Th38: :: RELOC:38

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

proof end;

theorem Th39: :: RELOC:39

for k being Element of NAT
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM 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))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))

proof end;

theorem Th40: :: RELOC:40

for k being Element of NAT
for p being FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM 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))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)

proof end;

theorem Th41: :: RELOC:41

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

proof end;

theorem Th42: :: RELOC:42

for p being non program-free autonomic halting FinPartState of SCM st IC SCM in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))

proof end;

registration

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

proof end;

end;

theorem :: RELOC:43

for F being PartFunc of (FinPartSt SCM),(FinPartSt SCM)
for l being Element of NAT
for p being b₂ -started non program-free autonomic halting FinPartState of SCM st IC SCM 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;