(VAR x y X Y Z)
(THEORY (AC app))
(THEORY (C max'))
(RULES
  1 -> s(0)
  2 -> s(1)
  3 -> s(2)
  4 -> s(3)
  5 -> s(4)
  6 -> s(5)
  7 -> s(6)
  8 -> s(7)
  9 -> s(8)
  max'(0, x) -> x
  max'(s(x), s(y)) -> s(max'(x, y))
  app(empty, X) -> X
  max(singl(x)) -> x
  max(app(singl(x), Y)) -> max2(x, Y)
  max2(x, empty) -> x
  max2(x, singl(y)) -> max'(x, y)
  max2(x, app(singl(y), Z)) -> max2(max'(x, y), Z)
)