(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following 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
Q is empty.