YES
Time: 0.021191
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:
    DP:
     {             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)}
    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),
                        plus(s x, y) -> s plus(x, y)}
    EDG:
     {(app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
      (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))
      (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
      (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# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
      (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# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> plus#(x, y))}
     SCCS (4):
      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 (1):
       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 (1):
       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:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [app](x0, x1) = x0 + x1 + 1,
         
         [cons](x0, x1) = x0 + 1,
         
         [plus](x0, x1) = 0,
         
         [sum](x0) = x0 + 1,
         
         [s](x0) = 0,
         
         [nil] = 1,
         
         [sum#](x0) = x0 + 1
        Strict:
         sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)
         3 + 1l + 0x + 0y >= 2 + 1l + 0x + 0y
        Weak:
         
       Qed
     SCC (1):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [app](x0, x1) = x0 + x1,
        
        [cons](x0, x1) = x0 + 1,
        
        [plus](x0, x1) = 0,
        
        [sum](x0) = 1,
        
        [s](x0) = 0,
        
        [nil] = 0,
        
        [sum#](x0) = x0
       Strict:
        sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))
        2 + 1k + 1l + 0x + 0y >= 1 + 0k + 1l + 0x + 0y
       Weak:
        
      Qed
     SCC (1):
      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