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

average(x, y) → if(ge(x, y), x, y)
if(true, x, y) → averIter(y, x, y)
if(false, x, y) → averIter(x, y, x)
averIter(x, y, z) → ifIter(ge(x, y), x, y, z)
ifIter(true, x, y, z) → z
ifIter(false, x, y, z) → averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0)))
append(nil, y) → y
append(cons(n, x), y) → cons(n, app(x, y))
low(n, nil) → nil
low(n, cons(m, x)) → if_low(ge(m, n), n, cons(m, x))
if_low(false, n, cons(m, x)) → cons(m, low(n, x))
if_low(true, n, cons(m, x)) → low(n, x)
high(n, nil) → nil
high(n, cons(m, x)) → if_high(ge(m, n), n, cons(m, x))
if_high(false, n, cons(m, x)) → high(n, x)
if_high(true, n, cons(m, x)) → cons(average(m, m), high(n, x))
quicksort(x) → ifquick(isempty(x), x)
ifquick(true, x) → nil
ifquick(false, x) → append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
isempty(nil) → true
isempty(cons(n, x)) → false
head(nil) → error
head(cons(n, x)) → n
tail(nil) → nil
tail(cons(n, x)) → x
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

average'(x, y) → if'(ge'(x, y), x, y)
if'(true', x, y) → averIter'(y, x, y)
if'(false', x, y) → averIter'(x, y, x)
averIter'(x, y, z) → ifIter'(ge'(x, y), x, y, z)
ifIter'(true', x, y, z) → z
ifIter'(false', x, y, z) → averIter'(plus'(x, s'(s'(s'(0')))), plus'(y, s'(0')), plus'(z, s'(0')))
append'(nil', y) → y
append'(cons'(n, x), y) → cons'(n, app'(x, y))
low'(n, nil') → nil'
low'(n, cons'(m, x)) → if_low'(ge'(m, n), n, cons'(m, x))
if_low'(false', n, cons'(m, x)) → cons'(m, low'(n, x))
if_low'(true', n, cons'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, cons'(m, x)) → if_high'(ge'(m, n), n, cons'(m, x))
if_high'(false', n, cons'(m, x)) → high'(n, x)
if_high'(true', n, cons'(m, x)) → cons'(average'(m, m), high'(n, x))
quicksort'(x) → ifquick'(isempty'(x), x)
ifquick'(true', x) → nil'
ifquick'(false', x) → append'(quicksort'(low'(head'(x), tail'(x))), cons'(tail'(x), quicksort'(high'(head'(x), tail'(x)))))
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
isempty'(nil') → true'
isempty'(cons'(n, x)) → false'
head'(nil') → error'
head'(cons'(n, x)) → n
tail'(nil') → nil'
tail'(cons'(n, x)) → x
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
a' → b'
a' → c'

Rewrite Strategy: INNERMOST

Sliced the following arguments:
app'/0
app'/1

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

average'(x, y) → if'(ge'(x, y), x, y)
if'(true', x, y) → averIter'(y, x, y)
if'(false', x, y) → averIter'(x, y, x)
averIter'(x, y, z) → ifIter'(ge'(x, y), x, y, z)
ifIter'(true', x, y, z) → z
ifIter'(false', x, y, z) → averIter'(plus'(x, s'(s'(s'(0')))), plus'(y, s'(0')), plus'(z, s'(0')))
append'(nil', y) → y
append'(cons'(n, x), y) → cons'(n, app')
low'(n, nil') → nil'
low'(n, cons'(m, x)) → if_low'(ge'(m, n), n, cons'(m, x))
if_low'(false', n, cons'(m, x)) → cons'(m, low'(n, x))
if_low'(true', n, cons'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, cons'(m, x)) → if_high'(ge'(m, n), n, cons'(m, x))
if_high'(false', n, cons'(m, x)) → high'(n, x)
if_high'(true', n, cons'(m, x)) → cons'(average'(m, m), high'(n, x))
quicksort'(x) → ifquick'(isempty'(x), x)
ifquick'(true', x) → nil'
ifquick'(false', x) → append'(quicksort'(low'(head'(x), tail'(x))), cons'(tail'(x), quicksort'(high'(head'(x), tail'(x)))))
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
isempty'(nil') → true'
isempty'(cons'(n, x)) → false'
head'(nil') → error'
head'(cons'(n, x)) → n
tail'(nil') → nil'
tail'(cons'(n, x)) → x
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
a' → b'
a' → c'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
average'(x, y) → if'(ge'(x, y), x, y)
if'(true', x, y) → averIter'(y, x, y)
if'(false', x, y) → averIter'(x, y, x)
averIter'(x, y, z) → ifIter'(ge'(x, y), x, y, z)
ifIter'(true', x, y, z) → z
ifIter'(false', x, y, z) → averIter'(plus'(x, s'(s'(s'(0')))), plus'(y, s'(0')), plus'(z, s'(0')))
append'(nil', y) → y
append'(cons'(n, x), y) → cons'(n, app')
low'(n, nil') → nil'
low'(n, cons'(m, x)) → if_low'(ge'(m, n), n, cons'(m, x))
if_low'(false', n, cons'(m, x)) → cons'(m, low'(n, x))
if_low'(true', n, cons'(m, x)) → low'(n, x)
high'(n, nil') → nil'
high'(n, cons'(m, x)) → if_high'(ge'(m, n), n, cons'(m, x))
if_high'(false', n, cons'(m, x)) → high'(n, x)
if_high'(true', n, cons'(m, x)) → cons'(average'(m, m), high'(n, x))
quicksort'(x) → ifquick'(isempty'(x), x)
ifquick'(true', x) → nil'
ifquick'(false', x) → append'(quicksort'(low'(head'(x), tail'(x))), cons'(tail'(x), quicksort'(high'(head'(x), tail'(x)))))
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
isempty'(nil') → true'
isempty'(cons'(n, x)) → false'
head'(nil') → error'
head'(cons'(n, x)) → n
tail'(nil') → nil'
tail'(cons'(n, x)) → x
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
a' → b'
a' → c'

Types:
average' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
if' :: true':false' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
ge' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → true':false'
true' :: true':false'
averIter' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
false' :: true':false'
ifIter' :: true':false' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
plus' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
s' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
0' :: 0':s':nil':cons':app':error'
append' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
nil' :: 0':s':nil':cons':app':error'
cons' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
app' :: 0':s':nil':cons':app':error'
low' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
if_low' :: true':false' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
high' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
if_high' :: true':false' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
quicksort' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
ifquick' :: true':false' → 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
isempty' :: 0':s':nil':cons':app':error' → true':false'
head' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
tail' :: 0':s':nil':cons':app':error' → 0':s':nil':cons':app':error'
error' :: 0':s':nil':cons':app':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':nil':cons':app':error'1 :: 0':s':nil':cons':app':error'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s':nil':cons':app':error'4 :: Nat → 0':s':nil':cons':app':error'

Heuristically decided to analyse the following defined symbols:
ge', averIter', plus', low', high', quicksort'

They will be analysed ascendingly in the following order:
ge' < averIter'
ge' < low'
ge' < high'
plus' < averIter'
low' < quicksort'
high' < quicksort'

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
ge', averIter', plus', low', high', quicksort'

They will be analysed ascendingly in the following order:
ge' < averIter'
ge' < low'
ge' < high'
plus' < averIter'
low' < quicksort'
high' < quicksort'

Proved the following rewrite lemma:
ge'(_gen_0':s':nil':cons':app':error'4(_n6), _gen_0':s':nil':cons':app':error'4(_n6)) → true', rt ∈ Ω(1 + _n6)

Induction Base:
ge'(_gen_0':s':nil':cons':app':error'4(0), _gen_0':s':nil':cons':app':error'4(0)) →_R^Ω(1)
true'

Induction Step:
ge'(_gen_0':s':nil':cons':app':error'4(+(_$n7, 1)), _gen_0':s':nil':cons':app':error'4(+(_$n7, 1))) →_R^Ω(1)
ge'(_gen_0':s':nil':cons':app':error'4(_$n7), _gen_0':s':nil':cons':app':error'4(_$n7)) →_IH
true'

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

Lemmas:
ge'(_gen_0':s':nil':cons':app':error'4(_n6), _gen_0':s':nil':cons':app':error'4(_n6)) → true', rt ∈ Ω(1 + _n6)

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
plus', averIter', low', high', quicksort'

They will be analysed ascendingly in the following order:
plus' < averIter'
low' < quicksort'
high' < quicksort'

Proved the following rewrite lemma:
plus'(_gen_0':s':nil':cons':app':error'4(_n1614), _gen_0':s':nil':cons':app':error'4(b)) → _gen_0':s':nil':cons':app':error'4(+(_n1614, b)), rt ∈ Ω(1 + _n1614)

Induction Base:
plus'(_gen_0':s':nil':cons':app':error'4(0), _gen_0':s':nil':cons':app':error'4(b)) →_R^Ω(1)
_gen_0':s':nil':cons':app':error'4(b)

Induction Step:
plus'(_gen_0':s':nil':cons':app':error'4(+(_$n1615, 1)), _gen_0':s':nil':cons':app':error'4(_b1747)) →_R^Ω(1)
s'(plus'(_gen_0':s':nil':cons':app':error'4(_$n1615), _gen_0':s':nil':cons':app':error'4(_b1747))) →_IH
s'(_gen_0':s':nil':cons':app':error'4(+(_$n1615, _b1747)))

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

Lemmas:
ge'(_gen_0':s':nil':cons':app':error'4(_n6), _gen_0':s':nil':cons':app':error'4(_n6)) → true', rt ∈ Ω(1 + _n6)
plus'(_gen_0':s':nil':cons':app':error'4(_n1614), _gen_0':s':nil':cons':app':error'4(b)) → _gen_0':s':nil':cons':app':error'4(+(_n1614, b)), rt ∈ Ω(1 + _n1614)

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
averIter', low', high', quicksort'

They will be analysed ascendingly in the following order:
low' < quicksort'
high' < quicksort'

Could not prove a rewrite lemma for the defined symbol averIter'.

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
low', high', quicksort'

They will be analysed ascendingly in the following order:
low' < quicksort'
high' < quicksort'

Could not prove a rewrite lemma for the defined symbol low'.

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
high', quicksort'

They will be analysed ascendingly in the following order:
high' < quicksort'

Could not prove a rewrite lemma for the defined symbol high'.

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

The following defined symbols remain to be analysed:
quicksort'

Could not prove a rewrite lemma for the defined symbol quicksort'.

Generator Equations:
_gen_0':s':nil':cons':app':error'4(0) ⇔ 0'
_gen_0':s':nil':cons':app':error'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':app':error'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
ge'(_gen_0':s':nil':cons':app':error'4(_n6), _gen_0':s':nil':cons':app':error'4(_n6)) → true', rt ∈ Ω(1 + _n6)