:: The Construction of { \bf SCM } over Ring :: by Artur Korni{\l}owicz :: :: Received November 29, 1998 :: Copyright (c) 1998-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, SUBSET_1, CARD_1, AMI_2, XBOOLE_0, STRUCT_0, ZFMISC_1, ARYTM_3, SUPINF_2, RELAT_1, FINSEQ_1, FUNCSDOM, FUNCT_1, CARD_3, AMI_1, FUNCT_4, FUNCOP_1, ARYTM_1, FUNCT_5, TARSKI, SCMRING1, GROUP_9, AFINSQ_1, PBOOLE, ORDINAL1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PBOOLE, AFINSQ_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1, MCART_1, CARD_3, FINSEQ_1, FUNCOP_1, FUNCT_4, FUNCT_5, AMI_2, SCMRINGI; constructors REALSET2, FUNCT_5, RELSET_1, AMI_2, FUNCOP_1, COMPOS_1, SCMRINGI, BINOP_1, FUNCT_4, XTUPLE_0, XCMPLX_0; registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSEQ_1, CARD_3, STRUCT_0, AMI_2, CARD_1, ORDINAL2, FUNCT_1, FUNCT_2, RELSET_1, AFINSQ_1, SCM_INST, XCMPLX_0, NAT_1; requirements NUMERALS, SUBSET, BOOLE; begin :: The construction of { \bf SCM } over ring reserve i, j, k for Element of NAT, I for Element of Segm 8, i1, i2 for Element of NAT, d1, d2, d3, d4 for Element of SCM-Data-Loc, S for non empty 1-sorted; reserve G for non empty 1-sorted; definition ::$CD 2 let S be non empty 1-sorted; func SCM-VAL S -> ManySortedSet of Segm 2 equals :: SCMRING1:def 3 <%NAT,the carrier of S%>; end; ::$CT theorem :: SCMRING1:2 ((SCM-VAL G)*SCM-OK).NAT = NAT; theorem :: SCMRING1:3 for i being Element of SCM-Memory st i in SCM-Data-Loc holds ((SCM-VAL G)*SCM-OK).i = the carrier of G; registration let G; cluster ((SCM-VAL G)*SCM-OK) -> non-empty; end; definition let S be non empty 1-sorted; mode SCM-State of S is Element of product((SCM-VAL S)*SCM-OK); end; theorem :: SCMRING1:4 ((SCM-VAL G)*SCM-OK).d1 = the carrier of G; theorem :: SCMRING1:5 pi(product((SCM-VAL G)*SCM-OK),NAT) = NAT; theorem :: SCMRING1:6 for a being Element of SCM-Data-Loc holds pi(product((SCM-VAL G)*SCM-OK),a) = the carrier of G; definition let G; let s be SCM-State of G; func IC s -> Element of NAT equals :: SCMRING1:def 4 s.NAT; end; definition let R be non empty 1-sorted, s be SCM-State of R, u be natural Number; func SCM-Chg(s,u) -> SCM-State of R equals :: SCMRING1:def 5 s +* (NAT .--> u); end; theorem :: SCMRING1:7 for s being SCM-State of G, u being natural Number holds SCM-Chg(s,u).NAT = u ; theorem :: SCMRING1:8 for s being SCM-State of G, u being natural Number, mk being Element of SCM-Data-Loc holds SCM-Chg(s,u).mk = s.mk; theorem :: SCMRING1:9 for s being SCM-State of G, u, v being natural Number holds SCM-Chg(s,u).v = s.v; definition let R be non empty 1-sorted, s be SCM-State of R, t be Element of SCM-Data-Loc, u be Element of R; func SCM-Chg(s,t,u) -> SCM-State of R equals :: SCMRING1:def 6 s +* (t .--> u); end; theorem :: SCMRING1:10 for s being SCM-State of G, t being Element of SCM-Data-Loc, u being Element of G holds SCM-Chg(s,t,u).NAT = s.NAT; theorem :: SCMRING1:11 for s being SCM-State of G, t being Element of SCM-Data-Loc, u being Element of G holds SCM-Chg(s,t,u).t = u; theorem :: SCMRING1:12 for s being SCM-State of G, t being Element of SCM-Data-Loc, u being Element of G, mk being Element of SCM-Data-Loc st mk <> t holds SCM-Chg(s,t,u). mk = s.mk; definition let R be non empty 1-sorted, s be SCM-State of R, a be Element of SCM-Data-Loc; redefine func s.a -> Element of R; end; definition let S be non empty 1-sorted, d be Element of SCM-Data-Loc, s be Element of S; redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S; end; definition ::$CD 7 let R be Ring, x be Element of SCM-Instr R, s be SCM-State of R; func SCM-Exec-Res (x,s) -> SCM-State of R equals :: SCMRING1:def 14 SCM-Chg(SCM-Chg(s, x address_1, s.(x address_2)), IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>], SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)+s.(x address_2)), IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>], SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)-s.(x address_2)), IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>], SCM-Chg(SCM-Chg(s, x address_1, s.(x address_1)*s.(x address_2)), IC s + 1) if ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>], SCM-Chg(s, x jump_address) if ex mk being Element of NAT st x = [6,<*mk*>,{}], SCM-Chg(s, IFEQ(s.(x cond_address), 0.R, x cjump_address, IC s + 1)) if ex mk being Element of NAT, ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>], SCM-Chg(SCM-Chg(s, x const_address, x const_value), IC s + 1) if ex mk being Element of SCM-Data-Loc, r being Element of R st x = [5,{},<*mk,r*>] otherwise s; end; definition let R be Ring; func SCM-Exec R -> Action of SCM-Instr R, product((SCM-VAL R)*SCM-OK) means :: SCMRING1:def 15 for x being Element of SCM-Instr R, y being SCM-State of R holds (it.x).y = SCM-Exec-Res (x,y); end; ::$CT 6 theorem :: SCMRING1:19 for s being SCM-State of S holds dom s = SCM-Memory;