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

plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
ab
ac

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
plusIter', le', sumIter'

They will be analysed ascendingly in the following order:
le' < plusIter'

Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
le', plusIter', sumIter'

They will be analysed ascendingly in the following order:
le' < plusIter'

Proved the following rewrite lemma:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)

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

Induction Step:
le'(_gen_0':s':error'5(+(1, +(_\$n9, 1))), _gen_0':s':error'5(+(_\$n9, 1))) →RΩ(1)
le'(_gen_0':s':error'5(+(1, _\$n9)), _gen_0':s':error'5(_\$n9)) →IH
false'

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

Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)

Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
plusIter', sumIter'

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

Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)

Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
sumIter'

Proved the following rewrite lemma:
sumIter'(_gen_nil':cons'6(_n2748), _gen_0':s':error'5(1)) → _*7, rt ∈ Ω(n2748)

Induction Base:
sumIter'(_gen_nil':cons'6(0), _gen_0':s':error'5(1))

Induction Step:
sumIter'(_gen_nil':cons'6(+(_\$n2749, 1)), _gen_0':s':error'5(1)) →RΩ(1)
ifSum'(isempty'(_gen_nil':cons'6(+(_\$n2749, 1))), _gen_nil':cons'6(+(_\$n2749, 1)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), head'(_gen_nil':cons'6(+(_\$n2749, 1))))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), head'(_gen_nil':cons'6(+(1, _\$n2749))))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), plusIter'(_gen_0':s':error'5(1), 0', 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(1), 0'), _gen_0':s':error'5(1), 0', 0')) →LΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), ifPlus'(false', _gen_0':s':error'5(1), 0', 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), plusIter'(_gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(1), s'(0')), _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(0), 0'), _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), ifPlus'(true', _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _\$n2749)), _gen_0':s':error'5(1), s'(0')) →RΩ(1)
sumIter'(tail'(_gen_nil':cons'6(+(1, _\$n2749))), s'(0')) →RΩ(1)
sumIter'(_gen_nil':cons'6(_\$n2749), s'(0')) →IH
_*7

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

Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a'b'
a'c'

Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
sumIter'(_gen_nil':cons'6(_n2748), _gen_0':s':error'5(1)) → _*7, rt ∈ Ω(n2748)

Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)