(VAR x y z)
(RULES
  +(0,y) -> y
  +(x,0) -> x
  +(s(x),y) -> s(+(x,y))
  +(x,s(y)) -> s(+(x,y))
  +(x,+(y,z)) -> +(+(x,y),z)
  +(x,y) -> +(y,x)
)
(COMMENT
doi:10.2168/LMCS-8(1:31)2012
[35] Example 3.31 (R_3)
)