YES

Problem:
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 quot(0(),s(y)) -> 0()
 quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 low(n,nil()) -> nil()
 low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
 if_low(true(),n,add(m,x)) -> add(m,low(n,x))
 if_low(false(),n,add(m,x)) -> low(n,x)
 high(n,nil()) -> nil()
 high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
 if_high(true(),n,add(m,x)) -> high(n,x)
 if_high(false(),n,add(m,x)) -> add(m,high(n,x))
 quicksort(nil()) -> nil()
 quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   le#(s(x),s(y)) -> le#(x,y)
   app#(add(n,x),y) -> app#(x,y)
   low#(n,add(m,x)) -> le#(m,n)
   low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
   if_low#(true(),n,add(m,x)) -> low#(n,x)
   if_low#(false(),n,add(m,x)) -> low#(n,x)
   high#(n,add(m,x)) -> le#(m,n)
   high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
   if_high#(true(),n,add(m,x)) -> high#(n,x)
   if_high#(false(),n,add(m,x)) -> high#(n,x)
   quicksort#(add(n,x)) -> high#(n,x)
   quicksort#(add(n,x)) -> quicksort#(high(n,x))
   quicksort#(add(n,x)) -> low#(n,x)
   quicksort#(add(n,x)) -> quicksort#(low(n,x))
   quicksort#(add(n,x)) -> app#(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   low(n,nil()) -> nil()
   low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
   if_low(true(),n,add(m,x)) -> add(m,low(n,x))
   if_low(false(),n,add(m,x)) -> low(n,x)
   high(n,nil()) -> nil()
   high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
   if_high(true(),n,add(m,x)) -> high(n,x)
   if_high(false(),n,add(m,x)) -> add(m,high(n,x))
   quicksort(nil()) -> nil()
   quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
  TDG Processor:
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    le#(s(x),s(y)) -> le#(x,y)
    app#(add(n,x),y) -> app#(x,y)
    low#(n,add(m,x)) -> le#(m,n)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(true(),n,add(m,x)) -> low#(n,x)
    if_low#(false(),n,add(m,x)) -> low#(n,x)
    high#(n,add(m,x)) -> le#(m,n)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(true(),n,add(m,x)) -> high#(n,x)
    if_high#(false(),n,add(m,x)) -> high#(n,x)
    quicksort#(add(n,x)) -> high#(n,x)
    quicksort#(add(n,x)) -> quicksort#(high(n,x))
    quicksort#(add(n,x)) -> low#(n,x)
    quicksort#(add(n,x)) -> quicksort#(low(n,x))
    quicksort#(add(n,x)) -> app#(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
   TRS:
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    quot(0(),s(y)) -> 0()
    quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    low(n,nil()) -> nil()
    low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
    if_low(true(),n,add(m,x)) -> add(m,low(n,x))
    if_low(false(),n,add(m,x)) -> low(n,x)
    high(n,nil()) -> nil()
    high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
    if_high(true(),n,add(m,x)) -> high(n,x)
    if_high(false(),n,add(m,x)) -> add(m,high(n,x))
    quicksort(nil()) -> nil()
    quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
   graph:
    quicksort#(add(n,x)) -> quicksort#(high(n,x)) ->
    quicksort#(add(n,x)) -> app#(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    quicksort#(add(n,x)) -> quicksort#(high(n,x)) ->
    quicksort#(add(n,x)) -> quicksort#(low(n,x))
    quicksort#(add(n,x)) -> quicksort#(high(n,x)) ->
    quicksort#(add(n,x)) -> low#(n,x)
    quicksort#(add(n,x)) -> quicksort#(high(n,x)) ->
    quicksort#(add(n,x)) -> quicksort#(high(n,x))
    quicksort#(add(n,x)) -> quicksort#(high(n,x)) ->
    quicksort#(add(n,x)) -> high#(n,x)
    quicksort#(add(n,x)) -> quicksort#(low(n,x)) ->
    quicksort#(add(n,x)) -> app#(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    quicksort#(add(n,x)) -> quicksort#(low(n,x)) ->
    quicksort#(add(n,x)) -> quicksort#(low(n,x))
    quicksort#(add(n,x)) -> quicksort#(low(n,x)) ->
    quicksort#(add(n,x)) -> low#(n,x)
    quicksort#(add(n,x)) -> quicksort#(low(n,x)) ->
    quicksort#(add(n,x)) -> quicksort#(high(n,x))
    quicksort#(add(n,x)) -> quicksort#(low(n,x)) ->
    quicksort#(add(n,x)) -> high#(n,x)
    quicksort#(add(n,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    quicksort#(add(n,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> le#(m,n)
    quicksort#(add(n,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    quicksort#(add(n,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> le#(m,n)
    quicksort#(add(n,x)) -> app#(quicksort(low(n,x)),add(n,quicksort(high(n,x)))) ->
    app#(add(n,x),y) -> app#(x,y)
    if_high#(false(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(false(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> le#(m,n)
    if_high#(true(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    if_high#(true(),n,add(m,x)) -> high#(n,x) ->
    high#(n,add(m,x)) -> le#(m,n)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x)) ->
    if_high#(false(),n,add(m,x)) -> high#(n,x)
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x)) ->
    if_high#(true(),n,add(m,x)) -> high#(n,x)
    high#(n,add(m,x)) -> le#(m,n) ->
    le#(s(x),s(y)) -> le#(x,y)
    if_low#(false(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(false(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> le#(m,n)
    if_low#(true(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    if_low#(true(),n,add(m,x)) -> low#(n,x) ->
    low#(n,add(m,x)) -> le#(m,n)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x)) ->
    if_low#(false(),n,add(m,x)) -> low#(n,x)
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x)) ->
    if_low#(true(),n,add(m,x)) -> low#(n,x)
    low#(n,add(m,x)) -> le#(m,n) -> le#(s(x),s(y)) -> le#(x,y)
    app#(add(n,x),y) -> app#(x,y) -> app#(add(n,x),y) -> app#(x,y)
    le#(s(x),s(y)) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
   SCC Processor:
    #sccs: 7
    #rules: 12
    #arcs: 35/324
    DPs:
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Usable Rule Processor:
     DPs:
      quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
     TRS:
      minus(x,0()) -> x
      minus(s(x),s(y)) -> minus(x,y)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
      interpretation:
       [quot#](x0, x1) = 3x0 + -16,
       
       [s](x0) = 1x0 + -3,
       
       [minus](x0, x1) = x0 + -11,
       
       [0] = 8
      orientation:
       quot#(s(x),s(y)) = 4x + 0 >= 3x + -8 = quot#(minus(x,y),s(y))
       
       minus(x,0()) = x + -11 >= x = x
       
       minus(s(x),s(y)) = 1x + -3 >= x + -11 = minus(x,y)
      problem:
       DPs:
        
       TRS:
        minus(x,0()) -> x
        minus(s(x),s(y)) -> minus(x,y)
      Qed
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Subterm Criterion Processor:
     simple projection:
      pi(minus#) = 1
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       quicksort(nil()) -> nil()
       quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     Qed
    
    DPs:
     quicksort#(add(n,x)) -> quicksort#(high(n,x))
     quicksort#(add(n,x)) -> quicksort#(low(n,x))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Usable Rule Processor:
     DPs:
      quicksort#(add(n,x)) -> quicksort#(high(n,x))
      quicksort#(add(n,x)) -> quicksort#(low(n,x))
     TRS:
      high(n,nil()) -> nil()
      high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
      if_high(true(),n,add(m,x)) -> high(n,x)
      if_high(false(),n,add(m,x)) -> add(m,high(n,x))
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      low(n,nil()) -> nil()
      low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
      if_low(true(),n,add(m,x)) -> add(m,low(n,x))
      if_low(false(),n,add(m,x)) -> low(n,x)
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(s) = 0
       pi(le) = 1
       pi(true) = []
       pi(false) = []
       pi(nil) = []
       pi(add) = [1]
       pi(low) = 1
       pi(if_low) = 2
       pi(high) = 1
       pi(if_high) = 2
       pi(quicksort#) = [0]
      usable rules:
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
      weight function:
       w0 = 1
       w(quicksort#) = w(if_high) = w(if_low) = w(nil) = w(false) = w(
       true) = w(0) = 1
       w(high) = w(low) = w(add) = w(le) = w(s) = 0
      precedence:
       quicksort# ~ if_high ~ high ~ if_low ~ low ~ add ~ nil ~ false ~ true ~ le ~ s ~ 0
      problem:
       DPs:
        
       TRS:
        high(n,nil()) -> nil()
        high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
        if_high(true(),n,add(m,x)) -> high(n,x)
        if_high(false(),n,add(m,x)) -> add(m,high(n,x))
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        low(n,nil()) -> nil()
        low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
        if_low(true(),n,add(m,x)) -> add(m,low(n,x))
        if_low(false(),n,add(m,x)) -> low(n,x)
      Qed
    
    DPs:
     app#(add(n,x),y) -> app#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       quicksort(nil()) -> nil()
       quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     Qed
    
    DPs:
     low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
     if_low#(true(),n,add(m,x)) -> low#(n,x)
     if_low#(false(),n,add(m,x)) -> low#(n,x)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Subterm Criterion Processor:
     simple projection:
      pi(low#) = 1
      pi(if_low#) = 2
     problem:
      DPs:
       low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       quicksort(nil()) -> nil()
       quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
     if_high#(true(),n,add(m,x)) -> high#(n,x)
     if_high#(false(),n,add(m,x)) -> high#(n,x)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Subterm Criterion Processor:
     simple projection:
      pi(high#) = 1
      pi(if_high#) = 2
     problem:
      DPs:
       high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       quicksort(nil()) -> nil()
       quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     low(n,nil()) -> nil()
     low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
     if_low(true(),n,add(m,x)) -> add(m,low(n,x))
     if_low(false(),n,add(m,x)) -> low(n,x)
     high(n,nil()) -> nil()
     high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
     if_high(true(),n,add(m,x)) -> high(n,x)
     if_high(false(),n,add(m,x)) -> add(m,high(n,x))
     quicksort(nil()) -> nil()
     quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       low(n,nil()) -> nil()
       low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
       if_low(true(),n,add(m,x)) -> add(m,low(n,x))
       if_low(false(),n,add(m,x)) -> low(n,x)
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       if_high(true(),n,add(m,x)) -> high(n,x)
       if_high(false(),n,add(m,x)) -> add(m,high(n,x))
       quicksort(nil()) -> nil()
       quicksort(add(n,x)) -> app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     Qed