WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A__AND(z0,z1) -> c1()
            A__AND(tt(),z0) -> c(MARK(z0))
            A__PLUS(z0,z1) -> c5()
            A__PLUS(z0,0()) -> c2(MARK(z0))
            A__PLUS(z0,s(z1)) -> c3(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            A__PLUS(z0,s(z1)) -> c4(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(0()) -> c10()
            MARK(and(z0,z1)) -> c6(A__AND(mark(z0),z1),MARK(z0))
            MARK(plus(z0,z1)) -> c7(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            MARK(plus(z0,z1)) -> c8(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(s(z0)) -> c11(MARK(z0))
            MARK(tt()) -> c9()
        - Weak TRS:
            a__and(z0,z1) -> and(z0,z1)
            a__and(tt(),z0) -> mark(z0)
            a__plus(z0,z1) -> plus(z0,z1)
            a__plus(z0,0()) -> mark(z0)
            a__plus(z0,s(z1)) -> s(a__plus(mark(z0),mark(z1)))
            mark(0()) -> 0()
            mark(and(z0,z1)) -> a__and(mark(z0),z1)
            mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1))
            mark(s(z0)) -> s(mark(z0))
            mark(tt()) -> tt()
        - Signature:
            {A__AND/2,A__PLUS/2,MARK/1,a__and/2,a__plus/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/1,c2/1,c3/2,c4/2,c5/0
            ,c6/2,c7/2,c8/2,c9/0,plus/2,s/1,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,MARK,a__and,a__plus
            ,mark} and constructors {0,and,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A__AND(z0,z1) -> c1()
            A__AND(tt(),z0) -> c(MARK(z0))
            A__PLUS(z0,z1) -> c5()
            A__PLUS(z0,0()) -> c2(MARK(z0))
            A__PLUS(z0,s(z1)) -> c3(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            A__PLUS(z0,s(z1)) -> c4(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(0()) -> c10()
            MARK(and(z0,z1)) -> c6(A__AND(mark(z0),z1),MARK(z0))
            MARK(plus(z0,z1)) -> c7(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            MARK(plus(z0,z1)) -> c8(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(s(z0)) -> c11(MARK(z0))
            MARK(tt()) -> c9()
        - Weak TRS:
            a__and(z0,z1) -> and(z0,z1)
            a__and(tt(),z0) -> mark(z0)
            a__plus(z0,z1) -> plus(z0,z1)
            a__plus(z0,0()) -> mark(z0)
            a__plus(z0,s(z1)) -> s(a__plus(mark(z0),mark(z1)))
            mark(0()) -> 0()
            mark(and(z0,z1)) -> a__and(mark(z0),z1)
            mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1))
            mark(s(z0)) -> s(mark(z0))
            mark(tt()) -> tt()
        - Signature:
            {A__AND/2,A__PLUS/2,MARK/1,a__and/2,a__plus/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/1,c2/1,c3/2,c4/2,c5/0
            ,c6/2,c7/2,c8/2,c9/0,plus/2,s/1,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,MARK,a__and,a__plus
            ,mark} and constructors {0,and,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            A__AND(z0,z1) -> c1()
            A__AND(tt(),z0) -> c(MARK(z0))
            A__PLUS(z0,z1) -> c5()
            A__PLUS(z0,0()) -> c2(MARK(z0))
            A__PLUS(z0,s(z1)) -> c3(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            A__PLUS(z0,s(z1)) -> c4(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(0()) -> c10()
            MARK(and(z0,z1)) -> c6(A__AND(mark(z0),z1),MARK(z0))
            MARK(plus(z0,z1)) -> c7(A__PLUS(mark(z0),mark(z1)),MARK(z0))
            MARK(plus(z0,z1)) -> c8(A__PLUS(mark(z0),mark(z1)),MARK(z1))
            MARK(s(z0)) -> c11(MARK(z0))
            MARK(tt()) -> c9()
        - Weak TRS:
            a__and(z0,z1) -> and(z0,z1)
            a__and(tt(),z0) -> mark(z0)
            a__plus(z0,z1) -> plus(z0,z1)
            a__plus(z0,0()) -> mark(z0)
            a__plus(z0,s(z1)) -> s(a__plus(mark(z0),mark(z1)))
            mark(0()) -> 0()
            mark(and(z0,z1)) -> a__and(mark(z0),z1)
            mark(plus(z0,z1)) -> a__plus(mark(z0),mark(z1))
            mark(s(z0)) -> s(mark(z0))
            mark(tt()) -> tt()
        - Signature:
            {A__AND/2,A__PLUS/2,MARK/1,a__and/2,a__plus/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/1,c2/1,c3/2,c4/2,c5/0
            ,c6/2,c7/2,c8/2,c9/0,plus/2,s/1,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,MARK,a__and,a__plus
            ,mark} and constructors {0,and,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          MARK(x){x -> and(x,y)} =
            MARK(and(x,y)) ->^+ c6(A__AND(mark(x),y),MARK(x))
              = C[MARK(x) = MARK(x){}]

WORST_CASE(Omega(n^1),?)