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

theorem :: RELOC:43

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