YES
TRS:
 {     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)))}
 DP:
  Strict:
   { 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))}
  Weak:
  {     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)))}
  EDG:
   {(reverse#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> reverse#(x))
    (reverse#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())))
    (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))
    (shuffle#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> app#(reverse(x), add(n, nil())))
    (shuffle#(add(n, x)) -> reverse#(x), reverse#(add(n, x)) -> reverse#(x))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))}
   SCCS:
    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:
     Strict:
      {shuffle#(add(n, x)) -> shuffle#(reverse(x))}
     Weak:
     {     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)))}
     POLY:
      Argument Filtering:
       pi(shuffle#) = 0, pi(shuffle) = [], pi(reverse) = 0, pi(add) = [1], pi(nil) = [], pi(app) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [add](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {     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)))}
      Qed
    SCC:
     Strict:
      {reverse#(add(n, x)) -> reverse#(x)}
     Weak:
     {     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)))}
     SPSC:
      Simple Projection:
       pi(reverse#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {app#(add(n, x), y) -> app#(x, y)}
     Weak:
     {     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)))}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed