|
105
|
1 |
BoolNat = Arith +
|
|
|
2 |
types bool,nat 0
|
|
|
3 |
arities bool,nat :: arith
|
|
|
4 |
consts Suc :: "nat=>nat"
|
|
|
5 |
rules add0 "0 + n = n::nat"
|
|
|
6 |
addS "Suc(m)+n = Suc(m+n)"
|
|
|
7 |
nat1 "1 = Suc(0)"
|
|
|
8 |
or0l "0 + x = x::bool"
|
|
|
9 |
or0r "x + 0 = x::bool"
|
|
|
10 |
or1l "1 + x = 1::bool"
|
|
|
11 |
or1r "x + 1 = 1::bool"
|
|
|
12 |
end
|