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

WORST_CASE(Omega(n^1),?)