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

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
maplog(xs) → mapIter(xs, nil)
mapIter(xs, ys) → ifmap(isempty(xs), xs, ys)
ifmap(true, xs, ys) → ys
ifmap(false, xs, ys) → mapIter(droplast(xs), cons(log(last(xs)), ys))
isempty(nil) → true
isempty(cons(x, xs)) → false
last(nil) → error
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
droplast(nil) → nil
droplast(cons(x, nil)) → nil
droplast(cons(x, cons(y, xs))) → cons(x, droplast(cons(y, xs)))
a → b
a → c

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
le', double', loop', mapIter', droplast', last'

They will be analysed ascendingly in the following order:
le' < loop'
double' < loop'
droplast' < mapIter'
last' < mapIter'

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
le', double', loop', mapIter', droplast', last'

They will be analysed ascendingly in the following order:
le' < loop'
double' < loop'
droplast' < mapIter'
last' < mapIter'

Proved the following rewrite lemma:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)

Induction Base:
le'(_gen_s':0':logError':error'5(+(1, 0)), _gen_s':0':logError':error'5(0)) →RΩ(1)
false'

Induction Step:
le'(_gen_s':0':logError':error'5(+(1, +(_$n9, 1))), _gen_s':0':logError':error'5(+(_$n9, 1))) →RΩ(1)
le'(_gen_s':0':logError':error'5(+(1, _$n9)), _gen_s':0':logError':error'5(_$n9)) →IH
false'

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
double', loop', mapIter', droplast', last'

They will be analysed ascendingly in the following order:
double' < loop'
droplast' < mapIter'
last' < mapIter'

Proved the following rewrite lemma:
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)

Induction Base:
double'(_gen_s':0':logError':error'5(0)) →RΩ(1)
0'

Induction Step:
double'(_gen_s':0':logError':error'5(+(_$n1190, 1))) →RΩ(1)
s'(s'(double'(_gen_s':0':logError':error'5(_$n1190)))) →IH
s'(s'(_gen_s':0':logError':error'5(*(2, _$n1190))))

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
loop', mapIter', droplast', last'

They will be analysed ascendingly in the following order:
droplast' < mapIter'
last' < mapIter'

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
droplast', mapIter', last'

They will be analysed ascendingly in the following order:
droplast' < mapIter'
last' < mapIter'

Proved the following rewrite lemma:
droplast'(_gen_nil':cons'6(+(1, _n2755))) → _gen_nil':cons'6(_n2755), rt ∈ Ω(1 + n2755)

Induction Base:
droplast'(_gen_nil':cons'6(+(1, 0))) →RΩ(1)
nil'

Induction Step:
droplast'(_gen_nil':cons'6(+(1, +(_$n2756, 1)))) →RΩ(1)
cons'(0', droplast'(cons'(0', _gen_nil':cons'6(_$n2756)))) →IH
cons'(0', _gen_nil':cons'6(_$n2756))

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)
droplast'(_gen_nil':cons'6(+(1, _n2755))) → _gen_nil':cons'6(_n2755), rt ∈ Ω(1 + n2755)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
last', mapIter'

They will be analysed ascendingly in the following order:
last' < mapIter'

Proved the following rewrite lemma:
last'(_gen_nil':cons'6(+(1, _n3848))) → _gen_s':0':logError':error'5(0), rt ∈ Ω(1 + n3848)

Induction Base:
last'(_gen_nil':cons'6(+(1, 0))) →RΩ(1)
0'

Induction Step:
last'(_gen_nil':cons'6(+(1, +(_$n3849, 1)))) →RΩ(1)
last'(cons'(0', _gen_nil':cons'6(_$n3849))) →IH
_gen_s':0':logError':error'5(0)

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)
droplast'(_gen_nil':cons'6(+(1, _n2755))) → _gen_nil':cons'6(_n2755), rt ∈ Ω(1 + n2755)
last'(_gen_nil':cons'6(+(1, _n3848))) → _gen_s':0':logError':error'5(0), rt ∈ Ω(1 + n3848)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
mapIter'

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

The following conjecture could not be proven:

mapIter'(_gen_nil':cons'6(_n4850), _gen_nil':cons'6(b)) →? _*7

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))
maplog'(xs) → mapIter'(xs, nil')
mapIter'(xs, ys) → ifmap'(isempty'(xs), xs, ys)
ifmap'(true', xs, ys) → ys
ifmap'(false', xs, ys) → mapIter'(droplast'(xs), cons'(log'(last'(xs)), ys))
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
last'(nil') → error'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
droplast'(nil') → nil'
droplast'(cons'(x, nil')) → nil'
droplast'(cons'(x, cons'(y, xs))) → cons'(x, droplast'(cons'(y, xs)))
a' → b'
a' → c'

Types:
le' :: s':0':logError':error' → s':0':logError':error' → false':true'
s' :: s':0':logError':error' → s':0':logError':error'
0' :: s':0':logError':error'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError':error' → s':0':logError':error'
log' :: s':0':logError':error' → s':0':logError':error'
logError' :: s':0':logError':error'
loop' :: s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
if' :: false':true' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error' → s':0':logError':error'
maplog' :: nil':cons' → nil':cons'
mapIter' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
ifmap' :: false':true' → nil':cons' → nil':cons' → nil':cons'
isempty' :: nil':cons' → false':true'
droplast' :: nil':cons' → nil':cons'
cons' :: s':0':logError':error' → nil':cons' → nil':cons'
last' :: nil':cons' → s':0':logError':error'
error' :: s':0':logError':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_false':true'1 :: false':true'
_hole_s':0':logError':error'2 :: s':0':logError':error'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_s':0':logError':error'5 :: Nat → s':0':logError':error'
_gen_nil':cons'6 :: Nat → nil':cons'

Lemmas:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
double'(_gen_s':0':logError':error'5(_n1189)) → _gen_s':0':logError':error'5(*(2, _n1189)), rt ∈ Ω(1 + n1189)
droplast'(_gen_nil':cons'6(+(1, _n2755))) → _gen_nil':cons'6(_n2755), rt ∈ Ω(1 + n2755)
last'(_gen_nil':cons'6(+(1, _n3848))) → _gen_s':0':logError':error'5(0), rt ∈ Ω(1 + n3848)

Generator Equations:
_gen_s':0':logError':error'5(0) ⇔ 0'
_gen_s':0':logError':error'5(+(x, 1)) ⇔ s'(_gen_s':0':logError':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
le'(_gen_s':0':logError':error'5(+(1, _n8)), _gen_s':0':logError':error'5(_n8)) → false', rt ∈ Ω(1 + n8)