The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs)))
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
part(x', Cons(x, xs), xs1, xs2) → part[Ite](>(x', x), x', Cons(x, xs), xs1, xs2)
part(x, Nil, xs1, xs2) → app(xs1, xs2)
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
>(S(x), S(y)) → >(x, y)
>(0, y) → False
>(S(x), 0) → True
part[Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2)
part[False][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, Cons(x, xs2))
part[Ite](False, x', Cons(x, xs), xs1, xs2) → part[False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)
part[False][Ite](False, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, xs2)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
part(S(x453230_3), Cons(0, xs), xs1, xs2) →⁺ part(S(x453230_3), xs, Cons(0, xs1), xs2)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(0, xs)].
The result substitution is [xs1 / Cons(0, xs1)].

(2) BOUNDS(n^1, INF)