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))),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                       reverse(nil()) -> nil(),
                   reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                       shuffle(nil()) -> nil(),
                   shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                    concat(leaf(), y) -> y,
                concat(cons(u, v), y) -> cons(u, concat(v, y)),
               less_leaves(x, leaf()) -> false(),
      less_leaves(leaf(), cons(w, z)) -> true(),
  less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
 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)),
                      app#(add(n, x), y) -> app#(x, y),
                     reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())),
                     reverse#(add(n, x)) -> reverse#(x),
                     shuffle#(add(n, x)) -> reverse#(x),
                     shuffle#(add(n, x)) -> shuffle#(reverse(x)),
                  concat#(cons(u, v), y) -> concat#(v, y),
    less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v),
    less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z),
    less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
  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))),
                         app(nil(), y) -> y,
                     app(add(n, x), y) -> add(n, app(x, y)),
                        reverse(nil()) -> nil(),
                    reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                        shuffle(nil()) -> nil(),
                    shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                     concat(leaf(), y) -> y,
                 concat(cons(u, v), y) -> cons(u, concat(v, y)),
                less_leaves(x, leaf()) -> false(),
       less_leaves(leaf(), cons(w, z)) -> true(),
   less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
  EDG:
   {(shuffle#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> reverse#(x))
    (shuffle#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())))
    (less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
    (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
    (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
    (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
    (quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
    (shuffle#(add(n, x)) -> shuffle#(reverse(x)), shuffle#(add(n, x)) -> shuffle#(reverse(x)))
    (shuffle#(add(n, x)) -> shuffle#(reverse(x)), shuffle#(add(n, x)) -> reverse#(x))
    (reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())), app#(add(n, x), y) -> app#(x, y))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, 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)))
    (reverse#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())))
    (reverse#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> reverse#(x))}
   SCCS:
    Scc:
     {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
    Scc:
     {concat#(cons(u, v), y) -> concat#(v, y)}
    Scc:
     {shuffle#(add(n, x)) -> shuffle#(reverse(x))}
    Scc:
     {reverse#(add(n, x)) -> reverse#(x)}
    Scc:
     {app#(add(n, x), y) -> app#(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:
      {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
     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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     POLY:
      Argument Filtering:
       pi(true) = [], pi(less_leaves#) = [0,1], pi(less_leaves) = [], pi(false) = [], pi(cons) = [0,1], pi(leaf) = [], pi(concat) = [0,1], pi(shuffle) = [], pi(reverse) = [], pi(add) = [], pi(nil) = [], pi(app) = [], pi(quot) = [], pi(s) = [], pi(0) = [], pi(minus) = []
      Usable Rules:
       {}
      Interpretation:
       [less_leaves#](x0, x1) = x0 + x1,
       [cons](x0, x1) = x0 + x1 + 1,
       [concat](x0, x1) = x0 + x1
      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))),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                             reverse(nil()) -> nil(),
                         reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                             shuffle(nil()) -> nil(),
                         shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                          concat(leaf(), y) -> y,
                      concat(cons(u, v), y) -> cons(u, concat(v, y)),
                     less_leaves(x, leaf()) -> false(),
            less_leaves(leaf(), cons(w, z)) -> true(),
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
      Qed
    SCC:
     Strict:
      {concat#(cons(u, v), y) -> concat#(v, 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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     SPSC:
      Simple Projection:
       pi(concat#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {shuffle#(add(n, x)) -> shuffle#(reverse(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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     POLY:
      Argument Filtering:
       pi(true) = [], pi(less_leaves) = [], pi(false) = [], pi(cons) = [], pi(leaf) = [], pi(concat) = [], pi(shuffle#) = 0, pi(shuffle) = [], pi(reverse) = 0, pi(add) = [1], pi(nil) = [], pi(app) = [0,1], 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))),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                             reverse(nil()) -> nil(),
                         reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                             shuffle(nil()) -> nil(),
                         shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                          concat(leaf(), y) -> y,
                      concat(cons(u, v), y) -> cons(u, concat(v, y)),
                     less_leaves(x, leaf()) -> false(),
            less_leaves(leaf(), cons(w, z)) -> true(),
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
      Qed
    SCC:
     Strict:
      {reverse#(add(n, x)) -> reverse#(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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     SPSC:
      Simple Projection:
       pi(reverse#) = 0
      Strict:
       {}
      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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     SPSC:
      Simple Projection:
       pi(app#) = 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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     POLY:
      Argument Filtering:
       pi(true) = [], pi(less_leaves) = [], pi(false) = [], pi(cons) = [], pi(leaf) = [], pi(concat) = [], pi(shuffle) = [], pi(reverse) = [], pi(add) = [], pi(nil) = [], pi(app) = [], 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))),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                             reverse(nil()) -> nil(),
                         reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                             shuffle(nil()) -> nil(),
                         shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                          concat(leaf(), y) -> y,
                      concat(cons(u, v), y) -> cons(u, concat(v, y)),
                     less_leaves(x, leaf()) -> false(),
            less_leaves(leaf(), cons(w, z)) -> true(),
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
      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))),
                            app(nil(), y) -> y,
                        app(add(n, x), y) -> add(n, app(x, y)),
                           reverse(nil()) -> nil(),
                       reverse(add(n, x)) -> app(reverse(x), add(n, nil())),
                           shuffle(nil()) -> nil(),
                       shuffle(add(n, x)) -> add(n, shuffle(reverse(x))),
                        concat(leaf(), y) -> y,
                    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                   less_leaves(x, leaf()) -> false(),
          less_leaves(leaf(), cons(w, z)) -> true(),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed