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

car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

Heuristically decided to analyse the following defined symbols:
plus', times', shorter', prod'

They will be analysed ascendingly in the following order:
plus' < times'
times' < prod'
shorter' < prod'

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

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

The following defined symbols remain to be analysed:
plus', times', shorter', prod'

They will be analysed ascendingly in the following order:
plus' < times'
times' < prod'
shorter' < prod'

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

Induction Base:
plus'(_gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
ifplus'(isZero'(_gen_0':s'4(0)), _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
ifplus'(true', _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
_gen_0':s'4(b)

Induction Step:
plus'(_gen_0':s'4(+(_\$n8, 1)), _gen_0':s'4(_b372)) →RΩ(1)
ifplus'(isZero'(_gen_0':s'4(+(_\$n8, 1))), _gen_0':s'4(+(_\$n8, 1)), _gen_0':s'4(_b372)) →RΩ(1)
ifplus'(false', _gen_0':s'4(+(1, _\$n8)), _gen_0':s'4(_b372)) →RΩ(1)
s'(plus'(p'(_gen_0':s'4(+(1, _\$n8))), _gen_0':s'4(_b372))) →RΩ(1)
s'(plus'(_gen_0':s'4(_\$n8), _gen_0':s'4(_b372))) →IH
s'(_gen_0':s'4(+(_\$n8, _b372)))

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

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)

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

The following defined symbols remain to be analysed:
times', shorter', prod'

They will be analysed ascendingly in the following order:
times' < prod'
shorter' < prod'

Proved the following rewrite lemma:
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)

Induction Base:
times'(_gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
iftimes'(isZero'(_gen_0':s'4(0)), _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
iftimes'(true', _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
0'

Induction Step:
times'(_gen_0':s'4(+(_\$n3006, 1)), _gen_0':s'4(_b3630)) →RΩ(1)
iftimes'(isZero'(_gen_0':s'4(+(_\$n3006, 1))), _gen_0':s'4(+(_\$n3006, 1)), _gen_0':s'4(_b3630)) →RΩ(1)
iftimes'(false', _gen_0':s'4(+(1, _\$n3006)), _gen_0':s'4(_b3630)) →RΩ(1)
plus'(_gen_0':s'4(_b3630), times'(p'(_gen_0':s'4(+(1, _\$n3006))), _gen_0':s'4(_b3630))) →RΩ(1)
plus'(_gen_0':s'4(_b3630), times'(_gen_0':s'4(_\$n3006), _gen_0':s'4(_b3630))) →IH
plus'(_gen_0':s'4(_b3630), _gen_0':s'4(*(_\$n3006, _b3630))) →LΩ(1 + b3630)
_gen_0':s'4(+(_b3630, *(_\$n3006, _b3630)))

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

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)

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

The following defined symbols remain to be analysed:
shorter', prod'

They will be analysed ascendingly in the following order:
shorter' < prod'

Proved the following rewrite lemma:
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)

Induction Base:
shorter'(_gen_cons':nil'5(0), _gen_0':s'4(0)) →RΩ(1)
true'

Induction Step:
shorter'(_gen_cons':nil'5(+(_\$n7221, 1)), _gen_0':s'4(+(_\$n7221, 1))) →RΩ(1)
shorter'(_gen_cons':nil'5(_\$n7221), _gen_0':s'4(_\$n7221)) →IH
true'

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

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)

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

The following defined symbols remain to be analysed:
prod'

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

Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))

Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'

Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)