WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c17()
            A() -> c18()
            APPEND(cons(z0,z1),z2) -> c13(APPEND(z1,z2))
            APPEND(nil(),z0) -> c12()
            IF(false(),false(),z0,z1,z2) -> c6(LESSE(z0,z1,s(z2)))
            IF(false(),true(),z0,z1,z2) -> c5()
            IF(true(),z0,z1,z2,z3) -> c4()
            LE(0(),z0) -> c15()
            LE(s(z0),0()) -> c14()
            LE(s(z0),s(z1)) -> c16(LE(z0,z1))
            LENGTH(cons(z0,z1)) -> c8(LENGTH(z1))
            LENGTH(nil()) -> c7()
            LESSE(z0,z1,z2) -> c2(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2),LE(length(z0),z2),LENGTH(z0))
            LESSE(z0,z1,z2) -> c3(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
                                 ,LE(length(toList(z1)),z2)
                                 ,LENGTH(toList(z1))
                                 ,TOLIST(z1))
            LESSELEMENTS(z0,z1) -> c1(LESSE(z0,z1,0()))
            TOLIST(leaf()) -> c9()
            TOLIST(node(z0,z1,z2)) -> c10(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z0))
            TOLIST(node(z0,z1,z2)) -> c11(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z2))
        - Weak TRS:
            a() -> c()
            a() -> d()
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> z0
            if(false(),false(),z0,z1,z2) -> lessE(z0,z1,s(z2))
            if(false(),true(),z0,z1,z2) -> z1
            if(true(),z0,z1,z2,z3) -> z1
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            length(cons(z0,z1)) -> s(length(z1))
            length(nil()) -> 0()
            lessE(z0,z1,z2) -> if(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
            lessElements(z0,z1) -> lessE(z0,z1,0())
            toList(leaf()) -> nil()
            toList(node(z0,z1,z2)) -> append(toList(z0),cons(z1,toList(z2)))
        - Signature:
            {A/0,APPEND/2,IF/5,LE/2,LENGTH/1,LESSE/3,LESSELEMENTS/2,TOLIST/1,a/0,append/2,if/5,le/2,length/1,lessE/3
            ,lessElements/2,toList/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/0,c2/3,c3/4
            ,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,APPEND,IF,LE,LENGTH,LESSE,LESSELEMENTS,TOLIST,a,append
            ,if,le,length,lessE,lessElements,toList} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3
            ,c4,c5,c6,c7,c8,c9,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c17()
            A() -> c18()
            APPEND(cons(z0,z1),z2) -> c13(APPEND(z1,z2))
            APPEND(nil(),z0) -> c12()
            IF(false(),false(),z0,z1,z2) -> c6(LESSE(z0,z1,s(z2)))
            IF(false(),true(),z0,z1,z2) -> c5()
            IF(true(),z0,z1,z2,z3) -> c4()
            LE(0(),z0) -> c15()
            LE(s(z0),0()) -> c14()
            LE(s(z0),s(z1)) -> c16(LE(z0,z1))
            LENGTH(cons(z0,z1)) -> c8(LENGTH(z1))
            LENGTH(nil()) -> c7()
            LESSE(z0,z1,z2) -> c2(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2),LE(length(z0),z2),LENGTH(z0))
            LESSE(z0,z1,z2) -> c3(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
                                 ,LE(length(toList(z1)),z2)
                                 ,LENGTH(toList(z1))
                                 ,TOLIST(z1))
            LESSELEMENTS(z0,z1) -> c1(LESSE(z0,z1,0()))
            TOLIST(leaf()) -> c9()
            TOLIST(node(z0,z1,z2)) -> c10(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z0))
            TOLIST(node(z0,z1,z2)) -> c11(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z2))
        - Weak TRS:
            a() -> c()
            a() -> d()
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> z0
            if(false(),false(),z0,z1,z2) -> lessE(z0,z1,s(z2))
            if(false(),true(),z0,z1,z2) -> z1
            if(true(),z0,z1,z2,z3) -> z1
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            length(cons(z0,z1)) -> s(length(z1))
            length(nil()) -> 0()
            lessE(z0,z1,z2) -> if(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
            lessElements(z0,z1) -> lessE(z0,z1,0())
            toList(leaf()) -> nil()
            toList(node(z0,z1,z2)) -> append(toList(z0),cons(z1,toList(z2)))
        - Signature:
            {A/0,APPEND/2,IF/5,LE/2,LENGTH/1,LESSE/3,LESSELEMENTS/2,TOLIST/1,a/0,append/2,if/5,le/2,length/1,lessE/3
            ,lessElements/2,toList/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/0,c2/3,c3/4
            ,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,APPEND,IF,LE,LENGTH,LESSE,LESSELEMENTS,TOLIST,a,append
            ,if,le,length,lessE,lessElements,toList} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3
            ,c4,c5,c6,c7,c8,c9,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A() -> c17()
            A() -> c18()
            APPEND(cons(z0,z1),z2) -> c13(APPEND(z1,z2))
            APPEND(nil(),z0) -> c12()
            IF(false(),false(),z0,z1,z2) -> c6(LESSE(z0,z1,s(z2)))
            IF(false(),true(),z0,z1,z2) -> c5()
            IF(true(),z0,z1,z2,z3) -> c4()
            LE(0(),z0) -> c15()
            LE(s(z0),0()) -> c14()
            LE(s(z0),s(z1)) -> c16(LE(z0,z1))
            LENGTH(cons(z0,z1)) -> c8(LENGTH(z1))
            LENGTH(nil()) -> c7()
            LESSE(z0,z1,z2) -> c2(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2),LE(length(z0),z2),LENGTH(z0))
            LESSE(z0,z1,z2) -> c3(IF(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
                                 ,LE(length(toList(z1)),z2)
                                 ,LENGTH(toList(z1))
                                 ,TOLIST(z1))
            LESSELEMENTS(z0,z1) -> c1(LESSE(z0,z1,0()))
            TOLIST(leaf()) -> c9()
            TOLIST(node(z0,z1,z2)) -> c10(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z0))
            TOLIST(node(z0,z1,z2)) -> c11(APPEND(toList(z0),cons(z1,toList(z2))),TOLIST(z2))
        - Weak TRS:
            a() -> c()
            a() -> d()
            append(cons(z0,z1),z2) -> cons(z0,append(z1,z2))
            append(nil(),z0) -> z0
            if(false(),false(),z0,z1,z2) -> lessE(z0,z1,s(z2))
            if(false(),true(),z0,z1,z2) -> z1
            if(true(),z0,z1,z2,z3) -> z1
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            length(cons(z0,z1)) -> s(length(z1))
            length(nil()) -> 0()
            lessE(z0,z1,z2) -> if(le(length(z0),z2),le(length(toList(z1)),z2),z0,z1,z2)
            lessElements(z0,z1) -> lessE(z0,z1,0())
            toList(leaf()) -> nil()
            toList(node(z0,z1,z2)) -> append(toList(z0),cons(z1,toList(z2)))
        - Signature:
            {A/0,APPEND/2,IF/5,LE/2,LENGTH/1,LESSE/3,LESSELEMENTS/2,TOLIST/1,a/0,append/2,if/5,le/2,length/1,lessE/3
            ,lessElements/2,toList/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/0,c2/3,c3/4
            ,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A,APPEND,IF,LE,LENGTH,LESSE,LESSELEMENTS,TOLIST,a,append
            ,if,le,length,lessE,lessElements,toList} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3
            ,c4,c5,c6,c7,c8,c9,cons,d,false,leaf,nil,node,s,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) ->^+ c13(APPEND(y,z))
              = C[APPEND(y,z) = APPEND(y,z){}]

WORST_CASE(Omega(n^1),?)