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

WORST_CASE(Omega(n^1),?)