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

rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(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:

rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'

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

They will be analysed ascendingly in the following order:
rev1' < rev'
rev' = rev2'

Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'

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

The following defined symbols remain to be analysed:
rev1', rev', rev2'

They will be analysed ascendingly in the following order:
rev1' < rev'
rev' = rev2'

Proved the following rewrite lemma:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)

Induction Base:
rev1'(_hole_rev1'2, _gen_nil':++'3(0)) →RΩ(1)
_hole_rev1'2

Induction Step:
rev1'(_hole_rev1'2, _gen_nil':++'3(+(_\$n6, 1))) →RΩ(1)
rev1'(_hole_rev1'2, _gen_nil':++'3(_\$n6)) →IH
_hole_rev1'2

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

Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'

Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)

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

The following defined symbols remain to be analysed:
rev2', rev'

They will be analysed ascendingly in the following order:
rev' = rev2'

Proved the following rewrite lemma:
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)

Induction Base:
rev2'(_hole_rev1'2, _gen_nil':++'3(0))

Induction Step:
rev2'(_hole_rev1'2, _gen_nil':++'3(+(_\$n244, 1))) →RΩ(1)
rev'(++'(_hole_rev1'2, rev'(rev2'(_hole_rev1'2, _gen_nil':++'3(_\$n244))))) →IH
rev'(++'(_hole_rev1'2, rev'(_*4)))

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

Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'

Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)

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

The following defined symbols remain to be analysed:
rev'

They will be analysed ascendingly in the following order:
rev' = rev2'

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

The following conjecture could not be proven:

rev'(_gen_nil':++'3(_n5559)) →? _gen_nil':++'3(_n5559)

Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))

Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'

Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)