(VAR x y xs)
(RULES
max(nil) -> 0
max(cons(x, nil)) -> x
max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)

if1(true, x, y, xs) -> max(cons(x, xs))
if1(false, x, y, xs) -> max(cons(y, xs))

del(x, nil) -> nil
del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)

if2(true, x, y, xs) -> xs
if2(false, x, y, xs) -> cons(y, del(x, xs))

eq(0, 0) -> true
eq(0, s(y)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)

sort(xs) -> if3(empty(xs),xs)
if3(true,xs) -> nil
if3(false,xs) -> sort(del(max(xs),xs))

empty(nil) -> true
empty(cons(x,xs)) -> false

ge(x, 0) -> true
ge(0, s(x)) -> false
ge(s(x), s(y)) -> ge(x, y)
)