WORST_CASE(Omega(n^1),?)
proof of input_VTqdKexOSr.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 45 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 389 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 71 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 41 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 1999 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 36 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 93.8 s]
        (28) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).


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

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   log(0) -> logError
   log(s(z0)) -> loop(s(z0), s(0), 0)
   loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
   maplog(z0) -> mapIter(z0, nil)
   mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
   ifmap(true, z0, z1) -> z1
   ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   last(nil) -> error
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   droplast(nil) -> nil
   droplast(cons(z0, nil)) -> nil
   droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
   a -> b
   a -> c
Tuples:
   LE(s(z0), 0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   DOUBLE(0) -> c4
   DOUBLE(s(z0)) -> c5(DOUBLE(z0))
   LOG(0) -> c6
   LOG(s(z0)) -> c7(LOOP(s(z0), s(0), 0))
   LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
   IF(true, z0, z1, z2) -> c9
   IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
   MAPLOG(z0) -> c11(MAPITER(z0, nil))
   MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
   IFMAP(true, z0, z1) -> c13
   IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
   IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
   ISEMPTY(nil) -> c16
   ISEMPTY(cons(z0, z1)) -> c17
   LAST(nil) -> c18
   LAST(cons(z0, nil)) -> c19
   LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c21
   DROPLAST(cons(z0, nil)) -> c22
   DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
   A -> c24
   A -> c25
S tuples:
   LE(s(z0), 0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   DOUBLE(0) -> c4
   DOUBLE(s(z0)) -> c5(DOUBLE(z0))
   LOG(0) -> c6
   LOG(s(z0)) -> c7(LOOP(s(z0), s(0), 0))
   LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
   IF(true, z0, z1, z2) -> c9
   IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
   MAPLOG(z0) -> c11(MAPITER(z0, nil))
   MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
   IFMAP(true, z0, z1) -> c13
   IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
   IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
   ISEMPTY(nil) -> c16
   ISEMPTY(cons(z0, z1)) -> c17
   LAST(nil) -> c18
   LAST(cons(z0, nil)) -> c19
   LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c21
   DROPLAST(cons(z0, nil)) -> c22
   DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
   A -> c24
   A -> c25
K tuples:none
Defined Rule Symbols:   le_2, double_1, log_1, loop_3, if_4, maplog_1, mapIter_2, ifmap_3, isempty_1, last_1, droplast_1, a

Defined Pair Symbols:   LE_2, DOUBLE_1, LOG_1, LOOP_3, IF_4, MAPLOG_1, MAPITER_2, IFMAP_3, ISEMPTY_1, LAST_1, DROPLAST_1, A

Compound Symbols:   c1, c2, c3_1, c4, c5_1, c6, c7_1, c8_2, c9, c10_2, c11_1, c12_2, c13, c14_2, c15_3, c16, c17, c18, c19, c20_1, c21, c22, c23_1, c24, c25


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   LE(s(z0), 0) -> c1
   LE(0, z0) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   DOUBLE(0) -> c4
   DOUBLE(s(z0)) -> c5(DOUBLE(z0))
   LOG(0) -> c6
   LOG(s(z0)) -> c7(LOOP(s(z0), s(0), 0))
   LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
   IF(true, z0, z1, z2) -> c9
   IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
   MAPLOG(z0) -> c11(MAPITER(z0, nil))
   MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
   IFMAP(true, z0, z1) -> c13
   IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
   IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
   ISEMPTY(nil) -> c16
   ISEMPTY(cons(z0, z1)) -> c17
   LAST(nil) -> c18
   LAST(cons(z0, nil)) -> c19
   LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c21
   DROPLAST(cons(z0, nil)) -> c22
   DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
   A -> c24
   A -> c25

The (relative) TRS S consists of the following rules:

   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0) -> 0
   double(s(z0)) -> s(s(double(z0)))
   log(0) -> logError
   log(s(z0)) -> loop(s(z0), s(0), 0)
   loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
   maplog(z0) -> mapIter(z0, nil)
   mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
   ifmap(true, z0, z1) -> z1
   ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   last(nil) -> error
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   droplast(nil) -> nil
   droplast(cons(z0, nil)) -> nil
   droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   LE(s(z0), 0') -> c1
   LE(0', z0) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   DOUBLE(0') -> c4
   DOUBLE(s(z0)) -> c5(DOUBLE(z0))
   LOG(0') -> c6
   LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
   LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
   IF(true, z0, z1, z2) -> c9
   IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
   MAPLOG(z0) -> c11(MAPITER(z0, nil))
   MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
   IFMAP(true, z0, z1) -> c13
   IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
   IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
   ISEMPTY(nil) -> c16
   ISEMPTY(cons(z0, z1)) -> c17
   LAST(nil) -> c18
   LAST(cons(z0, nil)) -> c19
   LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
   DROPLAST(nil) -> c21
   DROPLAST(cons(z0, nil)) -> c22
   DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
   A -> c24
   A -> c25

The (relative) TRS S consists of the following rules:

   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   double(0') -> 0'
   double(s(z0)) -> s(s(double(z0)))
   log(0') -> logError
   log(s(z0)) -> loop(s(z0), s(0'), 0')
   loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
   if(true, z0, z1, z2) -> z2
   if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
   maplog(z0) -> mapIter(z0, nil)
   mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
   ifmap(true, z0, z1) -> z1
   ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   last(nil) -> error
   last(cons(z0, nil)) -> z0
   last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
   droplast(nil) -> nil
   droplast(cons(z0, nil)) -> nil
   droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, DOUBLE, LOOP, le, double, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
LE < LOOP
DOUBLE < LOOP
le < LOOP
double < LOOP
le < loop
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
LE, DOUBLE, LOOP, le, double, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
LE < LOOP
DOUBLE < LOOP
le < LOOP
double < LOOP
le < loop
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)

Induction Base:
LE(gen_s:0':logError:error18_26(+(1, 0)), gen_s:0':logError:error18_26(0)) ->_R^Omega(1)
c1

Induction Step:
LE(gen_s:0':logError:error18_26(+(1, +(n24_26, 1))), gen_s:0':logError:error18_26(+(n24_26, 1))) ->_R^Omega(1)
c3(LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26))) ->_IH
c3(gen_c1:c2:c317_26(c25_26))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
LE, DOUBLE, LOOP, le, double, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
LE < LOOP
DOUBLE < LOOP
le < LOOP
double < LOOP
le < loop
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
DOUBLE, LOOP, le, double, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
DOUBLE < LOOP
le < LOOP
double < LOOP
le < loop
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)

Induction Base:
DOUBLE(gen_s:0':logError:error18_26(0)) ->_R^Omega(1)
c4

Induction Step:
DOUBLE(gen_s:0':logError:error18_26(+(n845_26, 1))) ->_R^Omega(1)
c5(DOUBLE(gen_s:0':logError:error18_26(n845_26))) ->_IH
c5(gen_c4:c519_26(c846_26))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
le, LOOP, double, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
le < LOOP
double < LOOP
le < loop
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)

Induction Base:
le(gen_s:0':logError:error18_26(+(1, 0)), gen_s:0':logError:error18_26(0)) ->_R^Omega(0)
false

Induction Step:
le(gen_s:0':logError:error18_26(+(1, +(n1331_26, 1))), gen_s:0':logError:error18_26(+(n1331_26, 1))) ->_R^Omega(0)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) ->_IH
false

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
double, LOOP, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
double < LOOP
double < loop
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
double(gen_s:0':logError:error18_26(n1896_26)) -> gen_s:0':logError:error18_26(*(2, n1896_26)), rt in Omega(0)

Induction Base:
double(gen_s:0':logError:error18_26(0)) ->_R^Omega(0)
0'

Induction Step:
double(gen_s:0':logError:error18_26(+(n1896_26, 1))) ->_R^Omega(0)
s(s(double(gen_s:0':logError:error18_26(n1896_26)))) ->_IH
s(s(gen_s:0':logError:error18_26(*(2, c1897_26))))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)
double(gen_s:0':logError:error18_26(n1896_26)) -> gen_s:0':logError:error18_26(*(2, n1896_26)), rt in Omega(0)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
LOOP, MAPITER, droplast, last, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
droplast < MAPITER
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
droplast < mapIter
last < mapIter

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
droplast(gen_nil:cons20_26(+(1, n15999_26))) -> gen_nil:cons20_26(n15999_26), rt in Omega(0)

Induction Base:
droplast(gen_nil:cons20_26(+(1, 0))) ->_R^Omega(0)
nil

Induction Step:
droplast(gen_nil:cons20_26(+(1, +(n15999_26, 1)))) ->_R^Omega(0)
cons(0', droplast(cons(0', gen_nil:cons20_26(n15999_26)))) ->_IH
cons(0', gen_nil:cons20_26(c16000_26))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)
double(gen_s:0':logError:error18_26(n1896_26)) -> gen_s:0':logError:error18_26(*(2, n1896_26)), rt in Omega(0)
droplast(gen_nil:cons20_26(+(1, n15999_26))) -> gen_nil:cons20_26(n15999_26), rt in Omega(0)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
last, MAPITER, DROPLAST, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
last < MAPITER
DROPLAST < MAPITER
LAST < MAPITER
last < mapIter

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
last(gen_nil:cons20_26(+(1, n16668_26))) -> gen_s:0':logError:error18_26(0), rt in Omega(0)

Induction Base:
last(gen_nil:cons20_26(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
last(gen_nil:cons20_26(+(1, +(n16668_26, 1)))) ->_R^Omega(0)
last(cons(0', gen_nil:cons20_26(n16668_26))) ->_IH
gen_s:0':logError:error18_26(0)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)
double(gen_s:0':logError:error18_26(n1896_26)) -> gen_s:0':logError:error18_26(*(2, n1896_26)), rt in Omega(0)
droplast(gen_nil:cons20_26(+(1, n15999_26))) -> gen_nil:cons20_26(n15999_26), rt in Omega(0)
last(gen_nil:cons20_26(+(1, n16668_26))) -> gen_s:0':logError:error18_26(0), rt in Omega(0)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
DROPLAST, MAPITER, LAST, loop, mapIter

They will be analysed ascendingly in the following order:
DROPLAST < MAPITER
LAST < MAPITER

----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DROPLAST(gen_nil:cons20_26(+(2, n17355_26))) -> *23_26, rt in Omega(n17355_26)

Induction Base:
DROPLAST(gen_nil:cons20_26(+(2, 0)))

Induction Step:
DROPLAST(gen_nil:cons20_26(+(2, +(n17355_26, 1)))) ->_R^Omega(1)
c23(DROPLAST(cons(0', gen_nil:cons20_26(+(1, n17355_26))))) ->_IH
c23(*23_26)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
LE(s(z0), 0') -> c1
LE(0', z0) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
DOUBLE(0') -> c4
DOUBLE(s(z0)) -> c5(DOUBLE(z0))
LOG(0') -> c6
LOG(s(z0)) -> c7(LOOP(s(z0), s(0'), 0'))
LOOP(z0, s(z1), z2) -> c8(IF(le(z0, s(z1)), z0, s(z1), z2), LE(z0, s(z1)))
IF(true, z0, z1, z2) -> c9
IF(false, z0, z1, z2) -> c10(LOOP(z0, double(z1), s(z2)), DOUBLE(z1))
MAPLOG(z0) -> c11(MAPITER(z0, nil))
MAPITER(z0, z1) -> c12(IFMAP(isempty(z0), z0, z1), ISEMPTY(z0))
IFMAP(true, z0, z1) -> c13
IFMAP(false, z0, z1) -> c14(MAPITER(droplast(z0), cons(log(last(z0)), z1)), DROPLAST(z0))
IFMAP(false, z0, z1) -> c15(MAPITER(droplast(z0), cons(log(last(z0)), z1)), LOG(last(z0)), LAST(z0))
ISEMPTY(nil) -> c16
ISEMPTY(cons(z0, z1)) -> c17
LAST(nil) -> c18
LAST(cons(z0, nil)) -> c19
LAST(cons(z0, cons(z1, z2))) -> c20(LAST(cons(z1, z2)))
DROPLAST(nil) -> c21
DROPLAST(cons(z0, nil)) -> c22
DROPLAST(cons(z0, cons(z1, z2))) -> c23(DROPLAST(cons(z1, z2)))
A -> c24
A -> c25
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
double(0') -> 0'
double(s(z0)) -> s(s(double(z0)))
log(0') -> logError
log(s(z0)) -> loop(s(z0), s(0'), 0')
loop(z0, s(z1), z2) -> if(le(z0, s(z1)), z0, s(z1), z2)
if(true, z0, z1, z2) -> z2
if(false, z0, z1, z2) -> loop(z0, double(z1), s(z2))
maplog(z0) -> mapIter(z0, nil)
mapIter(z0, z1) -> ifmap(isempty(z0), z0, z1)
ifmap(true, z0, z1) -> z1
ifmap(false, z0, z1) -> mapIter(droplast(z0), cons(log(last(z0)), z1))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
last(nil) -> error
last(cons(z0, nil)) -> z0
last(cons(z0, cons(z1, z2))) -> last(cons(z1, z2))
droplast(nil) -> nil
droplast(cons(z0, nil)) -> nil
droplast(cons(z0, cons(z1, z2))) -> cons(z0, droplast(cons(z1, z2)))
a -> b
a -> c

Types:
LE :: s:0':logError:error -> s:0':logError:error -> c1:c2:c3
s :: s:0':logError:error -> s:0':logError:error
0' :: s:0':logError:error
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3 -> c1:c2:c3
DOUBLE :: s:0':logError:error -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
LOG :: s:0':logError:error -> c6:c7
c6 :: c6:c7
c7 :: c8 -> c6:c7
LOOP :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c8
c8 :: c9:c10 -> c1:c2:c3 -> c8
IF :: true:false -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> c9:c10
le :: s:0':logError:error -> s:0':logError:error -> true:false
true :: true:false
c9 :: c9:c10
false :: true:false
c10 :: c8 -> c4:c5 -> c9:c10
double :: s:0':logError:error -> s:0':logError:error
MAPLOG :: nil:cons -> c11
c11 :: c12 -> c11
MAPITER :: nil:cons -> nil:cons -> c12
nil :: nil:cons
c12 :: c13:c14:c15 -> c16:c17 -> c12
IFMAP :: true:false -> nil:cons -> nil:cons -> c13:c14:c15
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c16:c17
c13 :: c13:c14:c15
c14 :: c12 -> c21:c22:c23 -> c13:c14:c15
droplast :: nil:cons -> nil:cons
cons :: s:0':logError:error -> nil:cons -> nil:cons
log :: s:0':logError:error -> s:0':logError:error
last :: nil:cons -> s:0':logError:error
DROPLAST :: nil:cons -> c21:c22:c23
c15 :: c12 -> c6:c7 -> c18:c19:c20 -> c13:c14:c15
LAST :: nil:cons -> c18:c19:c20
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
c21 :: c21:c22:c23
c22 :: c21:c22:c23
c23 :: c21:c22:c23 -> c21:c22:c23
A :: c24:c25
c24 :: c24:c25
c25 :: c24:c25
logError :: s:0':logError:error
loop :: s:0':logError:error -> s:0':logError:error -> s:0':logError:error -> s:0':logError:error
if :: true:false -> 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
ifmap :: true:false -> nil:cons -> nil:cons -> nil:cons
error :: s:0':logError:error
a :: b:c
b :: b:c
c :: b:c
hole_c1:c2:c31_26 :: c1:c2:c3
hole_s:0':logError:error2_26 :: s:0':logError:error
hole_c4:c53_26 :: c4:c5
hole_c6:c74_26 :: c6:c7
hole_c85_26 :: c8
hole_c9:c106_26 :: c9:c10
hole_true:false7_26 :: true:false
hole_c118_26 :: c11
hole_nil:cons9_26 :: nil:cons
hole_c1210_26 :: c12
hole_c13:c14:c1511_26 :: c13:c14:c15
hole_c16:c1712_26 :: c16:c17
hole_c21:c22:c2313_26 :: c21:c22:c23
hole_c18:c19:c2014_26 :: c18:c19:c20
hole_c24:c2515_26 :: c24:c25
hole_b:c16_26 :: b:c
gen_c1:c2:c317_26 :: Nat -> c1:c2:c3
gen_s:0':logError:error18_26 :: Nat -> s:0':logError:error
gen_c4:c519_26 :: Nat -> c4:c5
gen_nil:cons20_26 :: Nat -> nil:cons
gen_c21:c22:c2321_26 :: Nat -> c21:c22:c23
gen_c18:c19:c2022_26 :: Nat -> c18:c19:c20


Lemmas:
LE(gen_s:0':logError:error18_26(+(1, n24_26)), gen_s:0':logError:error18_26(n24_26)) -> gen_c1:c2:c317_26(n24_26), rt in Omega(1 + n24_26)
DOUBLE(gen_s:0':logError:error18_26(n845_26)) -> gen_c4:c519_26(n845_26), rt in Omega(1 + n845_26)
le(gen_s:0':logError:error18_26(+(1, n1331_26)), gen_s:0':logError:error18_26(n1331_26)) -> false, rt in Omega(0)
double(gen_s:0':logError:error18_26(n1896_26)) -> gen_s:0':logError:error18_26(*(2, n1896_26)), rt in Omega(0)
droplast(gen_nil:cons20_26(+(1, n15999_26))) -> gen_nil:cons20_26(n15999_26), rt in Omega(0)
last(gen_nil:cons20_26(+(1, n16668_26))) -> gen_s:0':logError:error18_26(0), rt in Omega(0)
DROPLAST(gen_nil:cons20_26(+(2, n17355_26))) -> *23_26, rt in Omega(n17355_26)


Generator Equations:
gen_c1:c2:c317_26(0) <=> c1
gen_c1:c2:c317_26(+(x, 1)) <=> c3(gen_c1:c2:c317_26(x))
gen_s:0':logError:error18_26(0) <=> 0'
gen_s:0':logError:error18_26(+(x, 1)) <=> s(gen_s:0':logError:error18_26(x))
gen_c4:c519_26(0) <=> c4
gen_c4:c519_26(+(x, 1)) <=> c5(gen_c4:c519_26(x))
gen_nil:cons20_26(0) <=> nil
gen_nil:cons20_26(+(x, 1)) <=> cons(0', gen_nil:cons20_26(x))
gen_c21:c22:c2321_26(0) <=> c21
gen_c21:c22:c2321_26(+(x, 1)) <=> c23(gen_c21:c22:c2321_26(x))
gen_c18:c19:c2022_26(0) <=> c18
gen_c18:c19:c2022_26(+(x, 1)) <=> c20(gen_c18:c19:c2022_26(x))


The following defined symbols remain to be analysed:
LAST, MAPITER, loop, mapIter

They will be analysed ascendingly in the following order:
LAST < MAPITER