WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c24()
            A() -> c25()
            DOUBLE(0()) -> c4()
            DOUBLE(s(z0)) -> c5(DOUBLE(z0))
            DROPLAST(cons(z0,cons(z1,z2))) -> c23(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c22()
            DROPLAST(nil()) -> c21()
            IF(false(),z0,z1,z2) -> c10(LOOP(z0,double(z1),s(z2)),DOUBLE(z1))
            IF(true(),z0,z1,z2) -> c9()
            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))
            IFMAP(true(),z0,z1) -> c13()
            ISEMPTY(cons(z0,z1)) -> c17()
            ISEMPTY(nil()) -> c16()
            LAST(cons(z0,cons(z1,z2))) -> c20(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c19()
            LAST(nil()) -> c18()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c1()
            LE(s(z0),s(z1)) -> c3(LE(z0,z1))
            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)))
            MAPITER(z0,z1) -> c12(IFMAP(isempty(z0),z0,z1),ISEMPTY(z0))
            MAPLOG(z0) -> c11(MAPITER(z0,nil()))
        - Weak TRS:
            a() -> b()
            a() -> c()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            droplast(cons(z0,cons(z1,z2))) -> cons(z0,droplast(cons(z1,z2)))
            droplast(cons(z0,nil())) -> nil()
            droplast(nil()) -> nil()
            if(false(),z0,z1,z2) -> loop(z0,double(z1),s(z2))
            if(true(),z0,z1,z2) -> z2
            ifmap(false(),z0,z1) -> mapIter(droplast(z0),cons(log(last(z0)),z1))
            ifmap(true(),z0,z1) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            last(nil()) -> error()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            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)
            mapIter(z0,z1) -> ifmap(isempty(z0),z0,z1)
            maplog(z0) -> mapIter(z0,nil())
        - Signature:
            {A/0,DOUBLE/1,DROPLAST/1,IF/4,IFMAP/3,ISEMPTY/1,LAST/1,LE/2,LOG/1,LOOP/3,MAPITER/2,MAPLOG/1,a/0,double/1
            ,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1} / {0/0,b/0,c/0,c1/0,c10/2
            ,c11/1,c12/2,c13/0,c14/2,c15/3,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/0,c22/0,c23/1,c24/0,c25/0,c3/1,c4/0
            ,c5/1,c6/0,c7/1,c8/2,c9/0,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,DOUBLE,DROPLAST,IF,IFMAP,ISEMPTY,LAST,LE,LOG,LOOP
            ,MAPITER,MAPLOG,a,double,droplast,if,ifmap,isempty,last,le,log,loop,mapIter,maplog} and constructors {0,b,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,error,false
            ,logError,nil,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c24()
            A() -> c25()
            DOUBLE(0()) -> c4()
            DOUBLE(s(z0)) -> c5(DOUBLE(z0))
            DROPLAST(cons(z0,cons(z1,z2))) -> c23(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c22()
            DROPLAST(nil()) -> c21()
            IF(false(),z0,z1,z2) -> c10(LOOP(z0,double(z1),s(z2)),DOUBLE(z1))
            IF(true(),z0,z1,z2) -> c9()
            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))
            IFMAP(true(),z0,z1) -> c13()
            ISEMPTY(cons(z0,z1)) -> c17()
            ISEMPTY(nil()) -> c16()
            LAST(cons(z0,cons(z1,z2))) -> c20(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c19()
            LAST(nil()) -> c18()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c1()
            LE(s(z0),s(z1)) -> c3(LE(z0,z1))
            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)))
            MAPITER(z0,z1) -> c12(IFMAP(isempty(z0),z0,z1),ISEMPTY(z0))
            MAPLOG(z0) -> c11(MAPITER(z0,nil()))
        - Weak TRS:
            a() -> b()
            a() -> c()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            droplast(cons(z0,cons(z1,z2))) -> cons(z0,droplast(cons(z1,z2)))
            droplast(cons(z0,nil())) -> nil()
            droplast(nil()) -> nil()
            if(false(),z0,z1,z2) -> loop(z0,double(z1),s(z2))
            if(true(),z0,z1,z2) -> z2
            ifmap(false(),z0,z1) -> mapIter(droplast(z0),cons(log(last(z0)),z1))
            ifmap(true(),z0,z1) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            last(nil()) -> error()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            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)
            mapIter(z0,z1) -> ifmap(isempty(z0),z0,z1)
            maplog(z0) -> mapIter(z0,nil())
        - Signature:
            {A/0,DOUBLE/1,DROPLAST/1,IF/4,IFMAP/3,ISEMPTY/1,LAST/1,LE/2,LOG/1,LOOP/3,MAPITER/2,MAPLOG/1,a/0,double/1
            ,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1} / {0/0,b/0,c/0,c1/0,c10/2
            ,c11/1,c12/2,c13/0,c14/2,c15/3,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/0,c22/0,c23/1,c24/0,c25/0,c3/1,c4/0
            ,c5/1,c6/0,c7/1,c8/2,c9/0,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,DOUBLE,DROPLAST,IF,IFMAP,ISEMPTY,LAST,LE,LOG,LOOP
            ,MAPITER,MAPLOG,a,double,droplast,if,ifmap,isempty,last,le,log,loop,mapIter,maplog} and constructors {0,b,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,error,false
            ,logError,nil,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c24()
            A() -> c25()
            DOUBLE(0()) -> c4()
            DOUBLE(s(z0)) -> c5(DOUBLE(z0))
            DROPLAST(cons(z0,cons(z1,z2))) -> c23(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c22()
            DROPLAST(nil()) -> c21()
            IF(false(),z0,z1,z2) -> c10(LOOP(z0,double(z1),s(z2)),DOUBLE(z1))
            IF(true(),z0,z1,z2) -> c9()
            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))
            IFMAP(true(),z0,z1) -> c13()
            ISEMPTY(cons(z0,z1)) -> c17()
            ISEMPTY(nil()) -> c16()
            LAST(cons(z0,cons(z1,z2))) -> c20(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c19()
            LAST(nil()) -> c18()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c1()
            LE(s(z0),s(z1)) -> c3(LE(z0,z1))
            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)))
            MAPITER(z0,z1) -> c12(IFMAP(isempty(z0),z0,z1),ISEMPTY(z0))
            MAPLOG(z0) -> c11(MAPITER(z0,nil()))
        - Weak TRS:
            a() -> b()
            a() -> c()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            droplast(cons(z0,cons(z1,z2))) -> cons(z0,droplast(cons(z1,z2)))
            droplast(cons(z0,nil())) -> nil()
            droplast(nil()) -> nil()
            if(false(),z0,z1,z2) -> loop(z0,double(z1),s(z2))
            if(true(),z0,z1,z2) -> z2
            ifmap(false(),z0,z1) -> mapIter(droplast(z0),cons(log(last(z0)),z1))
            ifmap(true(),z0,z1) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            last(nil()) -> error()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            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)
            mapIter(z0,z1) -> ifmap(isempty(z0),z0,z1)
            maplog(z0) -> mapIter(z0,nil())
        - Signature:
            {A/0,DOUBLE/1,DROPLAST/1,IF/4,IFMAP/3,ISEMPTY/1,LAST/1,LE/2,LOG/1,LOOP/3,MAPITER/2,MAPLOG/1,a/0,double/1
            ,droplast/1,if/4,ifmap/3,isempty/1,last/1,le/2,log/1,loop/3,mapIter/2,maplog/1} / {0/0,b/0,c/0,c1/0,c10/2
            ,c11/1,c12/2,c13/0,c14/2,c15/3,c16/0,c17/0,c18/0,c19/0,c2/0,c20/1,c21/0,c22/0,c23/1,c24/0,c25/0,c3/1,c4/0
            ,c5/1,c6/0,c7/1,c8/2,c9/0,cons/2,error/0,false/0,logError/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,DOUBLE,DROPLAST,IF,IFMAP,ISEMPTY,LAST,LE,LOG,LOOP
            ,MAPITER,MAPLOG,a,double,droplast,if,ifmap,isempty,last,le,log,loop,mapIter,maplog} and constructors {0,b,c
            ,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,error,false
            ,logError,nil,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          DOUBLE(x){x -> s(x)} =
            DOUBLE(s(x)) ->^+ c5(DOUBLE(x))
              = C[DOUBLE(x) = DOUBLE(x){}]

WORST_CASE(Omega(n^1),?)