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

WORST_CASE(Omega(n^1),?)