YES
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:
  Strict:
   {                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))}
  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))))}
  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))
    (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))
    (le#(s(X), s(Y)) -> le#(X, Y), le#(s(X), s(Y)) -> le#(X, Y))
    (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)))
    (app#(cons(N, L), Y) -> app#(L, Y), app#(cons(N, L), Y) -> app#(L, Y))
    (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))
    (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:
    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:
     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:
      Argument Filtering:
       pi(quicksort#) = 0, pi(quicksort) = [], pi(ifhigh) = 2, pi(high) = 1, pi(iflow) = 2, pi(low) = 1, pi(cons) = [1], pi(nil) = [], pi(app) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(le) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {}
      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))))}
      Qed
    SCC:
     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:
        Scc:
         {          high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)),
          ifhigh#(true(), N, cons(M, L)) -> high#(N, L)}
        SCC:
         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:
            
            Qed
    SCC:
     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#(false(), N, cons(M, L)) -> low#(N, L)}
      EDG:
       {(low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(false(), N, cons(M, L)) -> low#(N, L))
        (iflow#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))}
       SCCS:
        Scc:
         {           low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)),
          iflow#(false(), N, cons(M, L)) -> low#(N, L)}
        SCC:
         Strict:
          {           low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, 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))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     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:
     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#) = 0
      Strict:
       {}
      Qed