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


begin

registration
let a, b be Data-Location;
clustera := b ->  ins-loc-free ;
coherence
 a := b is ins-loc-free ;
cluster AddTo (a,b) ->  ins-loc-free ;
coherence
 AddTo (a,b) is ins-loc-free ;
cluster SubFrom (a,b) ->  ins-loc-free ;
coherence
 SubFrom (a,b) is ins-loc-free ;
cluster MultBy (a,b) ->  ins-loc-free ;
coherence
 MultBy (a,b) is ins-loc-free ;
cluster Divide (a,b) ->  ins-loc-free ;
coherence
 Divide (a,b) is ins-loc-free ;
end;

theorem Th1: :: RELOC:1
for k, loc being Nat holds IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k)
proofend;

theorem Th2: :: RELOC:2
for k, loc being Nat
for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
proofend;

theorem Th3: :: RELOC:3
for k, loc being Nat
for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
proofend;

theorem Th4: :: RELOC:4
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
proofend;

theorem :: RELOC:5
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
proofend;

registration
cluster SCM  ->  relocable ;
coherence
 SCM is relocable
proofend;
end;

begin

Lm1:  for k being Element of NAT
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
proofend;

theorem :: RELOC:6
for k being Element of NAT
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) by Lm1;

registration
cluster SCM  ->  relocable1 relocable2 ;
coherence
 ( SCM is relocable1 & SCM is relocable2 )
proofend;
end;

theorem :: RELOC:7
for k being Element of NAT
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of SCM
for s1, s2, s3 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds DataPart (Comput (P1,s3,i)) = DataPart (Comput (P2,s2,i)) by Lm1;