YES
Time: 0.056570
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())}
 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),
    sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(y, l)),
    sum# plus(cons(0(), x), cons(y, l)) -> pred# sum cons(s x, cons(y, l)),
                          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),
   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())}
  EDG:
   {(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))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
    (sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(y, l)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(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)) -> 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))
    (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# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (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# 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))}
   STATUS:
    arrows: 0.814815
    SCCS (4):
     Scc:
      {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
     Scc:
      {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     Scc:
      {app#(cons(x, l), k) -> app#(l, k)}
     
     
     
     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),
       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())}
      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) = 1,
        
        [s](x0) = 0,
        
        [pred](x0) = x0,
        
        [nil] = 0,
        
        [0] = 0,
        
        [sum#](x0) = x0 + 1
       Strict:
        sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))
        4 + 1k + 1l + 0x + 0y >= 3 + 0k + 1l + 0x + 0y
       Weak:
        pred cons(s x, nil()) -> cons(x, nil())
        1 + 0x >= 1 + 0x
        plus(s x, y) -> s plus(x, y)
        0 + 0x + 0y >= 0 + 0x + 0y
        plus(0(), y) -> y
        0 + 0y >= 1y
        sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l))
        1 + 0l + 0x + 0y >= 1 + 0l + 0x + 0y
        sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
        1 + 0l + 0x + 0y >= 1 + 0l + 0x + 0y
        sum cons(x, nil()) -> cons(x, nil())
        1 + 0x >= 1 + 0x
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
        1 + 0k + 0l + 0x + 0y >= 1 + 0k + 0l + 0x + 0y
        app(cons(x, l), k) -> cons(x, app(l, k))
        2 + 1k + 1l + 0x >= 2 + 1k + 1l + 0x
        app(nil(), k) -> k
        1 + 1k >= 1k
        app(l, nil()) -> l
        1 + 1l >= 1l
      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),
      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())}
     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) = 1,
       
       [sum](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [pred](x0) = x0,
       
       [nil] = 1,
       
       [0] = 0,
       
       [sum#](x0) = x0
      Strict:
       sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)
       2 + 1l + 0x + 0y >= 1 + 1l + 0x + 0y
      Weak:
       pred cons(s x, nil()) -> cons(x, nil())
       2 + 0x >= 2 + 0x
       plus(s x, y) -> s plus(x, y)
       1 + 0x + 0y >= 2 + 0x + 0y
       plus(0(), y) -> y
       1 + 0y >= 1y
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l))
       2 + 0l + 0x + 0y >= 3 + 1l + 0x + 0y
       sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
       3 + 1l + 0x + 0y >= 2 + 1l + 0x + 0y
       sum cons(x, nil()) -> cons(x, nil())
       3 + 0x >= 2 + 0x
       sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
       4 + 1k + 1l + 0x + 0y >= 5 + 1k + 1l + 0x + 0y
       app(cons(x, l), k) -> cons(x, app(l, k))
       2 + 1k + 1l + 0x >= 2 + 1k + 1l + 0x
       app(nil(), k) -> k
       2 + 1k >= 1k
       app(l, nil()) -> l
       2 + 1l >= 1l
     Qed
    
    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),
      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())}
     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) = 1,
       
       [sum](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [pred](x0) = x0,
       
       [nil] = 1,
       
       [0] = 0,
       
       [plus#](x0, x1) = x0 + 1
      Strict:
       plus#(s x, y) -> plus#(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       pred cons(s x, nil()) -> cons(x, nil())
       2 + 0x >= 2 + 0x
       plus(s x, y) -> s plus(x, y)
       1 + 0x + 0y >= 2 + 0x + 0y
       plus(0(), y) -> y
       1 + 0y >= 1y
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l))
       2 + 0l + 0x + 0y >= 3 + 1l + 0x + 0y
       sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
       3 + 1l + 0x + 0y >= 2 + 1l + 0x + 0y
       sum cons(x, nil()) -> cons(x, nil())
       3 + 0x >= 2 + 0x
       sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
       4 + 1k + 1l + 0x + 0y >= 5 + 1k + 1l + 0x + 0y
       app(cons(x, l), k) -> cons(x, app(l, k))
       2 + 1k + 1l + 0x >= 2 + 1k + 1l + 0x
       app(nil(), k) -> k
       2 + 1k >= 1k
       app(l, nil()) -> l
       2 + 1l >= 1l
     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),
     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())}
    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) = 1,
      
      [sum](x0) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [pred](x0) = x0,
      
      [nil] = 1,
      
      [0] = 0,
      
      [app#](x0, x1) = x0 + 1
     Strict:
      app#(cons(x, l), k) -> app#(l, k)
      2 + 0k + 1l + 0x >= 1 + 0k + 1l
     Weak:
      pred cons(s x, nil()) -> cons(x, nil())
      2 + 0x >= 2 + 0x
      plus(s x, y) -> s plus(x, y)
      1 + 0x + 0y >= 2 + 0x + 0y
      plus(0(), y) -> y
      1 + 0y >= 1y
      sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l))
      2 + 0l + 0x + 0y >= 3 + 1l + 0x + 0y
      sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
      3 + 1l + 0x + 0y >= 2 + 1l + 0x + 0y
      sum cons(x, nil()) -> cons(x, nil())
      3 + 0x >= 2 + 0x
      sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
      4 + 1k + 1l + 0x + 0y >= 5 + 1k + 1l + 0x + 0y
      app(cons(x, l), k) -> cons(x, app(l, k))
      2 + 1k + 1l + 0x >= 2 + 1k + 1l + 0x
      app(nil(), k) -> k
      2 + 1k >= 1k
      app(l, nil()) -> l
      2 + 1l >= 1l
    Qed