YES
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))))}
 DP:
  Strict:
   {             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)) -> app#(quicksort(low(n, x)), add(n, quicksort(high(n, x)))),
              quicksort#(add(n, x)) -> low#(n, x),
              quicksort#(add(n, x)) -> high#(n, x),
              quicksort#(add(n, x)) -> quicksort#(low(n, x)),
              quicksort#(add(n, x)) -> quicksort#(high(n, x))}
  Weak:
  {                 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))))}
  EDG:
   {(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))
    (low#(n, add(m, x)) -> le#(m, n), le#(s(x), s(y)) -> le#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (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))
    (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))
    (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))
    (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)) -> quicksort#(low(n, x)))
    (quicksort#(add(n, x)) -> quicksort#(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#(high(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)) -> app#(quicksort(low(n, x)), add(n, quicksort(high(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)) -> 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)) -> quicksort#(high(n, x)))
    (quicksort#(add(n, x)) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n))
    (quicksort#(add(n, 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#(false(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(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#(false(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (high#(n, add(m, x)) -> le#(m, n), le#(s(x), s(y)) -> le#(x, 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)) -> quot#(minus(x, y), s(y)), quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)))
    (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)) -> if_low#(le(m, n), n, add(m, x)), if_low#(false(), n, add(m, x)) -> low#(n, x))}
   SCCS:
    Scc:
     {quicksort#(add(n, x)) -> quicksort#(low(n, x)),
      quicksort#(add(n, x)) -> quicksort#(high(n, x))}
    Scc:
     {            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)}
    Scc:
     {            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)}
    Scc:
     {app#(add(n, x), y) -> app#(x, y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     Strict:
      {quicksort#(add(n, x)) -> quicksort#(low(n, x)),
       quicksort#(add(n, x)) -> quicksort#(high(n, x))}
     Weak:
     {                 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))))}
     POLY:
      Argument Filtering:
       pi(quicksort#) = [0], pi(quicksort) = [], pi(if_high) = 2, pi(high) = 1, pi(if_low) = [2], pi(low) = [1], pi(add) = [1], pi(nil) = [], pi(app) = [], pi(false) = [], pi(le) = [], pi(true) = [], pi(quot) = [], pi(s) = [], pi(0) = [], pi(minus) = []
      Usable Rules:
       {}
      Interpretation:
       [quicksort#](x0) = x0 + 1,
       [low](x0) = x0 + 1,
       [add](x0) = x0 + 1
      Strict:
       {quicksort#(add(n, x)) -> quicksort#(low(n, x))}
      Weak:
       {                 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))))}
      EDG:
       {(quicksort#(add(n, x)) -> quicksort#(low(n, x)), quicksort#(add(n, x)) -> quicksort#(low(n, x)))}
       SCCS:
        Scc:
         {quicksort#(add(n, x)) -> quicksort#(low(n, x))}
        SCC:
         Strict:
          {quicksort#(add(n, x)) -> quicksort#(low(n, x))}
         Weak:
         {                 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))))}
         POLY:
          Argument Filtering:
           pi(quicksort#) = 0, pi(quicksort) = [], pi(if_high) = [], pi(high) = [], pi(if_low) = 2, pi(low) = 1, pi(add) = [1], pi(nil) = [], pi(app) = [], pi(false) = [], pi(le) = [], pi(true) = [], pi(quot) = [], pi(s) = [], pi(0) = [], pi(minus) = []
          Usable Rules:
           {}
          Interpretation:
           [add](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {                 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
    SCC:
     Strict:
      {            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)}
     Weak:
     {                 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))))}
     SPSC:
      Simple Projection:
       pi(if_high#) = 2, pi(high#) = 1
      Strict:
       {           high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
        if_high#(true(), n, add(m, x)) -> high#(n, x)}
      EDG:
       {(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#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)))}
       SCCS:
        Scc:
         {           high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
          if_high#(true(), n, add(m, x)) -> high#(n, x)}
        SCC:
         Strict:
          {           high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
           if_high#(true(), n, add(m, x)) -> high#(n, x)}
         Weak:
         {                 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))))}
         SPSC:
          Simple Projection:
           pi(if_high#) = 2, pi(high#) = 1
          Strict:
           {high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {            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)}
     Weak:
     {                 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))))}
     SPSC:
      Simple Projection:
       pi(if_low#) = 2, pi(low#) = 1
      Strict:
       {           low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
        if_low#(true(), n, add(m, x)) -> low#(n, x)}
      EDG:
       {(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#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))}
       SCCS:
        Scc:
         {           low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
          if_low#(true(), n, add(m, x)) -> low#(n, x)}
        SCC:
         Strict:
          {           low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
           if_low#(true(), n, add(m, x)) -> low#(n, x)}
         Weak:
         {                 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))))}
         SPSC:
          Simple Projection:
           pi(if_low#) = 2, pi(low#) = 1
          Strict:
           {low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {app#(add(n, x), y) -> app#(x, y)}
     Weak:
     {                 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))))}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {                 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))))}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))}
     Weak:
     {                 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))))}
     POLY:
      Argument Filtering:
       pi(quicksort) = [], pi(if_high) = [], pi(high) = [], pi(if_low) = [], pi(low) = [], pi(add) = [], pi(nil) = [], pi(app) = [], pi(false) = [], pi(le) = [], pi(true) = [], pi(quot#) = 0, pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                 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
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {                 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))))}
     SPSC:
      Simple Projection:
       pi(minus#) = 1
      Strict:
       {}
      Qed