:: On the Instructions of { \bf SCM }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: AMI_6:1
theorem Th2: :: AMI_6:2
theorem Th3: :: AMI_6:3
theorem :: AMI_6:4
canceled;
theorem Th5: :: AMI_6:5
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 T being InsType of SCM holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
theorem :: AMI_6:6
canceled;
theorem Th7: :: AMI_6:7
theorem :: AMI_6:8
canceled;
theorem :: AMI_6:9
canceled;
theorem :: AMI_6:10
canceled;
theorem :: AMI_6:11
canceled;
theorem :: AMI_6:12
canceled;
theorem :: AMI_6:13
canceled;
theorem :: AMI_6:14
canceled;
theorem :: AMI_6:15
canceled;
theorem Th16: :: AMI_6:16
theorem Th17: :: AMI_6:17
theorem Th18: :: AMI_6:18
theorem Th19: :: AMI_6:19
theorem Th20: :: AMI_6:20
theorem Th21: :: AMI_6:21
theorem Th22: :: AMI_6:22
theorem Th23: :: AMI_6:23
theorem Th24: :: AMI_6:24
theorem Th25: :: AMI_6:25
theorem Th26: :: AMI_6:26
theorem Th27: :: AMI_6:27
theorem Th28: :: AMI_6:28
theorem Th29: :: AMI_6:29
theorem Th30: :: AMI_6:30
theorem Th31: :: AMI_6:31
theorem Th32: :: AMI_6:32
theorem Th33: :: AMI_6:33
theorem Th34: :: AMI_6:34
theorem Th35: :: AMI_6:35
theorem Th36: :: AMI_6:36
theorem Th37: :: AMI_6:37
theorem Th38: :: AMI_6:38
theorem Th39: :: AMI_6:39
Lm4:
for l being Instruction-Location of SCM
for i being Instruction of SCM st ( for s being State of SCM st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM ) = Next ) holds
NIC i,l = {(Next )}
Lm5:
for i being Instruction of SCM st ( for l being Instruction-Location of SCM holds NIC i,l = {(Next )} ) holds
JUMP i is empty
theorem Th40: :: AMI_6:40
theorem Th41: :: AMI_6:41
theorem Th42: :: AMI_6:42
theorem Th43: :: AMI_6:43
theorem Th44: :: AMI_6:44
theorem Th45: :: AMI_6:45
theorem Th46: :: AMI_6:46
theorem Th47: :: AMI_6:47
theorem Th48: :: AMI_6:48
theorem Th49: :: AMI_6:49
theorem Th50: :: AMI_6:50
theorem Th51: :: AMI_6:51
theorem Th52: :: AMI_6:52
theorem Th53: :: AMI_6:53
theorem Th54: :: AMI_6:54
theorem Th55: :: AMI_6:55
theorem Th56: :: AMI_6:56
Lm6:
dl. 0 <> dl. 1
by AMI_3:52;
registration
let a,
b be
Data-Location ;
cluster a := b -> non
jump-only sequential ;
coherence
( not a := b is jump-only & a := b is sequential )
cluster AddTo a,
b -> non
jump-only sequential ;
coherence
( not AddTo a,b is jump-only & AddTo a,b is sequential )
cluster SubFrom a,
b -> non
jump-only sequential ;
coherence
( not SubFrom a,b is jump-only & SubFrom a,b is sequential )
cluster MultBy a,
b -> non
jump-only sequential ;
coherence
( not MultBy a,b is jump-only & MultBy a,b is sequential )
cluster Divide a,
b -> non
jump-only sequential ;
coherence
( not Divide a,b is jump-only & Divide a,b is sequential )
end;
theorem Th57: :: AMI_6:57
theorem Th58: :: AMI_6:58
theorem Th59: :: AMI_6:59