(VAR n x xs y )
(STRATEGY INNERMOST)
(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))
        
)