:: On the Decomposition of the States of SCM :: by Yasushi Tanaka :: :: Received November 23, 1993 :: Copyright (c) 1993-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 NUMBERS, AMI_3, SUBSET_1, AMI_2, AMI_1, STRUCT_0, XBOOLE_0, FSM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, XXREAL_0, FINSEQ_1, GRAPHSP, ARYTM_3, ARYTM_1, INT_1, FUNCT_4, FUNCOP_1, CIRCUIT2, PARTFUN1, EXTPRO_1, RECDEF_2, CAT_1, AMISTD_5, COMPOS_1, NAT_1; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCOP_1, PARTFUN1, FUNCT_4, NUMBERS, INT_1, NAT_1, RECDEF_2, STRUCT_0, FINSET_1, FINSEQ_1, MEMSTR_0, COMPOS_0, SCM_INST, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0, AMISTD_5; constructors DOMAIN_1, FINSEQ_4, AMI_3, PRE_POLY, AMISTD_5, FUNCT_7, RELSET_1; registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1, AMI_3, FINSET_1, CARD_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, MEMSTR_0, COMPOS_0, XTUPLE_0, FACIRC_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve x,y for set; theorem :: AMI_5:1 for dl being Data-Location ex i being Nat st dl = dl.i; theorem :: AMI_5:2 for dl being Data-Location holds dl <> IC SCM; theorem :: AMI_5:3 for il being Nat, dl being Data-Location holds il <> dl; reserve i, j, k for Nat; theorem :: AMI_5:4 for s being State of SCM, d being Data-Location holds d in dom s; registration cluster Data-Locations SCM -> infinite; end; reserve I,J,K for Element of Segm 9, a,a1 for Nat, b,b1,c for Element of Data-Locations SCM; theorem :: AMI_5:5 for l being Instruction of SCM holds InsCode(l) <= 8; reserve a, b for Data-Location, loc for Nat; reserve I,J,K for Element of Segm 9, a,a1 for Nat, b,b1,c for Element of Data-Locations SCM, da,db for Data-Location; ::$CT theorem :: AMI_5:7 for ins being Instruction of SCM st InsCode ins = 0 holds ins = halt SCM; theorem :: AMI_5:8 for ins being Instruction of SCM st InsCode ins = 1 holds ex da, db st ins = da:=db; theorem :: AMI_5:9 for ins being Instruction of SCM st InsCode ins = 2 holds ex da, db st ins = AddTo(da,db); theorem :: AMI_5:10 for ins being Instruction of SCM st InsCode ins = 3 holds ex da, db st ins = SubFrom(da,db); theorem :: AMI_5:11 for ins being Instruction of SCM st InsCode ins = 4 holds ex da, db st ins = MultBy(da,db); theorem :: AMI_5:12 for ins being Instruction of SCM st InsCode ins = 5 holds ex da, db st ins = Divide(da,db); theorem :: AMI_5:13 for ins being Instruction of SCM st InsCode ins = 6 holds ex loc st ins = SCM-goto loc; theorem :: AMI_5:14 for ins being Instruction of SCM st InsCode ins = 7 holds ex loc ,da st ins = da=0_goto loc; theorem :: AMI_5:15 for ins being Instruction of SCM st InsCode ins = 8 holds ex loc ,da st ins = da>0_goto loc; begin :: Finite partial states of SCM theorem :: AMI_5:16 for s being State of SCM, iloc being Nat, a being Data-Location holds s.a = (s +* Start-At(iloc,SCM)).a; begin :: Autonomic finite partial states of SCM registration cluster SCM -> IC-recognized; end; registration cluster SCM -> CurIns-recognized; end; theorem :: AMI_5:17 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = da := db & da in dom p implies Comput(P1,s1,i).db = Comput(P2,s2,i).db; theorem :: AMI_5:18 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1, s1,i)) holds I = AddTo(da, db) & da in dom p implies Comput(P1,s1,i).da + Comput(P1,s1,i).db = Comput(P2,s2,i).da + Comput( P2,s2,i).db; theorem :: AMI_5:19 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1, s1,i)) holds I = SubFrom(da, db) & da in dom p implies Comput(P1,s1,i). da - Comput(P1,s1,i).db = Comput(P2,s2,i).da - Comput( P2,s2,i).db; theorem :: AMI_5:20 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = MultBy(da, db) & da in dom p implies Comput(P1,s1,i). da * Comput(P1,s1,i).db = Comput(P2,s2,i).da * Comput(P2,s2,i).db; theorem :: AMI_5:21 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = Divide(da, db) & da in dom p & da <> db implies Comput(P1,s1 ,i).da div Comput(P1,s1,i).db = Comput(P2,s2,i).da div Comput(P2,s2,i).db; theorem :: AMI_5:22 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da, db being Data-Location, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = Divide(da, db) & db in dom p implies Comput(P1,s1,i). da mod Comput(P1,s1,i).db = Comput(P2,s2,i).da mod Comput(P2,s2,i).db; theorem :: AMI_5:23 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da being Data-Location, loc being Nat, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = da=0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1 implies ( Comput(P1,s1,i).da = 0 iff Comput(P2,s2,i) .da = 0); theorem :: AMI_5:24 for q being non halt-free finite (the InstructionsF of SCM)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 for i being Nat, da being Data-Location, loc being Nat, I being Instruction of SCM st I = CurInstr(P1,Comput(P1,s1,i)) holds I = da>0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1 implies ( Comput(P1,s1,i).da > 0 iff Comput(P2,s2,i) .da > 0); theorem :: AMI_5:25 for s1,s2 being State of SCM st IC(s1) = IC(s2) & (for a being Data-Location holds s1.a = s2.a) holds s1 = s2;