(VAR x y)
(THEORY (AC plus))
(RULES
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
bin(0,s(y)) -> 0
bin(x,0) -> s(0)
bin(s(x),s(y)) -> plus(bin(x,y),bin(x,s(y)))
)