:: Relocatability
:: by Yasushi Tanaka
::
:: Received June 16, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, AMI_1, AMI_3, AMISTD_2, ARYTM_3, GRAPHSP,
CARD_1, RELAT_1, FUNCT_1, TARSKI, FUNCT_4, XBOOLE_0, FSM_1, CIRCUIT2,
EXTPRO_1, ARYTM_1, INT_1, XXREAL_0, STRUCT_0, RELOC, FINSET_1, FINSEQ_1,
NAT_1, AMISTD_5, COMPOS_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, INT_1, NAT_1, VALUED_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4,
PBOOLE, FINSEQ_1, NAT_D, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1,
EXTPRO_1, AMI_3, XXREAL_0, AMISTD_2, AMISTD_5;
constructors DOMAIN_1, XXREAL_0, AMI_3, NAT_D, PRE_POLY, AMISTD_2, VALUED_1,
AMI_2, AMISTD_1, AMISTD_5, PBOOLE, MEMSTR_0, RELSET_1, XTUPLE_0;
registrations FUNCT_1, ORDINAL1, XREAL_0, INT_1, AMI_3, FUNCT_4, AMI_6,
VALUED_0, AMISTD_2, COMPOS_1, EXTPRO_1, NAT_1, FINSEQ_1, AMI_5, MEMSTR_0,
COMPOS_0, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
begin :: Relocatability
reserve j, k, m for Nat;
registration
let a,b be Data-Location;
cluster a:=b -> ins-loc-free;
cluster AddTo(a,b) -> ins-loc-free;
cluster SubFrom(a,b) -> ins-loc-free;
cluster MultBy(a,b) -> ins-loc-free;
cluster Divide(a,b) -> ins-loc-free;
end;
theorem :: RELOC:1
for k,loc being Nat
holds IncAddr(SCM-goto loc,k) = SCM-goto (loc + k);
theorem :: RELOC:2
for k,loc being Nat, a being Data-Location
holds IncAddr(a=0_goto loc,k) = a=0_goto (loc + k);
theorem :: RELOC:3
for k,loc being Nat, a being Data-Location
holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k);
theorem :: RELOC:4
for I being Instruction of SCM, k being Element of NAT st
InsCode I = 0 or ... or InsCode I = 5 holds IncAddr (I, k) = I;
theorem :: RELOC:5
for II, I being Instruction of SCM, k being Element of NAT st (
InsCode I = 0 or ... or InsCode I = 5) & IncAddr (II, k) = I holds II = I;
registration
cluster SCM -> relocable;
end;
begin
theorem :: RELOC:6
for k being Element of NAT
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function,
p being q-autonomic non empty FinPartState of SCM , s1
, s2 being State of SCM
st IC SCM in dom p & p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & Reloc(q,k) c= P2
for i being Element of NAT holds IC Comput(P1,s1,i) + k = IC
Comput(P2,s2,i);
registration
cluster SCM -> relocable1 relocable2;
end;
theorem :: RELOC:7
for k being Element of NAT
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function,
p being q-autonomic non empty FinPartState of SCM , s1
, s2, s3 being State of SCM st IC SCM 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
for i being Element of NAT holds DataPart
Comput(P1,s3,i) = DataPart Comput(P2,s2,i);