(VAR l n m x y v u )
(RULES
sort(l) -> st(0, l)
st(n, l) -> cond1(member(n, l), n, l)
cond1(true, n, l) -> cons(n, st(s(n), l))
cond1(false, n, l) -> cond2(gt(n,max(l)), n, l)
cond2(true, n, l) -> nil
cond2(false, n, l) -> st(s(n), l)
member(n, nil) -> false
member(n, cons(m, l)) -> or(equal(n,m),member(n, l))
or(x, true) -> true
or(x, false) -> x
equal(0, 0) -> true
equal(s(x), 0) -> false
equal(0, s(y)) -> false
equal(s(x), s(y)) -> equal(x, y)
gt(0, v) -> false
gt(s(u), 0) -> true
gt(s(u), s(v)) -> gt(u, v)
max(nil) -> 0
max(cons(u, l)) -> if(gt(u,max(l)), u,max(l))
if(true, u, v) -> u
if(false, u, v) -> v
)