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