YES

Problem:
 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))
 head(add(n,x)) -> n
 tail(add(n,x)) -> x
 isempty(nil()) -> true()
 isempty(add(n,x)) -> false()
 quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
 if_qs(true(),x,n,y) -> nil()
 if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))

Proof:
 DP Processor:
  DPs:
   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#(x) -> high#(head(x),tail(x))
   quicksort#(x) -> tail#(x)
   quicksort#(x) -> head#(x)
   quicksort#(x) -> low#(head(x),tail(x))
   quicksort#(x) -> isempty#(x)
   quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
   if_qs#(false(),x,n,y) -> quicksort#(y)
   if_qs#(false(),x,n,y) -> quicksort#(x)
   if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
  TRS:
   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))
   head(add(n,x)) -> n
   tail(add(n,x)) -> x
   isempty(nil()) -> true()
   isempty(add(n,x)) -> false()
   quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
   if_qs(true(),x,n,y) -> nil()
   if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
  TDG Processor:
   DPs:
    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#(x) -> high#(head(x),tail(x))
    quicksort#(x) -> tail#(x)
    quicksort#(x) -> head#(x)
    quicksort#(x) -> low#(head(x),tail(x))
    quicksort#(x) -> isempty#(x)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(y)
    if_qs#(false(),x,n,y) -> quicksort#(x)
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
   TRS:
    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))
    head(add(n,x)) -> n
    tail(add(n,x)) -> x
    isempty(nil()) -> true()
    isempty(add(n,x)) -> false()
    quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs(true(),x,n,y) -> nil()
    if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
   graph:
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> isempty#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> low#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> head#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> tail#(x)
    if_qs#(false(),x,n,y) -> quicksort#(y) ->
    quicksort#(x) -> high#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> isempty#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> low#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> head#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> tail#(x)
    if_qs#(false(),x,n,y) -> quicksort#(x) ->
    quicksort#(x) -> high#(head(x),tail(x))
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y))) ->
    app#(add(n,x),y) -> app#(x,y)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> app#(quicksort(x),add(n,quicksort(y)))
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> quicksort#(x)
    quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x))) ->
    if_qs#(false(),x,n,y) -> quicksort#(y)
    quicksort#(x) -> high#(head(x),tail(x)) ->
    high#(n,add(m,x)) -> if_high#(le(m,n),n,add(m,x))
    quicksort#(x) -> high#(head(x),tail(x)) ->
    high#(n,add(m,x)) -> le#(m,n)
    quicksort#(x) -> low#(head(x),tail(x)) ->
    low#(n,add(m,x)) -> if_low#(le(m,n),n,add(m,x))
    quicksort#(x) -> low#(head(x),tail(x)) ->
    low#(n,add(m,x)) -> le#(m,n)
    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)
   SCC Processor:
    #sccs: 5
    #rules: 11
    #arcs: 36/361
    DPs:
     if_qs#(false(),x,n,y) -> quicksort#(y)
     quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs#(false(),x,n,y) -> quicksort#(x)
    TRS:
     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))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Usable Rule Processor:
     DPs:
      if_qs#(false(),x,n,y) -> quicksort#(y)
      quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
      if_qs#(false(),x,n,y) -> quicksort#(x)
     TRS:
      high(n,nil()) -> nil()
      high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
      tail(add(n,x)) -> x
      head(add(n,x)) -> n
      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)
      isempty(nil()) -> true()
      isempty(add(n,x)) -> false()
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       high(n,nil()) -> nil()
       high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
       tail(add(n,x)) -> 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)
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
      interpretation:
       [if_qs#](x0, x1, x2, x3) = 1x0 + 1x1 + 3x3 + -16,
       
       [quicksort#](x0) = 1x0 + 4,
       
       [isempty](x0) = x0 + 0,
       
       [tail](x0) = -4x0 + 0,
       
       [head](x0) = x0 + 7,
       
       [if_high](x0, x1, x2) = -3x0 + 1x2 + 0,
       
       [high](x0, x1) = 1x1,
       
       [if_low](x0, x1, x2) = x2 + 0,
       
       [low](x0, x1) = x1 + -12,
       
       [add](x0, x1) = 4x1 + 4,
       
       [nil] = 3,
       
       [false] = 4,
       
       [s](x0) = 4x0 + 2,
       
       [true] = 3,
       
       [le](x0, x1) = 4,
       
       [0] = 0
      orientation:
       if_qs#(false(),x,n,y) = 1x + 3y + 5 >= 1y + 4 = quicksort#(y)
       
       quicksort#(x) = 1x + 4 >= 1x + 4 = if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       
       if_qs#(false(),x,n,y) = 1x + 3y + 5 >= 1x + 4 = quicksort#(x)
       
       high(n,nil()) = 4 >= 3 = nil()
       
       high(n,add(m,x)) = 5x + 5 >= 5x + 5 = if_high(le(m,n),n,add(m,x))
       
       tail(add(n,x)) = x + 0 >= x = x
       
       head(add(n,x)) = 4x + 7 >= n = n
       
       if_high(true(),n,add(m,x)) = 5x + 5 >= 1x = high(n,x)
       
       if_high(false(),n,add(m,x)) = 5x + 5 >= 5x + 4 = add(m,high(n,x))
       
       le(0(),y) = 4 >= 3 = true()
       
       le(s(x),0()) = 4 >= 4 = false()
       
       le(s(x),s(y)) = 4 >= 4 = le(x,y)
       
       low(n,nil()) = 3 >= 3 = nil()
       
       low(n,add(m,x)) = 4x + 4 >= 4x + 4 = if_low(le(m,n),n,add(m,x))
       
       if_low(true(),n,add(m,x)) = 4x + 4 >= 4x + 4 = add(m,low(n,x))
       
       if_low(false(),n,add(m,x)) = 4x + 4 >= x + -12 = low(n,x)
       
       isempty(nil()) = 3 >= 3 = true()
       
       isempty(add(n,x)) = 4x + 4 >= 4 = false()
      problem:
       DPs:
        quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
        if_qs#(false(),x,n,y) -> quicksort#(x)
       TRS:
        high(n,nil()) -> nil()
        high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
        tail(add(n,x)) -> x
        head(add(n,x)) -> n
        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)
        isempty(nil()) -> true()
        isempty(add(n,x)) -> false()
      Restore Modifier:
       DPs:
        quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
        if_qs#(false(),x,n,y) -> quicksort#(x)
       TRS:
        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))
        head(add(n,x)) -> n
        tail(add(n,x)) -> x
        isempty(nil()) -> true()
        isempty(add(n,x)) -> false()
        quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
        if_qs(true(),x,n,y) -> nil()
        if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
       Usable Rule Processor:
        DPs:
         quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
         if_qs#(false(),x,n,y) -> quicksort#(x)
        TRS:
         high(n,nil()) -> nil()
         high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
         tail(add(n,x)) -> x
         head(add(n,x)) -> n
         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)
         isempty(nil()) -> true()
         isempty(add(n,x)) -> false()
        Matrix Interpretation Processor: dim=1
         
         usable rules:
          tail(add(n,x)) -> 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)
          isempty(nil()) -> true()
          isempty(add(n,x)) -> false()
         interpretation:
          [if_qs#](x0, x1, x2, x3) = 2x0 + 2x1,
          
          [quicksort#](x0) = 2x0,
          
          [isempty](x0) = 1/2x0,
          
          [tail](x0) = 1/2x0,
          
          [head](x0) = x0 + 2,
          
          [if_high](x0, x1, x2) = 1/2x1 + 2x2 + 2,
          
          [high](x0, x1) = 5/2x0 + x1 + 1,
          
          [if_low](x0, x1, x2) = x2,
          
          [low](x0, x1) = x1,
          
          [add](x0, x1) = 2x1 + 2,
          
          [nil] = 0,
          
          [false] = 1/2,
          
          [s](x0) = 2x0 + 1,
          
          [true] = 0,
          
          [le](x0, x1) = 2x0 + 2x1,
          
          [0] = 1
         orientation:
          quicksort#(x) = 2x >= 2x = if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
          
          if_qs#(false(),x,n,y) = 2x + 1 >= 2x = quicksort#(x)
          
          high(n,nil()) = 5/2n + 1 >= 0 = nil()
          
          high(n,add(m,x)) = 5/2n + 2x + 3 >= 1/2n + 4x + 6 = if_high(le(m,n),n,add(m,x))
          
          tail(add(n,x)) = x + 1 >= x = x
          
          head(add(n,x)) = 2x + 4 >= n = n
          
          if_high(true(),n,add(m,x)) = 1/2n + 4x + 6 >= 5/2n + x + 1 = high(n,x)
          
          if_high(false(),n,add(m,x)) = 1/2n + 4x + 6 >= 5n + 2x + 4 = add(m,high(n,x))
          
          le(0(),y) = 2y + 2 >= 0 = true()
          
          le(s(x),0()) = 4x + 4 >= 1/2 = false()
          
          le(s(x),s(y)) = 4x + 4y + 4 >= 2x + 2y = le(x,y)
          
          low(n,nil()) = 0 >= 0 = nil()
          
          low(n,add(m,x)) = 2x + 2 >= 2x + 2 = if_low(le(m,n),n,add(m,x))
          
          if_low(true(),n,add(m,x)) = 2x + 2 >= 2x + 2 = add(m,low(n,x))
          
          if_low(false(),n,add(m,x)) = 2x + 2 >= x = low(n,x)
          
          isempty(nil()) = 0 >= 0 = true()
          
          isempty(add(n,x)) = x + 1 >= 1/2 = false()
         problem:
          DPs:
           quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
          TRS:
           high(n,nil()) -> nil()
           high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
           tail(add(n,x)) -> x
           head(add(n,x)) -> n
           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)
           isempty(nil()) -> true()
           isempty(add(n,x)) -> false()
         Restore Modifier:
          DPs:
           quicksort#(x) -> if_qs#(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
          TRS:
           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))
           head(add(n,x)) -> n
           tail(add(n,x)) -> x
           isempty(nil()) -> true()
           isempty(add(n,x)) -> false()
           quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
           if_qs(true(),x,n,y) -> nil()
           if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 4/1
           
    
    DPs:
     app#(add(n,x),y) -> app#(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(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))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     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(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))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     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:
     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))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    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:
       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))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     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:
     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))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    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:
       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))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    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(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))
     head(add(n,x)) -> n
     tail(add(n,x)) -> x
     isempty(nil()) -> true()
     isempty(add(n,x)) -> false()
     quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
     if_qs(true(),x,n,y) -> nil()
     if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 0
     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(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))
       head(add(n,x)) -> n
       tail(add(n,x)) -> x
       isempty(nil()) -> true()
       isempty(add(n,x)) -> false()
       quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
       if_qs(true(),x,n,y) -> nil()
       if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))
     Qed