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
weight(cons(n, cons(m, x))) → weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) → n

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
weight'(cons'(n, cons'(m, x))) → weight'(sum'(cons'(n, cons'(m, x)), cons'(0', x)))
weight'(cons'(n, nil')) → n

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
weight'(cons'(n, cons'(m, x))) → weight'(sum'(cons'(n, cons'(m, x)), cons'(0', x)))
weight'(cons'(n, nil')) → n

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0' → cons':nil' → cons':nil'
s' :: s':0' → s':0'
0' :: s':0'
nil' :: cons':nil'
weight' :: cons':nil' → s':0'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0'2 :: s':0'
_gen_cons':nil'3 :: Nat → cons':nil'
_gen_s':0'4 :: Nat → s':0'

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
weight'(cons'(n, cons'(m, x))) → weight'(sum'(cons'(n, cons'(m, x)), cons'(0', x)))
weight'(cons'(n, nil')) → n

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0' → cons':nil' → cons':nil'
s' :: s':0' → s':0'
0' :: s':0'
nil' :: cons':nil'
weight' :: cons':nil' → s':0'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0'2 :: s':0'
_gen_cons':nil'3 :: Nat → cons':nil'
_gen_s':0'4 :: Nat → s':0'

Generator Equations:
_gen_cons':nil'3(0) ⇔ nil'
_gen_cons':nil'3(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'3(x))
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(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'3(_n6), _gen_cons':nil'3(b)) → _gen_cons':nil'3(b), rt ∈ Ω(1 + n6)

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

Induction Step:
sum'(_gen_cons':nil'3(+(_\$n7, 1)), _gen_cons':nil'3(_b206)) →RΩ(1)
sum'(_gen_cons':nil'3(_\$n7), _gen_cons':nil'3(_b206)) →IH
_gen_cons':nil'3(_b206)

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
weight'(cons'(n, cons'(m, x))) → weight'(sum'(cons'(n, cons'(m, x)), cons'(0', x)))
weight'(cons'(n, nil')) → n

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0' → cons':nil' → cons':nil'
s' :: s':0' → s':0'
0' :: s':0'
nil' :: cons':nil'
weight' :: cons':nil' → s':0'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0'2 :: s':0'
_gen_cons':nil'3 :: Nat → cons':nil'
_gen_s':0'4 :: Nat → s':0'

Lemmas:
sum'(_gen_cons':nil'3(_n6), _gen_cons':nil'3(b)) → _gen_cons':nil'3(b), rt ∈ Ω(1 + n6)

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

The following defined symbols remain to be analysed:
weight'

Proved the following rewrite lemma:
weight'(_gen_cons':nil'3(+(1, _n559))) → _gen_s':0'4(0), rt ∈ Ω(1 + n559 + n5592)

Induction Base:
weight'(_gen_cons':nil'3(+(1, 0))) →RΩ(1)
0'

Induction Step:
weight'(_gen_cons':nil'3(+(1, +(_\$n560, 1)))) →RΩ(1)
weight'(sum'(cons'(0', cons'(0', _gen_cons':nil'3(_\$n560))), cons'(0', _gen_cons':nil'3(_\$n560)))) →LΩ(3 + \$n560)
weight'(_gen_cons':nil'3(+(_\$n560, 1))) →IH
_gen_s':0'4(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
weight'(cons'(n, cons'(m, x))) → weight'(sum'(cons'(n, cons'(m, x)), cons'(0', x)))
weight'(cons'(n, nil')) → n

Types:
sum' :: cons':nil' → cons':nil' → cons':nil'
cons' :: s':0' → cons':nil' → cons':nil'
s' :: s':0' → s':0'
0' :: s':0'
nil' :: cons':nil'
weight' :: cons':nil' → s':0'
_hole_cons':nil'1 :: cons':nil'
_hole_s':0'2 :: s':0'
_gen_cons':nil'3 :: Nat → cons':nil'
_gen_s':0'4 :: Nat → s':0'

Lemmas:
sum'(_gen_cons':nil'3(_n6), _gen_cons':nil'3(b)) → _gen_cons':nil'3(b), rt ∈ Ω(1 + n6)
weight'(_gen_cons':nil'3(+(1, _n559))) → _gen_s':0'4(0), rt ∈ Ω(1 + n559 + n5592)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
weight'(_gen_cons':nil'3(+(1, _n559))) → _gen_s':0'4(0), rt ∈ Ω(1 + n559 + n5592)