WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c19()
            A() -> c20()
            HEAD(cons(z0,z1)) -> c16()
            HEAD(nil()) -> c15()
            IFPLUS(false(),z0,z1,z2) -> c4(PLUSITER(z0,s(z1),s(z2)))
            IFPLUS(true(),z0,z1,z2) -> c3()
            IFSUM(false(),z0,z1,z2) -> c12(SUMITER(tail(z0),z2),TAIL(z0))
            IFSUM(true(),z0,z1,z2) -> c11()
            ISEMPTY(cons(z0,z1)) -> c14()
            ISEMPTY(nil()) -> c13()
            LE(0(),z0) -> c6()
            LE(s(z0),0()) -> c5()
            LE(s(z0),s(z1)) -> c7(LE(z0,z1))
            PLUS(z0,z1) -> c1(PLUSITER(z0,z1,0()))
            PLUSITER(z0,z1,z2) -> c2(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2))
            SUM(z0) -> c8(SUMITER(z0,0()))
            SUMITER(z0,z1) -> c10(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),PLUS(z1,head(z0)),HEAD(z0))
            SUMITER(z0,z1) -> c9(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),ISEMPTY(z0))
            TAIL(cons(z0,z1)) -> c18()
            TAIL(nil()) -> c17()
        - Weak TRS:
            a() -> b()
            a() -> c()
            head(cons(z0,z1)) -> z0
            head(nil()) -> error()
            ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2))
            ifPlus(true(),z0,z1,z2) -> z1
            ifSum(false(),z0,z1,z2) -> sumIter(tail(z0),z2)
            ifSum(true(),z0,z1,z2) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            plus(z0,z1) -> plusIter(z0,z1,0())
            plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2)
            sum(z0) -> sumIter(z0,0())
            sumIter(z0,z1) -> ifSum(isempty(z0),z0,z1,plus(z1,head(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {A/0,HEAD/1,IFPLUS/4,IFSUM/4,ISEMPTY/1,LE/2,PLUS/2,PLUSITER/3,SUM/1,SUMITER/2,TAIL/1,a/0,head/1,ifPlus/4
            ,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1} / {0/0,b/0,c/0,c1/1,c10/3,c11/0,c12/2
            ,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c3/0,c4/1,c5/0,c6/0,c7/1,c8/1,c9/2,cons/2,error/0
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,HEAD,IFPLUS,IFSUM,ISEMPTY,LE,PLUS,PLUSITER,SUM,SUMITER
            ,TAIL,a,head,ifPlus,ifSum,isempty,le,plus,plusIter,sum,sumIter,tail} and constructors {0,b,c,c1,c10,c11,c12
            ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5,c6,c7,c8,c9,cons,error,false,nil,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c19()
            A() -> c20()
            HEAD(cons(z0,z1)) -> c16()
            HEAD(nil()) -> c15()
            IFPLUS(false(),z0,z1,z2) -> c4(PLUSITER(z0,s(z1),s(z2)))
            IFPLUS(true(),z0,z1,z2) -> c3()
            IFSUM(false(),z0,z1,z2) -> c12(SUMITER(tail(z0),z2),TAIL(z0))
            IFSUM(true(),z0,z1,z2) -> c11()
            ISEMPTY(cons(z0,z1)) -> c14()
            ISEMPTY(nil()) -> c13()
            LE(0(),z0) -> c6()
            LE(s(z0),0()) -> c5()
            LE(s(z0),s(z1)) -> c7(LE(z0,z1))
            PLUS(z0,z1) -> c1(PLUSITER(z0,z1,0()))
            PLUSITER(z0,z1,z2) -> c2(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2))
            SUM(z0) -> c8(SUMITER(z0,0()))
            SUMITER(z0,z1) -> c10(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),PLUS(z1,head(z0)),HEAD(z0))
            SUMITER(z0,z1) -> c9(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),ISEMPTY(z0))
            TAIL(cons(z0,z1)) -> c18()
            TAIL(nil()) -> c17()
        - Weak TRS:
            a() -> b()
            a() -> c()
            head(cons(z0,z1)) -> z0
            head(nil()) -> error()
            ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2))
            ifPlus(true(),z0,z1,z2) -> z1
            ifSum(false(),z0,z1,z2) -> sumIter(tail(z0),z2)
            ifSum(true(),z0,z1,z2) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            plus(z0,z1) -> plusIter(z0,z1,0())
            plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2)
            sum(z0) -> sumIter(z0,0())
            sumIter(z0,z1) -> ifSum(isempty(z0),z0,z1,plus(z1,head(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {A/0,HEAD/1,IFPLUS/4,IFSUM/4,ISEMPTY/1,LE/2,PLUS/2,PLUSITER/3,SUM/1,SUMITER/2,TAIL/1,a/0,head/1,ifPlus/4
            ,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1} / {0/0,b/0,c/0,c1/1,c10/3,c11/0,c12/2
            ,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c3/0,c4/1,c5/0,c6/0,c7/1,c8/1,c9/2,cons/2,error/0
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,HEAD,IFPLUS,IFSUM,ISEMPTY,LE,PLUS,PLUSITER,SUM,SUMITER
            ,TAIL,a,head,ifPlus,ifSum,isempty,le,plus,plusIter,sum,sumIter,tail} and constructors {0,b,c,c1,c10,c11,c12
            ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5,c6,c7,c8,c9,cons,error,false,nil,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c19()
            A() -> c20()
            HEAD(cons(z0,z1)) -> c16()
            HEAD(nil()) -> c15()
            IFPLUS(false(),z0,z1,z2) -> c4(PLUSITER(z0,s(z1),s(z2)))
            IFPLUS(true(),z0,z1,z2) -> c3()
            IFSUM(false(),z0,z1,z2) -> c12(SUMITER(tail(z0),z2),TAIL(z0))
            IFSUM(true(),z0,z1,z2) -> c11()
            ISEMPTY(cons(z0,z1)) -> c14()
            ISEMPTY(nil()) -> c13()
            LE(0(),z0) -> c6()
            LE(s(z0),0()) -> c5()
            LE(s(z0),s(z1)) -> c7(LE(z0,z1))
            PLUS(z0,z1) -> c1(PLUSITER(z0,z1,0()))
            PLUSITER(z0,z1,z2) -> c2(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2))
            SUM(z0) -> c8(SUMITER(z0,0()))
            SUMITER(z0,z1) -> c10(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),PLUS(z1,head(z0)),HEAD(z0))
            SUMITER(z0,z1) -> c9(IFSUM(isempty(z0),z0,z1,plus(z1,head(z0))),ISEMPTY(z0))
            TAIL(cons(z0,z1)) -> c18()
            TAIL(nil()) -> c17()
        - Weak TRS:
            a() -> b()
            a() -> c()
            head(cons(z0,z1)) -> z0
            head(nil()) -> error()
            ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2))
            ifPlus(true(),z0,z1,z2) -> z1
            ifSum(false(),z0,z1,z2) -> sumIter(tail(z0),z2)
            ifSum(true(),z0,z1,z2) -> z1
            isempty(cons(z0,z1)) -> false()
            isempty(nil()) -> true()
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            plus(z0,z1) -> plusIter(z0,z1,0())
            plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2)
            sum(z0) -> sumIter(z0,0())
            sumIter(z0,z1) -> ifSum(isempty(z0),z0,z1,plus(z1,head(z0)))
            tail(cons(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {A/0,HEAD/1,IFPLUS/4,IFSUM/4,ISEMPTY/1,LE/2,PLUS/2,PLUSITER/3,SUM/1,SUMITER/2,TAIL/1,a/0,head/1,ifPlus/4
            ,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1} / {0/0,b/0,c/0,c1/1,c10/3,c11/0,c12/2
            ,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c3/0,c4/1,c5/0,c6/0,c7/1,c8/1,c9/2,cons/2,error/0
            ,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,HEAD,IFPLUS,IFSUM,ISEMPTY,LE,PLUS,PLUSITER,SUM,SUMITER
            ,TAIL,a,head,ifPlus,ifSum,isempty,le,plus,plusIter,sum,sumIter,tail} and constructors {0,b,c,c1,c10,c11,c12
            ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5,c6,c7,c8,c9,cons,error,false,nil,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          LE(x,y){x -> s(x),y -> s(y)} =
            LE(s(x),s(y)) ->^+ c7(LE(x,y))
              = C[LE(x,y) = LE(x,y){}]

WORST_CASE(Omega(n^1),?)