(VAR x y)
(RULES
  +(s(x),y) -> s(+(x,y))
  +(x,s(y)) -> s(+(x,y))
  +(x,y) -> +(y,x)
)
(COMMENT Example 6.3.4 of \cite{BN98})