:: The Basic Properties of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem Def1 defines SCM SCMRING2:def 1 :
:: deftheorem Def2 defines Data-Location SCMRING2:def 2 :
theorem Th1: :: SCMRING2:1
theorem Th2: :: SCMRING2:2
theorem Th3: :: SCMRING2:3
theorem Th4: :: SCMRING2:4
theorem Th5: :: SCMRING2:5
theorem Th6: :: SCMRING2:6
theorem Th7: :: SCMRING2:7
definition
let R be
good Ring;
let a,
b be
Data-Location of
R;
func a := b -> Instruction of
(SCM R) equals :: SCMRING2:def 3
[1,<*a,b*>];
coherence
[1,<*a,b*>] is Instruction of (SCM R)
func AddTo a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 4
[2,<*a,b*>];
coherence
[2,<*a,b*>] is Instruction of (SCM R)
func SubFrom a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 5
[3,<*a,b*>];
coherence
[3,<*a,b*>] is Instruction of (SCM R)
func MultBy a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 6
[4,<*a,b*>];
coherence
[4,<*a,b*>] is Instruction of (SCM R)
end;
:: deftheorem defines := SCMRING2:def 3 :
:: deftheorem defines AddTo SCMRING2:def 4 :
:: deftheorem defines SubFrom SCMRING2:def 5 :
:: deftheorem defines MultBy SCMRING2:def 6 :
:: deftheorem defines := SCMRING2:def 7 :
:: deftheorem defines goto SCMRING2:def 8 :
:: deftheorem defines =0_goto SCMRING2:def 9 :
theorem Th8: :: SCMRING2:8
theorem :: SCMRING2:9
theorem :: SCMRING2:10
theorem :: SCMRING2:11
canceled;
theorem Th12: :: SCMRING2:12
theorem Th13: :: SCMRING2:13
theorem Th14: :: SCMRING2:14
theorem Th15: :: SCMRING2:15
theorem Th16: :: SCMRING2:16
theorem :: SCMRING2:17
theorem Th18: :: SCMRING2:18
theorem Th19: :: SCMRING2:19
theorem Th20: :: SCMRING2:20
theorem Th21: :: SCMRING2:21
Lm1:
for R being good Ring
for a, b being Data-Location of R holds not a := b is halting
Lm2:
for R being good Ring
for a, b being Data-Location of R holds not AddTo a,b is halting
Lm3:
for R being good Ring
for a, b being Data-Location of R holds not SubFrom a,b is halting
Lm4:
for R being good Ring
for a, b being Data-Location of R holds not MultBy a,b is halting
Lm5:
for R being good Ring
for i1 being Instruction-Location of SCM R holds not goto i1 is halting
Lm6:
for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of SCM R holds not a =0_goto i1 is halting
Lm7:
for R being good Ring
for r being Element of R
for a being Data-Location of R holds not a := r is halting
Lm8:
for R being good Ring
for W being Instruction of (SCM R) st W is halting holds
W = [0 ,{} ]
theorem :: SCMRING2:22
canceled;
theorem :: SCMRING2:23
canceled;
theorem :: SCMRING2:24
canceled;
theorem :: SCMRING2:25
canceled;
theorem :: SCMRING2:26
canceled;
theorem :: SCMRING2:27
canceled;
theorem :: SCMRING2:28
canceled;
theorem Th29: :: SCMRING2:29
theorem :: SCMRING2:30
theorem :: SCMRING2:31