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))))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [quot#](x0, x1) = 4x0,
      
      [quicksort](x0) = 5,
      
      [if_high](x0, x1, x2) = x0 + 4x2 + 0,
      
      [high](x0, x1) = 4x1,
      
      [if_low](x0, x1, x2) = x1 + x2,
      
      [low](x0, x1) = x0 + x1,
      
      [add](x0, x1) = x1 + 1,
      
      [app](x0, x1) = x0 + x1 + 0,
      
      [nil] = 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [le](x0, x1) = 0,
      
      [quot](x0, x1) = 1x0,
      
      [s](x0) = 2x0,
      
      [minus](x0, x1) = x0,
      
      [0] = 1
     orientation:
      quot#(s(x),s(y)) = 6x >= 4x = quot#(minus(x,y),s(y))
      
      minus(x,0()) = x >= x = x
      
      minus(s(x),s(y)) = 2x >= x = minus(x,y)
      
      quot(0(),s(y)) = 2 >= 1 = 0()
      
      quot(s(x),s(y)) = 3x >= 3x = s(quot(minus(x,y),s(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 + 1 >= y = y
      
      app(add(n,x),y) = x + y + 1 >= x + y + 1 = add(n,app(x,y))
      
      low(n,nil()) = n + 1 >= 1 = nil()
      
      low(n,add(m,x)) = n + x + 1 >= n + x + 1 = if_low(le(m,n),n,add(m,x))
      
      if_low(true(),n,add(m,x)) = n + x + 1 >= n + x + 1 = add(m,low(n,x))
      
      if_low(false(),n,add(m,x)) = n + x + 1 >= n + x = low(n,x)
      
      high(n,nil()) = 5 >= 1 = nil()
      
      high(n,add(m,x)) = 4x + 5 >= 4x + 5 = if_high(le(m,n),n,add(m,x))
      
      if_high(true(),n,add(m,x)) = 4x + 5 >= 4x = high(n,x)
      
      if_high(false(),n,add(m,x)) = 4x + 5 >= 4x + 1 = add(m,high(n,x))
      
      quicksort(nil()) = 5 >= 1 = nil()
      
      quicksort(add(n,x)) = 5 >= 5 = app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))
     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:
     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))))
    LPO Processor:
     argument filtering:
      pi(0) = []
      pi(minus) = 0
      pi(s) = [0]
      pi(quot) = 0
      pi(le) = 0
      pi(true) = []
      pi(false) = []
      pi(nil) = []
      pi(app) = [0,1]
      pi(add) = [1]
      pi(low) = 1
      pi(if_low) = 2
      pi(high) = 1
      pi(if_high) = 2
      pi(quicksort) = [0]
      pi(quicksort#) = 0
     precedence:
      quicksort > app ~ s ~ 0 > quicksort# ~ if_high ~ high ~ if_low ~ 
      low ~ add ~ nil ~ false ~ true ~ le ~ quot ~ minus
     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:
     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