(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)) )