(CONDITIONTYPE ORIENTED)
(VAR x y z)
(RULES
  add(x, 0) -> x
  add(x, s(y)) -> s(z) | add(x, y) == z
  sub(z, y) -> x | add(x, y) == z
)
(COMMENT
  \cite{NSS12b}, Example 1: E_sub + R_add
  doi: 10.1016/j.tcs.2012.09.005
)