:: On the Instructions of { \bf SCM+FSA }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: SCMFSA10:1
canceled;
theorem :: SCMFSA10:2
canceled;
theorem Th3: :: SCMFSA10:3
theorem Th4: :: SCMFSA10:4
theorem Th5: :: SCMFSA10:5
theorem Th6: :: SCMFSA10:6
theorem Th7: :: SCMFSA10:7
theorem :: SCMFSA10:8
canceled;
theorem Th9: :: SCMFSA10:9
theorem Th10: :: SCMFSA10:10
theorem Th11: :: SCMFSA10:11
theorem Th12: :: SCMFSA10:12
theorem Th13: :: SCMFSA10:13
theorem Th14: :: SCMFSA10:14
theorem Th15: :: SCMFSA10:15
theorem Th16: :: SCMFSA10:16
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 x, y, z, t being set holds
( not x in dom <*y,z,t*> or x = 1 or x = 2 or x = 3 )
Lm4:
for T being InsType of SCM+FSA 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 or T = 9 or T = 10 or T = 11 or T = 12 )
theorem Th17: :: SCMFSA10:17
theorem Th18: :: SCMFSA10:18
theorem Th19: :: SCMFSA10:19
theorem Th20: :: SCMFSA10:20
theorem Th21: :: SCMFSA10:21
theorem Th22: :: SCMFSA10:22
theorem Th23: :: SCMFSA10:23
theorem Th24: :: SCMFSA10:24
theorem Th25: :: SCMFSA10:25
theorem :: SCMFSA10:26
theorem :: SCMFSA10:27
theorem :: SCMFSA10:28
theorem :: SCMFSA10:29
theorem Th30: :: SCMFSA10:30
theorem Th31: :: SCMFSA10:31
theorem Th32: :: SCMFSA10:32
theorem Th33: :: SCMFSA10:33
theorem Th34: :: SCMFSA10:34
theorem Th35: :: SCMFSA10:35
theorem Th36: :: SCMFSA10:36
theorem Th37: :: SCMFSA10:37
theorem Th38: :: SCMFSA10:38
theorem Th39: :: SCMFSA10:39
theorem Th40: :: SCMFSA10:40
theorem Th41: :: SCMFSA10:41
theorem Th42: :: SCMFSA10:42
theorem Th43: :: SCMFSA10:43
theorem Th44: :: SCMFSA10:44
theorem Th45: :: SCMFSA10:45
theorem Th46: :: SCMFSA10:46
theorem Th47: :: SCMFSA10:47
theorem Th48: :: SCMFSA10:48
theorem Th49: :: SCMFSA10:49
theorem Th50: :: SCMFSA10:50
theorem Th51: :: SCMFSA10:51
theorem Th52: :: SCMFSA10:52
theorem Th53: :: SCMFSA10:53
theorem Th54: :: SCMFSA10:54
theorem Th55: :: SCMFSA10:55
theorem Th56: :: SCMFSA10:56
theorem Th57: :: SCMFSA10:57
theorem Th58: :: SCMFSA10:58
theorem Th59: :: SCMFSA10:59
theorem Th60: :: SCMFSA10:60
theorem Th61: :: SCMFSA10:61
theorem Th62: :: SCMFSA10:62
theorem Th63: :: SCMFSA10:63
theorem Th64: :: SCMFSA10:64
theorem Th65: :: SCMFSA10:65
theorem Th66: :: SCMFSA10:66
theorem Th67: :: SCMFSA10:67
Lm5:
for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA st ( for s being State of SCM+FSA st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM+FSA ) = Next (IC s) ) holds
NIC i,l = {(Next l)}
Lm6:
for i being Instruction of SCM+FSA st ( for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ) holds
JUMP i is empty
theorem Th68: :: SCMFSA10:68
theorem Th69: :: SCMFSA10:69
theorem Th70: :: SCMFSA10:70
theorem Th71: :: SCMFSA10:71
theorem Th72: :: SCMFSA10:72
theorem Th73: :: SCMFSA10:73
theorem Th74: :: SCMFSA10:74
theorem Th75: :: SCMFSA10:75
theorem Th76: :: SCMFSA10:76
theorem Th77: :: SCMFSA10:77
theorem Th78: :: SCMFSA10:78
theorem Th79: :: SCMFSA10:79
theorem Th80: :: SCMFSA10:80
theorem Th81: :: SCMFSA10:81
theorem Th82: :: SCMFSA10:82
theorem Th83: :: SCMFSA10:83
theorem Th84: :: SCMFSA10:84
theorem Th85: :: SCMFSA10:85
theorem Th86: :: SCMFSA10:86
theorem Th87: :: SCMFSA10:87
theorem Th88: :: SCMFSA10:88
Lm7:
intloc 0 <> intloc 1
by AMI_3:52;
registration
let a,
b be
Int-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;
Lm8:
fsloc 0 <> intloc 0
by SCMFSA_2:126;
Lm9:
fsloc 0 <> intloc 1
by SCMFSA_2:126;
theorem Th89: :: SCMFSA10:89
theorem Th90: :: SCMFSA10:90
theorem Th91: :: SCMFSA10:91