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

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

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


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

Rewrite Strategy: INNERMOST

Sliced the following arguments:
.'/0
make'/0

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


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

Rewrite Strategy: INNERMOST

Infered types.

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

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

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

They will be analysed ascendingly in the following order:
++' < rev'

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

Types:
rev' :: nil':.' → nil':.'
nil' :: nil':.'
++' :: nil':.' → nil':.' → nil':.'
.' :: nil':.' → nil':.'
make' :: 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:
++', rev'

They will be analysed ascendingly in the following order:
++' < rev'

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(_b197)) →RΩ(1)
.'(++'(_gen_nil':.'2(_$n5), _gen_nil':.'2(_b197))) →IH
.'(_gen_nil':.'2(+(_$n5, _b197)))

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

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

Types:
rev' :: nil':.' → nil':.'
nil' :: nil':.'
++' :: nil':.' → nil':.' → nil':.'
.' :: nil':.' → nil':.'
make' :: 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))

The following defined symbols remain to be analysed:
rev'

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

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

Types:
rev' :: nil':.' → nil':.'
nil' :: nil':.'
++' :: nil':.' → nil':.' → nil':.'
.' :: nil':.' → nil':.'
make' :: 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)