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

WORST_CASE(Omega(n^1),?)