(CONDITIONTYPE ORIENTED)
(VAR x y q r)
(RULES
  lt(x,0) -> false
  lt(0,s(x)) -> true
  lt(s(x),s(y)) -> lt(x,y)
  m(0,s(y)) -> 0
  m(x,0) -> x
  m(s(x),s(y)) -> m(x,y)
  div(0,s(x)) -> pair(0,0)
  div(s(x),s(y)) -> pair(0,s(x)) | lt(x,y) == true
  div(s(x),s(y)) -> pair(s(q),r) | lt(x,y) == false, div(m(x,y),s(y)) == pair(q,r)
)
(COMMENT
  \cite{SMI95}, p. 12 (Modified version of the concluding example)
  doi: 10.1007/3-540-59200-8_56
)