:: The Properties of Instructions of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: SCMRING3:1
theorem Th2: :: SCMRING3:2
theorem Th3: :: SCMRING3:3
theorem Th4: :: SCMRING3:4
theorem Th5: :: SCMRING3:5
theorem :: SCMRING3:6
canceled;
theorem Th7: :: SCMRING3:7
theorem Th8: :: SCMRING3:8
theorem :: SCMRING3:9
theorem Th10: :: SCMRING3:10
theorem Th11: :: SCMRING3:11
theorem Th12: :: SCMRING3:12
theorem Th13: :: SCMRING3:13
theorem Th14: :: SCMRING3:14
theorem Th15: :: SCMRING3:15
theorem Th16: :: SCMRING3:16
theorem Th17: :: SCMRING3:17
theorem Th18: :: SCMRING3:18
theorem Th19: :: SCMRING3:19
theorem Th20: :: SCMRING3:20
theorem Th21: :: SCMRING3:21
theorem Th22: :: SCMRING3:22
theorem Th23: :: SCMRING3:23
Lm1:
for x, y being set st x in dom <*y*> holds
x = 1
Lm2:
for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )
Lm3:
for R being good Ring
for T being InsType of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
theorem Th24: :: SCMRING3:24
theorem :: SCMRING3:25
canceled;
theorem :: SCMRING3:26
canceled;
theorem :: SCMRING3:27
canceled;
theorem :: SCMRING3:28
canceled;
theorem :: SCMRING3:29
canceled;
theorem :: SCMRING3:30
canceled;
theorem :: SCMRING3:31
canceled;
theorem Th32: :: SCMRING3:32
theorem Th33: :: SCMRING3:33
theorem Th34: :: SCMRING3:34
theorem Th35: :: SCMRING3:35
theorem Th36: :: SCMRING3:36
theorem Th37: :: SCMRING3:37
theorem Th38: :: SCMRING3:38
theorem Th39: :: SCMRING3:39
theorem Th40: :: SCMRING3:40
theorem Th41: :: SCMRING3:41
theorem Th42: :: SCMRING3:42
theorem Th43: :: SCMRING3:43
theorem Th44: :: SCMRING3:44
theorem Th45: :: SCMRING3:45
theorem Th46: :: SCMRING3:46
theorem Th47: :: SCMRING3:47
theorem Th48: :: SCMRING3:48
theorem Th49: :: SCMRING3:49
theorem Th50: :: SCMRING3:50
theorem Th51: :: SCMRING3:51
theorem Th52: :: SCMRING3:52
Lm5:
for R being good Ring
for l being Instruction-Location of SCM R
for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = Next (IC s) ) holds
NIC i,l = {(Next l)}
Lm6:
for R being good Ring
for i being Instruction of (SCM R) st ( for l being Instruction-Location of SCM R holds NIC i,l = {(Next l)} ) holds
JUMP i is empty
theorem Th53: :: SCMRING3:53
theorem Th54: :: SCMRING3:54
theorem Th55: :: SCMRING3:55
theorem Th56: :: SCMRING3:56
theorem Th57: :: SCMRING3:57
theorem Th58: :: SCMRING3:58
theorem Th59: :: SCMRING3:59
theorem Th60: :: SCMRING3:60
theorem Th61: :: SCMRING3:61
theorem :: SCMRING3:62
theorem Th63: :: SCMRING3:63
theorem Th64: :: SCMRING3:64
theorem Th65: :: SCMRING3:65
theorem Th66: :: SCMRING3:66
theorem Th67: :: SCMRING3:67
theorem Th68: :: SCMRING3:68
:: deftheorem defines dl. SCMRING3:def 1 :
theorem Th69: :: SCMRING3:69
theorem Th70: :: SCMRING3:70
theorem :: SCMRING3:71