WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) avg(xs) -> quot(hd(sum(xs)),length(xs)) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1} / {0/0,:/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {+,++,-,avg,hd,length,quot,sum} and constructors {0,:,nil ,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs +#(0(),y) -> c_1() +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) ++#(nil(),ys) -> c_4() -#(x,0()) -> c_5() -#(0(),s(y)) -> c_6() -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) hd#(:(x,xs)) -> c_9() length#(:(x,xs)) -> c_10(length#(xs)) length#(nil()) -> c_11() quot#(0(),s(y)) -> c_12() quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) sum#(:(x,nil())) -> c_16() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: +#(0(),y) -> c_1() +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) ++#(nil(),ys) -> c_4() -#(x,0()) -> c_5() -#(0(),s(y)) -> c_6() -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) hd#(:(x,xs)) -> c_9() length#(:(x,xs)) -> c_10(length#(xs)) length#(nil()) -> c_11() quot#(0(),s(y)) -> c_12() quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) sum#(:(x,nil())) -> c_16() - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) avg(xs) -> quot(hd(sum(xs)),length(xs)) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,5,6,9,11,12,16} by application of Pre({1,4,5,6,9,11,12,16}) = {2,3,7,8,10,13,14,15}. Here rules are labelled as follows: 1: +#(0(),y) -> c_1() 2: +#(s(x),y) -> c_2(+#(x,y)) 3: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) 4: ++#(nil(),ys) -> c_4() 5: -#(x,0()) -> c_5() 6: -#(0(),s(y)) -> c_6() 7: -#(s(x),s(y)) -> c_7(-#(x,y)) 8: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) 9: hd#(:(x,xs)) -> c_9() 10: length#(:(x,xs)) -> c_10(length#(xs)) 11: length#(nil()) -> c_11() 12: quot#(0(),s(y)) -> c_12() 13: quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) 14: sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) 15: sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) 16: sum#(:(x,nil())) -> c_16() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak DPs: +#(0(),y) -> c_1() ++#(nil(),ys) -> c_4() -#(x,0()) -> c_5() -#(0(),s(y)) -> c_6() hd#(:(x,xs)) -> c_9() length#(nil()) -> c_11() quot#(0(),s(y)) -> c_12() sum#(:(x,nil())) -> c_16() - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) avg(xs) -> quot(hd(sum(xs)),length(xs)) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:+#(s(x),y) -> c_2(+#(x,y)) -->_1 +#(0(),y) -> c_1():9 -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 2:S:++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -->_1 ++#(nil(),ys) -> c_4():10 -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):2 3:S:-#(s(x),s(y)) -> c_7(-#(x,y)) -->_1 -#(0(),s(y)) -> c_6():12 -->_1 -#(x,0()) -> c_5():11 -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):3 4:S:avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) -->_3 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_3 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):7 -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):6 -->_4 length#(:(x,xs)) -> c_10(length#(xs)):5 -->_3 sum#(:(x,nil())) -> c_16():16 -->_1 quot#(0(),s(y)) -> c_12():15 -->_4 length#(nil()) -> c_11():14 -->_2 hd#(:(x,xs)) -> c_9():13 5:S:length#(:(x,xs)) -> c_10(length#(xs)) -->_1 length#(nil()) -> c_11():14 -->_1 length#(:(x,xs)) -> c_10(length#(xs)):5 6:S:quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) -->_1 quot#(0(),s(y)) -> c_12():15 -->_2 -#(0(),s(y)) -> c_6():12 -->_2 -#(x,0()) -> c_5():11 -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):6 -->_2 -#(s(x),s(y)) -> c_7(-#(x,y)):3 7:S:sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) -->_3 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_1 sum#(:(x,nil())) -> c_16():16 -->_2 ++#(nil(),ys) -> c_4():10 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):7 -->_2 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):2 8:S:sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) -->_1 sum#(:(x,nil())) -> c_16():16 -->_2 +#(0(),y) -> c_1():9 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_2 +#(s(x),y) -> c_2(+#(x,y)):1 9:W:+#(0(),y) -> c_1() 10:W:++#(nil(),ys) -> c_4() 11:W:-#(x,0()) -> c_5() 12:W:-#(0(),s(y)) -> c_6() 13:W:hd#(:(x,xs)) -> c_9() 14:W:length#(nil()) -> c_11() 15:W:quot#(0(),s(y)) -> c_12() 16:W:sum#(:(x,nil())) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: hd#(:(x,xs)) -> c_9() 14: length#(nil()) -> c_11() 15: quot#(0(),s(y)) -> c_12() 16: sum#(:(x,nil())) -> c_16() 11: -#(x,0()) -> c_5() 12: -#(0(),s(y)) -> c_6() 10: ++#(nil(),ys) -> c_4() 9: +#(0(),y) -> c_1() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) avg(xs) -> quot(hd(sum(xs)),length(xs)) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:+#(s(x),y) -> c_2(+#(x,y)) -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 2:S:++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):2 3:S:-#(s(x),s(y)) -> c_7(-#(x,y)) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):3 4:S:avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),hd#(sum(xs)),sum#(xs),length#(xs)) -->_3 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_3 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):7 -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):6 -->_4 length#(:(x,xs)) -> c_10(length#(xs)):5 5:S:length#(:(x,xs)) -> c_10(length#(xs)) -->_1 length#(:(x,xs)) -> c_10(length#(xs)):5 6:S:quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):6 -->_2 -#(s(x),s(y)) -> c_7(-#(x,y)):3 7:S:sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) -->_3 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):7 -->_2 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):2 8:S:sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):8 -->_2 +#(s(x),y) -> c_2(+#(x,y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) avg(xs) -> quot(hd(sum(xs)),length(xs)) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) and a lower component +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) Further, following extension rules are added to the lower component. avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) -->_2 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):4 -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):3 -->_3 length#(:(x,xs)) -> c_10(length#(xs)):2 2:S:length#(:(x,xs)) -> c_10(length#(xs)) -->_1 length#(:(x,xs)) -> c_10(length#(xs)):2 3:S:quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)) -->_1 quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y)),-#(x,y)):3 4:S:sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys))))) ,++#(xs,sum(:(x,:(y,ys)))) ,sum#(:(x,:(y,ys)))):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) ** Step 6.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_8) = {1,2,3}, uargs(c_10) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x2 + [0] p(++) = [1] x1 + [1] x2 + [0] p(-) = [1] x1 + [1] p(0) = [0] p(:) = [1] x1 + [1] x2 + [5] p(avg) = [0] p(hd) = [1] x1 + [7] p(length) = [1] p(nil) = [6] p(quot) = [0] p(s) = [1] x1 + [0] p(sum) = [1] x1 + [0] p(+#) = [2] x2 + [0] p(++#) = [4] x1 + [1] x2 + [0] p(-#) = [4] x1 + [1] x2 + [0] p(avg#) = [5] x1 + [4] p(hd#) = [2] x1 + [1] p(length#) = [1] x1 + [3] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [2] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_9) = [0] p(c_10) = [1] x1 + [3] p(c_11) = [2] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [1] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [1] Following rules are strictly oriented: length#(:(x,xs)) = [1] x + [1] xs + [8] > [1] xs + [6] = c_10(length#(xs)) Following rules are (at-least) weakly oriented: avg#(xs) = [5] xs + [4] >= [3] xs + [13] = c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [1] = c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) = [1] x + [1] xs + [1] y + [1] ys + [12] >= [1] x + [1] xs + [1] y + [1] ys + [13] = c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) +(0(),y) = [1] y + [0] >= [1] y + [0] = y +(s(x),y) = [1] y + [0] >= [1] y + [0] = s(+(x,y)) ++(:(x,xs),ys) = [1] x + [1] xs + [1] ys + [5] >= [1] x + [1] xs + [1] ys + [5] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [6] >= [1] ys + [0] = ys -(x,0()) = [1] x + [1] >= [1] x + [0] = x -(0(),s(y)) = [1] >= [0] = 0() -(s(x),s(y)) = [1] x + [1] >= [1] x + [1] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [12] >= [1] x + [0] = x length(:(x,xs)) = [1] >= [1] = s(length(xs)) length(nil()) = [1] >= [0] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [1] xs + [1] y + [1] ys + [10] >= [1] x + [1] xs + [1] y + [1] ys + [10] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [10] >= [1] xs + [1] y + [5] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [11] >= [1] x + [11] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) - Weak DPs: length#(:(x,xs)) -> c_10(length#(xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_8) = {1,2,3}, uargs(c_10) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x2 + [0] p(++) = [2] x1 + [1] x2 + [0] p(-) = [1] x1 + [0] p(0) = [0] p(:) = [1] x1 + [1] x2 + [1] p(avg) = [0] p(hd) = [1] x1 + [0] p(length) = [1] p(nil) = [3] p(quot) = [0] p(s) = [1] x1 + [0] p(sum) = [1] x1 + [0] p(+#) = [0] p(++#) = [0] p(-#) = [2] x1 + [0] p(avg#) = [5] x1 + [7] p(hd#) = [1] p(length#) = [3] x1 + [4] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] x1 + [0] p(c_8) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [2] p(c_13) = [1] x1 + [3] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [2] p(c_16) = [1] Following rules are strictly oriented: avg#(xs) = [5] xs + [7] > [5] xs + [6] = c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) Following rules are (at-least) weakly oriented: length#(:(x,xs)) = [3] x + [3] xs + [7] >= [3] xs + [4] = c_10(length#(xs)) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [3] = c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) = [1] x + [2] xs + [1] y + [1] ys + [3] >= [1] x + [2] xs + [1] y + [1] ys + [3] = c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) +(0(),y) = [1] y + [0] >= [1] y + [0] = y +(s(x),y) = [1] y + [0] >= [1] y + [0] = s(+(x,y)) ++(:(x,xs),ys) = [2] x + [2] xs + [1] ys + [2] >= [1] x + [2] xs + [1] ys + [1] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [6] >= [1] ys + [0] = ys -(x,0()) = [1] x + [0] >= [1] x + [0] = x -(0(),s(y)) = [0] >= [0] = 0() -(s(x),s(y)) = [1] x + [0] >= [1] x + [0] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [1] >= [1] x + [0] = x length(:(x,xs)) = [1] >= [1] = s(length(xs)) length(nil()) = [1] >= [0] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [2] xs + [1] y + [1] ys + [2] >= [1] x + [2] xs + [1] y + [1] ys + [2] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [2] >= [1] xs + [1] y + [1] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [4] >= [1] x + [4] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) - Weak DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_8) = {1,2,3}, uargs(c_10) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x1 + [1] x2 + [2] p(++) = [1] x1 + [1] x2 + [1] p(-) = [1] x1 + [0] p(0) = [0] p(:) = [1] x1 + [1] x2 + [2] p(avg) = [0] p(hd) = [1] x1 + [0] p(length) = [1] x1 + [0] p(nil) = [3] p(quot) = [0] p(s) = [1] x1 + [1] p(sum) = [1] x1 + [0] p(+#) = [0] p(++#) = [0] p(-#) = [2] x1 + [1] x2 + [0] p(avg#) = [7] x1 + [7] p(hd#) = [1] x1 + [0] p(length#) = [4] x1 + [7] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_9) = [0] p(c_10) = [1] x1 + [1] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [0] Following rules are strictly oriented: quot#(s(x),s(y)) = [1] x + [1] y + [2] > [1] x + [1] y + [1] = c_13(quot#(-(x,y),s(y))) Following rules are (at-least) weakly oriented: avg#(xs) = [7] xs + [7] >= [7] xs + [7] = c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) = [4] x + [4] xs + [15] >= [4] xs + [8] = c_10(length#(xs)) sum#(++(xs,:(x,:(y,ys)))) = [1] x + [1] xs + [1] y + [1] ys + [5] >= [1] x + [1] xs + [1] y + [1] ys + [5] = c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) +(0(),y) = [1] y + [2] >= [1] y + [0] = y +(s(x),y) = [1] x + [1] y + [3] >= [1] x + [1] y + [3] = s(+(x,y)) ++(:(x,xs),ys) = [1] x + [1] xs + [1] ys + [3] >= [1] x + [1] xs + [1] ys + [3] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [4] >= [1] ys + [0] = ys -(x,0()) = [1] x + [0] >= [1] x + [0] = x -(0(),s(y)) = [0] >= [0] = 0() -(s(x),s(y)) = [1] x + [1] >= [1] x + [0] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [2] >= [1] x + [0] = x length(:(x,xs)) = [1] x + [1] xs + [2] >= [1] xs + [1] = s(length(xs)) length(nil()) = [3] >= [0] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [1] xs + [1] y + [1] ys + [5] >= [1] x + [1] xs + [1] y + [1] ys + [5] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [4] >= [1] x + [1] xs + [1] y + [4] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [5] >= [1] x + [5] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:5: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) - Weak DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_8) = {1,2,3}, uargs(c_10) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {++,sum,+#,++#,-#,avg#,hd#,length#,quot#,sum#} TcT has computed the following interpretation: p(+) = [0] p(++) = [1] x1 + [1] x2 + [1] p(-) = [0] p(0) = [1] p(:) = [1] x2 + [2] p(avg) = [4] x1 + [1] p(hd) = [0] p(length) = [0] p(nil) = [0] p(quot) = [0] p(s) = [1] x1 + [0] p(sum) = [3] p(+#) = [4] x1 + [0] p(++#) = [0] p(-#) = [4] x1 + [1] x2 + [0] p(avg#) = [6] x1 + [5] p(hd#) = [2] x1 + [1] p(length#) = [2] x1 + [0] p(quot#) = [0] p(sum#) = [2] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [2] x1 + [2] p(c_4) = [4] p(c_5) = [2] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [1] x2 + [2] x3 + [1] p(c_9) = [4] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [4] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] Following rules are strictly oriented: sum#(++(xs,:(x,:(y,ys)))) = [2] xs + [2] ys + [10] > [2] xs + [8] = c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) Following rules are (at-least) weakly oriented: avg#(xs) = [6] xs + [5] >= [6] xs + [1] = c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) = [2] xs + [4] >= [2] xs + [0] = c_10(length#(xs)) quot#(s(x),s(y)) = [0] >= [0] = c_13(quot#(-(x,y),s(y))) ++(:(x,xs),ys) = [1] xs + [1] ys + [3] >= [1] xs + [1] ys + [3] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [1] >= [1] ys + [0] = ys sum(++(xs,:(x,:(y,ys)))) = [3] >= [3] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [3] >= [3] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [3] >= [2] = :(x,nil()) ** Step 6.a:6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: avg#(xs) -> c_8(quot#(hd(sum(xs)),length(xs)),sum#(xs),length#(xs)) length#(:(x,xs)) -> c_10(length#(xs)) quot#(s(x),s(y)) -> c_13(quot#(-(x,y),s(y))) sum#(++(xs,:(x,:(y,ys)))) -> c_14(sum#(++(xs,sum(:(x,:(y,ys)))))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak DPs: avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) and a lower component +#(s(x),y) -> c_2(+#(x,y)) Further, following extension rules are added to the lower component. ++#(:(x,xs),ys) -> ++#(xs,ys) -#(s(x),s(y)) -> -#(x,y) avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) *** Step 6.b:1.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak DPs: avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 2:S:-#(s(x),s(y)) -> c_7(-#(x,y)) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 3:S:sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 4:W:avg#(xs) -> length#(xs) -->_1 length#(:(x,xs)) -> length#(xs):7 5:W:avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 6:W:avg#(xs) -> sum#(xs) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 7:W:length#(:(x,xs)) -> length#(xs) -->_1 length#(:(x,xs)) -> length#(xs):7 8:W:quot#(s(x),s(y)) -> -#(x,y) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 9:W:quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 10:W:sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 11:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 12:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: avg#(xs) -> length#(xs) 7: length#(:(x,xs)) -> length#(xs) *** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) - Weak DPs: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 2:S:-#(s(x),s(y)) -> c_7(-#(x,y)) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 3:S:sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 5:W:avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 6:W:avg#(xs) -> sum#(xs) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 8:W:quot#(s(x),s(y)) -> -#(x,y) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 9:W:quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 10:W:sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 11:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 12:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs)),+#(x,y)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) *** Step 6.b:1.a:3: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak DPs: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 2:S:-#(s(x),s(y)) -> c_7(-#(x,y)) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 3:S:sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))):3 4:W:avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):7 -->_1 quot#(s(x),s(y)) -> -#(x,y):6 5:W:avg#(xs) -> sum#(xs) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):10 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):9 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):8 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))):3 6:W:quot#(s(x),s(y)) -> -#(x,y) -->_1 -#(s(x),s(y)) -> c_7(-#(x,y)):2 7:W:quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):7 -->_1 quot#(s(x),s(y)) -> -#(x,y):6 8:W:sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -->_1 ++#(:(x,xs),ys) -> c_3(++#(xs,ys)):1 9:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):10 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):9 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):8 -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))):3 10:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -->_1 sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))):3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(5,avg#(xs) -> sum#(xs))] *** Step 6.b:1.a:4: RemoveInapplicable WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak DPs: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveInapplicable + Details: Only the nodes {1,2,3,4,7,6} are reachable from nodes {1,2,3,4,6,7} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. *** Step 6.b:1.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak DPs: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_3) = {1}, uargs(c_7) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x2 + [0] p(++) = [4] x1 + [1] x2 + [7] p(-) = [1] x1 + [0] p(0) = [0] p(:) = [1] x1 + [1] x2 + [1] p(avg) = [0] p(hd) = [1] x1 + [0] p(length) = [5] x1 + [0] p(nil) = [2] p(quot) = [0] p(s) = [1] x1 + [0] p(sum) = [1] x1 + [0] p(+#) = [0] p(++#) = [0] p(-#) = [1] x1 + [1] x2 + [0] p(avg#) = [6] x1 + [0] p(hd#) = [0] p(length#) = [0] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [2] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [2] p(c_15) = [1] x1 + [0] p(c_16) = [1] Following rules are strictly oriented: sum#(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [4] > [1] xs + [1] y + [3] = c_15(sum#(:(+(x,y),xs))) Following rules are (at-least) weakly oriented: ++#(:(x,xs),ys) = [0] >= [0] = c_3(++#(xs,ys)) -#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_7(-#(x,y)) avg#(xs) = [6] xs + [0] >= [6] xs + [0] = quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = -#(x,y) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = quot#(-(x,y),s(y)) +(0(),y) = [1] y + [0] >= [1] y + [0] = y +(s(x),y) = [1] y + [0] >= [1] y + [0] = s(+(x,y)) ++(:(x,xs),ys) = [4] x + [4] xs + [1] ys + [11] >= [1] x + [4] xs + [1] ys + [8] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [15] >= [1] ys + [0] = ys -(x,0()) = [1] x + [0] >= [1] x + [0] = x -(0(),s(y)) = [0] >= [0] = 0() -(s(x),s(y)) = [1] x + [0] >= [1] x + [0] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [1] >= [1] x + [0] = x length(:(x,xs)) = [5] x + [5] xs + [5] >= [5] xs + [0] = s(length(xs)) length(nil()) = [10] >= [0] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [4] xs + [1] y + [1] ys + [9] >= [1] x + [4] xs + [1] y + [1] ys + [9] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [2] >= [1] xs + [1] y + [1] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [3] >= [1] x + [3] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:6: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) - Weak DPs: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_3) = {1}, uargs(c_7) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x2 + [2] p(++) = [1] x1 + [1] x2 + [0] p(-) = [1] x1 + [0] p(0) = [0] p(:) = [1] x1 + [1] x2 + [3] p(avg) = [0] p(hd) = [1] x1 + [1] p(length) = [4] x1 + [3] p(nil) = [2] p(quot) = [0] p(s) = [1] x1 + [0] p(sum) = [1] x1 + [0] p(+#) = [2] x1 + [1] x2 + [2] p(++#) = [4] x1 + [3] p(-#) = [1] x1 + [0] p(avg#) = [6] x1 + [4] p(hd#) = [0] p(length#) = [0] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [4] p(c_1) = [2] p(c_2) = [0] p(c_3) = [1] x1 + [3] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [2] x1 + [1] x2 + [0] p(c_14) = [2] x1 + [2] x2 + [0] p(c_15) = [1] x1 + [1] p(c_16) = [0] Following rules are strictly oriented: ++#(:(x,xs),ys) = [4] x + [4] xs + [15] > [4] xs + [6] = c_3(++#(xs,ys)) Following rules are (at-least) weakly oriented: -#(s(x),s(y)) = [1] x + [0] >= [1] x + [0] = c_7(-#(x,y)) avg#(xs) = [6] xs + [4] >= [5] xs + [4] = quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [0] = -#(x,y) quot#(s(x),s(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = quot#(-(x,y),s(y)) sum#(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [10] >= [1] xs + [1] y + [10] = c_15(sum#(:(+(x,y),xs))) +(0(),y) = [1] y + [2] >= [1] y + [0] = y +(s(x),y) = [1] y + [2] >= [1] y + [2] = s(+(x,y)) ++(:(x,xs),ys) = [1] x + [1] xs + [1] ys + [3] >= [1] x + [1] xs + [1] ys + [3] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [2] >= [1] ys + [0] = ys -(x,0()) = [1] x + [0] >= [1] x + [0] = x -(0(),s(y)) = [0] >= [0] = 0() -(s(x),s(y)) = [1] x + [0] >= [1] x + [0] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [4] >= [1] x + [0] = x length(:(x,xs)) = [4] x + [4] xs + [15] >= [4] xs + [3] = s(length(xs)) length(nil()) = [11] >= [0] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [1] xs + [1] y + [1] ys + [6] >= [1] x + [1] xs + [1] y + [1] ys + [6] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [6] >= [1] xs + [1] y + [5] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [5] >= [1] x + [5] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:7: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: -#(s(x),s(y)) -> c_7(-#(x,y)) - Weak DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {2}, uargs(:) = {1,2}, uargs(hd) = {1}, uargs(s) = {1}, uargs(sum) = {1}, uargs(quot#) = {1,2}, uargs(sum#) = {1}, uargs(c_3) = {1}, uargs(c_7) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x1 + [1] x2 + [4] p(++) = [2] x1 + [1] x2 + [0] p(-) = [1] x1 + [0] p(0) = [3] p(:) = [1] x1 + [1] x2 + [4] p(avg) = [0] p(hd) = [1] x1 + [0] p(length) = [1] x1 + [3] p(nil) = [2] p(quot) = [2] x1 + [2] p(s) = [1] x1 + [1] p(sum) = [1] x1 + [0] p(+#) = [0] p(++#) = [1] x1 + [0] p(-#) = [1] x2 + [1] p(avg#) = [3] x1 + [5] p(hd#) = [1] p(length#) = [4] x1 + [0] p(quot#) = [1] x1 + [1] x2 + [0] p(sum#) = [1] x1 + [0] p(c_1) = [2] p(c_2) = [1] x1 + [1] p(c_3) = [1] x1 + [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [1] x2 + [1] x3 + [2] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [2] x2 + [1] p(c_14) = [4] x1 + [1] x2 + [4] x3 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [0] Following rules are strictly oriented: -#(s(x),s(y)) = [1] y + [2] > [1] y + [1] = c_7(-#(x,y)) Following rules are (at-least) weakly oriented: ++#(:(x,xs),ys) = [1] x + [1] xs + [4] >= [1] xs + [0] = c_3(++#(xs,ys)) avg#(xs) = [3] xs + [5] >= [2] xs + [3] = quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) = [1] x + [1] y + [2] >= [1] y + [1] = -#(x,y) quot#(s(x),s(y)) = [1] x + [1] y + [2] >= [1] x + [1] y + [1] = quot#(-(x,y),s(y)) sum#(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [8] >= [1] x + [1] xs + [1] y + [8] = c_15(sum#(:(+(x,y),xs))) +(0(),y) = [1] y + [7] >= [1] y + [0] = y +(s(x),y) = [1] x + [1] y + [5] >= [1] x + [1] y + [5] = s(+(x,y)) ++(:(x,xs),ys) = [2] x + [2] xs + [1] ys + [8] >= [1] x + [2] xs + [1] ys + [4] = :(x,++(xs,ys)) ++(nil(),ys) = [1] ys + [4] >= [1] ys + [0] = ys -(x,0()) = [1] x + [0] >= [1] x + [0] = x -(0(),s(y)) = [3] >= [3] = 0() -(s(x),s(y)) = [1] x + [1] >= [1] x + [0] = -(x,y) hd(:(x,xs)) = [1] x + [1] xs + [4] >= [1] x + [0] = x length(:(x,xs)) = [1] x + [1] xs + [7] >= [1] xs + [4] = s(length(xs)) length(nil()) = [5] >= [3] = 0() sum(++(xs,:(x,:(y,ys)))) = [1] x + [2] xs + [1] y + [1] ys + [8] >= [1] x + [2] xs + [1] y + [1] ys + [8] = sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [8] >= [1] x + [1] xs + [1] y + [8] = sum(:(+(x,y),xs)) sum(:(x,nil())) = [1] x + [6] >= [1] x + [6] = :(x,nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ++#(:(x,xs),ys) -> c_3(++#(xs,ys)) -#(s(x),s(y)) -> c_7(-#(x,y)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(:(x,:(y,xs))) -> c_15(sum#(:(+(x,y),xs))) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) - Weak DPs: ++#(:(x,xs),ys) -> ++#(xs,ys) -#(s(x),s(y)) -> -#(x,y) avg#(xs) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) avg#(xs) -> sum#(xs) length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:+#(s(x),y) -> c_2(+#(x,y)) -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 2:W:++#(:(x,xs),ys) -> ++#(xs,ys) -->_1 ++#(:(x,xs),ys) -> ++#(xs,ys):2 3:W:-#(s(x),s(y)) -> -#(x,y) -->_1 -#(s(x),s(y)) -> -#(x,y):3 4:W:avg#(xs) -> length#(xs) -->_1 length#(:(x,xs)) -> length#(xs):7 5:W:avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 6:W:avg#(xs) -> sum#(xs) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 7:W:length#(:(x,xs)) -> length#(xs) -->_1 length#(:(x,xs)) -> length#(xs):7 8:W:quot#(s(x),s(y)) -> -#(x,y) -->_1 -#(s(x),s(y)) -> -#(x,y):3 9:W:quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -->_1 quot#(s(x),s(y)) -> quot#(-(x,y),s(y)):9 -->_1 quot#(s(x),s(y)) -> -#(x,y):8 10:W:sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -->_1 ++#(:(x,xs),ys) -> ++#(xs,ys):2 11:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))):10 12:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 13:W:sum#(:(x,:(y,xs))) -> +#(x,y) -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 14:W:sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) 5: avg#(xs) -> quot#(hd(sum(xs)),length(xs)) 9: quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) 8: quot#(s(x),s(y)) -> -#(x,y) 4: avg#(xs) -> length#(xs) 7: length#(:(x,xs)) -> length#(xs) 3: -#(s(x),s(y)) -> -#(x,y) 2: ++#(:(x,xs),ys) -> ++#(xs,ys) *** Step 6.b:1.b:2: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) - Weak DPs: avg#(xs) -> sum#(xs) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:+#(s(x),y) -> c_2(+#(x,y)) -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 6:W:avg#(xs) -> sum#(xs) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 11:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))):12 -->_1 sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))):11 12:W:sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 13:W:sum#(:(x,:(y,xs))) -> +#(x,y) -->_1 +#(s(x),y) -> c_2(+#(x,y)):1 14:W:sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -->_1 sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)):14 -->_1 sum#(:(x,:(y,xs))) -> +#(x,y):13 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(6,avg#(xs) -> sum#(xs))] *** Step 6.b:1.b:3: RemoveInapplicable WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) - Weak DPs: sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: RemoveInapplicable + Details: Only the nodes {1,13,14} are reachable from nodes {1,13,14} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. *** Step 6.b:1.b:4: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) - Weak DPs: sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(:(x,xs),ys) -> :(x,++(xs,ys)) ++(nil(),ys) -> ys -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) hd(:(x,xs)) -> x length(:(x,xs)) -> s(length(xs)) length(nil()) -> 0() sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +#(s(x),y) -> c_2(+#(x,y)) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) *** Step 6.b:1.b:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(s(x),y) -> c_2(+#(x,y)) - Weak DPs: sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(:) = {1}, uargs(s) = {1}, uargs(sum#) = {1}, uargs(c_2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(+) = [1] x1 + [1] x2 + [0] p(++) = [2] x1 + [1] p(-) = [0] p(0) = [3] p(:) = [1] x1 + [1] x2 + [8] p(avg) = [0] p(hd) = [0] p(length) = [0] p(nil) = [0] p(quot) = [0] p(s) = [1] x1 + [4] p(sum) = [0] p(+#) = [1] x1 + [10] p(++#) = [0] p(-#) = [0] p(avg#) = [0] p(hd#) = [2] x1 + [0] p(length#) = [0] p(quot#) = [4] x2 + [0] p(sum#) = [1] x1 + [1] p(c_1) = [1] p(c_2) = [1] x1 + [2] p(c_3) = [2] x1 + [8] p(c_4) = [0] p(c_5) = [0] p(c_6) = [4] p(c_7) = [0] p(c_8) = [1] x1 + [1] x2 + [0] p(c_9) = [1] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] p(c_13) = [2] x1 + [1] x2 + [2] p(c_14) = [2] x2 + [1] x3 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] Following rules are strictly oriented: +#(s(x),y) = [1] x + [14] > [1] x + [12] = c_2(+#(x,y)) Following rules are (at-least) weakly oriented: sum#(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [17] >= [1] x + [10] = +#(x,y) sum#(:(x,:(y,xs))) = [1] x + [1] xs + [1] y + [17] >= [1] x + [1] xs + [1] y + [9] = sum#(:(+(x,y),xs)) +(0(),y) = [1] y + [3] >= [1] y + [0] = y +(s(x),y) = [1] x + [1] y + [4] >= [1] x + [1] y + [4] = s(+(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: +#(s(x),y) -> c_2(+#(x,y)) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) - Weak TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) - Signature: {+/2,++/2,-/2,avg/1,hd/1,length/1,quot/2,sum/1,+#/2,++#/2,-#/2,avg#/1,hd#/1,length#/1,quot#/2,sum#/1} / {0/0 ,:/2,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/3,c_9/0,c_10/1,c_11/0,c_12/0,c_13/2,c_14/3 ,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,++#,-#,avg#,hd#,length#,quot# ,sum#} and constructors {0,:,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))