(CONDITIONTYPE ORIENTED)
(VAR x y z)
(RULES
  sub(z, 0) -> z
  sub(s(z), s(y)) -> x | sub(z, y) == x
)
(COMMENT
  \cite{NSS12b}, Introduction: R_sub
  doi: 10.1016/j.tcs.2012.09.005
)