:: The { \bf SCM_FSA } computer
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 7, 1996
:: Copyright (c) 1996 Association of Mizar Users
definition
func SCM+FSA -> strict AMI-Struct of
NAT ,
{INT ,(INT * )} equals :: SCMFSA_2:def 1
AMI-Struct(#
SCM+FSA-Memory ,
(In NAT ,SCM+FSA-Memory ),
SCM+FSA-Instr ,
SCM+FSA-OK ,
SCM+FSA-Exec #);
coherence
AMI-Struct(# SCM+FSA-Memory ,(In NAT ,SCM+FSA-Memory ),SCM+FSA-Instr ,SCM+FSA-OK ,SCM+FSA-Exec #) is strict AMI-Struct of NAT ,{INT ,(INT * )}
;
end;
:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :
theorem :: SCMFSA_2:1
canceled;
theorem :: SCMFSA_2:2
canceled;
theorem :: SCMFSA_2:3
canceled;
theorem :: SCMFSA_2:4
canceled;
theorem :: SCMFSA_2:5
canceled;
theorem :: SCMFSA_2:6
canceled;
theorem Th7: :: SCMFSA_2:7
:: deftheorem defines Int-Locations SCMFSA_2:def 2 :
:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :
theorem :: SCMFSA_2:8
:: deftheorem Def4 defines Int-Location SCMFSA_2:def 4 :
:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def 5 :
theorem :: SCMFSA_2:9
theorem :: SCMFSA_2:10
theorem :: SCMFSA_2:11
theorem :: SCMFSA_2:12
theorem :: SCMFSA_2:13
theorem Th14: :: SCMFSA_2:14
theorem :: SCMFSA_2:15
:: deftheorem defines intloc SCMFSA_2:def 6 :
:: deftheorem defines insloc SCMFSA_2:def 7 :
:: deftheorem defines fsloc SCMFSA_2:def 8 :
theorem :: SCMFSA_2:16
canceled;
theorem :: SCMFSA_2:17
theorem :: SCMFSA_2:18
canceled;
theorem :: SCMFSA_2:19
theorem Th20: :: SCMFSA_2:20
theorem :: SCMFSA_2:21
canceled;
theorem :: SCMFSA_2:22
canceled;
theorem :: SCMFSA_2:23
theorem :: SCMFSA_2:24
theorem Th25: :: SCMFSA_2:25
theorem Th26: :: SCMFSA_2:26
theorem Th27: :: SCMFSA_2:27
theorem :: SCMFSA_2:28
theorem :: SCMFSA_2:29
theorem :: SCMFSA_2:30
canceled;
theorem :: SCMFSA_2:31
canceled;
theorem :: SCMFSA_2:32
canceled;
theorem :: SCMFSA_2:33
canceled;
theorem Th34: :: SCMFSA_2:34
theorem Th35: :: SCMFSA_2:35
theorem :: SCMFSA_2:36
canceled;
theorem :: SCMFSA_2:37
theorem Th38: :: SCMFSA_2:38
definition
let a,
b be
Int-Location ;
canceled;canceled;func a := b -> Instruction of
SCM+FSA means :
Def11:
:: SCMFSA_2:def 11
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = A := B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = A := B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = A := B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = A := B ) holds
b1 = b2;
;
func AddTo a,
b -> Instruction of
SCM+FSA means :
Def12:
:: SCMFSA_2:def 12
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = AddTo A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = AddTo A,B ) holds
b1 = b2;
;
func SubFrom a,
b -> Instruction of
SCM+FSA means :
Def13:
:: SCMFSA_2:def 13
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = SubFrom A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = SubFrom A,B ) holds
b1 = b2;
;
func MultBy a,
b -> Instruction of
SCM+FSA means :
Def14:
:: SCMFSA_2:def 14
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = MultBy A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = MultBy A,B ) holds
b1 = b2;
;
func Divide a,
b -> Instruction of
SCM+FSA means :
Def15:
:: SCMFSA_2:def 15
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = Divide A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = Divide A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = Divide A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = Divide A,B ) holds
b1 = b2;
;
end;
:: deftheorem SCMFSA_2:def 9 :
canceled;
:: deftheorem SCMFSA_2:def 10 :
canceled;
:: deftheorem Def11 defines := SCMFSA_2:def 11 :
:: deftheorem Def12 defines AddTo SCMFSA_2:def 12 :
:: deftheorem Def13 defines SubFrom SCMFSA_2:def 13 :
:: deftheorem Def14 defines MultBy SCMFSA_2:def 14 :
:: deftheorem Def15 defines Divide SCMFSA_2:def 15 :
theorem :: SCMFSA_2:39
:: deftheorem Def16 defines goto SCMFSA_2:def 16 :
:: deftheorem Def17 defines =0_goto SCMFSA_2:def 17 :
:: deftheorem Def18 defines >0_goto SCMFSA_2:def 18 :
definition
let c,
i be
Int-Location ;
let a be
FinSeq-Location ;
func c := a,
i -> Instruction of
SCM+FSA equals :: SCMFSA_2:def 19
[9,<*c,a,i*>];
coherence
[9,<*c,a,i*>] is Instruction of SCM+FSA
func a,
i := c -> Instruction of
SCM+FSA equals :: SCMFSA_2:def 20
[10,<*c,a,i*>];
coherence
[10,<*c,a,i*>] is Instruction of SCM+FSA
end;
:: deftheorem defines := SCMFSA_2:def 19 :
:: deftheorem defines := SCMFSA_2:def 20 :
definition
let i be
Int-Location ;
let a be
FinSeq-Location ;
func i :=len a -> Instruction of
SCM+FSA equals :: SCMFSA_2:def 21
[11,<*i,a*>];
coherence
[11,<*i,a*>] is Instruction of SCM+FSA
func a :=<0,...,0> i -> Instruction of
SCM+FSA equals :: SCMFSA_2:def 22
[12,<*i,a*>];
coherence
[12,<*i,a*>] is Instruction of SCM+FSA
end;
:: deftheorem defines :=len SCMFSA_2:def 21 :
:: deftheorem defines :=<0,...,0> SCMFSA_2:def 22 :
theorem :: SCMFSA_2:40
canceled;
theorem :: SCMFSA_2:41
canceled;
theorem :: SCMFSA_2:42
theorem :: SCMFSA_2:43
theorem :: SCMFSA_2:44
theorem :: SCMFSA_2:45
theorem :: SCMFSA_2:46
theorem :: SCMFSA_2:47
theorem :: SCMFSA_2:48
theorem :: SCMFSA_2:49
theorem :: SCMFSA_2:50
theorem :: SCMFSA_2:51
theorem :: SCMFSA_2:52
theorem :: SCMFSA_2:53
theorem Th54: :: SCMFSA_2:54
theorem Th55: :: SCMFSA_2:55
theorem Th56: :: SCMFSA_2:56
theorem Th57: :: SCMFSA_2:57
theorem Th58: :: SCMFSA_2:58
theorem Th59: :: SCMFSA_2:59
theorem Th60: :: SCMFSA_2:60
theorem Th61: :: SCMFSA_2:61
theorem Th62: :: SCMFSA_2:62
theorem Th63: :: SCMFSA_2:63
theorem Th64: :: SCMFSA_2:64
theorem Th65: :: SCMFSA_2:65
theorem :: SCMFSA_2:66
theorem :: SCMFSA_2:67
theorem Th68: :: SCMFSA_2:68
theorem Th69: :: SCMFSA_2:69
theorem Th70: :: SCMFSA_2:70
theorem :: SCMFSA_2:71
theorem :: SCMFSA_2:72
theorem :: SCMFSA_2:73
theorem :: SCMFSA_2:74
theorem Th75: :: SCMFSA_2:75
theorem Th76: :: SCMFSA_2:76
theorem :: SCMFSA_2:77
canceled;
theorem Th78: :: SCMFSA_2:78
theorem Th79: :: SCMFSA_2:79
theorem Th80: :: SCMFSA_2:80
theorem :: SCMFSA_2:81
theorem :: SCMFSA_2:82
theorem :: SCMFSA_2:83
theorem :: SCMFSA_2:84
theorem :: SCMFSA_2:85
theorem :: SCMFSA_2:86
theorem :: SCMFSA_2:87
canceled;
theorem Th88: :: SCMFSA_2:88
theorem Th89: :: SCMFSA_2:89
theorem Th90: :: SCMFSA_2:90
theorem Th91: :: SCMFSA_2:91
theorem Th92: :: SCMFSA_2:92
theorem Th93: :: SCMFSA_2:93
for
a,
b being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (Divide a,b),s) . (IC SCM+FSA ) = Next & (
a <> b implies
(Exec (Divide a,b),s) . a = (s . a) div (s . b) ) &
(Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for
c being
Int-Location st
c <> a &
c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for
f being
FinSeq-Location holds
(Exec (Divide a,b),s) . f = s . f ) )
theorem :: SCMFSA_2:94
theorem Th95: :: SCMFSA_2:95
theorem Th96: :: SCMFSA_2:96
theorem Th97: :: SCMFSA_2:97
theorem Th98: :: SCMFSA_2:98
theorem Th99: :: SCMFSA_2:99
for
g being
FinSeq-Location for
a,
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (g,a := c),s) . (IC SCM+FSA ) = Next & ex
k being
Element of
NAT st
(
k = abs (s . a) &
(Exec (g,a := c),s) . g = (s . g) +* k,
(s . c) ) & ( for
b being
Int-Location holds
(Exec (g,a := c),s) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec (g,a := c),s) . f = s . f ) )
theorem Th100: :: SCMFSA_2:100
theorem Th101: :: SCMFSA_2:101
for
g being
FinSeq-Location for
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex
k being
Element of
NAT st
(
k = abs (s . c) &
(Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for
b being
Int-Location holds
(Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
theorem :: SCMFSA_2:102
theorem Th103: :: SCMFSA_2:103
theorem Th104: :: SCMFSA_2:104
theorem Th105: :: SCMFSA_2:105
theorem Th106: :: SCMFSA_2:106
theorem Th107: :: SCMFSA_2:107
theorem Th108: :: SCMFSA_2:108
theorem Th109: :: SCMFSA_2:109
theorem Th110: :: SCMFSA_2:110
theorem Th111: :: SCMFSA_2:111
theorem Th112: :: SCMFSA_2:112
theorem Th113: :: SCMFSA_2:113
theorem Th114: :: SCMFSA_2:114
theorem Th115: :: SCMFSA_2:115
theorem Th116: :: SCMFSA_2:116
theorem :: SCMFSA_2:117
canceled;
theorem :: SCMFSA_2:118
theorem Th119: :: SCMFSA_2:119
theorem Th120: :: SCMFSA_2:120
for
I being
set holds
(
I is
Instruction of
SCM+FSA iff (
I = [0 ,{} ] or ex
a,
b being
Int-Location st
I = a := b or ex
a,
b being
Int-Location st
I = AddTo a,
b or ex
a,
b being
Int-Location st
I = SubFrom a,
b or ex
a,
b being
Int-Location st
I = MultBy a,
b or ex
a,
b being
Int-Location st
I = Divide a,
b or ex
la being
Instruction-Location of
SCM+FSA st
I = goto la or ex
lb being
Instruction-Location of
SCM+FSA ex
da being
Int-Location st
I = da =0_goto lb or ex
lb being
Instruction-Location of
SCM+FSA ex
da being
Int-Location st
I = da >0_goto lb or ex
b,
a being
Int-Location ex
fa being
FinSeq-Location st
I = a := fa,
b or ex
a,
b being
Int-Location ex
fa being
FinSeq-Location st
I = fa,
a := b or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = a :=len f or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = f :=<0,...,0> a ) )
Lm1:
for W being Instruction of SCM+FSA st W is halting holds
W = [0 ,{} ]
theorem Th121: :: SCMFSA_2:121
theorem Th122: :: SCMFSA_2:122
theorem Th123: :: SCMFSA_2:123
theorem :: SCMFSA_2:124
theorem :: SCMFSA_2:125
theorem :: SCMFSA_2:126
theorem :: SCMFSA_2:127