(VAR x y)
(RULES
  max(x,0)  -> x
  max(0,y)  -> y
  max(s(x),s(y)) -> s(max(y,x))
  max(x,y) -> max(y,x)
)
(COMMENT from the collection of \cite{AT2012})