YES
TRS:
 {                      app(l, nil()) -> l,
                        app(nil(), k) -> k,
                   app(cons(x, l), k) -> cons(x, app(l, k)),
     sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                  sum(cons(x, nil())) -> cons(x, nil()),
             sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
  sum(plus(cons(0(), x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l)))),
                         plus(0(), y) -> y,
                        plus(s(x), y) -> s(plus(x, y)),
              pred(cons(s(x), nil())) -> cons(x, nil())}
 RUF:
  Strict:
   {                   app(l, nil()) -> l,
                       app(nil(), k) -> k,
                  app(cons(x, l), k) -> cons(x, app(l, k)),
    sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                 sum(cons(x, nil())) -> cons(x, nil()),
            sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                       plus(s(x), y) -> s(plus(x, y)),
             pred(cons(s(x), nil())) -> cons(x, nil())}
  Weak:
   {}
  RUF:
   Strict:
    {                   app(l, nil()) -> l,
                        app(nil(), k) -> k,
                   app(cons(x, l), k) -> cons(x, app(l, k)),
     sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                  sum(cons(x, nil())) -> cons(x, nil()),
             sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                        plus(s(x), y) -> s(plus(x, y))}
   Weak:
    {}
   DP:
    Strict:
     {              app#(cons(x, l), k) -> app#(l, k),
      sum#(app(l, cons(x, cons(y, k)))) -> app#(l, sum(cons(x, cons(y, k)))),
      sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))),
      sum#(app(l, cons(x, cons(y, k)))) -> sum#(cons(x, cons(y, k))),
              sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)),
              sum#(cons(x, cons(y, l))) -> plus#(x, y),
                         plus#(s(x), y) -> plus#(x, y)}
    Weak:
    {                   app(l, nil()) -> l,
                        app(nil(), k) -> k,
                   app(cons(x, l), k) -> cons(x, app(l, k)),
     sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                  sum(cons(x, nil())) -> cons(x, nil()),
             sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                        plus(s(x), y) -> s(plus(x, y))}
    EDG:
     {(sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)), sum#(cons(x, cons(y, l))) -> plus#(x, y))
      (sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)), sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(cons(x, cons(y, k))), sum#(cons(x, cons(y, l))) -> plus#(x, y))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(cons(x, cons(y, k))), sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)))
      (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))), sum#(app(l, cons(x, cons(y, k)))) -> app#(l, sum(cons(x, cons(y, k)))))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))), sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))), sum#(app(l, cons(x, cons(y, k)))) -> sum#(cons(x, cons(y, k))))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))), sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l)))
      (sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k))))), sum#(cons(x, cons(y, l))) -> plus#(x, y))
      (sum#(cons(x, cons(y, l))) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
      (sum#(app(l, cons(x, cons(y, k)))) -> app#(l, sum(cons(x, cons(y, k)))), app#(cons(x, l), k) -> app#(l, k))
      (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))}
     SCCS:
      Scc:
       {plus#(s(x), y) -> plus#(x, y)}
      Scc:
       {sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l))}
      Scc:
       {sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k)))))}
      Scc:
       {app#(cons(x, l), k) -> app#(l, k)}
      SCC:
       Strict:
        {plus#(s(x), y) -> plus#(x, y)}
       Weak:
       {                   app(l, nil()) -> l,
                           app(nil(), k) -> k,
                      app(cons(x, l), k) -> cons(x, app(l, k)),
        sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                     sum(cons(x, nil())) -> cons(x, nil()),
                sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                           plus(s(x), y) -> s(plus(x, y))}
       SPSC:
        Simple Projection:
         pi(plus#) = 0
        Strict:
         {}
        Qed
      SCC:
       Strict:
        {sum#(cons(x, cons(y, l))) -> sum#(cons(plus(x, y), l))}
       Weak:
       {                   app(l, nil()) -> l,
                           app(nil(), k) -> k,
                      app(cons(x, l), k) -> cons(x, app(l, k)),
        sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                     sum(cons(x, nil())) -> cons(x, nil()),
                sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                           plus(s(x), y) -> s(plus(x, y))}
       POLY:
        Argument Filtering:
         pi(s) = [], pi(plus) = [], pi(sum#) = 0, pi(sum) = [], pi(cons) = [1], pi(nil) = [], pi(app) = []
        Usable Rules:
         {}
        Interpretation:
         [cons](x0) = x0 + 1
        Strict:
         {}
        Weak:
         {                   app(l, nil()) -> l,
                             app(nil(), k) -> k,
                        app(cons(x, l), k) -> cons(x, app(l, k)),
          sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                       sum(cons(x, nil())) -> cons(x, nil()),
                  sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                             plus(s(x), y) -> s(plus(x, y))}
        Qed
      SCC:
       Strict:
        {sum#(app(l, cons(x, cons(y, k)))) -> sum#(app(l, sum(cons(x, cons(y, k)))))}
       Weak:
       {                   app(l, nil()) -> l,
                           app(nil(), k) -> k,
                      app(cons(x, l), k) -> cons(x, app(l, k)),
        sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                     sum(cons(x, nil())) -> cons(x, nil()),
                sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                           plus(s(x), y) -> s(plus(x, y))}
       POLY:
        Argument Filtering:
         pi(s) = [], pi(plus) = [], pi(sum#) = 0, pi(sum) = [], pi(cons) = [1], pi(nil) = [], pi(app) = [0,1]
        Usable Rules:
         {}
        Interpretation:
         [cons](x0) = x0 + 1,
         [app](x0, x1) = x0 + x1,
         [sum] = 1
        Strict:
         {}
        Weak:
         {                   app(l, nil()) -> l,
                             app(nil(), k) -> k,
                        app(cons(x, l), k) -> cons(x, app(l, k)),
          sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                       sum(cons(x, nil())) -> cons(x, nil()),
                  sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                             plus(s(x), y) -> s(plus(x, y))}
        Qed
      SCC:
       Strict:
        {app#(cons(x, l), k) -> app#(l, k)}
       Weak:
       {                   app(l, nil()) -> l,
                           app(nil(), k) -> k,
                      app(cons(x, l), k) -> cons(x, app(l, k)),
        sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))),
                     sum(cons(x, nil())) -> cons(x, nil()),
                sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)),
                           plus(s(x), y) -> s(plus(x, y))}
       SPSC:
        Simple Projection:
         pi(app#) = 0
        Strict:
         {}
        Qed