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

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, x, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', x, y) → cons'(0', nil')
if1'(false', x, y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
if1'/1

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

empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

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

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

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

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

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

Proved the following rewrite lemma:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)

Induction Base:
p'(_gen_0':s'5(+(1, 0))) →RΩ(1)
0'

Induction Step:
p'(_gen_0':s'5(+(1, +(_\$n8, 1)))) →RΩ(1)
s'(p'(s'(_gen_0':s'5(_\$n8)))) →IH
s'(_gen_0':s'5(_\$n8))

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)

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

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

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

Proved the following rewrite lemma:
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)

Induction Base:
intlist'(_gen_nil':cons'4(0))

Induction Step:
intlist'(_gen_nil':cons'4(+(_\$n735, 1))) →RΩ(1)
if_intlist'(empty'(_gen_nil':cons'4(+(_\$n735, 1))), _gen_nil':cons'4(+(_\$n735, 1))) →RΩ(1)
if_intlist'(false', _gen_nil':cons'4(+(1, _\$n735))) →RΩ(1)
cons'(s'(0'), intlist'(tail'(_gen_nil':cons'4(+(1, _\$n735))))) →RΩ(1)
cons'(s'(0'), intlist'(_gen_nil':cons'4(_\$n735))) →IH
cons'(s'(0'), _*6)

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)

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

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

They will be analysed ascendingly in the following order:
int' = if1'

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)

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

The following defined symbols remain to be analysed:
int'

They will be analysed ascendingly in the following order:
int' = if1'

Proved the following rewrite lemma:
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)

Induction Base:
int'(_gen_0':s'5(+(1, 0)), _gen_0':s'5(0)) →RΩ(1)
if_int'(zero'(_gen_0':s'5(+(1, 0))), zero'(_gen_0':s'5(0)), _gen_0':s'5(+(1, 0)), _gen_0':s'5(0)) →RΩ(1)
if_int'(false', zero'(_gen_0':s'5(0)), _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
if_int'(false', true', _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
if2'(true', _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
nil'

Induction Step:
int'(_gen_0':s'5(+(1, +(_\$n204009, 1))), _gen_0':s'5(+(_\$n204009, 1))) →RΩ(1)
if_int'(zero'(_gen_0':s'5(+(1, +(_\$n204009, 1)))), zero'(_gen_0':s'5(+(_\$n204009, 1))), _gen_0':s'5(+(1, +(_\$n204009, 1))), _gen_0':s'5(+(_\$n204009, 1))) →RΩ(1)
if_int'(false', zero'(_gen_0':s'5(+(1, _\$n204009))), _gen_0':s'5(+(2, _\$n204009)), _gen_0':s'5(+(1, _\$n204009))) →RΩ(1)
if_int'(false', false', _gen_0':s'5(+(2, _\$n204009)), _gen_0':s'5(+(1, _\$n204009))) →RΩ(1)
if2'(false', _gen_0':s'5(+(2, _\$n204009)), _gen_0':s'5(+(1, _\$n204009))) →RΩ(1)
intlist'(int'(p'(_gen_0':s'5(+(2, _\$n204009))), p'(_gen_0':s'5(+(1, _\$n204009))))) →LΩ(2 + \$n204009)
intlist'(int'(_gen_0':s'5(+(1, _\$n204009)), p'(_gen_0':s'5(+(1, _\$n204009))))) →LΩ(1 + \$n204009)
intlist'(int'(_gen_0':s'5(+(1, _\$n204009)), _gen_0':s'5(_\$n204009))) →IH
intlist'(_gen_nil':cons'4(0)) →RΩ(1)
if_intlist'(empty'(_gen_nil':cons'4(0)), _gen_nil':cons'4(0)) →RΩ(1)
if_intlist'(true', _gen_nil':cons'4(0)) →RΩ(1)
nil'

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)

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

The following defined symbols remain to be analysed:
if1'

They will be analysed ascendingly in the following order:
int' = if1'

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

Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))

Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'

Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)