WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2))
            APPEND(nil(),z0) -> c7()
            DROPLAST(cons(z0,cons(z1,z2))) -> c6(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c5()
            DROPLAST(nil()) -> c4()
            IF(false(),z0,z1,z2) -> c14(REV(z0,z1))
            IF(true(),z0,z1,z2) -> c13()
            ISEMPTY(cons(z0,z1)) -> c1()
            ISEMPTY(nil()) -> c()
            LAST(cons(z0,cons(z1,z2))) -> c3(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c2()
            REV(z0,z1) -> c10(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),ISEMPTY(z0))
            REV(z0,z1) -> c11(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),DROPLAST(z0))
            REV(z0,z1) -> c12(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),APPEND(z1,last(z0)),LAST(z0))
            REVERSE(z0) -> c9(REV(z0,nil()))
        - Weak TRS:
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> 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) -> rev(z0,z1)
            if(true(),z0,z1,z2) -> z2
            isEmpty(cons(z0,z1)) -> false()
            isEmpty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            rev(z0,z1) -> if(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1)
            reverse(z0) -> rev(z0,nil())
        - Signature:
            {APPEND/2,DROPLAST/1,IF/4,ISEMPTY/1,LAST/1,REV/2,REVERSE/1,append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2
            ,reverse/1} / {c/0,c1/0,c10/2,c11/2,c12/3,c13/0,c14/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APPEND,DROPLAST,IF,ISEMPTY,LAST,REV,REVERSE,append
            ,dropLast,if,isEmpty,last,rev,reverse} and constructors {c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9
            ,cons,false,nil,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2))
            APPEND(nil(),z0) -> c7()
            DROPLAST(cons(z0,cons(z1,z2))) -> c6(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c5()
            DROPLAST(nil()) -> c4()
            IF(false(),z0,z1,z2) -> c14(REV(z0,z1))
            IF(true(),z0,z1,z2) -> c13()
            ISEMPTY(cons(z0,z1)) -> c1()
            ISEMPTY(nil()) -> c()
            LAST(cons(z0,cons(z1,z2))) -> c3(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c2()
            REV(z0,z1) -> c10(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),ISEMPTY(z0))
            REV(z0,z1) -> c11(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),DROPLAST(z0))
            REV(z0,z1) -> c12(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),APPEND(z1,last(z0)),LAST(z0))
            REVERSE(z0) -> c9(REV(z0,nil()))
        - Weak TRS:
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> 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) -> rev(z0,z1)
            if(true(),z0,z1,z2) -> z2
            isEmpty(cons(z0,z1)) -> false()
            isEmpty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            rev(z0,z1) -> if(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1)
            reverse(z0) -> rev(z0,nil())
        - Signature:
            {APPEND/2,DROPLAST/1,IF/4,ISEMPTY/1,LAST/1,REV/2,REVERSE/1,append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2
            ,reverse/1} / {c/0,c1/0,c10/2,c11/2,c12/3,c13/0,c14/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APPEND,DROPLAST,IF,ISEMPTY,LAST,REV,REVERSE,append
            ,dropLast,if,isEmpty,last,rev,reverse} and constructors {c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9
            ,cons,false,nil,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2))
            APPEND(nil(),z0) -> c7()
            DROPLAST(cons(z0,cons(z1,z2))) -> c6(DROPLAST(cons(z1,z2)))
            DROPLAST(cons(z0,nil())) -> c5()
            DROPLAST(nil()) -> c4()
            IF(false(),z0,z1,z2) -> c14(REV(z0,z1))
            IF(true(),z0,z1,z2) -> c13()
            ISEMPTY(cons(z0,z1)) -> c1()
            ISEMPTY(nil()) -> c()
            LAST(cons(z0,cons(z1,z2))) -> c3(LAST(cons(z1,z2)))
            LAST(cons(z0,nil())) -> c2()
            REV(z0,z1) -> c10(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),ISEMPTY(z0))
            REV(z0,z1) -> c11(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),DROPLAST(z0))
            REV(z0,z1) -> c12(IF(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1),APPEND(z1,last(z0)),LAST(z0))
            REVERSE(z0) -> c9(REV(z0,nil()))
        - Weak TRS:
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> 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) -> rev(z0,z1)
            if(true(),z0,z1,z2) -> z2
            isEmpty(cons(z0,z1)) -> false()
            isEmpty(nil()) -> true()
            last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2))
            last(cons(z0,nil())) -> z0
            rev(z0,z1) -> if(isEmpty(z0),dropLast(z0),append(z1,last(z0)),z1)
            reverse(z0) -> rev(z0,nil())
        - Signature:
            {APPEND/2,DROPLAST/1,IF/4,ISEMPTY/1,LAST/1,REV/2,REVERSE/1,append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2
            ,reverse/1} / {c/0,c1/0,c10/2,c11/2,c12/3,c13/0,c14/1,c2/0,c3/1,c4/0,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APPEND,DROPLAST,IF,ISEMPTY,LAST,REV,REVERSE,append
            ,dropLast,if,isEmpty,last,rev,reverse} and constructors {c,c1,c10,c11,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9
            ,cons,false,nil,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          APPEND(y,z){y -> cons(x,y)} =
            APPEND(cons(x,y),z) ->^+ c8(APPEND(y,z))
              = C[APPEND(y,z) = APPEND(y,z){}]

WORST_CASE(Omega(n^1),?)