(VAR x y)
(RULES 
  min(0, y) -> 0
  min(x, 0) -> 0
  min(s(x), s(y)) -> s(min(x, y))
  max(0, y) -> y
  max(x, 0) -> x
  max(s(x), s(y)) -> s(max(x, y))
  +(0, y) -> y
  +(s(x), y) -> s(+(x, y))
  -(x, 0) -> x
  -(s(x), s(y)) -> -(x, y)
  *(x, 0) -> 0
  *(x, s(y)) -> +(x, *(x, y))
  f(s(x)) -> f(-(max(*(s(x), s(x)), +(s(x), s(s(s(0))))), max(s(*(s(x), s(x))), +(s(x), s(s(s(s(0))))))))
)