MAYBE Problem: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Proof: DP Processor: DPs: le#(s(X),s(Y)) -> le#(X,Y) app#(cons(N,L),Y) -> app#(L,Y) low#(N,cons(M,L)) -> le#(M,N) low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) iflow#(true(),N,cons(M,L)) -> low#(N,L) iflow#(false(),N,cons(M,L)) -> low#(N,L) high#(N,cons(M,L)) -> le#(M,N) high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) quicksort#(cons(N,L)) -> high#(N,L) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> low#(N,L) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) CDG Processor: DPs: le#(s(X),s(Y)) -> le#(X,Y) app#(cons(N,L),Y) -> app#(L,Y) low#(N,cons(M,L)) -> le#(M,N) low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) iflow#(true(),N,cons(M,L)) -> low#(N,L) iflow#(false(),N,cons(M,L)) -> low#(N,L) high#(N,cons(M,L)) -> le#(M,N) high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) quicksort#(cons(N,L)) -> high#(N,L) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> low#(N,L) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) graph: quicksort#(cons(N,L)) -> quicksort#(high(N,L)) -> quicksort#(cons(N,L)) -> high#(N,L) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) -> quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) -> quicksort#(cons(N,L)) -> low#(N,L) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) -> quicksort#(cons(N,L)) -> quicksort#(low(N,L)) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) -> quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) -> quicksort#(cons(N,L)) -> high#(N,L) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) -> quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) -> quicksort#(cons(N,L)) -> low#(N,L) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) -> quicksort#(cons(N,L)) -> quicksort#(low(N,L)) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) -> quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) quicksort#(cons(N,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> le#(M,N) quicksort#(cons(N,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) quicksort#(cons(N,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> le#(M,N) quicksort#(cons(N,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) -> app#(cons(N,L),Y) -> app#(L,Y) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> le#(M,N) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> le#(M,N) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) -> high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) -> ifhigh#(true(),N,cons(M,L)) -> high#(N,L) high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) -> ifhigh#(false(),N,cons(M,L)) -> high#(N,L) high#(N,cons(M,L)) -> le#(M,N) -> le#(s(X),s(Y)) -> le#(X,Y) iflow#(false(),N,cons(M,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> le#(M,N) iflow#(false(),N,cons(M,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) iflow#(true(),N,cons(M,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> le#(M,N) iflow#(true(),N,cons(M,L)) -> low#(N,L) -> low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) -> iflow#(true(),N,cons(M,L)) -> low#(N,L) low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) -> iflow#(false(),N,cons(M,L)) -> low#(N,L) low#(N,cons(M,L)) -> le#(M,N) -> le#(s(X),s(Y)) -> le#(X,Y) app#(cons(N,L),Y) -> app#(L,Y) -> app#(cons(N,L),Y) -> app#(L,Y) le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y) Restore Modifier: DPs: le#(s(X),s(Y)) -> le#(X,Y) app#(cons(N,L),Y) -> app#(L,Y) low#(N,cons(M,L)) -> le#(M,N) low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) iflow#(true(),N,cons(M,L)) -> low#(N,L) iflow#(false(),N,cons(M,L)) -> low#(N,L) high#(N,cons(M,L)) -> le#(M,N) high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) quicksort#(cons(N,L)) -> high#(N,L) quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> low#(N,L) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) SCC Processor: #sccs: 5 #rules: 10 #arcs: 31/225 DPs: quicksort#(cons(N,L)) -> quicksort#(high(N,L)) quicksort#(cons(N,L)) -> quicksort#(low(N,L)) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Open DPs: high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ifhigh#(false(),N,cons(M,L)) -> high#(N,L) ifhigh#(true(),N,cons(M,L)) -> high#(N,L) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Open DPs: low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) iflow#(false(),N,cons(M,L)) -> low#(N,L) iflow#(true(),N,cons(M,L)) -> low#(N,L) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Open DPs: le#(s(X),s(Y)) -> le#(X,Y) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Matrix Interpretation Processor: dimension: 1 interpretation: [le#](x0, x1) = x0 + 1, [quicksort](x0) = 0, [ifhigh](x0, x1, x2) = 0, [high](x0, x1) = 0, [iflow](x0, x1, x2) = 0, [low](x0, x1) = 0, [cons](x0, x1) = x1, [app](x0, x1) = x1, [nil] = 0, [false] = 0, [s](x0) = x0 + 1, [true] = 0, [le](x0, x1) = 0, [0] = 0 orientation: le#(s(X),s(Y)) = X + 2 >= X + 1 = le#(X,Y) le(0(),Y) = 0 >= 0 = true() le(s(X),0()) = 0 >= 0 = false() le(s(X),s(Y)) = 0 >= 0 = le(X,Y) app(nil(),Y) = Y >= Y = Y app(cons(N,L),Y) = Y >= Y = cons(N,app(L,Y)) low(N,nil()) = 0 >= 0 = nil() low(N,cons(M,L)) = 0 >= 0 = iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) = 0 >= 0 = cons(M,low(N,L)) iflow(false(),N,cons(M,L)) = 0 >= 0 = low(N,L) high(N,nil()) = 0 >= 0 = nil() high(N,cons(M,L)) = 0 >= 0 = ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) = 0 >= 0 = high(N,L) ifhigh(false(),N,cons(M,L)) = 0 >= 0 = cons(M,high(N,L)) quicksort(nil()) = 0 >= 0 = nil() quicksort(cons(N,L)) = 0 >= 0 = app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) problem: DPs: TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Qed DPs: app#(cons(N,L),Y) -> app#(L,Y) TRS: le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) app(nil(),Y) -> Y app(cons(N,L),Y) -> cons(N,app(L,Y)) low(N,nil()) -> nil() low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) iflow(true(),N,cons(M,L)) -> cons(M,low(N,L)) iflow(false(),N,cons(M,L)) -> low(N,L) high(N,nil()) -> nil() high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) ifhigh(true(),N,cons(M,L)) -> high(N,L) ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L)) quicksort(nil()) -> nil() quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Open