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

@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
binom(Cons(x, xs), Cons(x', xs')) → @(binom(xs, xs'), binom(xs, Cons(x', xs')))
binom(Cons(x, xs), Nil) → Cons(Nil, Nil)
binom(Nil, k) → Cons(Nil, Nil)
goal(x, y) → binom(x, y)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


@'(Cons'(x, xs), ys) → Cons'(x, @'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(x, xs), Cons'(x', xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(x', xs')))
binom'(Cons'(x, xs), Nil') → Cons'(Nil', Nil')
binom'(Nil', k) → Cons'(Nil', Nil')
goal'(x, y) → binom'(x, y)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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


@'(Cons'(xs), ys) → Cons'(@'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(xs), Cons'(xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(xs')))
binom'(Cons'(xs), Nil') → Cons'(Nil')
binom'(Nil', k) → Cons'(Nil')
goal'(x, y) → binom'(x, y)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
@'(Cons'(xs), ys) → Cons'(@'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(xs), Cons'(xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(xs')))
binom'(Cons'(xs), Nil') → Cons'(Nil')
binom'(Nil', k) → Cons'(Nil')
goal'(x, y) → binom'(x, y)

Types:
@' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
binom' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
@', binom'

They will be analysed ascendingly in the following order:
@' < binom'

Rules:
@'(Cons'(xs), ys) → Cons'(@'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(xs), Cons'(xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(xs')))
binom'(Cons'(xs), Nil') → Cons'(Nil')
binom'(Nil', k) → Cons'(Nil')
goal'(x, y) → binom'(x, y)

Types:
@' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
binom' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
@', binom'

They will be analysed ascendingly in the following order:
@' < binom'

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

Induction Base:
@'(_gen_Cons':Nil'2(0), _gen_Cons':Nil'2(b)) →RΩ(1)
_gen_Cons':Nil'2(b)

Induction Step:
@'(_gen_Cons':Nil'2(+(_$n5, 1)), _gen_Cons':Nil'2(_b139)) →RΩ(1)
Cons'(@'(_gen_Cons':Nil'2(_$n5), _gen_Cons':Nil'2(_b139))) →IH
Cons'(_gen_Cons':Nil'2(+(_$n5, _b139)))

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

Rules:
@'(Cons'(xs), ys) → Cons'(@'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(xs), Cons'(xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(xs')))
binom'(Cons'(xs), Nil') → Cons'(Nil')
binom'(Nil', k) → Cons'(Nil')
goal'(x, y) → binom'(x, y)

Types:
@' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
binom' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
@'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
binom'

Proved the following rewrite lemma:
binom'(_gen_Cons':Nil'2(+(1, _n485)), _gen_Cons':Nil'2(+(1, _n485))) → _*3, rt ∈ Ω(n485)

Induction Base:
binom'(_gen_Cons':Nil'2(+(1, 0)), _gen_Cons':Nil'2(+(1, 0)))

Induction Step:
binom'(_gen_Cons':Nil'2(+(1, +(_$n486, 1))), _gen_Cons':Nil'2(+(1, +(_$n486, 1)))) →RΩ(1)
@'(binom'(_gen_Cons':Nil'2(+(1, _$n486)), _gen_Cons':Nil'2(+(1, _$n486))), binom'(_gen_Cons':Nil'2(+(1, _$n486)), Cons'(_gen_Cons':Nil'2(+(1, _$n486))))) →IH
@'(_*3, binom'(_gen_Cons':Nil'2(+(1, _$n486)), Cons'(_gen_Cons':Nil'2(+(1, _$n486))))) →RΩ(1)
@'(_*3, @'(binom'(_gen_Cons':Nil'2(_$n486), _gen_Cons':Nil'2(+(1, _$n486))), binom'(_gen_Cons':Nil'2(_$n486), Cons'(_gen_Cons':Nil'2(+(1, _$n486))))))

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

Rules:
@'(Cons'(xs), ys) → Cons'(@'(xs, ys))
@'(Nil', ys) → ys
binom'(Cons'(xs), Cons'(xs')) → @'(binom'(xs, xs'), binom'(xs, Cons'(xs')))
binom'(Cons'(xs), Nil') → Cons'(Nil')
binom'(Nil', k) → Cons'(Nil')
goal'(x, y) → binom'(x, y)

Types:
@' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
binom' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
@'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
binom'(_gen_Cons':Nil'2(+(1, _n485)), _gen_Cons':Nil'2(+(1, _n485))) → _*3, rt ∈ Ω(n485)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

No more defined symbols left to analyse.

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