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))))
  TDG 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)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(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)) -> low#(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)) -> high#(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)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> quicksort#(low(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#(high(N,L))
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> high#(N,L)
    quicksort#(cons(N,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
    quicksort#(cons(N,L)) -> high#(N,L) ->
    high#(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)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> le#(M,N)
    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)) -> 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)
    ifhigh#(true(),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)
    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)) -> 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) ->
    le#(s(X),s(Y)) -> le#(X,Y)
    iflow#(false(),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)
    iflow#(true(),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)
    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)) -> 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) -> 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:
      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
     
     DPs:
      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)
     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#(true(),N,cons(M,L)) -> high#(N,L)
      ifhigh#(false(),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:
      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