YES
(VAR Y X N L M)
(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))))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for quick:

-> Dependency pairs:
nF_le(s(X),s(Y)) -> nF_le(X,Y)
nF_app(cons(N,L),Y) -> nF_app(L,Y)
nF_low(N,cons(M,L)) -> nF_iflow(le(M,N),N,cons(M,L))
nF_low(N,cons(M,L)) -> nF_le(M,N)
nF_iflow(true,N,cons(M,L)) -> nF_low(N,L)
nF_iflow(false,N,cons(M,L)) -> nF_low(N,L)
nF_high(N,cons(M,L)) -> nF_ifhigh(le(M,N),N,cons(M,L))
nF_high(N,cons(M,L)) -> nF_le(M,N)
nF_ifhigh(true,N,cons(M,L)) -> nF_high(N,L)
nF_ifhigh(false,N,cons(M,L)) -> nF_high(N,L)
nF_quicksort(cons(N,L)) -> nF_app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
nF_quicksort(cons(N,L)) -> nF_quicksort(low(N,L))
nF_quicksort(cons(N,L)) -> nF_low(N,L)
nF_quicksort(cons(N,L)) -> nF_quicksort(high(N,L))
nF_quicksort(cons(N,L)) -> nF_high(N,L)

-> Proof of termination for quick_1_1:
-> -> Dependency pairs in cycle:
nF_quicksort(cons(N,L)) -> nF_quicksort(low(N,L))
nF_quicksort(cons(N,L)) -> nF_quicksort(high(N,L))

UsableRules:
le(0,Y) -> true
le(s(X),0) -> false
le(s(X),s(Y)) -> le(X,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))

Polynomial Interpretation:

[le](X1,X2) = X2
[0] = 1
[true] = 0
[s](X) = X
[false] = 0
[app](X1,X2) = 0
[nil] = 1
[cons](X1,X2) = X2 + 1
[low](X1,X2) = X2 + 1
[iflow](X1,X2,X3) = X3 + 1
[high](X1,X2) = X2
[ifhigh](X1,X2,X3) = X3
[quicksort](X) = 0
[nF_quicksort](X) = X

TIME: 4.6953e-2

-> -> Dependency pairs in cycle:
nF_quicksort(cons(N,L)) -> nF_quicksort(low(N,L))

UsableRules:
le(0,Y) -> true
le(s(X),0) -> false
le(s(X),s(Y)) -> le(X,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)

Polynomial Interpretation:

[le](X1,X2) = X1
[0] = 1
[true] = 0
[s](X) = X + 1
[false] = 0
[app](X1,X2) = 0
[nil] = 1
[cons](X1,X2) = X2 + 1
[low](X1,X2) = X2
[iflow](X1,X2,X3) = X3
[high](X1,X2) = 0
[ifhigh](X1,X2,X3) = 0
[quicksort](X) = 0
[nF_quicksort](X) = X

TIME: 4.2028e-2


-> Proof of termination for quick_1_2:
-> -> Dependency pairs in cycle:
nF_high(N,cons(M,L)) -> nF_ifhigh(le(M,N),N,cons(M,L))
nF_ifhigh(false,N,cons(M,L)) -> nF_high(N,L)
nF_ifhigh(true,N,cons(M,L)) -> nF_high(N,L)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for quick_1_3:
-> -> Dependency pairs in cycle:
nF_low(N,cons(M,L)) -> nF_iflow(le(M,N),N,cons(M,L))
nF_iflow(false,N,cons(M,L)) -> nF_low(N,L)
nF_iflow(true,N,cons(M,L)) -> nF_low(N,L)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for quick_1_4:
-> -> Dependency pairs in cycle:
nF_app(cons(N,L),Y) -> nF_app(L,Y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for quick_1_5:
-> -> Dependency pairs in cycle:
nF_le(s(X),s(Y)) -> nF_le(X,Y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.