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)) A__X(z0,z1) -> c10() A__X(z0,0()) -> c6() A__X(z0,s(z1)) -> c7(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z0)) A__X(z0,s(z1)) -> c8(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z1)) A__X(z0,s(z1)) -> c9(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),MARK(z0)) MARK(0()) -> c17() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(plus(z0,z1)) -> c12(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c13(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c18(MARK(z0)) MARK(tt()) -> c16() MARK(x(z0,z1)) -> c14(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c15(A__X(mark(z0),mark(z1)),MARK(z1)) - 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))) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__plus(a__x(mark(z0),mark(z1)),mark(z0)) 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() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__AND/2,A__PLUS/2,A__X/2,MARK/1,a__and/2,a__plus/2,a__x/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/2,c12/2 ,c13/2,c14/2,c15/2,c16/0,c17/0,c18/1,c2/1,c3/2,c4/2,c5/0,c6/0,c7/3,c8/3,c9/2,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,A__X,MARK,a__and,a__plus,a__x ,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt,x} + 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)) A__X(z0,z1) -> c10() A__X(z0,0()) -> c6() A__X(z0,s(z1)) -> c7(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z0)) A__X(z0,s(z1)) -> c8(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z1)) A__X(z0,s(z1)) -> c9(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),MARK(z0)) MARK(0()) -> c17() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(plus(z0,z1)) -> c12(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c13(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c18(MARK(z0)) MARK(tt()) -> c16() MARK(x(z0,z1)) -> c14(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c15(A__X(mark(z0),mark(z1)),MARK(z1)) - 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))) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__plus(a__x(mark(z0),mark(z1)),mark(z0)) 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() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__AND/2,A__PLUS/2,A__X/2,MARK/1,a__and/2,a__plus/2,a__x/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/2,c12/2 ,c13/2,c14/2,c15/2,c16/0,c17/0,c18/1,c2/1,c3/2,c4/2,c5/0,c6/0,c7/3,c8/3,c9/2,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,A__X,MARK,a__and,a__plus,a__x ,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt,x} + 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)) A__X(z0,z1) -> c10() A__X(z0,0()) -> c6() A__X(z0,s(z1)) -> c7(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z0)) A__X(z0,s(z1)) -> c8(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),A__X(mark(z0),mark(z1)),MARK(z1)) A__X(z0,s(z1)) -> c9(A__PLUS(a__x(mark(z0),mark(z1)),mark(z0)),MARK(z0)) MARK(0()) -> c17() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(plus(z0,z1)) -> c12(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c13(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c18(MARK(z0)) MARK(tt()) -> c16() MARK(x(z0,z1)) -> c14(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c15(A__X(mark(z0),mark(z1)),MARK(z1)) - 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))) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__plus(a__x(mark(z0),mark(z1)),mark(z0)) 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() mark(x(z0,z1)) -> a__x(mark(z0),mark(z1)) - Signature: {A__AND/2,A__PLUS/2,A__X/2,MARK/1,a__and/2,a__plus/2,a__x/2,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/2,c12/2 ,c13/2,c14/2,c15/2,c16/0,c17/0,c18/1,c2/1,c3/2,c4/2,c5/0,c6/0,c7/3,c8/3,c9/2,plus/2,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__PLUS,A__X,MARK,a__and,a__plus,a__x ,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5,c6,c7,c8,c9,plus,s,tt,x} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> and(x,y)} = MARK(and(x,y)) ->^+ c11(A__AND(mark(x),y),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)