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

WORST_CASE(Omega(n^1),?)