WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,weight} and constructors {0,cons,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,weight} and constructors {0,cons,nil,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: sum(x,y){x -> cons(0(),x)} = sum(cons(0(),x),y) ->^+ sum(x,y) = C[sum(x,y) = sum(x,y){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,weight} and constructors {0,cons,nil,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) sum#(nil(),y) -> c_3() weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) weight#(cons(n,nil())) -> c_5() Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) sum#(nil(),y) -> c_3() weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) weight#(cons(n,nil())) -> c_5() - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,5} by application of Pre({3,5}) = {1,4}. Here rules are labelled as follows: 1: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) 2: sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) 3: sum#(nil(),y) -> c_3() 4: weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) 5: weight#(cons(n,nil())) -> c_5() ** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) - Weak DPs: sum#(nil(),y) -> c_3() weight#(cons(n,nil())) -> c_5() - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:sum#(cons(0(),x),y) -> c_1(sum#(x,y)) -->_1 sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))):2 -->_1 sum#(nil(),y) -> c_3():4 -->_1 sum#(cons(0(),x),y) -> c_1(sum#(x,y)):1 2:S:sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) -->_1 sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))):2 -->_1 sum#(cons(0(),x),y) -> c_1(sum#(x,y)):1 3:S:weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) -->_1 weight#(cons(n,nil())) -> c_5():5 -->_1 weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))):3 -->_2 sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))):2 -->_2 sum#(cons(0(),x),y) -> c_1(sum#(x,y)):1 4:W:sum#(nil(),y) -> c_3() 5:W:weight#(cons(n,nil())) -> c_5() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: weight#(cons(n,nil())) -> c_5() 4: sum#(nil(),y) -> c_3() ** Step 1.b:4: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x))) weight(cons(n,nil())) -> n - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) ** Step 1.b:5: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) and a lower component sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) Further, following extension rules are added to the lower component. weight#(cons(n,cons(m,x))) -> sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) -> weight#(sum(cons(n,cons(m,x)),cons(0(),x))) *** Step 1.b:5.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))) -->_1 weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x))) ,sum#(cons(n,cons(m,x)),cons(0(),x))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x)))) *** Step 1.b:5.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x)))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + 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_4) = {1} Following symbols are considered usable: {sum,sum#,weight#} TcT has computed the following interpretation: p(0) = [0] p(cons) = [1] x1 + [1] x2 + [4] p(nil) = [8] p(s) = [0] p(sum) = [1] x2 + [0] p(weight) = [1] p(sum#) = [1] x1 + [1] p(weight#) = [2] x1 + [0] p(c_1) = [1] x1 + [2] p(c_2) = [1] x1 + [8] p(c_3) = [2] p(c_4) = [1] x1 + [7] p(c_5) = [0] Following rules are strictly oriented: weight#(cons(n,cons(m,x))) = [2] m + [2] n + [2] x + [16] > [2] x + [15] = c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x)))) Following rules are (at-least) weakly oriented: sum(cons(0(),x),y) = [1] y + [0] >= [1] y + [0] = sum(x,y) sum(cons(s(n),x),cons(m,y)) = [1] m + [1] y + [4] >= [1] y + [4] = sum(cons(n,x),cons(s(m),y)) sum(nil(),y) = [1] y + [0] >= [1] y + [0] = y *** Step 1.b:5.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: weight#(cons(n,cons(m,x))) -> c_4(weight#(sum(cons(n,cons(m,x)),cons(0(),x)))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/1,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:5.b:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) - Weak DPs: weight#(cons(n,cons(m,x))) -> sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) -> weight#(sum(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + 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} Following symbols are considered usable: {sum,sum#,weight#} TcT has computed the following interpretation: p(0) = [0] p(cons) = [1] x2 + [4] p(nil) = [4] p(s) = [1] x1 + [4] p(sum) = [1] x2 + [2] p(weight) = [1] x1 + [0] p(sum#) = [1] x1 + [1] x2 + [8] p(weight#) = [2] x1 + [10] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] p(c_4) = [2] x1 + [2] x2 + [1] p(c_5) = [0] Following rules are strictly oriented: sum#(cons(0(),x),y) = [1] x + [1] y + [12] > [1] x + [1] y + [8] = c_1(sum#(x,y)) Following rules are (at-least) weakly oriented: sum#(cons(s(n),x),cons(m,y)) = [1] x + [1] y + [16] >= [1] x + [1] y + [16] = c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) = [2] x + [26] >= [2] x + [20] = sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) = [2] x + [26] >= [2] x + [22] = weight#(sum(cons(n,cons(m,x)),cons(0(),x))) sum(cons(0(),x),y) = [1] y + [2] >= [1] y + [2] = sum(x,y) sum(cons(s(n),x),cons(m,y)) = [1] y + [6] >= [1] y + [6] = sum(cons(n,x),cons(s(m),y)) sum(nil(),y) = [1] y + [2] >= [1] y + [0] = y *** Step 1.b:5.b:2: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) - Weak DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) weight#(cons(n,cons(m,x))) -> sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) -> weight#(sum(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1} Following symbols are considered usable: {sum,sum#,weight#} TcT has computed the following interpretation: p(0) = [4] [0] p(cons) = [0 1] x_1 + [1 2] x_2 + [0] [0 1] [0 1] [0] p(nil) = [1] [1] p(s) = [0 0] x_1 + [0] [0 1] [1] p(sum) = [0 1] x_1 + [1 0] x_2 + [0] [0 1] [0 1] [0] p(weight) = [0 0] x_1 + [1] [0 1] [1] p(sum#) = [2 4] x_1 + [0] [0 1] [0] p(weight#) = [3 3] x_1 + [1] [1 1] [0] p(c_1) = [1 2] x_1 + [0] [0 0] [0] p(c_2) = [1 0] x_1 + [0] [0 0] [0] p(c_3) = [0] [0] p(c_4) = [0 2] x_1 + [1 1] x_2 + [0] [1 0] [1 1] [2] p(c_5) = [1] [4] Following rules are strictly oriented: sum#(cons(s(n),x),cons(m,y)) = [0 6] n + [2 8] x + [6] [0 1] [0 1] [1] > [0 6] n + [2 8] x + [0] [0 0] [0 0] [0] = c_2(sum#(cons(n,x),cons(s(m),y))) Following rules are (at-least) weakly oriented: sum#(cons(0(),x),y) = [2 8] x + [0] [0 1] [0] >= [2 6] x + [0] [0 0] [0] = c_1(sum#(x,y)) weight#(cons(n,cons(m,x))) = [0 12] m + [0 6] n + [3 15] x + [1] [0 4] [0 2] [1 5] [0] >= [0 10] m + [0 6] n + [2 12] x + [0] [0 1] [0 1] [0 1] [0] = sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) = [0 12] m + [0 6] n + [3 15] x + [1] [0 4] [0 2] [1 5] [0] >= [0 6] m + [0 6] n + [3 15] x + [1] [0 2] [0 2] [1 5] [0] = weight#(sum(cons(n,cons(m,x)),cons(0(),x))) sum(cons(0(),x),y) = [0 1] x + [1 0] y + [0] [0 1] [0 1] [0] >= [0 1] x + [1 0] y + [0] [0 1] [0 1] [0] = sum(x,y) sum(cons(s(n),x),cons(m,y)) = [0 1] m + [0 1] n + [0 1] x + [1 2] y + [1] [0 1] [0 1] [0 1] [0 1] [1] >= [0 1] m + [0 1] n + [0 1] x + [1 2] y + [1] [0 1] [0 1] [0 1] [0 1] [1] = sum(cons(n,x),cons(s(m),y)) sum(nil(),y) = [1 0] y + [1] [0 1] [1] >= [1 0] y + [0] [0 1] [0] = y *** Step 1.b:5.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sum#(cons(0(),x),y) -> c_1(sum#(x,y)) sum#(cons(s(n),x),cons(m,y)) -> c_2(sum#(cons(n,x),cons(s(m),y))) weight#(cons(n,cons(m,x))) -> sum#(cons(n,cons(m,x)),cons(0(),x)) weight#(cons(n,cons(m,x))) -> weight#(sum(cons(n,cons(m,x)),cons(0(),x))) - Weak TRS: sum(cons(0(),x),y) -> sum(x,y) sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y)) sum(nil(),y) -> y - Signature: {sum/2,weight/1,sum#/2,weight#/1} / {0/0,cons/2,nil/0,s/1,c_1/1,c_2/1,c_3/0,c_4/2,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {sum#,weight#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))