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