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

++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


++'(nil', y) → y
++'(x, nil') → x
++'(.'(x, y), z) → .'(x, ++'(y, z))
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
.'/0

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


++'(nil', y) → y
++'(x, nil') → x
++'(.'(y), z) → .'(++'(y, z))
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
++'(nil', y) → y
++'(x, nil') → x
++'(.'(y), z) → .'(++'(y, z))
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
++' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Heuristically decided to analyse the following defined symbols:
++'

Rules:
++'(nil', y) → y
++'(x, nil') → x
++'(.'(y), z) → .'(++'(y, z))
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
++' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(_gen_nil':.'2(x))

The following defined symbols remain to be analysed:
++'

Proved the following rewrite lemma:
++'(_gen_nil':.'2(_n4), _gen_nil':.'2(b)) → _gen_nil':.'2(+(_n4, b)), rt ∈ Ω(1 + n4)

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

Induction Step:
++'(_gen_nil':.'2(+(_$n5, 1)), _gen_nil':.'2(_b225)) →RΩ(1)
.'(++'(_gen_nil':.'2(_$n5), _gen_nil':.'2(_b225))) →IH
.'(_gen_nil':.'2(+(_$n5, _b225)))

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

Rules:
++'(nil', y) → y
++'(x, nil') → x
++'(.'(y), z) → .'(++'(y, z))
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
++' :: nil':.' → nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Lemmas:
++'(_gen_nil':.'2(_n4), _gen_nil':.'2(b)) → _gen_nil':.'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(_gen_nil':.'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
++'(_gen_nil':.'2(_n4), _gen_nil':.'2(b)) → _gen_nil':.'2(+(_n4, b)), rt ∈ Ω(1 + n4)