YES
Time: 0.070072
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:
  DP:
   {               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)}
  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)))}
  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 (7):
    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 (2):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if_low](x0, x1, x2) = x0 + 1,
       
       [if_high](x0, x1, x2) = x0,
       
       [minus](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [le](x0, x1) = 0,
       
       [app](x0, x1) = x0 + 1,
       
       [add](x0, x1) = x0 + 1,
       
       [low](x0, x1) = x0 + 1,
       
       [high](x0, x1) = x0,
       
       [s](x0) = 1,
       
       [quicksort](x0) = 0,
       
       [0] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [nil] = 1,
       
       [quicksort#](x0) = x0 + 1
      Strict:
       quicksort# add(n, x) -> quicksort# high(n, x)
       2 + 1x + 0n >= 1 + 1x + 0n
       quicksort# add(n, x) -> quicksort# low(n, x)
       2 + 1x + 0n >= 2 + 1x + 0n
      Weak:
       
     EDG:
      {(quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# low(n, x))}
      SCCS (1):
       Scc:
        {quicksort# add(n, x) -> quicksort# low(n, x)}
       SCC (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)))}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [if_low](x0, x1, x2) = x0,
          
          [if_high](x0, x1, x2) = x0 + x1,
          
          [minus](x0, x1) = x0 + 1,
          
          [quot](x0, x1) = x0 + x1 + 1,
          
          [le](x0, x1) = x0,
          
          [app](x0, x1) = x0 + 1,
          
          [add](x0, x1) = x0 + x1 + 1,
          
          [low](x0, x1) = x0,
          
          [high](x0, x1) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [quicksort](x0) = x0,
          
          [0] = 0,
          
          [true] = 0,
          
          [false] = 0,
          
          [nil] = 1,
          
          [quicksort#](x0) = x0 + 1
         Strict:
          quicksort# add(n, x) -> quicksort# low(n, x)
          2 + 1x + 1n >= 1 + 1x + 0n
         Weak:
          
        Qed
   SCC (3):
    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:
      {(if_high#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, 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))}
      SCCS (1):
       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 (2):
        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 (0):
           
           Qed
   SCC (3):
    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:
      {(if_low#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, 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))}
      SCCS (1):
       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 (2):
        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 (0):
           
           Qed
   SCC (1):
    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 (1):
    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#) = 1
     Strict:
      {}
     Qed
   SCC (1):
    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:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [if_low](x0, x1, x2) = 0,
      
      [if_high](x0, x1, x2) = 1,
      
      [minus](x0, x1) = x0,
      
      [quot](x0, x1) = x0 + 1,
      
      [le](x0, x1) = x0 + 1,
      
      [app](x0, x1) = x0 + 1,
      
      [add](x0, x1) = x0 + 1,
      
      [low](x0, x1) = x0 + 1,
      
      [high](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [quicksort](x0) = 1,
      
      [0] = 1,
      
      [true] = 0,
      
      [false] = 0,
      
      [nil] = 1,
      
      [quot#](x0, x1) = x0 + 1
     Strict:
      quot#(s x, s y) -> quot#(minus(x, y), s y)
      2 + 1x + 0y >= 1 + 1x + 0y
     Weak:
      
    Qed
  SCC (1):
   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