MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(cons(N,L),Y) -> cons(N,app(L,Y)) app(nil(),Y) -> Y high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) high(N,nil()) -> nil() ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) iflow(false(),N,cons(M,L)) -> low(N,L) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) low(N,nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort(nil()) -> nil() - Signature: {app/2,high/2,ifhigh/3,iflow/3,le/2,low/2,quicksort/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {app,high,ifhigh,iflow,le,low ,quicksort} and constructors {0,cons,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(cons(N,L),Y) -> c_1(app#(L,Y)) app#(nil(),Y) -> c_2() high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) high#(N,nil()) -> c_4() ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) le#(0(),Y) -> c_9() le#(s(X),0()) -> c_10() le#(s(X),s(Y)) -> c_11(le#(X,Y)) low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) low#(N,nil()) -> c_13() quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) quicksort#(nil()) -> c_15() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(cons(N,L),Y) -> c_1(app#(L,Y)) app#(nil(),Y) -> c_2() high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) high#(N,nil()) -> c_4() ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) le#(0(),Y) -> c_9() le#(s(X),0()) -> c_10() le#(s(X),s(Y)) -> c_11(le#(X,Y)) low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) low#(N,nil()) -> c_13() quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) quicksort#(nil()) -> c_15() - Weak TRS: app(cons(N,L),Y) -> cons(N,app(L,Y)) app(nil(),Y) -> Y high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) high(N,nil()) -> nil() ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) iflow(false(),N,cons(M,L)) -> low(N,L) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) low(N,nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort(nil()) -> nil() - Signature: {app/2,high/2,ifhigh/3,iflow/3,le/2,low/2,quicksort/1,app#/2,high#/2,ifhigh#/3,iflow#/3,le#/2,low#/2 ,quicksort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/2,c_13/0,c_14/5,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,high#,ifhigh#,iflow#,le#,low# ,quicksort#} and constructors {0,cons,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,9,10,13,15} by application of Pre({2,4,9,10,13,15}) = {1,3,5,6,7,8,11,12,14}. Here rules are labelled as follows: 1: app#(cons(N,L),Y) -> c_1(app#(L,Y)) 2: app#(nil(),Y) -> c_2() 3: high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) 4: high#(N,nil()) -> c_4() 5: ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) 6: ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) 7: iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) 8: iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) 9: le#(0(),Y) -> c_9() 10: le#(s(X),0()) -> c_10() 11: le#(s(X),s(Y)) -> c_11(le#(X,Y)) 12: low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) 13: low#(N,nil()) -> c_13() 14: quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) 15: quicksort#(nil()) -> c_15() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(cons(N,L),Y) -> c_1(app#(L,Y)) high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) le#(s(X),s(Y)) -> c_11(le#(X,Y)) low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) - Weak DPs: app#(nil(),Y) -> c_2() high#(N,nil()) -> c_4() le#(0(),Y) -> c_9() le#(s(X),0()) -> c_10() low#(N,nil()) -> c_13() quicksort#(nil()) -> c_15() - Weak TRS: app(cons(N,L),Y) -> cons(N,app(L,Y)) app(nil(),Y) -> Y high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) high(N,nil()) -> nil() ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) iflow(false(),N,cons(M,L)) -> low(N,L) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) low(N,nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort(nil()) -> nil() - Signature: {app/2,high/2,ifhigh/3,iflow/3,le/2,low/2,quicksort/1,app#/2,high#/2,ifhigh#/3,iflow#/3,le#/2,low#/2 ,quicksort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/2,c_13/0,c_14/5,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,high#,ifhigh#,iflow#,le#,low# ,quicksort#} and constructors {0,cons,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(cons(N,L),Y) -> c_1(app#(L,Y)) -->_1 app#(nil(),Y) -> c_2():10 -->_1 app#(cons(N,L),Y) -> c_1(app#(L,Y)):1 2:S:high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) -->_2 le#(s(X),s(Y)) -> c_11(le#(X,Y)):7 -->_1 ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)):4 -->_1 ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)):3 -->_2 le#(s(X),0()) -> c_10():13 -->_2 le#(0(),Y) -> c_9():12 3:S:ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) -->_1 high#(N,nil()) -> c_4():11 -->_1 high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)):2 4:S:ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) -->_1 high#(N,nil()) -> c_4():11 -->_1 high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)):2 5:S:iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) -->_1 low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)):8 -->_1 low#(N,nil()) -> c_13():14 6:S:iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) -->_1 low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)):8 -->_1 low#(N,nil()) -> c_13():14 7:S:le#(s(X),s(Y)) -> c_11(le#(X,Y)) -->_1 le#(s(X),0()) -> c_10():13 -->_1 le#(0(),Y) -> c_9():12 -->_1 le#(s(X),s(Y)) -> c_11(le#(X,Y)):7 8:S:low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) -->_2 le#(s(X),0()) -> c_10():13 -->_2 le#(0(),Y) -> c_9():12 -->_2 le#(s(X),s(Y)) -> c_11(le#(X,Y)):7 -->_1 iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)):6 -->_1 iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)):5 9:S:quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) -->_4 quicksort#(nil()) -> c_15():15 -->_2 quicksort#(nil()) -> c_15():15 -->_3 low#(N,nil()) -> c_13():14 -->_5 high#(N,nil()) -> c_4():11 -->_1 app#(nil(),Y) -> c_2():10 -->_4 quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)):9 -->_2 quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)):9 -->_3 low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)):8 -->_5 high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)):2 -->_1 app#(cons(N,L),Y) -> c_1(app#(L,Y)):1 10:W:app#(nil(),Y) -> c_2() 11:W:high#(N,nil()) -> c_4() 12:W:le#(0(),Y) -> c_9() 13:W:le#(s(X),0()) -> c_10() 14:W:low#(N,nil()) -> c_13() 15:W:quicksort#(nil()) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 15: quicksort#(nil()) -> c_15() 14: low#(N,nil()) -> c_13() 11: high#(N,nil()) -> c_4() 12: le#(0(),Y) -> c_9() 13: le#(s(X),0()) -> c_10() 10: app#(nil(),Y) -> c_2() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: app#(cons(N,L),Y) -> c_1(app#(L,Y)) high#(N,cons(M,L)) -> c_3(ifhigh#(le(M,N),N,cons(M,L)),le#(M,N)) ifhigh#(false(),N,cons(M,L)) -> c_5(high#(N,L)) ifhigh#(true(),N,cons(M,L)) -> c_6(high#(N,L)) iflow#(false(),N,cons(M,L)) -> c_7(low#(N,L)) iflow#(true(),N,cons(M,L)) -> c_8(low#(N,L)) le#(s(X),s(Y)) -> c_11(le#(X,Y)) low#(N,cons(M,L)) -> c_12(iflow#(le(M,N),N,cons(M,L)),le#(M,N)) quicksort#(cons(N,L)) -> c_14(app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ,quicksort#(low(N,L)) ,low#(N,L) ,quicksort#(high(N,L)) ,high#(N,L)) - Weak TRS: app(cons(N,L),Y) -> cons(N,app(L,Y)) app(nil(),Y) -> Y high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) high(N,nil()) -> nil() ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) iflow(false(),N,cons(M,L)) -> low(N,L) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) low(N,nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort(nil()) -> nil() - Signature: {app/2,high/2,ifhigh/3,iflow/3,le/2,low/2,quicksort/1,app#/2,high#/2,ifhigh#/3,iflow#/3,le#/2,low#/2 ,quicksort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/2,c_13/0,c_14/5,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,high#,ifhigh#,iflow#,le#,low# ,quicksort#} and constructors {0,cons,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE