YES
Time: 0.020387
TRS:
 {                    le(0(), Y) -> true(),
                    le(s X, 0()) -> false(),
                    le(s X, s Y) -> le(X, Y),
                   app(nil(), Y) -> Y,
              app(cons(N, L), Y) -> cons(N, app(L, Y)),
                   low(N, nil()) -> nil(),
              low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
    iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
   iflow(false(), N, cons(M, L)) -> low(N, L),
                  high(N, nil()) -> nil(),
             high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
   ifhigh(true(), N, cons(M, L)) -> high(N, L),
  ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                 quicksort nil() -> nil(),
            quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
 DP:
  DP:
   {                  le#(s X, s Y) -> le#(X, Y),
                app#(cons(N, L), Y) -> app#(L, Y),
                low#(N, cons(M, L)) -> le#(M, N),
                low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
      iflow#(true(), N, cons(M, L)) -> low#(N, L),
     iflow#(false(), N, cons(M, L)) -> low#(N, L),
               high#(N, cons(M, L)) -> le#(M, N),
               high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
     ifhigh#(true(), N, cons(M, L)) -> high#(N, L),
    ifhigh#(false(), N, cons(M, L)) -> high#(N, L),
              quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))),
              quicksort# cons(N, L) -> low#(N, L),
              quicksort# cons(N, L) -> high#(N, L),
              quicksort# cons(N, L) -> quicksort# low(N, L),
              quicksort# cons(N, L) -> quicksort# high(N, L)}
  TRS:
  {                    le(0(), Y) -> true(),
                     le(s X, 0()) -> false(),
                     le(s X, s Y) -> le(X, Y),
                    app(nil(), Y) -> Y,
               app(cons(N, L), Y) -> cons(N, app(L, Y)),
                    low(N, nil()) -> nil(),
               low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
     iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
    iflow(false(), N, cons(M, L)) -> low(N, L),
                   high(N, nil()) -> nil(),
              high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
    ifhigh(true(), N, cons(M, L)) -> high(N, L),
   ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                  quicksort nil() -> nil(),
             quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
  EDG:
   {(iflow#(true(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))
    (iflow#(true(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N))
    (ifhigh#(true(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)))
    (ifhigh#(true(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N))
    (quicksort# cons(N, L) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))
    (quicksort# cons(N, L) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N))
    (low#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y))
    (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))
    (low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(false(), N, cons(M, L)) -> low#(N, L))
    (low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# high(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# low(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> high#(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> low#(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> low#(N, L))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> high#(N, L))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> quicksort# low(N, L))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> quicksort# high(N, L))
    (high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L))
    (high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(false(), N, cons(M, L)) -> high#(N, L))
    (app#(cons(N, L), Y) -> app#(L, Y), app#(cons(N, L), Y) -> app#(L, Y))
    (high#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y))
    (quicksort# cons(N, L) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N))
    (quicksort# cons(N, L) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)))
    (ifhigh#(false(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N))
    (ifhigh#(false(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)))
    (iflow#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N))
    (iflow#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))
    (quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))), app#(cons(N, L), Y) -> app#(L, Y))}
   SCCS (5):
    Scc:
     {quicksort# cons(N, L) -> quicksort# low(N, L),
      quicksort# cons(N, L) -> quicksort# high(N, L)}
    Scc:
     {           high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
       ifhigh#(true(), N, cons(M, L)) -> high#(N, L),
      ifhigh#(false(), N, cons(M, L)) -> high#(N, L)}
    Scc:
     {           low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
       iflow#(true(), N, cons(M, L)) -> low#(N, L),
      iflow#(false(), N, cons(M, L)) -> low#(N, L)}
    Scc:
     {app#(cons(N, L), Y) -> app#(L, Y)}
    Scc:
     {le#(s X, s Y) -> le#(X, Y)}
    SCC (2):
     Strict:
      {quicksort# cons(N, L) -> quicksort# low(N, L),
       quicksort# cons(N, L) -> quicksort# high(N, L)}
     Weak:
     {                    le(0(), Y) -> true(),
                        le(s X, 0()) -> false(),
                        le(s X, s Y) -> le(X, Y),
                       app(nil(), Y) -> Y,
                  app(cons(N, L), Y) -> cons(N, app(L, Y)),
                       low(N, nil()) -> nil(),
                  low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
        iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
       iflow(false(), N, cons(M, L)) -> low(N, L),
                      high(N, nil()) -> nil(),
                 high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
       ifhigh(true(), N, cons(M, L)) -> high(N, L),
      ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                     quicksort nil() -> nil(),
                quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [iflow](x0, x1, x2) = x0,
       
       [ifhigh](x0, x1, x2) = x0,
       
       [le](x0, x1) = 0,
       
       [app](x0, x1) = x0 + 1,
       
       [cons](x0, x1) = x0 + 1,
       
       [low](x0, x1) = x0,
       
       [high](x0, x1) = x0,
       
       [s](x0) = 0,
       
       [quicksort](x0) = 0,
       
       [true] = 0,
       
       [0] = 0,
       
       [false] = 0,
       
       [nil] = 1,
       
       [quicksort#](x0) = x0
      Strict:
       quicksort# cons(N, L) -> quicksort# high(N, L)
       1 + 0N + 1L >= 0 + 0N + 1L
       quicksort# cons(N, L) -> quicksort# low(N, L)
       1 + 0N + 1L >= 0 + 0N + 1L
      Weak:
       
     Qed
   SCC (3):
    Strict:
     {           high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
       ifhigh#(true(), N, cons(M, L)) -> high#(N, L),
      ifhigh#(false(), N, cons(M, L)) -> high#(N, L)}
    Weak:
    {                    le(0(), Y) -> true(),
                       le(s X, 0()) -> false(),
                       le(s X, s Y) -> le(X, Y),
                      app(nil(), Y) -> Y,
                 app(cons(N, L), Y) -> cons(N, app(L, Y)),
                      low(N, nil()) -> nil(),
                 low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
       iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
      iflow(false(), N, cons(M, L)) -> low(N, L),
                     high(N, nil()) -> nil(),
                high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
      ifhigh(true(), N, cons(M, L)) -> high(N, L),
     ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                    quicksort nil() -> nil(),
               quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
    SPSC:
     Simple Projection:
      pi(ifhigh#) = 2, pi(high#) = 1
     Strict:
      {          high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
       ifhigh#(true(), N, cons(M, L)) -> high#(N, L)}
     EDG:
      {(high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L))
       (ifhigh#(true(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)))}
      SCCS (1):
       Scc:
        {          high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
         ifhigh#(true(), N, cons(M, L)) -> high#(N, L)}
       SCC (2):
        Strict:
         {          high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
          ifhigh#(true(), N, cons(M, L)) -> high#(N, L)}
        Weak:
        {                    le(0(), Y) -> true(),
                           le(s X, 0()) -> false(),
                           le(s X, s Y) -> le(X, Y),
                          app(nil(), Y) -> Y,
                     app(cons(N, L), Y) -> cons(N, app(L, Y)),
                          low(N, nil()) -> nil(),
                     low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
           iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
          iflow(false(), N, cons(M, L)) -> low(N, L),
                         high(N, nil()) -> nil(),
                    high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
          ifhigh(true(), N, cons(M, L)) -> high(N, L),
         ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                        quicksort nil() -> nil(),
                   quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
        SPSC:
         Simple Projection:
          pi(ifhigh#) = 2, pi(high#) = 1
         Strict:
          {high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L))}
         EDG:
          {}
          SCCS (0):
           
           Qed
   SCC (3):
    Strict:
     {           low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
       iflow#(true(), N, cons(M, L)) -> low#(N, L),
      iflow#(false(), N, cons(M, L)) -> low#(N, L)}
    Weak:
    {                    le(0(), Y) -> true(),
                       le(s X, 0()) -> false(),
                       le(s X, s Y) -> le(X, Y),
                      app(nil(), Y) -> Y,
                 app(cons(N, L), Y) -> cons(N, app(L, Y)),
                      low(N, nil()) -> nil(),
                 low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
       iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
      iflow(false(), N, cons(M, L)) -> low(N, L),
                     high(N, nil()) -> nil(),
                high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
      ifhigh(true(), N, cons(M, L)) -> high(N, L),
     ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                    quicksort nil() -> nil(),
               quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
    SPSC:
     Simple Projection:
      pi(iflow#) = 2, pi(low#) = 1
     Strict:
      {          low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
       iflow#(true(), N, cons(M, L)) -> low#(N, L)}
     EDG:
      {(low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L))
       (iflow#(true(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))}
      SCCS (1):
       Scc:
        {          low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
         iflow#(true(), N, cons(M, L)) -> low#(N, L)}
       SCC (2):
        Strict:
         {          low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
          iflow#(true(), N, cons(M, L)) -> low#(N, L)}
        Weak:
        {                    le(0(), Y) -> true(),
                           le(s X, 0()) -> false(),
                           le(s X, s Y) -> le(X, Y),
                          app(nil(), Y) -> Y,
                     app(cons(N, L), Y) -> cons(N, app(L, Y)),
                          low(N, nil()) -> nil(),
                     low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
           iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
          iflow(false(), N, cons(M, L)) -> low(N, L),
                         high(N, nil()) -> nil(),
                    high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
          ifhigh(true(), N, cons(M, L)) -> high(N, L),
         ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                        quicksort nil() -> nil(),
                   quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
        SPSC:
         Simple Projection:
          pi(iflow#) = 2, pi(low#) = 1
         Strict:
          {low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L))}
         EDG:
          {}
          SCCS (0):
           
           Qed
   SCC (1):
    Strict:
     {app#(cons(N, L), Y) -> app#(L, Y)}
    Weak:
    {                    le(0(), Y) -> true(),
                       le(s X, 0()) -> false(),
                       le(s X, s Y) -> le(X, Y),
                      app(nil(), Y) -> Y,
                 app(cons(N, L), Y) -> cons(N, app(L, Y)),
                      low(N, nil()) -> nil(),
                 low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
       iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
      iflow(false(), N, cons(M, L)) -> low(N, L),
                     high(N, nil()) -> nil(),
                high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
      ifhigh(true(), N, cons(M, L)) -> high(N, L),
     ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                    quicksort nil() -> nil(),
               quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
    SPSC:
     Simple Projection:
      pi(app#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {le#(s X, s Y) -> le#(X, Y)}
    Weak:
    {                    le(0(), Y) -> true(),
                       le(s X, 0()) -> false(),
                       le(s X, s Y) -> le(X, Y),
                      app(nil(), Y) -> Y,
                 app(cons(N, L), Y) -> cons(N, app(L, Y)),
                      low(N, nil()) -> nil(),
                 low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)),
       iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)),
      iflow(false(), N, cons(M, L)) -> low(N, L),
                     high(N, nil()) -> nil(),
                high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)),
      ifhigh(true(), N, cons(M, L)) -> high(N, L),
     ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)),
                    quicksort nil() -> nil(),
               quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))}
    SPSC:
     Simple Projection:
      pi(le#) = 1
     Strict:
      {}
     Qed