(VAR n x y xs)
(RULES
qsort(xs) -> qs(half(length(xs)),xs)

qs(n,nil) -> nil
qs(n,cons(x, xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),
                            cons(get(n,cons(x,xs)),
                                 qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))))

filterlow(n,nil) -> nil
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true,n,x,xs) -> filterlow(n,xs)
if1(false,n,x,xs) -> cons(x,filterlow(n,xs))


filterhigh(n,nil) -> nil
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true,n,x,xs) -> filterhigh(n,xs)
if2(false,n,x,xs) -> cons(x,filterhigh(n,xs))


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

append(nil,ys) -> ys
append(cons(x,xs),ys) -> cons(x, append(xs,ys))

length(nil) -> 0
length(cons(x,xs)) -> s(length(xs))

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
 
get(n,nil) -> 0
get(n,cons(x,nil)) -> x
get(0,cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
)
(COMMENT quicksort with middle element as pivot)