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