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

intlist(nil) → nil
int(s(x), 0) → nil
int(x, x) → cons(x, nil)
intlist(cons(x, y)) → cons(s(x), intlist(y))
int(s(x), s(y)) → intlist(int(x, y))
int(0, s(y)) → cons(0, int(s(0), s(y)))
intlist(cons(x, nil)) → cons(s(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:


intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(x, nil')
intlist'(cons'(x, y)) → cons'(s'(x), intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(0', int'(s'(0'), s'(y)))
intlist'(cons'(x, nil')) → cons'(s'(x), nil')

Rewrite Strategy: INNERMOST

Sliced the following arguments:
cons'/0

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


intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(nil')
intlist'(cons'(y)) → cons'(intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(int'(s'(0'), s'(y)))
intlist'(cons'(nil')) → cons'(nil')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(nil')
intlist'(cons'(y)) → cons'(intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(int'(s'(0'), s'(y)))
intlist'(cons'(nil')) → cons'(nil')

Types:
intlist' :: nil':cons' → nil':cons'
nil' :: nil':cons'
int' :: s':0' → s':0' → nil':cons'
s' :: s':0' → s':0'
0' :: s':0'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_hole_s':0'2 :: s':0'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_s':0'4 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
intlist', int'

They will be analysed ascendingly in the following order:
intlist' < int'

Rules:
intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(nil')
intlist'(cons'(y)) → cons'(intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(int'(s'(0'), s'(y)))
intlist'(cons'(nil')) → cons'(nil')

Types:
intlist' :: nil':cons' → nil':cons'
nil' :: nil':cons'
int' :: s':0' → s':0' → nil':cons'
s' :: s':0' → s':0'
0' :: s':0'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_hole_s':0'2 :: s':0'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_s':0'4 :: Nat → s':0'

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(_gen_nil':cons'3(x))
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))

The following defined symbols remain to be analysed:
intlist', int'

They will be analysed ascendingly in the following order:
intlist' < int'

Proved the following rewrite lemma:
intlist'(_gen_nil':cons'3(_n6)) → _gen_nil':cons'3(_n6), rt ∈ Ω(1 + n6)

Induction Base:
intlist'(_gen_nil':cons'3(0)) →RΩ(1)
nil'

Induction Step:
intlist'(_gen_nil':cons'3(+(_$n7, 1))) →RΩ(1)
cons'(intlist'(_gen_nil':cons'3(_$n7))) →IH
cons'(_gen_nil':cons'3(_$n7))

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

Rules:
intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(nil')
intlist'(cons'(y)) → cons'(intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(int'(s'(0'), s'(y)))
intlist'(cons'(nil')) → cons'(nil')

Types:
intlist' :: nil':cons' → nil':cons'
nil' :: nil':cons'
int' :: s':0' → s':0' → nil':cons'
s' :: s':0' → s':0'
0' :: s':0'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_hole_s':0'2 :: s':0'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_s':0'4 :: Nat → s':0'

Lemmas:
intlist'(_gen_nil':cons'3(_n6)) → _gen_nil':cons'3(_n6), rt ∈ Ω(1 + n6)

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(_gen_nil':cons'3(x))
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))

The following defined symbols remain to be analysed:
int'

Proved the following rewrite lemma:
int'(_gen_s':0'4(+(1, _n245)), _gen_s':0'4(_n245)) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n245)

Induction Base:
int'(_gen_s':0'4(+(1, 0)), _gen_s':0'4(0)) →RΩ(1)
nil'

Induction Step:
int'(_gen_s':0'4(+(1, +(_$n246, 1))), _gen_s':0'4(+(_$n246, 1))) →RΩ(1)
intlist'(int'(_gen_s':0'4(+(1, _$n246)), _gen_s':0'4(_$n246))) →IH
intlist'(_gen_nil':cons'3(0)) →LΩ(1)
_gen_nil':cons'3(0)

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

Rules:
intlist'(nil') → nil'
int'(s'(x), 0') → nil'
int'(x, x) → cons'(nil')
intlist'(cons'(y)) → cons'(intlist'(y))
int'(s'(x), s'(y)) → intlist'(int'(x, y))
int'(0', s'(y)) → cons'(int'(s'(0'), s'(y)))
intlist'(cons'(nil')) → cons'(nil')

Types:
intlist' :: nil':cons' → nil':cons'
nil' :: nil':cons'
int' :: s':0' → s':0' → nil':cons'
s' :: s':0' → s':0'
0' :: s':0'
cons' :: nil':cons' → nil':cons'
_hole_nil':cons'1 :: nil':cons'
_hole_s':0'2 :: s':0'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_s':0'4 :: Nat → s':0'

Lemmas:
intlist'(_gen_nil':cons'3(_n6)) → _gen_nil':cons'3(_n6), rt ∈ Ω(1 + n6)
int'(_gen_s':0'4(+(1, _n245)), _gen_s':0'4(_n245)) → _gen_nil':cons'3(0), rt ∈ Ω(1 + n245)

Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(_gen_nil':cons'3(x))
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
intlist'(_gen_nil':cons'3(_n6)) → _gen_nil':cons'3(_n6), rt ∈ Ω(1 + n6)