WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(MARK(z0)) A__PLUS(z0,s(z1)) -> c12(A__U11(tt(),z1,z0)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(tt(),z0,z1)) A__U12(z0,z1,z2) -> c4() A__U12(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U12(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U21(z0,z1,z2) -> c6() A__U21(tt(),z0,z1) -> c5(A__U22(tt(),z0,z1)) A__U22(z0,z1,z2) -> c10() A__U22(tt(),z0,z1) -> c7(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U22(tt(),z0,z1) -> c8(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U22(tt(),z0,z1) -> c9(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c16() A__X(z0,0()) -> c14() A__X(z0,s(z1)) -> c15(A__U21(tt(),z1,z0)) MARK(0()) -> c27() MARK(U11(z0,z1,z2)) -> c17(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c18(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U21(z0,z1,z2)) -> c21(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(U22(z0,z1,z2)) -> c22(A__U22(mark(z0),z1,z2),MARK(z0)) MARK(plus(z0,z1)) -> c19(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c20(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c26(MARK(z0)) MARK(tt()) -> c25() MARK(x(z0,z1)) -> c23(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c24(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(tt(),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(tt(),z0,z1) -> a__U22(tt(),z0,z1) a__U22(z0,z1,z2) -> U22(z0,z1,z2) a__U22(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> mark(z0) a__plus(z0,s(z1)) -> a__U11(tt(),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__U21(tt(),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(U22(z0,z1,z2)) -> a__U22(mark(z0),z1,z2) 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__PLUS/2,A__U11/3,A__U12/3,A__U21/3,A__U22/3,A__X/2,MARK/1,a__U11/3,a__U12/3,a__U21/3,a__U22/3,a__plus/2 ,a__x/2,mark/1} / {0/0,U11/3,U12/3,U21/3,U22/3,c/1,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/1,c16/0,c17/2 ,c18/2,c19/2,c2/2,c20/2,c21/2,c22/2,c23/2,c24/2,c25/0,c26/1,c27/0,c3/2,c4/0,c5/1,c6/0,c7/3,c8/3,c9/2,plus/2 ,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__PLUS,A__U11,A__U12,A__U21,A__U22,A__X,MARK,a__U11 ,a__U12,a__U21,a__U22,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U22,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,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__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(MARK(z0)) A__PLUS(z0,s(z1)) -> c12(A__U11(tt(),z1,z0)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(tt(),z0,z1)) A__U12(z0,z1,z2) -> c4() A__U12(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U12(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U21(z0,z1,z2) -> c6() A__U21(tt(),z0,z1) -> c5(A__U22(tt(),z0,z1)) A__U22(z0,z1,z2) -> c10() A__U22(tt(),z0,z1) -> c7(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U22(tt(),z0,z1) -> c8(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U22(tt(),z0,z1) -> c9(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c16() A__X(z0,0()) -> c14() A__X(z0,s(z1)) -> c15(A__U21(tt(),z1,z0)) MARK(0()) -> c27() MARK(U11(z0,z1,z2)) -> c17(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c18(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U21(z0,z1,z2)) -> c21(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(U22(z0,z1,z2)) -> c22(A__U22(mark(z0),z1,z2),MARK(z0)) MARK(plus(z0,z1)) -> c19(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c20(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c26(MARK(z0)) MARK(tt()) -> c25() MARK(x(z0,z1)) -> c23(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c24(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(tt(),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(tt(),z0,z1) -> a__U22(tt(),z0,z1) a__U22(z0,z1,z2) -> U22(z0,z1,z2) a__U22(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> mark(z0) a__plus(z0,s(z1)) -> a__U11(tt(),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__U21(tt(),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(U22(z0,z1,z2)) -> a__U22(mark(z0),z1,z2) 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__PLUS/2,A__U11/3,A__U12/3,A__U21/3,A__U22/3,A__X/2,MARK/1,a__U11/3,a__U12/3,a__U21/3,a__U22/3,a__plus/2 ,a__x/2,mark/1} / {0/0,U11/3,U12/3,U21/3,U22/3,c/1,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/1,c16/0,c17/2 ,c18/2,c19/2,c2/2,c20/2,c21/2,c22/2,c23/2,c24/2,c25/0,c26/1,c27/0,c3/2,c4/0,c5/1,c6/0,c7/3,c8/3,c9/2,plus/2 ,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__PLUS,A__U11,A__U12,A__U21,A__U22,A__X,MARK,a__U11 ,a__U12,a__U21,a__U22,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U22,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,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__PLUS(z0,z1) -> c13() A__PLUS(z0,0()) -> c11(MARK(z0)) A__PLUS(z0,s(z1)) -> c12(A__U11(tt(),z1,z0)) A__U11(z0,z1,z2) -> c1() A__U11(tt(),z0,z1) -> c(A__U12(tt(),z0,z1)) A__U12(z0,z1,z2) -> c4() A__U12(tt(),z0,z1) -> c2(A__PLUS(mark(z1),mark(z0)),MARK(z1)) A__U12(tt(),z0,z1) -> c3(A__PLUS(mark(z1),mark(z0)),MARK(z0)) A__U21(z0,z1,z2) -> c6() A__U21(tt(),z0,z1) -> c5(A__U22(tt(),z0,z1)) A__U22(z0,z1,z2) -> c10() A__U22(tt(),z0,z1) -> c7(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z1)) A__U22(tt(),z0,z1) -> c8(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),A__X(mark(z1),mark(z0)),MARK(z0)) A__U22(tt(),z0,z1) -> c9(A__PLUS(a__x(mark(z1),mark(z0)),mark(z1)),MARK(z1)) A__X(z0,z1) -> c16() A__X(z0,0()) -> c14() A__X(z0,s(z1)) -> c15(A__U21(tt(),z1,z0)) MARK(0()) -> c27() MARK(U11(z0,z1,z2)) -> c17(A__U11(mark(z0),z1,z2),MARK(z0)) MARK(U12(z0,z1,z2)) -> c18(A__U12(mark(z0),z1,z2),MARK(z0)) MARK(U21(z0,z1,z2)) -> c21(A__U21(mark(z0),z1,z2),MARK(z0)) MARK(U22(z0,z1,z2)) -> c22(A__U22(mark(z0),z1,z2),MARK(z0)) MARK(plus(z0,z1)) -> c19(A__PLUS(mark(z0),mark(z1)),MARK(z0)) MARK(plus(z0,z1)) -> c20(A__PLUS(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c26(MARK(z0)) MARK(tt()) -> c25() MARK(x(z0,z1)) -> c23(A__X(mark(z0),mark(z1)),MARK(z0)) MARK(x(z0,z1)) -> c24(A__X(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__U12(tt(),z0,z1) a__U12(z0,z1,z2) -> U12(z0,z1,z2) a__U12(tt(),z0,z1) -> s(a__plus(mark(z1),mark(z0))) a__U21(z0,z1,z2) -> U21(z0,z1,z2) a__U21(tt(),z0,z1) -> a__U22(tt(),z0,z1) a__U22(z0,z1,z2) -> U22(z0,z1,z2) a__U22(tt(),z0,z1) -> a__plus(a__x(mark(z1),mark(z0)),mark(z1)) a__plus(z0,z1) -> plus(z0,z1) a__plus(z0,0()) -> mark(z0) a__plus(z0,s(z1)) -> a__U11(tt(),z1,z0) a__x(z0,z1) -> x(z0,z1) a__x(z0,0()) -> 0() a__x(z0,s(z1)) -> a__U21(tt(),z1,z0) mark(0()) -> 0() mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) mark(U12(z0,z1,z2)) -> a__U12(mark(z0),z1,z2) mark(U21(z0,z1,z2)) -> a__U21(mark(z0),z1,z2) mark(U22(z0,z1,z2)) -> a__U22(mark(z0),z1,z2) 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__PLUS/2,A__U11/3,A__U12/3,A__U21/3,A__U22/3,A__X/2,MARK/1,a__U11/3,a__U12/3,a__U21/3,a__U22/3,a__plus/2 ,a__x/2,mark/1} / {0/0,U11/3,U12/3,U21/3,U22/3,c/1,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/1,c16/0,c17/2 ,c18/2,c19/2,c2/2,c20/2,c21/2,c22/2,c23/2,c24/2,c25/0,c26/1,c27/0,c3/2,c4/0,c5/1,c6/0,c7/3,c8/3,c9/2,plus/2 ,s/1,tt/0,x/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__PLUS,A__U11,A__U12,A__U21,A__U22,A__X,MARK,a__U11 ,a__U12,a__U21,a__U22,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U22,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,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 -> U11(x,y,z)} = MARK(U11(x,y,z)) ->^+ c17(A__U11(mark(x),y,z),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)