(VAR x y)
(THEORY (AC plus))
(RULES
minus(plus(x,y),y) -> x
dix(zero, s(y)) -> 0
div(s(x),s(y)) -> s(div(minus(x,y), s(y)))
plus(0,x) -> x
plus(s(x),y) -> s(plus(x,y))
)