/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/quick.trs

The program

(VAR N M X Y L)
(RULES

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))))

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend