(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following 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))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
filterlow(n, cons(0, xs)) →+ filterlow(n, xs)
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 [ ].
(2) BOUNDS(n^1, INF)