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