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

  ack(0,y) -> s(y)
  ack(s(x),0) -> ack(x,s(0))
  ack(s(x),s(y)) -> ack(x,plus(y,ack(s(x),y)))
)