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

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(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:

flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'

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

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

Rules:
flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'

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

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

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

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

Rules:
flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'

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

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

Proved the following rewrite lemma:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)

Induction Base:
flatten'(_gen_nil':unit'2(0)) →RΩ(1)
nil'

Induction Step:
flatten'(_gen_nil':unit'2(+(_\$n33, 1))) →RΩ(1)
flatten'(_gen_nil':unit'2(_\$n33)) →IH
_gen_nil':unit'2(0)

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

Rules:
flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'

Lemmas:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)

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

The following defined symbols remain to be analysed:
rev'

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

Rules:
flatten'(nil') → nil'
flatten'(unit'(x)) → flatten'(x)
flatten'(++'(x, y)) → ++'(flatten'(x), flatten'(y))
flatten'(++'(unit'(x), y)) → ++'(flatten'(x), flatten'(y))
flatten'(flatten'(x)) → flatten'(x)
rev'(nil') → nil'
rev'(unit'(x)) → unit'(x)
rev'(++'(x, y)) → ++'(rev'(y), rev'(x))
rev'(rev'(x)) → x
++'(x, nil') → x
++'(nil', y) → y
++'(++'(x, y), z) → ++'(x, ++'(y, z))

Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'

Lemmas:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)