MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,prod,sum} and constructors {0,cons,nil,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(x,0()) -> c_1() *#(0(),x) -> c_2() *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_4() +#(0(),x) -> c_5() +#(s(x),s(y)) -> c_6(+#(x,y)) prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_8() sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_10() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(0(),x) -> c_2() *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_4() +#(0(),x) -> c_5() +#(s(x),s(y)) -> c_6(+#(x,y)) prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_8() sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_10() - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,5,8,10} by application of Pre({1,2,4,5,8,10}) = {3,6,7,9}. Here rules are labelled as follows: 1: *#(x,0()) -> c_1() 2: *#(0(),x) -> c_2() 3: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 4: +#(x,0()) -> c_4() 5: +#(0(),x) -> c_5() 6: +#(s(x),s(y)) -> c_6(+#(x,y)) 7: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) 8: prod#(nil()) -> c_8() 9: sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) 10: sum#(nil()) -> c_10() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(x,0()) -> c_1() *#(0(),x) -> c_2() +#(x,0()) -> c_4() +#(0(),x) -> c_5() prod#(nil()) -> c_8() sum#(nil()) -> c_10() - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_6(+#(x,y)):2 -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):2 -->_3 +#(0(),x) -> c_5():8 -->_1 +#(0(),x) -> c_5():8 -->_3 +#(x,0()) -> c_4():7 -->_1 +#(x,0()) -> c_4():7 -->_2 *#(0(),x) -> c_2():6 -->_2 *#(x,0()) -> c_1():5 -->_2 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 2:S:+#(s(x),s(y)) -> c_6(+#(x,y)) -->_1 +#(0(),x) -> c_5():8 -->_1 +#(x,0()) -> c_4():7 -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):2 3:S:prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) -->_2 prod#(nil()) -> c_8():9 -->_1 *#(0(),x) -> c_2():6 -->_1 *#(x,0()) -> c_1():5 -->_2 prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)):3 -->_1 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 4:S:sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) -->_2 sum#(nil()) -> c_10():10 -->_1 +#(0(),x) -> c_5():8 -->_1 +#(x,0()) -> c_4():7 -->_2 sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)):4 -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):2 5:W:*#(x,0()) -> c_1() 6:W:*#(0(),x) -> c_2() 7:W:+#(x,0()) -> c_4() 8:W:+#(0(),x) -> c_5() 9:W:prod#(nil()) -> c_8() 10:W:sum#(nil()) -> c_10() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: sum#(nil()) -> c_10() 9: prod#(nil()) -> c_8() 5: *#(x,0()) -> c_1() 6: *#(0(),x) -> c_2() 7: +#(x,0()) -> c_4() 8: +#(0(),x) -> c_5() * Step 4: Decompose MAYBE + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0 ,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} Problem (S) - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0 ,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} ** Step 4.a:1: DecomposeDG MAYBE + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) and a lower component *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) Further, following extension rules are added to the lower component. prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) *** Step 4.a:1.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) The strictly oriented rules are moved into the weak component. **** Step 4.a:1.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1,2}, uargs(c_9) = {1,2} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [1] x1 + [1] x2 + [2] p(+) = [6] x1 + [4] x2 + [0] p(0) = [0] p(cons) = [1] x1 + [1] x2 + [4] p(nil) = [1] p(prod) = [0] p(s) = [1] x1 + [1] p(sum) = [2] p(*#) = [0] p(+#) = [4] x1 + [1] p(prod#) = [0] p(sum#) = [4] x1 + [12] p(c_1) = [4] p(c_2) = [2] p(c_3) = [2] x1 + [1] x2 + [1] x3 + [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [2] p(c_7) = [8] x1 + [4] x2 + [0] p(c_8) = [2] p(c_9) = [1] x1 + [1] x2 + [8] p(c_10) = [1] Following rules are strictly oriented: sum#(cons(x,l)) = [4] l + [4] x + [28] > [4] l + [4] x + [21] = c_9(+#(x,sum(l)),sum#(l)) Following rules are (at-least) weakly oriented: prod#(cons(x,l)) = [0] >= [0] = c_7(*#(x,prod(l)),prod#(l)) **** Step 4.a:1.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 4.a:1.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)):1 2:W:sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) **** Step 4.a:1.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: prod#(cons(x,l)) -> c_7(prod#(l)) **** Step 4.a:1.a:1.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: prod#(cons(x,l)) -> c_7(prod#(l)) **** Step 4.a:1.a:1.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: prod#(cons(x,l)) -> c_7(prod#(l)) The strictly oriented rules are moved into the weak component. ***** Step 4.a:1.a:1.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [1] p(+) = [2] x1 + [1] p(0) = [1] p(cons) = [1] x2 + [8] p(nil) = [1] p(prod) = [1] x1 + [4] p(s) = [1] x1 + [0] p(sum) = [0] p(*#) = [1] x1 + [1] x2 + [0] p(+#) = [8] x1 + [1] p(prod#) = [1] x1 + [8] p(sum#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [2] p(c_3) = [1] x2 + [1] x3 + [0] p(c_4) = [2] p(c_5) = [1] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [2] p(c_9) = [8] x2 + [1] p(c_10) = [1] Following rules are strictly oriented: prod#(cons(x,l)) = [1] l + [16] > [1] l + [8] = c_7(prod#(l)) Following rules are (at-least) weakly oriented: ***** Step 4.a:1.a:1.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 4.a:1.a:1.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:prod#(cons(x,l)) -> c_7(prod#(l)) -->_1 prod#(cons(x,l)) -> c_7(prod#(l)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: prod#(cons(x,l)) -> c_7(prod#(l)) ***** Step 4.a:1.a:1.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 4.a:1.b:1: DecomposeDG MAYBE + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) and a lower component +#(s(x),s(y)) -> c_6(+#(x,y)) Further, following extension rules are added to the lower component. *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) **** Step 4.a:1.b:1.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) -> +#(x,sum(l)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: sum#(cons(x,l)) -> +#(x,sum(l)) The strictly oriented rules are moved into the weak component. ***** Step 4.a:1.b:1.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) -> +#(x,sum(l)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1,2} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [4] x1 + [1] p(+) = [9] p(0) = [5] p(cons) = [4] p(nil) = [1] p(prod) = [9] p(s) = [1] x1 + [0] p(sum) = [4] x1 + [8] p(*#) = [0] p(+#) = [0] p(prod#) = [0] p(sum#) = [8] p(c_1) = [1] p(c_2) = [0] p(c_3) = [8] x1 + [8] x2 + [0] p(c_4) = [0] p(c_5) = [8] p(c_6) = [1] p(c_7) = [1] x1 + [1] p(c_8) = [0] p(c_9) = [1] x1 + [2] x2 + [1] p(c_10) = [0] Following rules are strictly oriented: sum#(cons(x,l)) = [8] > [0] = +#(x,sum(l)) Following rules are (at-least) weakly oriented: *#(s(x),s(y)) = [0] >= [0] = c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) prod#(cons(x,l)) = [0] >= [0] = *#(x,prod(l)) prod#(cons(x,l)) = [0] >= [0] = prod#(l) sum#(cons(x,l)) = [8] >= [8] = sum#(l) ***** Step 4.a:1.b:1.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 4.a:1.b:1.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_2 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 2:W:prod#(cons(x,l)) -> *#(x,prod(l)) -->_1 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 3:W:prod#(cons(x,l)) -> prod#(l) -->_1 prod#(cons(x,l)) -> prod#(l):3 -->_1 prod#(cons(x,l)) -> *#(x,prod(l)):2 4:W:sum#(cons(x,l)) -> +#(x,sum(l)) 5:W:sum#(cons(x,l)) -> sum#(l) -->_1 sum#(cons(x,l)) -> sum#(l):5 -->_1 sum#(cons(x,l)) -> +#(x,sum(l)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: sum#(cons(x,l)) -> sum#(l) 4: sum#(cons(x,l)) -> +#(x,sum(l)) ***** Step 4.a:1.b:1.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:*#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_2 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 2:W:prod#(cons(x,l)) -> *#(x,prod(l)) -->_1 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):1 3:W:prod#(cons(x,l)) -> prod#(l) -->_1 prod#(cons(x,l)) -> prod#(l):3 -->_1 prod#(cons(x,l)) -> *#(x,prod(l)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: *#(s(x),s(y)) -> c_3(*#(x,y)) ***** Step 4.a:1.b:1.a:1.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(*#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) *#(s(x),s(y)) -> c_3(*#(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) ***** Step 4.a:1.b:1.a:1.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(*#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: *#(s(x),s(y)) -> c_3(*#(x,y)) The strictly oriented rules are moved into the weak component. ****** Step 4.a:1.b:1.a:1.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_3(*#(x,y)) - Weak DPs: prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [4] x1 + [0] p(+) = [0] p(0) = [1] p(cons) = [1] x1 + [1] x2 + [0] p(nil) = [0] p(prod) = [8] x1 + [2] p(s) = [1] x1 + [4] p(sum) = [0] p(*#) = [2] x1 + [0] p(+#) = [0] p(prod#) = [8] x1 + [0] p(sum#) = [0] p(c_1) = [0] p(c_2) = [2] p(c_3) = [1] x1 + [6] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [1] p(c_7) = [2] x1 + [1] x2 + [1] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] Following rules are strictly oriented: *#(s(x),s(y)) = [2] x + [8] > [2] x + [6] = c_3(*#(x,y)) Following rules are (at-least) weakly oriented: prod#(cons(x,l)) = [8] l + [8] x + [0] >= [2] x + [0] = *#(x,prod(l)) prod#(cons(x,l)) = [8] l + [8] x + [0] >= [8] l + [0] = prod#(l) ****** Step 4.a:1.b:1.a:1.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: *#(s(x),s(y)) -> c_3(*#(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 4.a:1.b:1.a:1.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: *#(s(x),s(y)) -> c_3(*#(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:*#(s(x),s(y)) -> c_3(*#(x,y)) -->_1 *#(s(x),s(y)) -> c_3(*#(x,y)):1 2:W:prod#(cons(x,l)) -> *#(x,prod(l)) -->_1 *#(s(x),s(y)) -> c_3(*#(x,y)):1 3:W:prod#(cons(x,l)) -> prod#(l) -->_1 prod#(cons(x,l)) -> prod#(l):3 -->_1 prod#(cons(x,l)) -> *#(x,prod(l)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: prod#(cons(x,l)) -> prod#(l) 2: prod#(cons(x,l)) -> *#(x,prod(l)) 1: *#(s(x),s(y)) -> c_3(*#(x,y)) ****** Step 4.a:1.b:1.a:1.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 4.a:1.b:1.b:1: Failure MAYBE + Considered Problem: - Strict DPs: +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak DPs: *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(s(x),s(y)) -> c_6(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) -->_1 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):3 -->_2 prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)):1 2:S:sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):4 -->_2 sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)):2 3:W:*#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_6(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):4 -->_2 *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):3 4:W:+#(s(x),s(y)) -> c_6(+#(x,y)) -->_1 +#(s(x),s(y)) -> c_6(+#(x,y)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: *#(s(x),s(y)) -> c_3(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 4: +#(s(x),s(y)) -> c_6(+#(x,y)) ** Step 4.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_7(*#(x,prod(l)),prod#(l)):1 2:S:sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_9(+#(x,sum(l)),sum#(l)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: prod#(cons(x,l)) -> c_7(prod#(l)) sum#(cons(x,l)) -> c_9(sum#(l)) ** Step 4.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) sum#(cons(x,l)) -> c_9(sum#(l)) - Weak TRS: *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: prod#(cons(x,l)) -> c_7(prod#(l)) sum#(cons(x,l)) -> c_9(sum#(l)) ** Step 4.b:4: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0 ,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} Problem (S) - Strict DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0 ,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} *** Step 4.b:4.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(cons(x,l)) -> c_7(prod#(l)) -->_1 prod#(cons(x,l)) -> c_7(prod#(l)):1 2:W:sum#(cons(x,l)) -> c_9(sum#(l)) -->_1 sum#(cons(x,l)) -> c_9(sum#(l)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: sum#(cons(x,l)) -> c_9(sum#(l)) *** Step 4.b:4.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: prod#(cons(x,l)) -> c_7(prod#(l)) The strictly oriented rules are moved into the weak component. **** Step 4.b:4.a:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [4] x2 + [8] p(+) = [1] p(0) = [0] p(cons) = [1] x1 + [1] x2 + [4] p(nil) = [0] p(prod) = [4] p(s) = [0] p(sum) = [2] x1 + [1] p(*#) = [1] x1 + [2] p(+#) = [2] x1 + [8] p(prod#) = [4] x1 + [0] p(sum#) = [1] x1 + [2] p(c_1) = [0] p(c_2) = [1] p(c_3) = [2] x1 + [4] p(c_4) = [2] p(c_5) = [1] p(c_6) = [2] x1 + [0] p(c_7) = [1] x1 + [14] p(c_8) = [1] p(c_9) = [4] x1 + [2] p(c_10) = [1] Following rules are strictly oriented: prod#(cons(x,l)) = [4] l + [4] x + [16] > [4] l + [14] = c_7(prod#(l)) Following rules are (at-least) weakly oriented: **** Step 4.b:4.a:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 4.b:4.a:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:prod#(cons(x,l)) -> c_7(prod#(l)) -->_1 prod#(cons(x,l)) -> c_7(prod#(l)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: prod#(cons(x,l)) -> c_7(prod#(l)) **** Step 4.b:4.a:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 4.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_7(prod#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:sum#(cons(x,l)) -> c_9(sum#(l)) -->_1 sum#(cons(x,l)) -> c_9(sum#(l)):1 2:W:prod#(cons(x,l)) -> c_7(prod#(l)) -->_1 prod#(cons(x,l)) -> c_7(prod#(l)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: prod#(cons(x,l)) -> c_7(prod#(l)) *** Step 4.b:4.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: sum#(cons(x,l)) -> c_9(sum#(l)) The strictly oriented rules are moved into the weak component. **** Step 4.b:4.b:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_9) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [2] p(+) = [2] x1 + [1] x2 + [1] p(0) = [1] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [1] p(prod) = [1] x1 + [0] p(s) = [0] p(sum) = [1] x1 + [2] p(*#) = [2] p(+#) = [1] x1 + [0] p(prod#) = [1] p(sum#) = [2] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [8] p(c_5) = [4] p(c_6) = [4] x1 + [0] p(c_7) = [2] x1 + [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] Following rules are strictly oriented: sum#(cons(x,l)) = [2] l + [2] x + [4] > [2] l + [0] = c_9(sum#(l)) Following rules are (at-least) weakly oriented: **** Step 4.b:4.b:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 4.b:4.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sum#(cons(x,l)) -> c_9(sum#(l)) - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:sum#(cons(x,l)) -> c_9(sum#(l)) -->_1 sum#(cons(x,l)) -> c_9(sum#(l)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: sum#(cons(x,l)) -> c_9(sum#(l)) **** Step 4.b:4.b:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,prod/1,sum/1,*#/2,+#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/0,c_3/3,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). MAYBE