:: Relocability for { \bf SCM } over Ring :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received February 6, 2004 :: Copyright (c) 2004-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, XBOOLE_0, SETFAM_1, FUNCSDOM, AMI_3, AMI_1, FSM_1, STRUCT_0, AMI_2, FUNCT_1, TARSKI, RELAT_1, AMISTD_2, ARYTM_3, FUNCT_4, CIRCUIT2, CARD_1, GRAPHSP, ARYTM_1, SUPINF_2, FUNCOP_1, ZFMISC_1, PARTFUN1, RELOC, NAT_1, AMISTD_5, COMPOS_1, FINSET_1, GOBRD13, MEMSTR_0, EXTPRO_1; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1, RELAT_1, FINSET_1, NUMBERS, FUNCT_1, PARTFUN1, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCOP_1, XCMPLX_0, NAT_1, FUNCT_4, FUNCT_7, NAT_D, VALUED_1, PBOOLE, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRING1, SCMRING2, SCMRING3, AMISTD_2, AMISTD_5; constructors XXREAL_0, REALSET2, AMI_3, AMISTD_2, SCMRING3, PRE_POLY, NAT_D, AMISTD_1, AMISTD_5, PBOOLE, INT_3, FUNCT_7, RELSET_1, MEMSTR_0, SCMRING1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XREAL_0, NAT_1, CARD_3, STRUCT_0, AMI_3, SCMRING2, AMISTD_2, SCMRING3, FINSET_1, ORDINAL1, FUNCT_4, COMPOS_1, EXTPRO_1, AMI_5, MEMSTR_0, INT_3, COMPOS_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: SCM R reserve i, j, k for Nat, n for Nat, IL for non empty set, N for with_non-empty_elements set; reserve R for non trivial Ring, a, b for Data-Location of R, loc for Nat, I for Instruction of SCM R, p for FinPartState of SCM R, s, s1, s2 for State of SCM R, P,P1,P2 for Instruction-Sequence of SCM R, q for FinPartState of SCM; theorem :: SCMRING4:1 dl.(R,n) = [1,n]; theorem :: SCMRING4:2 for dl being Data-Location of R ex i being Nat st dl = dl.(R,i); theorem :: SCMRING4:3 for i,j being Nat holds i <> j implies dl.(R,i) <> dl.(R,j); theorem :: SCMRING4:4 Data-Locations SCM c= dom s; theorem :: SCMRING4:5 s.a = (s +* Start-At(loc,SCM R)).a; theorem :: SCMRING4:6 for s1,s2 being State of SCM R st IC(s1) = IC(s2) & (for a being Data-Location of R holds s1.a = s2.a) holds s1 = s2; registration let R; cluster SCM R -> relocable; end; definition let R; let a be Data-Location of R; let r be Element of R; redefine func a .--> r -> FinPartState of SCM R; end; registration let R be non trivial Ring; cluster SCM R -> IC-recognized; end; registration let R be non trivial Ring; cluster SCM R -> CurIns-recognized; end; theorem :: SCMRING4:7 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM R st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr(P1,Comput(P1,s1,n)) = a := b & a in dom p holds Comput(P1,s1,n).b = Comput(P2,s2,n).b; theorem :: SCMRING4:8 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM R st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr(P1,Comput(P1,s1,n)) = AddTo(a,b) & a in dom p holds Comput(P1,s1,n).a + Comput(P1,s1,n).b = Comput(P2,s2,n).a + Comput(P2,s2,n).b; theorem :: SCMRING4:9 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM R st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr(P1,Comput(P1,s1,n)) = SubFrom(a, b) & a in dom p holds Comput(P1,s1,n).a - Comput( P1,s1,n).b = Comput(P2,s2,n).a - Comput(P2,s2,n).b; theorem :: SCMRING4:10 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM R st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr(P1,Comput(P1,s1,n)) = MultBy(a, b) & a in dom p holds Comput(P1,s1,n).a * Comput( P1,s1,n).b = Comput(P2,s2,n).a * Comput(P2,s2,n).b; theorem :: SCMRING4:11 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM R st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr(P1,Comput(P1,s1,n)) = a =0_goto loc & loc <> (IC Comput(P1,s1,n)) + 1 holds Comput( P1,s1,n).a = 0. R iff Comput(P2,s2,n).a = 0.R; begin :: Relocability theorem :: SCMRING4:12 for q being non halt-free finite (the InstructionsF of SCM R)-valued NAT-defined Function for p being non empty q-autonomic FinPartState of SCM R st p c= s1 & IncIC( p,k) c= s2 for P1,P2 being Instruction-Sequence of SCM R st q c= P1 & Reloc(q,k) c= P2 for i being 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); registration let R be non trivial Ring; cluster SCM R -> relocable1 relocable2; end;