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

concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


concat'(leaf', Y) → Y
concat'(cons'(U, V), Y) → cons'(U, concat'(V, Y))
lessleaves'(X, leaf') → false'
lessleaves'(leaf', cons'(W, Z)) → true'
lessleaves'(cons'(U, V), cons'(W, Z)) → lessleaves'(concat'(U, V), concat'(W, Z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
concat'(leaf', Y) → Y
concat'(cons'(U, V), Y) → cons'(U, concat'(V, Y))
lessleaves'(X, leaf') → false'
lessleaves'(leaf', cons'(W, Z)) → true'
lessleaves'(cons'(U, V), cons'(W, Z)) → lessleaves'(concat'(U, V), concat'(W, Z))

Types:
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
leaf' :: leaf':cons'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
lessleaves' :: leaf':cons' → leaf':cons' → false':true'
false' :: false':true'
true' :: false':true'
_hole_leaf':cons'1 :: leaf':cons'
_hole_false':true'2 :: false':true'
_gen_leaf':cons'3 :: Nat → leaf':cons'

Heuristically decided to analyse the following defined symbols:
concat', lessleaves'

They will be analysed ascendingly in the following order:
concat' < lessleaves'

Rules:
concat'(leaf', Y) → Y
concat'(cons'(U, V), Y) → cons'(U, concat'(V, Y))
lessleaves'(X, leaf') → false'
lessleaves'(leaf', cons'(W, Z)) → true'
lessleaves'(cons'(U, V), cons'(W, Z)) → lessleaves'(concat'(U, V), concat'(W, Z))

Types:
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
leaf' :: leaf':cons'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
lessleaves' :: leaf':cons' → leaf':cons' → false':true'
false' :: false':true'
true' :: false':true'
_hole_leaf':cons'1 :: leaf':cons'
_hole_false':true'2 :: false':true'
_gen_leaf':cons'3 :: Nat → leaf':cons'

Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))

The following defined symbols remain to be analysed:
concat', lessleaves'

They will be analysed ascendingly in the following order:
concat' < lessleaves'

Proved the following rewrite lemma:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)

Induction Base:
concat'(_gen_leaf':cons'3(0), _gen_leaf':cons'3(b)) →RΩ(1)
_gen_leaf':cons'3(b)

Induction Step:
concat'(_gen_leaf':cons'3(+(_$n6, 1)), _gen_leaf':cons'3(_b146)) →RΩ(1)
cons'(leaf', concat'(_gen_leaf':cons'3(_$n6), _gen_leaf':cons'3(_b146))) →IH
cons'(leaf', _gen_leaf':cons'3(+(_$n6, _b146)))

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

Rules:
concat'(leaf', Y) → Y
concat'(cons'(U, V), Y) → cons'(U, concat'(V, Y))
lessleaves'(X, leaf') → false'
lessleaves'(leaf', cons'(W, Z)) → true'
lessleaves'(cons'(U, V), cons'(W, Z)) → lessleaves'(concat'(U, V), concat'(W, Z))

Types:
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
leaf' :: leaf':cons'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
lessleaves' :: leaf':cons' → leaf':cons' → false':true'
false' :: false':true'
true' :: false':true'
_hole_leaf':cons'1 :: leaf':cons'
_hole_false':true'2 :: false':true'
_gen_leaf':cons'3 :: Nat → leaf':cons'

Lemmas:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))

The following defined symbols remain to be analysed:
lessleaves'

Proved the following rewrite lemma:
lessleaves'(_gen_leaf':cons'3(_n515), _gen_leaf':cons'3(_n515)) → false', rt ∈ Ω(1 + n515)

Induction Base:
lessleaves'(_gen_leaf':cons'3(0), _gen_leaf':cons'3(0)) →RΩ(1)
false'

Induction Step:
lessleaves'(_gen_leaf':cons'3(+(_$n516, 1)), _gen_leaf':cons'3(+(_$n516, 1))) →RΩ(1)
lessleaves'(concat'(leaf', _gen_leaf':cons'3(_$n516)), concat'(leaf', _gen_leaf':cons'3(_$n516))) →LΩ(1)
lessleaves'(_gen_leaf':cons'3(+(0, _$n516)), concat'(leaf', _gen_leaf':cons'3(_$n516))) →LΩ(1)
lessleaves'(_gen_leaf':cons'3(_$n516), _gen_leaf':cons'3(+(0, _$n516))) →IH
false'

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

Rules:
concat'(leaf', Y) → Y
concat'(cons'(U, V), Y) → cons'(U, concat'(V, Y))
lessleaves'(X, leaf') → false'
lessleaves'(leaf', cons'(W, Z)) → true'
lessleaves'(cons'(U, V), cons'(W, Z)) → lessleaves'(concat'(U, V), concat'(W, Z))

Types:
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
leaf' :: leaf':cons'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
lessleaves' :: leaf':cons' → leaf':cons' → false':true'
false' :: false':true'
true' :: false':true'
_hole_leaf':cons'1 :: leaf':cons'
_hole_false':true'2 :: false':true'
_gen_leaf':cons'3 :: Nat → leaf':cons'

Lemmas:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)
lessleaves'(_gen_leaf':cons'3(_n515), _gen_leaf':cons'3(_n515)) → false', rt ∈ Ω(1 + n515)

Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)