Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### The Basic Properties of \SCM over Ring

**by****Artur Kornilowicz**- Received November 29, 1998
- MML identifier: SCMRING2

- [ Mizar article, MML identifier index ]

environ vocabulary GR_CY_1, SCMFSA7B, FUNCSDOM, AMI_3, AMI_1, AMI_2, FUNCT_1, CAT_1, BOOLE, FINSEQ_1, FUNCT_2, CARD_3, ARYTM_1, RLVECT_1, CQC_LANG, SCMRING1, MCART_1, FUNCT_4, RELAT_1; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, GR_CY_1, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, MCART_1, NUMBERS, XREAL_0, CARD_3, NAT_1, FINSEQ_1, CQC_LANG, FUNCT_4, AMI_1, AMI_2, AMI_3, SCMRING1; constructors AMI_3, CAT_2, DOMAIN_1, FINSEQ_4, NAT_1, REALSET1, SCMRING1, MEMBERED; clusters AMI_1, CQC_LANG, SCMRING1, STRUCT_0, RELSET_1, AMI_5, AMI_3, FINSEQ_5, XBOOLE_0, FRAENKEL, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: { \bf SCM } over ring reserve i for Nat, I for Element of Segm 8, S for non empty 1-sorted, t for Element of S, x for set; definition let R be good Ring; func SCM R -> strict AMI-Struct over { the carrier of R } means :: SCMRING2:def 1 the carrier of it = NAT & the Instruction-Counter of it = 0 & the Instruction-Locations of it = SCM-Instr-Loc & the Instruction-Codes of it = Segm 8 & the Instructions of it = SCM-Instr R & the Object-Kind of it = SCM-OK R & the Execution of it = SCM-Exec R; end; definition let R be good Ring; cluster SCM R -> non empty non void; end; definition let R be good Ring, s be State of SCM R, a be Element of SCM-Data-Loc; redefine func s.a -> Element of R; end; definition let R be good Ring; mode Data-Location of R -> Object of SCM R means :: SCMRING2:def 2 it in (the carrier of SCM R) \ (SCM-Instr-Loc \/ {0}); end; reserve R for good Ring, r for Element of R, a, b, c, d1, d2 for Data-Location of R, i1 for Instruction-Location of SCM R; theorem :: SCMRING2:1 x is Data-Location of R iff x in SCM-Data-Loc; definition let R be good Ring, s be State of SCM R, a be Data-Location of R; redefine func s.a -> Element of R; end; theorem :: SCMRING2:2 [0,{}] in SCM-Instr S; theorem :: SCMRING2:3 [0,{}] is Instruction of SCM R; theorem :: SCMRING2:4 x in {1,2,3,4} implies [x,<*d1,d2*>] in SCM-Instr S; theorem :: SCMRING2:5 [5,<*d1,t*>] in SCM-Instr S; theorem :: SCMRING2:6 [6,<*i1*>] in SCM-Instr S; theorem :: SCMRING2:7 [7,<*i1,d1*>] in SCM-Instr S; definition let R be good Ring, a, b be Data-Location of R; func a := b -> Instruction of SCM R equals :: SCMRING2:def 3 [ 1, <*a, b*>]; func AddTo(a,b) -> Instruction of SCM R equals :: SCMRING2:def 4 [ 2, <*a, b*>]; func SubFrom(a,b) -> Instruction of SCM R equals :: SCMRING2:def 5 [ 3, <*a, b*>]; func MultBy(a,b) -> Instruction of SCM R equals :: SCMRING2:def 6 [ 4, <*a, b*>]; end; definition let R be good Ring, a be Data-Location of R, r be Element of R; func a := r -> Instruction of SCM R equals :: SCMRING2:def 7 [ 5, <*a,r*>]; end; definition let R be good Ring, l be Instruction-Location of SCM R; func goto l -> Instruction of SCM R equals :: SCMRING2:def 8 [ 6, <*l*>]; end; definition let R be good Ring, l be Instruction-Location of SCM R, a be Data-Location of R; func a=0_goto l -> Instruction of SCM R equals :: SCMRING2:def 9 [ 7, <*l,a*>]; end; theorem :: SCMRING2:8 for I being set holds I is Instruction of SCM R iff I = [0,{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or (ex i1 st I = goto i1) or (ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r; reserve s for State of SCM R; definition let R; cluster SCM R -> IC-Ins-separated; end; theorem :: SCMRING2:9 IC SCM R = 0; theorem :: SCMRING2:10 for S being SCM-State of R st S = s holds IC s = IC S; definition let R be good Ring, i1 be Instruction-Location of SCM R; func Next i1 -> Instruction-Location of SCM R means :: SCMRING2:def 10 ex mj being Element of SCM-Instr-Loc st mj = i1 & it = Next mj; end; theorem :: SCMRING2:11 for i1 being Instruction-Location of SCM R, mj being Element of SCM-Instr-Loc st mj = i1 holds Next mj = Next i1; theorem :: SCMRING2:12 for I being Instruction of SCM R for i being Element of SCM-Instr R st i = I for S being SCM-State of R st S = s holds Exec(I,s) = SCM-Exec-Res(i,S); begin :: Users guide theorem :: SCMRING2:13 Exec(a := b, s).IC SCM R = Next IC s & Exec(a := b, s).a = s.b & for c st c <> a holds Exec(a := b, s).c = s.c; theorem :: SCMRING2:14 Exec(AddTo(a,b), s).IC SCM R = Next IC s & Exec(AddTo(a,b), s).a = s.a + s.b & for c st c <> a holds Exec(AddTo(a,b), s).c = s.c; theorem :: SCMRING2:15 Exec(SubFrom(a,b), s).IC SCM R = Next IC s & Exec(SubFrom(a,b), s).a = s.a - s.b & for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c; theorem :: SCMRING2:16 Exec(MultBy(a,b), s).IC SCM R = Next IC s & Exec(MultBy(a,b), s).a = s.a * s.b & for c st c <> a holds Exec(MultBy(a,b), s).c = s.c; theorem :: SCMRING2:17 Exec(goto i1, s).IC SCM R = i1 & Exec(goto i1, s).c = s.c; theorem :: SCMRING2:18 (s.a = 0.R implies Exec(a =0_goto i1, s).IC SCM R = i1) & (s.a <> 0.R implies Exec(a =0_goto i1, s).IC SCM R = Next IC s) & Exec(a =0_goto i1, s).c = s.c; theorem :: SCMRING2:19 Exec(a := r, s).IC SCM R = Next IC s & Exec(a := r, s).a = r & for c st c <> a holds Exec(a := r, s).c = s.c; begin :: Halt instruction theorem :: SCMRING2:20 for I being Instruction of SCM R st ex s st Exec(I,s).IC SCM R = Next IC s holds I is non halting; theorem :: SCMRING2:21 for I being Instruction of SCM R st I = [0,{}] holds I is halting; definition let R, a, b; cluster a:=b -> non halting; cluster AddTo(a,b) -> non halting; cluster SubFrom(a,b) -> non halting; cluster MultBy(a,b) -> non halting; end; definition let R, i1; cluster goto i1 -> non halting; end; definition let R, a, i1; cluster a =0_goto i1 -> non halting; end; definition let R, a, r; cluster a:=r -> non halting; end; definition let R; cluster SCM R -> halting definite data-oriented steady-programmed realistic; end; canceled 7; theorem :: SCMRING2:29 for I being Instruction of SCM R st I is halting holds I = halt SCM R; theorem :: SCMRING2:30 halt SCM R = [0,{}];

Back to top