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

sum(cons(s(n), x), cons(m, y)) → sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) → sum(x, y)
sum(nil, y) → y
empty(nil) → true
empty(cons(n, x)) → false
tail(nil) → nil
tail(cons(n, x)) → x
head(cons(n, x)) → n
weight(x) → if(empty(x), empty(tail(x)), x)
if(true, b, x) → weight_undefined_error
if(false, b, x) → if2(b, x)
if2(true, x) → head(x)
if2(false, x) → weight(sum(x, cons(0, tail(tail(x)))))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


sum'(cons'(s'(n), x), cons'(m, y)) → sum'(cons'(n, x), cons'(s'(m), y))
sum'(cons'(0', x), y) → sum'(x, y)
sum'(nil', y) → y
empty'(nil') → true'
empty'(cons'(n, x)) → false'
tail'(nil') → nil'
tail'(cons'(n, x)) → x
head'(cons'(n, x)) → n
weight'(x) → if'(empty'(x), empty'(tail'(x)), x)
if'(true', b, x) → weight_undefined_error'
if'(false', b, x) → if2'(b, x)
if2'(true', x) → head'(x)
if2'(false', x) → weight'(sum'(x, cons'(0', tail'(tail'(x)))))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
sum'(cons'(s'(n), x), cons'(m, y)) → sum'(cons'(n, x), cons'(s'(m), y))
sum'(cons'(0', x), y) → sum'(x, y)
sum'(nil', y) → y
empty'(nil') → true'
empty'(cons'(n, x)) → false'
tail'(nil') → nil'
tail'(cons'(n, x)) → x
head'(cons'(n, x)) → n
weight'(x) → if'(empty'(x), empty'(tail'(x)), x)
if'(true', b, x) → weight_undefined_error'
if'(false', b, x) → if2'(b, x)
if2'(true', x) → head'(x)
if2'(false', x) → weight'(sum'(x, cons'(0', tail'(tail'(x)))))

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0':weight_undefined_error' → cons':nil' → cons':nil'
s' :: s':0':weight_undefined_error' → s':0':weight_undefined_error'
0' :: s':0':weight_undefined_error'
nil' :: cons':nil'
empty' :: cons':nil' → true':false'
true' :: true':false'
false' :: true':false'
tail' :: cons':nil' → cons':nil'
head' :: cons':nil' → s':0':weight_undefined_error'
weight' :: cons':nil' → s':0':weight_undefined_error'
if' :: true':false' → true':false' → cons':nil' → s':0':weight_undefined_error'
weight_undefined_error' :: s':0':weight_undefined_error'
if2' :: true':false' → cons':nil' → s':0':weight_undefined_error'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0':weight_undefined_error'2 :: s':0':weight_undefined_error'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_s':0':weight_undefined_error'5 :: Nat → s':0':weight_undefined_error'

Heuristically decided to analyse the following defined symbols:
sum', weight'

They will be analysed ascendingly in the following order:
sum' < weight'

Rules:
sum'(cons'(s'(n), x), cons'(m, y)) → sum'(cons'(n, x), cons'(s'(m), y))
sum'(cons'(0', x), y) → sum'(x, y)
sum'(nil', y) → y
empty'(nil') → true'
empty'(cons'(n, x)) → false'
tail'(nil') → nil'
tail'(cons'(n, x)) → x
head'(cons'(n, x)) → n
weight'(x) → if'(empty'(x), empty'(tail'(x)), x)
if'(true', b, x) → weight_undefined_error'
if'(false', b, x) → if2'(b, x)
if2'(true', x) → head'(x)
if2'(false', x) → weight'(sum'(x, cons'(0', tail'(tail'(x)))))

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0':weight_undefined_error' → cons':nil' → cons':nil'
s' :: s':0':weight_undefined_error' → s':0':weight_undefined_error'
0' :: s':0':weight_undefined_error'
nil' :: cons':nil'
empty' :: cons':nil' → true':false'
true' :: true':false'
false' :: true':false'
tail' :: cons':nil' → cons':nil'
head' :: cons':nil' → s':0':weight_undefined_error'
weight' :: cons':nil' → s':0':weight_undefined_error'
if' :: true':false' → true':false' → cons':nil' → s':0':weight_undefined_error'
weight_undefined_error' :: s':0':weight_undefined_error'
if2' :: true':false' → cons':nil' → s':0':weight_undefined_error'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0':weight_undefined_error'2 :: s':0':weight_undefined_error'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_s':0':weight_undefined_error'5 :: Nat → s':0':weight_undefined_error'

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

The following defined symbols remain to be analysed:
sum', weight'

They will be analysed ascendingly in the following order:
sum' < weight'

Proved the following rewrite lemma:
sum'(_gen_cons':nil'4(_n7), _gen_cons':nil'4(b)) → _gen_cons':nil'4(b), rt ∈ Ω(1 + n7)

Induction Base:
sum'(_gen_cons':nil'4(0), _gen_cons':nil'4(b)) →RΩ(1)
_gen_cons':nil'4(b)

Induction Step:
sum'(_gen_cons':nil'4(+(_$n8, 1)), _gen_cons':nil'4(_b207)) →RΩ(1)
sum'(_gen_cons':nil'4(_$n8), _gen_cons':nil'4(_b207)) →IH
_gen_cons':nil'4(_b207)

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

Rules:
sum'(cons'(s'(n), x), cons'(m, y)) → sum'(cons'(n, x), cons'(s'(m), y))
sum'(cons'(0', x), y) → sum'(x, y)
sum'(nil', y) → y
empty'(nil') → true'
empty'(cons'(n, x)) → false'
tail'(nil') → nil'
tail'(cons'(n, x)) → x
head'(cons'(n, x)) → n
weight'(x) → if'(empty'(x), empty'(tail'(x)), x)
if'(true', b, x) → weight_undefined_error'
if'(false', b, x) → if2'(b, x)
if2'(true', x) → head'(x)
if2'(false', x) → weight'(sum'(x, cons'(0', tail'(tail'(x)))))

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0':weight_undefined_error' → cons':nil' → cons':nil'
s' :: s':0':weight_undefined_error' → s':0':weight_undefined_error'
0' :: s':0':weight_undefined_error'
nil' :: cons':nil'
empty' :: cons':nil' → true':false'
true' :: true':false'
false' :: true':false'
tail' :: cons':nil' → cons':nil'
head' :: cons':nil' → s':0':weight_undefined_error'
weight' :: cons':nil' → s':0':weight_undefined_error'
if' :: true':false' → true':false' → cons':nil' → s':0':weight_undefined_error'
weight_undefined_error' :: s':0':weight_undefined_error'
if2' :: true':false' → cons':nil' → s':0':weight_undefined_error'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0':weight_undefined_error'2 :: s':0':weight_undefined_error'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_s':0':weight_undefined_error'5 :: Nat → s':0':weight_undefined_error'

Lemmas:
sum'(_gen_cons':nil'4(_n7), _gen_cons':nil'4(b)) → _gen_cons':nil'4(b), 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_s':0':weight_undefined_error'5(0) ⇔ 0'
_gen_s':0':weight_undefined_error'5(+(x, 1)) ⇔ s'(_gen_s':0':weight_undefined_error'5(x))

The following defined symbols remain to be analysed:
weight'

Proved the following rewrite lemma:
weight'(_gen_cons':nil'4(+(1, _n835))) → _gen_s':0':weight_undefined_error'5(0), rt ∈ Ω(1 + n835 + n8352)

Induction Base:
weight'(_gen_cons':nil'4(+(1, 0))) →RΩ(1)
if'(empty'(_gen_cons':nil'4(+(1, 0))), empty'(tail'(_gen_cons':nil'4(+(1, 0)))), _gen_cons':nil'4(+(1, 0))) →RΩ(1)
if'(false', empty'(tail'(_gen_cons':nil'4(1))), _gen_cons':nil'4(1)) →RΩ(1)
if'(false', empty'(_gen_cons':nil'4(0)), _gen_cons':nil'4(1)) →RΩ(1)
if'(false', true', _gen_cons':nil'4(1)) →RΩ(1)
if2'(true', _gen_cons':nil'4(1)) →RΩ(1)
head'(_gen_cons':nil'4(1)) →RΩ(1)
0'

Induction Step:
weight'(_gen_cons':nil'4(+(1, +(_$n836, 1)))) →RΩ(1)
if'(empty'(_gen_cons':nil'4(+(1, +(_$n836, 1)))), empty'(tail'(_gen_cons':nil'4(+(1, +(_$n836, 1))))), _gen_cons':nil'4(+(1, +(_$n836, 1)))) →RΩ(1)
if'(false', empty'(tail'(_gen_cons':nil'4(+(2, _$n836)))), _gen_cons':nil'4(+(2, _$n836))) →RΩ(1)
if'(false', empty'(_gen_cons':nil'4(+(1, _$n836))), _gen_cons':nil'4(+(2, _$n836))) →RΩ(1)
if'(false', false', _gen_cons':nil'4(+(2, _$n836))) →RΩ(1)
if2'(false', _gen_cons':nil'4(+(2, _$n836))) →RΩ(1)
weight'(sum'(_gen_cons':nil'4(+(2, _$n836)), cons'(0', tail'(tail'(_gen_cons':nil'4(+(2, _$n836))))))) →RΩ(1)
weight'(sum'(_gen_cons':nil'4(+(2, _$n836)), cons'(0', tail'(_gen_cons':nil'4(+(1, _$n836)))))) →RΩ(1)
weight'(sum'(_gen_cons':nil'4(+(2, _$n836)), cons'(0', _gen_cons':nil'4(_$n836)))) →LΩ(3 + $n836)
weight'(_gen_cons':nil'4(+(_$n836, 1))) →IH
_gen_s':0':weight_undefined_error'5(0)

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

Rules:
sum'(cons'(s'(n), x), cons'(m, y)) → sum'(cons'(n, x), cons'(s'(m), y))
sum'(cons'(0', x), y) → sum'(x, y)
sum'(nil', y) → y
empty'(nil') → true'
empty'(cons'(n, x)) → false'
tail'(nil') → nil'
tail'(cons'(n, x)) → x
head'(cons'(n, x)) → n
weight'(x) → if'(empty'(x), empty'(tail'(x)), x)
if'(true', b, x) → weight_undefined_error'
if'(false', b, x) → if2'(b, x)
if2'(true', x) → head'(x)
if2'(false', x) → weight'(sum'(x, cons'(0', tail'(tail'(x)))))

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0':weight_undefined_error' → cons':nil' → cons':nil'
s' :: s':0':weight_undefined_error' → s':0':weight_undefined_error'
0' :: s':0':weight_undefined_error'
nil' :: cons':nil'
empty' :: cons':nil' → true':false'
true' :: true':false'
false' :: true':false'
tail' :: cons':nil' → cons':nil'
head' :: cons':nil' → s':0':weight_undefined_error'
weight' :: cons':nil' → s':0':weight_undefined_error'
if' :: true':false' → true':false' → cons':nil' → s':0':weight_undefined_error'
weight_undefined_error' :: s':0':weight_undefined_error'
if2' :: true':false' → cons':nil' → s':0':weight_undefined_error'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0':weight_undefined_error'2 :: s':0':weight_undefined_error'
_hole_true':false'3 :: true':false'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_s':0':weight_undefined_error'5 :: Nat → s':0':weight_undefined_error'

Lemmas:
sum'(_gen_cons':nil'4(_n7), _gen_cons':nil'4(b)) → _gen_cons':nil'4(b), rt ∈ Ω(1 + n7)
weight'(_gen_cons':nil'4(+(1, _n835))) → _gen_s':0':weight_undefined_error'5(0), rt ∈ Ω(1 + n835 + n8352)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
weight'(_gen_cons':nil'4(+(1, _n835))) → _gen_s':0':weight_undefined_error'5(0), rt ∈ Ω(1 + n835 + n8352)