(VAR x y)
(RULES
  +(x,0) -> x
  +(x,s(y)) -> s(+(x,y))
)