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

qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


qsort'(nil') → nil'
qsort'(.'(x, y)) → ++'(qsort'(lowers'(x, y)), .'(x, qsort'(greaters'(x, y))))
lowers'(x, nil') → nil'
lowers'(x, .'(y, z)) → if'(<='(y, x), .'(y, lowers'(x, z)), lowers'(x, z))
greaters'(x, nil') → nil'
greaters'(x, .'(y, z)) → if'(<='(y, x), greaters'(x, z), .'(y, greaters'(x, z)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
.'/0
lowers'/0
greaters'/0
if'/0
<='/0
<='/1

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


qsort'(nil') → nil'
qsort'(.'(y)) → ++'(qsort'(lowers'(y)), .'(qsort'(greaters'(y))))
lowers'(nil') → nil'
lowers'(.'(z)) → if'(.'(lowers'(z)), lowers'(z))
greaters'(nil') → nil'
greaters'(.'(z)) → if'(greaters'(z), .'(y, greaters'(z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
qsort'(nil') → nil'
qsort'(.'(y)) → ++'(qsort'(lowers'(y)), .'(qsort'(greaters'(y))))
lowers'(nil') → nil'
lowers'(.'(z)) → if'(.'(lowers'(z)), lowers'(z))
greaters'(nil') → nil'
greaters'(.'(z)) → if'(greaters'(z), .'(y, greaters'(z)))

Types:
qsort' :: nil':.':++':if':.' → nil':.':++':if':.'
nil' :: nil':.':++':if':.'
.' :: nil':.':++':if':.' → nil':.':++':if':.'
++' :: nil':.':++':if':.' → nil':.':++':if':.' → nil':.':++':if':.'
lowers' :: nil':.':++':if':.' → nil':.':++':if':.'
greaters' :: nil':.':++':if':.' → nil':.':++':if':.'
if' :: nil':.':++':if':.' → nil':.':++':if':.' → nil':.':++':if':.'
.' :: y → nil':.':++':if':.' → nil':.':++':if':.'
y :: y
_hole_nil':.':++':if':.'1 :: nil':.':++':if':.'
_hole_y2 :: y
_gen_nil':.':++':if':.'3 :: Nat → nil':.':++':if':.'

Heuristically decided to analyse the following defined symbols:
qsort', lowers', greaters'

They will be analysed ascendingly in the following order:
lowers' < qsort'
greaters' < qsort'

Rules:
qsort'(nil') → nil'
qsort'(.'(y)) → ++'(qsort'(lowers'(y)), .'(qsort'(greaters'(y))))
lowers'(nil') → nil'
lowers'(.'(z)) → if'(.'(lowers'(z)), lowers'(z))
greaters'(nil') → nil'
greaters'(.'(z)) → if'(greaters'(z), .'(y, greaters'(z)))

Types:
qsort' :: nil':.':++':if':.' → nil':.':++':if':.'
nil' :: nil':.':++':if':.'
.' :: nil':.':++':if':.' → nil':.':++':if':.'
++' :: nil':.':++':if':.' → nil':.':++':if':.' → nil':.':++':if':.'
lowers' :: nil':.':++':if':.' → nil':.':++':if':.'
greaters' :: nil':.':++':if':.' → nil':.':++':if':.'
if' :: nil':.':++':if':.' → nil':.':++':if':.' → nil':.':++':if':.'
.' :: y → nil':.':++':if':.' → nil':.':++':if':.'
y :: y
_hole_nil':.':++':if':.'1 :: nil':.':++':if':.'
_hole_y2 :: y
_gen_nil':.':++':if':.'3 :: Nat → nil':.':++':if':.'

Generator Equations:
_gen_nil':.':++':if':.'3(0) ⇔ nil'
_gen_nil':.':++':if':.'3(+(x, 1)) ⇔ .'(_gen_nil':.':++':if':.'3(x))

The following defined symbols remain to be analysed:
lowers', qsort', greaters'

They will be analysed ascendingly in the following order:
lowers' < qsort'
greaters' < qsort'

Proved the following rewrite lemma:
lowers'(_gen_nil':.':++':if':.'3(+(1, _n5))) → _*4, rt ∈ Ω(2n)

Induction Base:
lowers'(_gen_nil':.':++':if':.'3(+(1, 0)))

Induction Step:
lowers'(_gen_nil':.':++':if':.'3(+(1, +(_$n6, 1)))) →RΩ(1)
if'(.'(lowers'(_gen_nil':.':++':if':.'3(+(1, _$n6)))), lowers'(_gen_nil':.':++':if':.'3(+(1, _$n6)))) →IH
if'(.'(_*4), lowers'(_gen_nil':.':++':if':.'3(+(1, _$n6)))) →IH
if'(.'(_*4), _*4)

We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)