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