MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y head(add(n,x)) -> n high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) high(n,nil()) -> nil() if_high(false(),n,add(m,x)) -> add(m,high(n,x)) if_high(true(),n,add(m,x)) -> high(n,x) if_low(false(),n,add(m,x)) -> low(n,x) if_low(true(),n,add(m,x)) -> add(m,low(n,x)) if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) if_qs(true(),x,n,y) -> nil() isempty(add(n,x)) -> false() isempty(nil()) -> true() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) low(n,nil()) -> nil() quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) tail(add(n,x)) -> x - Signature: {app/2,head/1,high/2,if_high/3,if_low/3,if_qs/4,isempty/1,le/2,low/2,quicksort/1,tail/1} / {0/0,add/2 ,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {app,head,high,if_high,if_low,if_qs,isempty,le,low ,quicksort,tail} and constructors {0,add,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() head#(add(n,x)) -> c_3() high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) high#(n,nil()) -> c_5() if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) if_qs#(true(),x,n,y) -> c_11() isempty#(add(n,x)) -> c_12() isempty#(nil()) -> c_13() le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) low#(n,nil()) -> c_18() quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) tail#(add(n,x)) -> c_20() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() head#(add(n,x)) -> c_3() high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) high#(n,nil()) -> c_5() if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) if_qs#(true(),x,n,y) -> c_11() isempty#(add(n,x)) -> c_12() isempty#(nil()) -> c_13() le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) low#(n,nil()) -> c_18() quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) tail#(add(n,x)) -> c_20() - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y head(add(n,x)) -> n high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) high(n,nil()) -> nil() if_high(false(),n,add(m,x)) -> add(m,high(n,x)) if_high(true(),n,add(m,x)) -> high(n,x) if_low(false(),n,add(m,x)) -> low(n,x) if_low(true(),n,add(m,x)) -> add(m,low(n,x)) if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) if_qs(true(),x,n,y) -> nil() isempty(add(n,x)) -> false() isempty(nil()) -> true() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) low(n,nil()) -> nil() quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) tail(add(n,x)) -> x - Signature: {app/2,head/1,high/2,if_high/3,if_low/3,if_qs/4,isempty/1,le/2,low/2,quicksort/1,tail/1,app#/2,head#/1 ,high#/2,if_high#/3,if_low#/3,if_qs#/4,isempty#/1,le#/2,low#/2,quicksort#/1,tail#/1} / {0/0,add/2,false/0 ,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/1,c_17/2,c_18/0,c_19/9,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,head#,high#,if_high#,if_low#,if_qs#,isempty#,le# ,low#,quicksort#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,5,11,12,13,14,15,18,20} by application of Pre({2,3,5,11,12,13,14,15,18,20}) = {1,4,6,7,8,9,10,16,17,19}. Here rules are labelled as follows: 1: app#(add(n,x),y) -> c_1(app#(x,y)) 2: app#(nil(),y) -> c_2() 3: head#(add(n,x)) -> c_3() 4: high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) 5: high#(n,nil()) -> c_5() 6: if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) 7: if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) 8: if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) 9: if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) 10: if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) 11: if_qs#(true(),x,n,y) -> c_11() 12: isempty#(add(n,x)) -> c_12() 13: isempty#(nil()) -> c_13() 14: le#(0(),y) -> c_14() 15: le#(s(x),0()) -> c_15() 16: le#(s(x),s(y)) -> c_16(le#(x,y)) 17: low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) 18: low#(n,nil()) -> c_18() 19: quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) 20: tail#(add(n,x)) -> c_20() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) le#(s(x),s(y)) -> c_16(le#(x,y)) low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) - Weak DPs: app#(nil(),y) -> c_2() head#(add(n,x)) -> c_3() high#(n,nil()) -> c_5() if_qs#(true(),x,n,y) -> c_11() isempty#(add(n,x)) -> c_12() isempty#(nil()) -> c_13() le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() low#(n,nil()) -> c_18() tail#(add(n,x)) -> c_20() - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y head(add(n,x)) -> n high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) high(n,nil()) -> nil() if_high(false(),n,add(m,x)) -> add(m,high(n,x)) if_high(true(),n,add(m,x)) -> high(n,x) if_low(false(),n,add(m,x)) -> low(n,x) if_low(true(),n,add(m,x)) -> add(m,low(n,x)) if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) if_qs(true(),x,n,y) -> nil() isempty(add(n,x)) -> false() isempty(nil()) -> true() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) low(n,nil()) -> nil() quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) tail(add(n,x)) -> x - Signature: {app/2,head/1,high/2,if_high/3,if_low/3,if_qs/4,isempty/1,le/2,low/2,quicksort/1,tail/1,app#/2,head#/1 ,high#/2,if_high#/3,if_low#/3,if_qs#/4,isempty#/1,le#/2,low#/2,quicksort#/1,tail#/1} / {0/0,add/2,false/0 ,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/1,c_17/2,c_18/0,c_19/9,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,head#,high#,if_high#,if_low#,if_qs#,isempty#,le# ,low#,quicksort#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(add(n,x),y) -> c_1(app#(x,y)) -->_1 app#(nil(),y) -> c_2():11 -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1 2:S:high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) -->_2 le#(s(x),s(y)) -> c_16(le#(x,y)):8 -->_1 if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)):4 -->_1 if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)):3 -->_2 le#(s(x),0()) -> c_15():18 -->_2 le#(0(),y) -> c_14():17 3:S:if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) -->_1 high#(n,nil()) -> c_5():13 -->_1 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 4:S:if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) -->_1 high#(n,nil()) -> c_5():13 -->_1 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 5:S:if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) -->_1 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 -->_1 low#(n,nil()) -> c_18():19 6:S:if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) -->_1 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 -->_1 low#(n,nil()) -> c_18():19 7:S:if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) -->_3 quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)):10 -->_2 quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)):10 -->_1 app#(nil(),y) -> c_2():11 -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1 8:S:le#(s(x),s(y)) -> c_16(le#(x,y)) -->_1 le#(s(x),0()) -> c_15():18 -->_1 le#(0(),y) -> c_14():17 -->_1 le#(s(x),s(y)) -> c_16(le#(x,y)):8 9:S:low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) -->_2 le#(s(x),0()) -> c_15():18 -->_2 le#(0(),y) -> c_14():17 -->_2 le#(s(x),s(y)) -> c_16(le#(x,y)):8 -->_1 if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)):6 -->_1 if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)):5 10:S:quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) -->_9 tail#(add(n,x)) -> c_20():20 -->_5 tail#(add(n,x)) -> c_20():20 -->_3 low#(n,nil()) -> c_18():19 -->_2 isempty#(nil()) -> c_13():16 -->_2 isempty#(add(n,x)) -> c_12():15 -->_1 if_qs#(true(),x,n,y) -> c_11():14 -->_7 high#(n,nil()) -> c_5():13 -->_8 head#(add(n,x)) -> c_3():12 -->_6 head#(add(n,x)) -> c_3():12 -->_4 head#(add(n,x)) -> c_3():12 -->_3 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 -->_1 if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)):7 -->_7 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 11:W:app#(nil(),y) -> c_2() 12:W:head#(add(n,x)) -> c_3() 13:W:high#(n,nil()) -> c_5() 14:W:if_qs#(true(),x,n,y) -> c_11() 15:W:isempty#(add(n,x)) -> c_12() 16:W:isempty#(nil()) -> c_13() 17:W:le#(0(),y) -> c_14() 18:W:le#(s(x),0()) -> c_15() 19:W:low#(n,nil()) -> c_18() 20:W:tail#(add(n,x)) -> c_20() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: head#(add(n,x)) -> c_3() 14: if_qs#(true(),x,n,y) -> c_11() 15: isempty#(add(n,x)) -> c_12() 16: isempty#(nil()) -> c_13() 20: tail#(add(n,x)) -> c_20() 19: low#(n,nil()) -> c_18() 13: high#(n,nil()) -> c_5() 17: le#(0(),y) -> c_14() 18: le#(s(x),0()) -> c_15() 11: app#(nil(),y) -> c_2() * Step 4: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) le#(s(x),s(y)) -> c_16(le#(x,y)) low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y head(add(n,x)) -> n high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) high(n,nil()) -> nil() if_high(false(),n,add(m,x)) -> add(m,high(n,x)) if_high(true(),n,add(m,x)) -> high(n,x) if_low(false(),n,add(m,x)) -> low(n,x) if_low(true(),n,add(m,x)) -> add(m,low(n,x)) if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) if_qs(true(),x,n,y) -> nil() isempty(add(n,x)) -> false() isempty(nil()) -> true() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) low(n,nil()) -> nil() quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) tail(add(n,x)) -> x - Signature: {app/2,head/1,high/2,if_high/3,if_low/3,if_qs/4,isempty/1,le/2,low/2,quicksort/1,tail/1,app#/2,head#/1 ,high#/2,if_high#/3,if_low#/3,if_qs#/4,isempty#/1,le#/2,low#/2,quicksort#/1,tail#/1} / {0/0,add/2,false/0 ,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/1,c_17/2,c_18/0,c_19/9,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,head#,high#,if_high#,if_low#,if_qs#,isempty#,le# ,low#,quicksort#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(add(n,x),y) -> c_1(app#(x,y)) -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1 2:S:high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) -->_2 le#(s(x),s(y)) -> c_16(le#(x,y)):8 -->_1 if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)):4 -->_1 if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)):3 3:S:if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) -->_1 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 4:S:if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) -->_1 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 5:S:if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) -->_1 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 6:S:if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) -->_1 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 7:S:if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) -->_3 quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)):10 -->_2 quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)):10 -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1 8:S:le#(s(x),s(y)) -> c_16(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_16(le#(x,y)):8 9:S:low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) -->_2 le#(s(x),s(y)) -> c_16(le#(x,y)):8 -->_1 if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)):6 -->_1 if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)):5 10:S:quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,isempty#(x) ,low#(head(x),tail(x)) ,head#(x) ,tail#(x) ,head#(x) ,high#(head(x),tail(x)) ,head#(x) ,tail#(x)) -->_3 low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)):9 -->_1 if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)):7 -->_7 high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,low#(head(x),tail(x)) ,high#(head(x),tail(x))) * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) high#(n,add(m,x)) -> c_4(if_high#(le(m,n),n,add(m,x)),le#(m,n)) if_high#(false(),n,add(m,x)) -> c_6(high#(n,x)) if_high#(true(),n,add(m,x)) -> c_7(high#(n,x)) if_low#(false(),n,add(m,x)) -> c_8(low#(n,x)) if_low#(true(),n,add(m,x)) -> c_9(low#(n,x)) if_qs#(false(),x,n,y) -> c_10(app#(quicksort(x),add(n,quicksort(y))),quicksort#(x),quicksort#(y)) le#(s(x),s(y)) -> c_16(le#(x,y)) low#(n,add(m,x)) -> c_17(if_low#(le(m,n),n,add(m,x)),le#(m,n)) quicksort#(x) -> c_19(if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ,low#(head(x),tail(x)) ,high#(head(x),tail(x))) - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y head(add(n,x)) -> n high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x)) high(n,nil()) -> nil() if_high(false(),n,add(m,x)) -> add(m,high(n,x)) if_high(true(),n,add(m,x)) -> high(n,x) if_low(false(),n,add(m,x)) -> low(n,x) if_low(true(),n,add(m,x)) -> add(m,low(n,x)) if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y))) if_qs(true(),x,n,y) -> nil() isempty(add(n,x)) -> false() isempty(nil()) -> true() le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x)) low(n,nil()) -> nil() quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) tail(add(n,x)) -> x - Signature: {app/2,head/1,high/2,if_high/3,if_low/3,if_qs/4,isempty/1,le/2,low/2,quicksort/1,tail/1,app#/2,head#/1 ,high#/2,if_high#/3,if_low#/3,if_qs#/4,isempty#/1,le#/2,low#/2,quicksort#/1,tail#/1} / {0/0,add/2,false/0 ,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/1,c_17/2,c_18/0,c_19/3,c_20/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,head#,high#,if_high#,if_low#,if_qs#,isempty#,le# ,low#,quicksort#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE