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

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
if(true, b, y, xs, ys, x) → y
if(false, true, y, xs, ys, x) → sumList(xs, y)
if(false, false, y, xs, ys, x) → sumList(ys, x)
sum(xs) → sumList(xs, 0)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'

Heuristically decided to analyse the following defined symbols:
p', inc', sumList'

They will be analysed ascendingly in the following order:
p' < sumList'
inc' < sumList'

Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'

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

The following defined symbols remain to be analysed:
p', inc', sumList'

They will be analysed ascendingly in the following order:
p' < sumList'
inc' < sumList'

Proved the following rewrite lemma:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)

Induction Base:
p'(_gen_0':s'5(+(1, 0))) →RΩ(1)
0'

Induction Step:
p'(_gen_0':s'5(+(1, +(_\$n8, 1)))) →RΩ(1)
s'(p'(s'(_gen_0':s'5(_\$n8)))) →IH
s'(_gen_0':s'5(_\$n8))

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

Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)

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

The following defined symbols remain to be analysed:
inc', sumList'

They will be analysed ascendingly in the following order:
inc' < sumList'

Proved the following rewrite lemma:
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)

Induction Base:
inc'(_gen_0':s'5(0)) →RΩ(1)
s'(0')

Induction Step:
inc'(_gen_0':s'5(+(_\$n738, 1))) →RΩ(1)
s'(inc'(_gen_0':s'5(_\$n738))) →IH
s'(_gen_0':s'5(+(1, _\$n738)))

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

Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)

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

The following defined symbols remain to be analysed:
sumList'

Proved the following rewrite lemma:
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)

Induction Base:
sumList'(_gen_cons':nil'4(0), _gen_0':s'5(b)) →RΩ(1)
_gen_0':s'5(b)

Induction Step:
sumList'(_gen_cons':nil'4(+(_\$n1440, 1)), _gen_0':s'5(_b2188)) →RΩ(1)
if'(isEmpty'(_gen_cons':nil'4(+(_\$n1440, 1))), isZero'(head'(_gen_cons':nil'4(+(_\$n1440, 1)))), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(_\$n1440, 1))), cons'(p'(head'(_gen_cons':nil'4(+(_\$n1440, 1)))), tail'(_gen_cons':nil'4(+(_\$n1440, 1)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', isZero'(head'(_gen_cons':nil'4(+(1, _\$n1440)))), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _\$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _\$n1440)))), tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', isZero'(0'), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _\$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _\$n1440)))), tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _\$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _\$n1440)))), tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_\$n1440), cons'(p'(head'(_gen_cons':nil'4(+(1, _\$n1440)))), tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_\$n1440), cons'(p'(0'), tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_\$n1440), cons'(0', tail'(_gen_cons':nil'4(+(1, _\$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_\$n1440), cons'(0', _gen_cons':nil'4(_\$n1440)), inc'(_gen_0':s'5(_b2188))) →LΩ(1 + b2188)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_\$n1440), cons'(0', _gen_cons':nil'4(_\$n1440)), _gen_0':s'5(+(1, _b2188))) →RΩ(1)
sumList'(_gen_cons':nil'4(_\$n1440), _gen_0':s'5(_b2188)) →IH
_gen_0':s'5(_b2188)

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

Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')

Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)