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

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Heuristically decided to analyse the following defined symbols:
+', ++', sum', -', quot', length'

They will be analysed ascendingly in the following order:
+' < sum'
++' < sum'
-' < quot'

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
+', ++', sum', -', quot', length'

They will be analysed ascendingly in the following order:
+' < sum'
++' < sum'
-' < quot'

Proved the following rewrite lemma:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)

Induction Base:
+'(_gen_0':s'3(0), _gen_0':s'3(b)) →RΩ(1)
_gen_0':s'3(b)

Induction Step:
+'(_gen_0':s'3(+(_\$n7, 1)), _gen_0':s'3(_b175)) →RΩ(1)
s'(+'(_gen_0':s'3(_\$n7), _gen_0':s'3(_b175))) →IH
s'(_gen_0':s'3(+(_\$n7, _b175)))

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
++', sum', -', quot', length'

They will be analysed ascendingly in the following order:
++' < sum'
-' < quot'

Proved the following rewrite lemma:
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)

Induction Base:
++'(_gen_nil'::'4(0), _gen_nil'::'4(b)) →RΩ(1)
_gen_nil'::'4(b)

Induction Step:
++'(_gen_nil'::'4(+(_\$n1086, 1)), _gen_nil'::'4(_b1316)) →RΩ(1)
:'(0', ++'(_gen_nil'::'4(_\$n1086), _gen_nil'::'4(_b1316))) →IH
:'(0', _gen_nil'::'4(+(_\$n1086, _b1316)))

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
sum', -', quot', length'

They will be analysed ascendingly in the following order:
-' < quot'

Proved the following rewrite lemma:
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)

Induction Base:
sum'(_gen_nil'::'4(+(1, 0))) →RΩ(1)
:'(0', nil')

Induction Step:
sum'(_gen_nil'::'4(+(1, +(_\$n2296, 1)))) →RΩ(1)
sum'(:'(+'(0', 0'), _gen_nil'::'4(_\$n2296))) →LΩ(1)
sum'(:'(_gen_0':s'3(+(0, 0)), _gen_nil'::'4(_\$n2296))) →IH
_gen_nil'::'4(1)

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
-', quot', length'

They will be analysed ascendingly in the following order:
-' < quot'

Proved the following rewrite lemma:
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)

Induction Base:
-'(_gen_0':s'3(0), _gen_0':s'3(0)) →RΩ(1)
_gen_0':s'3(0)

Induction Step:
-'(_gen_0':s'3(+(_\$n4031, 1)), _gen_0':s'3(+(_\$n4031, 1))) →RΩ(1)
-'(_gen_0':s'3(_\$n4031), _gen_0':s'3(_\$n4031)) →IH
_gen_0':s'3(0)

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
quot', length'

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

The following defined symbols remain to be analysed:
length'

Proved the following rewrite lemma:
length'(_gen_nil'::'4(_n5532)) → _gen_0':s'3(_n5532), rt ∈ Ω(1 + n5532)

Induction Base:
length'(_gen_nil'::'4(0)) →RΩ(1)
0'

Induction Step:
length'(_gen_nil'::'4(+(_\$n5533, 1))) →RΩ(1)
s'(length'(_gen_nil'::'4(_\$n5533))) →IH
s'(_gen_0':s'3(_\$n5533))

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

Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'

Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)
length'(_gen_nil'::'4(_n5532)) → _gen_0':s'3(_n5532), rt ∈ Ω(1 + n5532)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)