MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_10() sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_12() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_10() sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_12() - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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,3,5,7,10,12} by application of Pre({1,3,5,7,10,12}) = {2,4,6,8,9,11}. Here rules are labelled as follows: 1: *#(x,0()) -> c_1() 2: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 3: *#(0(),x) -> c_3() 4: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 5: +#(x,0()) -> c_5() 6: +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) 7: +#(0(),x) -> c_7() 8: +#(s(x),s(y)) -> c_8(+#(x,y)) 9: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) 10: prod#(nil()) -> c_10() 11: sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) 12: sum#(nil()) -> c_12() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(x,0()) -> c_1() *#(0(),x) -> c_3() +#(x,0()) -> c_5() +#(0(),x) -> c_7() prod#(nil()) -> c_10() sum#(nil()) -> c_12() - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(0(),x) -> c_3():8 -->_1 *#(0(),x) -> c_3():8 -->_2 *#(x,0()) -> c_1():7 -->_1 *#(x,0()) -> c_1():7 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 2:S:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_3 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_3 +#(0(),x) -> c_7():10 -->_1 +#(0(),x) -> c_7():10 -->_3 +#(x,0()) -> c_5():9 -->_1 +#(x,0()) -> c_5():9 -->_2 *#(0(),x) -> c_3():8 -->_2 *#(x,0()) -> c_1():7 -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 3:S:+#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) -->_2 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_2 +#(0(),x) -> c_7():10 -->_1 +#(0(),x) -> c_7():10 -->_2 +#(x,0()) -> c_5():9 -->_1 +#(x,0()) -> c_5():9 -->_2 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 4:S:+#(s(x),s(y)) -> c_8(+#(x,y)) -->_1 +#(0(),x) -> c_7():10 -->_1 +#(x,0()) -> c_5():9 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 5:S:prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) -->_2 prod#(nil()) -> c_10():11 -->_1 *#(0(),x) -> c_3():8 -->_1 *#(x,0()) -> c_1():7 -->_2 prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)):5 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 6:S:sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) -->_2 sum#(nil()) -> c_12():12 -->_1 +#(0(),x) -> c_7():10 -->_1 +#(x,0()) -> c_5():9 -->_2 sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)):6 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 7:W:*#(x,0()) -> c_1() 8:W:*#(0(),x) -> c_3() 9:W:+#(x,0()) -> c_5() 10:W:+#(0(),x) -> c_7() 11:W:prod#(nil()) -> c_10() 12:W:sum#(nil()) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: sum#(nil()) -> c_12() 11: prod#(nil()) -> c_10() 7: *#(x,0()) -> c_1() 8: *#(0(),x) -> c_3() 9: +#(x,0()) -> c_5() 10: +#(0(),x) -> c_7() * Step 4: Decompose MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0 ,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0 ,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) and a lower component *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(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_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(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_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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,2}, uargs(c_11) = {1,2} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [9] p(+) = [1] x1 + [3] p(0) = [12] p(cons) = [1] x1 + [1] x2 + [1] p(nil) = [1] p(prod) = [2] p(s) = [1] x1 + [1] p(sum) = [12] p(*#) = [4] x1 + [0] p(+#) = [0] p(prod#) = [6] x1 + [4] p(sum#) = [4] x1 + [8] p(c_1) = [1] p(c_2) = [1] x1 + [2] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [2] p(c_6) = [2] x1 + [1] x2 + [1] p(c_7) = [1] p(c_8) = [4] x1 + [8] p(c_9) = [1] x1 + [1] x2 + [2] p(c_10) = [2] p(c_11) = [2] x1 + [1] x2 + [4] p(c_12) = [1] Following rules are strictly oriented: prod#(cons(x,l)) = [6] l + [6] x + [10] > [6] l + [4] x + [6] = c_9(*#(x,prod(l)),prod#(l)) Following rules are (at-least) weakly oriented: sum#(cons(x,l)) = [4] l + [4] x + [12] >= [4] l + [12] = c_11(+#(x,sum(l)),sum#(l)) **** Step 4.a:1.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_11(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)):1 2:W:prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_9(*#(x,prod(l)),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_9(*#(x,prod(l)),prod#(l)) **** Step 4.a:1.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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:sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: sum#(cons(x,l)) -> c_11(sum#(l)) **** Step 4.a:1.a:1.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_11(sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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: sum#(cons(x,l)) -> c_11(sum#(l)) **** Step 4.a:1.a:1.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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_11(sum#(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: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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_11) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [2] x2 + [1] p(+) = [8] x1 + [4] x2 + [1] p(0) = [0] p(cons) = [1] x2 + [2] p(nil) = [0] p(prod) = [1] x1 + [0] p(s) = [1] p(sum) = [1] x1 + [2] p(*#) = [1] x1 + [4] p(+#) = [1] x1 + [1] x2 + [0] p(prod#) = [1] x1 + [2] p(sum#) = [8] x1 + [4] p(c_1) = [2] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [1] x2 + [2] p(c_5) = [1] p(c_6) = [2] x1 + [1] p(c_7) = [1] p(c_8) = [1] x1 + [1] p(c_9) = [1] x2 + [1] p(c_10) = [1] p(c_11) = [1] x1 + [14] p(c_12) = [0] Following rules are strictly oriented: sum#(cons(x,l)) = [8] l + [20] > [8] l + [18] = c_11(sum#(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: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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_11(sum#(l)) -->_1 sum#(cons(x,l)) -> c_11(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_11(sum#(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/1,c_12/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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(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() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(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 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) Further, following extension rules are added to the lower component. *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(y,z) *#(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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(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() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 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: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(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() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_2) = {1,2}, uargs(c_4) = {1,2} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [3] x1 + [1] x2 + [2] p(+) = [4] p(0) = [0] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [0] p(prod) = [4] p(s) = [1] x1 + [0] p(sum) = [4] p(*#) = [4] x1 + [0] p(+#) = [0] p(prod#) = [4] x1 + [1] p(sum#) = [0] p(c_1) = [1] p(c_2) = [1] x1 + [1] x2 + [4] p(c_3) = [4] p(c_4) = [4] x1 + [1] x2 + [0] p(c_5) = [0] p(c_6) = [1] x2 + [0] p(c_7) = [0] p(c_8) = [1] p(c_9) = [2] x1 + [0] p(c_10) = [2] p(c_11) = [4] x1 + [4] x2 + [0] p(c_12) = [1] Following rules are strictly oriented: *#(*(x,y),z) = [12] x + [4] y + [8] > [4] x + [4] y + [4] = c_2(*#(x,*(y,z)),*#(y,z)) Following rules are (at-least) weakly oriented: *#(s(x),s(y)) = [4] x + [0] >= [4] x + [0] = c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) prod#(cons(x,l)) = [4] l + [4] x + [9] >= [4] x + [0] = *#(x,prod(l)) prod#(cons(x,l)) = [4] l + [4] x + [9] >= [4] l + [1] = prod#(l) sum#(cons(x,l)) = [0] >= [0] = +#(x,sum(l)) sum#(cons(x,l)) = [0] >= [0] = 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_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) -> +#(x,sum(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) -> +#(x,sum(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 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.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) -> +#(x,sum(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_2) = {1,2}, uargs(c_4) = {1,2} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [2] x1 + [2] x2 + [2] p(+) = [4] p(0) = [1] p(cons) = [1] x1 + [1] x2 + [2] p(nil) = [3] p(prod) = [2] x1 + [2] p(s) = [1] x1 + [1] p(sum) = [2] p(*#) = [4] x1 + [0] p(+#) = [0] p(prod#) = [4] x1 + [0] p(sum#) = [6] x1 + [0] p(c_1) = [0] p(c_2) = [2] x1 + [2] x2 + [6] p(c_3) = [0] p(c_4) = [1] x1 + [1] x2 + [0] p(c_5) = [1] p(c_6) = [4] p(c_7) = [1] p(c_8) = [1] x1 + [1] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [4] p(c_12) = [2] Following rules are strictly oriented: *#(s(x),s(y)) = [4] x + [4] > [4] x + [0] = c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) sum#(cons(x,l)) = [6] l + [6] x + [12] > [0] = +#(x,sum(l)) Following rules are (at-least) weakly oriented: *#(*(x,y),z) = [8] x + [8] y + [8] >= [8] x + [8] y + [6] = c_2(*#(x,*(y,z)),*#(y,z)) prod#(cons(x,l)) = [4] l + [4] x + [8] >= [4] x + [0] = *#(x,prod(l)) prod#(cons(x,l)) = [4] l + [4] x + [8] >= [4] l + [0] = prod#(l) sum#(cons(x,l)) = [6] l + [6] x + [12] >= [6] l + [0] = sum#(l) ****** Step 4.a:1.b:1.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(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) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(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) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 2:W:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 3:W:prod#(cons(x,l)) -> *#(x,prod(l)) -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 4:W:prod#(cons(x,l)) -> prod#(l) -->_1 prod#(cons(x,l)) -> prod#(l):4 -->_1 prod#(cons(x,l)) -> *#(x,prod(l)):3 5:W:sum#(cons(x,l)) -> +#(x,sum(l)) 6:W:sum#(cons(x,l)) -> sum#(l) -->_1 sum#(cons(x,l)) -> sum#(l):6 -->_1 sum#(cons(x,l)) -> +#(x,sum(l)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: sum#(cons(x,l)) -> sum#(l) 5: sum#(cons(x,l)) -> +#(x,sum(l)) 4: prod#(cons(x,l)) -> prod#(l) 3: prod#(cons(x,l)) -> *#(x,prod(l)) 1: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 2: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) ****** Step 4.a:1.b:1.a:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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: +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(y,z) *#(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() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(l)) -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):4 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):3 -->_2 prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)):1 2:S:sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 -->_2 sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)):2 3:W:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):4 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):4 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):3 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):3 4:W:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_3 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):4 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):3 5:W:+#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) -->_2 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_2 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 6:W:+#(s(x),s(y)) -> c_8(+#(x,y)) -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 3: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 6: +#(s(x),s(y)) -> c_8(+#(x,y)) 5: +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) ** Step 4.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)) sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/2,c_10/0,c_11/2,c_12/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_9(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_9(*#(x,prod(l)),prod#(l)):1 2:S:sum#(cons(x,l)) -> c_11(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_11(+#(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_9(prod#(l)) sum#(cons(x,l)) -> c_11(sum#(l)) ** Step 4.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_9(prod#(l)) sum#(cons(x,l)) -> c_11(sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(prod#(l)) sum#(cons(x,l)) -> c_11(sum#(l)) ** Step 4.b:4: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_9(prod#(l)) sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0 ,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_9(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/2,c_3/0,c_4/3,c_5/0 ,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(prod#(l)) - Weak DPs: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(prod#(l)) -->_1 prod#(cons(x,l)) -> c_9(prod#(l)):1 2:W:sum#(cons(x,l)) -> c_11(sum#(l)) -->_1 sum#(cons(x,l)) -> c_11(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_11(sum#(l)) *** Step 4.b:4.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(cons(x,l)) -> c_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(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_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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] x1 + [2] p(+) = [8] p(0) = [0] p(cons) = [1] x1 + [1] x2 + [1] p(nil) = [0] p(prod) = [0] p(s) = [1] p(sum) = [1] x1 + [0] p(*#) = [4] x1 + [1] p(+#) = [1] x2 + [2] p(prod#) = [4] x1 + [0] p(sum#) = [1] x1 + [8] p(c_1) = [1] p(c_2) = [1] x1 + [1] x2 + [1] p(c_3) = [8] p(c_4) = [1] x2 + [1] x3 + [0] p(c_5) = [1] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [2] p(c_9) = [1] x1 + [2] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] Following rules are strictly oriented: prod#(cons(x,l)) = [4] l + [4] x + [4] > [4] l + [2] = c_9(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_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_9(prod#(l)) -->_1 prod#(cons(x,l)) -> c_9(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_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(sum#(l)) - Weak DPs: prod#(cons(x,l)) -> c_9(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(sum#(l)) -->_1 sum#(cons(x,l)) -> c_11(sum#(l)):1 2:W:prod#(cons(x,l)) -> c_9(prod#(l)) -->_1 prod#(cons(x,l)) -> c_9(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_9(prod#(l)) *** Step 4.b:4.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(cons(x,l)) -> c_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(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_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11) = {1} Following symbols are considered usable: {*#,+#,prod#,sum#} TcT has computed the following interpretation: p(*) = [8] x1 + [1] x2 + [2] p(+) = [1] x1 + [1] p(0) = [1] p(cons) = [1] x2 + [1] p(nil) = [1] p(prod) = [4] p(s) = [1] x1 + [1] p(sum) = [0] p(*#) = [1] x2 + [0] p(+#) = [2] x2 + [0] p(prod#) = [1] p(sum#) = [2] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [1] x2 + [0] p(c_3) = [0] p(c_4) = [1] x2 + [2] x3 + [2] p(c_5) = [0] p(c_6) = [8] x2 + [1] p(c_7) = [2] p(c_8) = [8] x1 + [8] p(c_9) = [4] p(c_10) = [2] p(c_11) = [1] x1 + [0] p(c_12) = [0] Following rules are strictly oriented: sum#(cons(x,l)) = [2] l + [2] > [2] l + [0] = c_11(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_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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_11(sum#(l)) -->_1 sum#(cons(x,l)) -> c_11(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_11(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/2,c_3/0,c_4/3,c_5/0,c_6/2 ,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/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