WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DEL(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),z0,z1,z2),EQ(z0,z1))
            DEL(z0,nil()) -> c2()
            DOUBLE(0()) -> c()
            DOUBLE(s(z0)) -> c1(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c13(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c14(DOUBLELIST(del(first(cons(z0,z1)),cons(z0,z1)))
                                          ,DEL(first(cons(z0,z1)),cons(z0,z1))
                                          ,FIRST(cons(z0,z1)))
            DOUBLELIST(nil()) -> c12()
            EQ(0(),0()) -> c6()
            EQ(0(),s(z0)) -> c7()
            EQ(s(z0),0()) -> c8()
            EQ(s(z0),s(z1)) -> c9(EQ(z0,z1))
            FIRST(cons(z0,z1)) -> c11()
            FIRST(nil()) -> c10()
            IF(false(),z0,z1,z2) -> c5(DEL(z0,z2))
            IF(true(),z0,z1,z2) -> c4()
        - Weak TRS:
            del(z0,cons(z1,z2)) -> if(eq(z0,z1),z0,z1,z2)
            del(z0,nil()) -> nil()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            doublelist(cons(z0,z1)) -> cons(double(z0),doublelist(del(first(cons(z0,z1)),cons(z0,z1))))
            doublelist(nil()) -> nil()
            eq(0(),0()) -> true()
            eq(0(),s(z0)) -> false()
            eq(s(z0),0()) -> false()
            eq(s(z0),s(z1)) -> eq(z0,z1)
            first(cons(z0,z1)) -> z0
            first(nil()) -> 0()
            if(false(),z0,z1,z2) -> cons(z1,del(z0,z2))
            if(true(),z0,z1,z2) -> z2
        - Signature:
            {DEL/2,DOUBLE/1,DOUBLELIST/1,EQ/2,FIRST/1,IF/4,del/2,double/1,doublelist/1,eq/2,first/1,if/4} / {0/0,c/0
            ,c1/1,c10/0,c11/0,c12/0,c13/1,c14/3,c2/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DEL,DOUBLE,DOUBLELIST,EQ,FIRST,IF,del,double,doublelist
            ,eq,first,if} and constructors {0,c,c1,c10,c11,c12,c13,c14,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)) -> c3(IF(eq(z0,z1),z0,z1,z2),EQ(z0,z1))
            DEL(z0,nil()) -> c2()
            DOUBLE(0()) -> c()
            DOUBLE(s(z0)) -> c1(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c13(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c14(DOUBLELIST(del(first(cons(z0,z1)),cons(z0,z1)))
                                          ,DEL(first(cons(z0,z1)),cons(z0,z1))
                                          ,FIRST(cons(z0,z1)))
            DOUBLELIST(nil()) -> c12()
            EQ(0(),0()) -> c6()
            EQ(0(),s(z0)) -> c7()
            EQ(s(z0),0()) -> c8()
            EQ(s(z0),s(z1)) -> c9(EQ(z0,z1))
            FIRST(cons(z0,z1)) -> c11()
            FIRST(nil()) -> c10()
            IF(false(),z0,z1,z2) -> c5(DEL(z0,z2))
            IF(true(),z0,z1,z2) -> c4()
        - Weak TRS:
            del(z0,cons(z1,z2)) -> if(eq(z0,z1),z0,z1,z2)
            del(z0,nil()) -> nil()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            doublelist(cons(z0,z1)) -> cons(double(z0),doublelist(del(first(cons(z0,z1)),cons(z0,z1))))
            doublelist(nil()) -> nil()
            eq(0(),0()) -> true()
            eq(0(),s(z0)) -> false()
            eq(s(z0),0()) -> false()
            eq(s(z0),s(z1)) -> eq(z0,z1)
            first(cons(z0,z1)) -> z0
            first(nil()) -> 0()
            if(false(),z0,z1,z2) -> cons(z1,del(z0,z2))
            if(true(),z0,z1,z2) -> z2
        - Signature:
            {DEL/2,DOUBLE/1,DOUBLELIST/1,EQ/2,FIRST/1,IF/4,del/2,double/1,doublelist/1,eq/2,first/1,if/4} / {0/0,c/0
            ,c1/1,c10/0,c11/0,c12/0,c13/1,c14/3,c2/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DEL,DOUBLE,DOUBLELIST,EQ,FIRST,IF,del,double,doublelist
            ,eq,first,if} and constructors {0,c,c1,c10,c11,c12,c13,c14,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)) -> c3(IF(eq(z0,z1),z0,z1,z2),EQ(z0,z1))
            DEL(z0,nil()) -> c2()
            DOUBLE(0()) -> c()
            DOUBLE(s(z0)) -> c1(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c13(DOUBLE(z0))
            DOUBLELIST(cons(z0,z1)) -> c14(DOUBLELIST(del(first(cons(z0,z1)),cons(z0,z1)))
                                          ,DEL(first(cons(z0,z1)),cons(z0,z1))
                                          ,FIRST(cons(z0,z1)))
            DOUBLELIST(nil()) -> c12()
            EQ(0(),0()) -> c6()
            EQ(0(),s(z0)) -> c7()
            EQ(s(z0),0()) -> c8()
            EQ(s(z0),s(z1)) -> c9(EQ(z0,z1))
            FIRST(cons(z0,z1)) -> c11()
            FIRST(nil()) -> c10()
            IF(false(),z0,z1,z2) -> c5(DEL(z0,z2))
            IF(true(),z0,z1,z2) -> c4()
        - Weak TRS:
            del(z0,cons(z1,z2)) -> if(eq(z0,z1),z0,z1,z2)
            del(z0,nil()) -> nil()
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            doublelist(cons(z0,z1)) -> cons(double(z0),doublelist(del(first(cons(z0,z1)),cons(z0,z1))))
            doublelist(nil()) -> nil()
            eq(0(),0()) -> true()
            eq(0(),s(z0)) -> false()
            eq(s(z0),0()) -> false()
            eq(s(z0),s(z1)) -> eq(z0,z1)
            first(cons(z0,z1)) -> z0
            first(nil()) -> 0()
            if(false(),z0,z1,z2) -> cons(z1,del(z0,z2))
            if(true(),z0,z1,z2) -> z2
        - Signature:
            {DEL/2,DOUBLE/1,DOUBLELIST/1,EQ/2,FIRST/1,IF/4,del/2,double/1,doublelist/1,eq/2,first/1,if/4} / {0/0,c/0
            ,c1/1,c10/0,c11/0,c12/0,c13/1,c14/3,c2/0,c3/2,c4/0,c5/1,c6/0,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DEL,DOUBLE,DOUBLELIST,EQ,FIRST,IF,del,double,doublelist
            ,eq,first,if} and constructors {0,c,c1,c10,c11,c12,c13,c14,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:
          DOUBLE(x){x -> s(x)} =
            DOUBLE(s(x)) ->^+ c1(DOUBLE(x))
              = C[DOUBLE(x) = DOUBLE(x){}]

WORST_CASE(Omega(n^1),?)