MAYBE

Problem:
 le(0(),Y) -> true()
 le(s(X),0()) -> false()
 le(s(X),s(Y)) -> le(X,Y)
 app(nil(),Y) -> Y
 app(cons(N,L),Y) -> cons(N,app(L,Y))
 low(N,nil()) -> nil()
 low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
 iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
 iflow(false(),N,cons(M,L)) -> low(N,L)
 high(N,nil()) -> nil()
 high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
 ifhigh(true(),N,cons(M,L)) -> high(N,L)
 ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
 quicksort(nil()) -> nil()
 quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))

Proof:
 Open