WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 - Signature: {*/2,*'/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,*'} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 - Signature: {*/2,*'/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,*'} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 - Signature: {*/2,*'/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,*'} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: *'(x,y){y -> +(y,z)} = *'(x,+(y,z)) ->^+ c(*'(x,y)) = C[*'(x,y) = *'(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 - Signature: {*/2,*'/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,*'} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(z0,1()) -> c_3() *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) *'#(1(),z0) -> c_6() Weak DPs *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) *#(z0,1()) -> c_8() *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) *#(1(),z0) -> c_10() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(z0,1()) -> c_3() *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) *'#(1(),z0) -> c_6() - Weak DPs: *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) *#(z0,1()) -> c_8() *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) *#(1(),z0) -> c_10() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,6} by application of Pre({3,6}) = {1,2,4,5}. Here rules are labelled as follows: 1: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) 2: *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) 3: *'#(z0,1()) -> c_3() 4: *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) 5: *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) 6: *'#(1(),z0) -> c_6() 7: *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) 8: *#(z0,1()) -> c_8() 9: *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) 10: *#(1(),z0) -> c_10() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Weak DPs: *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) *#(z0,1()) -> c_8() *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) *#(1(),z0) -> c_10() *'#(z0,1()) -> c_3() *'#(1(),z0) -> c_6() - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) -->_1 *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)):4 -->_1 *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)):3 -->_1 *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)):2 -->_1 *'#(1(),z0) -> c_6():10 -->_1 *'#(z0,1()) -> c_3():9 -->_1 *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)):1 2:S:*'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) -->_1 *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)):4 -->_1 *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)):3 -->_1 *'#(1(),z0) -> c_6():10 -->_1 *'#(z0,1()) -> c_3():9 -->_1 *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)):2 -->_1 *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)):1 3:S:*'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) -->_1 *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)):4 -->_1 *'#(1(),z0) -> c_6():10 -->_1 *'#(z0,1()) -> c_3():9 -->_1 *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)):3 -->_1 *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)):2 -->_1 *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)):1 4:S:*'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) -->_1 *'#(1(),z0) -> c_6():10 -->_1 *'#(z0,1()) -> c_3():9 -->_1 *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)):4 -->_1 *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)):3 -->_1 *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)):2 -->_1 *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)):1 5:W:*#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) -->_2 *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)):7 -->_1 *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)):7 -->_2 *#(1(),z0) -> c_10():8 -->_1 *#(1(),z0) -> c_10():8 -->_2 *#(z0,1()) -> c_8():6 -->_1 *#(z0,1()) -> c_8():6 -->_2 *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)):5 -->_1 *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)):5 6:W:*#(z0,1()) -> c_8() 7:W:*#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) -->_2 *#(1(),z0) -> c_10():8 -->_1 *#(1(),z0) -> c_10():8 -->_2 *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)):7 -->_1 *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)):7 -->_2 *#(z0,1()) -> c_8():6 -->_1 *#(z0,1()) -> c_8():6 -->_2 *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)):5 -->_1 *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)):5 8:W:*#(1(),z0) -> c_10() 9:W:*'#(z0,1()) -> c_3() 10:W:*'#(1(),z0) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: *#(z0,+(z1,z2)) -> c_7(*#(z0,z1),*#(z0,z2)) 7: *#(+(z0,z1),z2) -> c_9(*#(z0,z2),*#(z1,z2)) 6: *#(z0,1()) -> c_8() 8: *#(1(),z0) -> c_10() 9: *'#(z0,1()) -> c_3() 10: *'#(1(),z0) -> c_6() ** Step 1.b:4: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Weak TRS: *(z0,+(z1,z2)) -> +(*(z0,z1),*(z0,z2)) *(z0,1()) -> z0 *(+(z0,z1),z2) -> +(*(z0,z2),*(z1,z2)) *(1(),z0) -> z0 *'(z0,+(z1,z2)) -> c(*'(z0,z1)) *'(z0,+(z1,z2)) -> c1(*'(z0,z2)) *'(z0,1()) -> c4() *'(+(z0,z1),z2) -> c2(*'(z0,z2)) *'(+(z0,z1),z2) -> c3(*'(z1,z2)) *'(1(),z0) -> c5() - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) ** Step 1.b:5: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {*#,*'#} TcT has computed the following interpretation: p(*) = [1] x2 + [2] p(*') = [1] x1 + [4] p(+) = [1] x1 + [1] x2 + [2] p(1) = [1] p(c) = [0] p(c1) = [2] p(c2) = [1] p(c3) = [1] x1 + [1] p(c4) = [0] p(c5) = [1] p(*#) = [1] x1 + [2] x2 + [2] p(*'#) = [1] x2 + [0] p(c_1) = [1] x1 + [2] p(c_2) = [1] x1 + [1] p(c_3) = [2] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [4] p(c_8) = [1] p(c_9) = [2] x1 + [1] x2 + [1] p(c_10) = [1] Following rules are strictly oriented: *'#(z0,+(z1,z2)) = [1] z1 + [1] z2 + [2] > [1] z2 + [1] = c_2(*'#(z0,z2)) Following rules are (at-least) weakly oriented: *'#(z0,+(z1,z2)) = [1] z1 + [1] z2 + [2] >= [1] z1 + [2] = c_1(*'#(z0,z1)) *'#(+(z0,z1),z2) = [1] z2 + [0] >= [1] z2 + [0] = c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) = [1] z2 + [0] >= [1] z2 + [0] = c_5(*'#(z1,z2)) ** Step 1.b:6: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Weak DPs: *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(*) = [0] p(*') = [0] p(+) = [1] x1 + [1] x2 + [3] p(1) = [0] p(c) = [1] x1 + [0] p(c1) = [1] x1 + [0] p(c2) = [1] x1 + [0] p(c3) = [1] x1 + [0] p(c4) = [0] p(c5) = [0] p(*#) = [0] p(*'#) = [9] x1 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] Following rules are strictly oriented: *'#(+(z0,z1),z2) = [9] z0 + [9] z1 + [27] > [9] z0 + [0] = c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) = [9] z0 + [9] z1 + [27] > [9] z1 + [0] = c_5(*'#(z1,z2)) Following rules are (at-least) weakly oriented: *'#(z0,+(z1,z2)) = [9] z0 + [0] >= [9] z0 + [0] = c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) = [9] z0 + [0] >= [9] z0 + [0] = c_2(*'#(z0,z2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:7: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) - Weak DPs: *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {*#,*'#} TcT has computed the following interpretation: p(*) = [1] x1 + [2] x2 + [0] p(*') = [0] p(+) = [1] x1 + [1] x2 + [2] p(1) = [0] p(c) = [1] p(c1) = [0] p(c2) = [1] x1 + [1] p(c3) = [1] p(c4) = [1] p(c5) = [4] p(*#) = [1] x2 + [8] p(*'#) = [4] x1 + [8] x2 + [0] p(c_1) = [1] x1 + [8] p(c_2) = [1] x1 + [0] p(c_3) = [4] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [6] p(c_6) = [1] p(c_7) = [1] x2 + [4] p(c_8) = [1] p(c_9) = [2] x1 + [1] x2 + [0] p(c_10) = [1] Following rules are strictly oriented: *'#(z0,+(z1,z2)) = [4] z0 + [8] z1 + [8] z2 + [16] > [4] z0 + [8] z1 + [8] = c_1(*'#(z0,z1)) Following rules are (at-least) weakly oriented: *'#(z0,+(z1,z2)) = [4] z0 + [8] z1 + [8] z2 + [16] >= [4] z0 + [8] z2 + [0] = c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) = [4] z0 + [4] z1 + [8] z2 + [8] >= [4] z0 + [8] z2 + [0] = c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) = [4] z0 + [4] z1 + [8] z2 + [8] >= [4] z1 + [8] z2 + [6] = c_5(*'#(z1,z2)) ** Step 1.b:8: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: *'#(z0,+(z1,z2)) -> c_1(*'#(z0,z1)) *'#(z0,+(z1,z2)) -> c_2(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_4(*'#(z0,z2)) *'#(+(z0,z1),z2) -> c_5(*'#(z1,z2)) - Signature: {*/2,*'/2,*#/2,*'#/2} / {+/2,1/0,c/1,c1/1,c2/1,c3/1,c4/0,c5/0,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/2 ,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,*'#} and constructors {+,1,c,c1,c2,c3,c4,c5} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))