(VAR x y)
(RULES
   +(x,0) -> x
   +(x,s(y)) -> s(+(x,y))
   -(0,x) -> 0
   -(x,0) -> x
   -(s(x),s(y)) -> -(x,y)
)
(COMMENT from a collection of Aoto/Toyama, FSCD 2016)