YES

Problem:
 app(nil(),k) -> k
 app(l,nil()) -> l
 app(cons(x,l),k) -> cons(x,app(l,k))
 sum(cons(x,nil())) -> cons(x,nil())
 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)))))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
 pred(cons(s(x),nil())) -> cons(x,nil())

Proof:
 DP Processor:
  DPs:
   app#(cons(x,l),k) -> app#(l,k)
   sum#(cons(x,cons(y,l))) -> plus#(x,y)
   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#(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)))))
   plus#(s(x),y) -> 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))))
  TRS:
   app(nil(),k) -> k
   app(l,nil()) -> l
   app(cons(x,l),k) -> cons(x,app(l,k))
   sum(cons(x,nil())) -> cons(x,nil())
   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)))))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
   pred(cons(s(x),nil())) -> cons(x,nil())
  EDG Processor:
   DPs:
    app#(cons(x,l),k) -> app#(l,k)
    sum#(cons(x,cons(y,l))) -> plus#(x,y)
    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#(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)))))
    plus#(s(x),y) -> 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))))
   TRS:
    app(nil(),k) -> k
    app(l,nil()) -> l
    app(cons(x,l),k) -> cons(x,app(l,k))
    sum(cons(x,nil())) -> cons(x,nil())
    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)))))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
    pred(cons(s(x),nil())) -> cons(x,nil())
   graph:
    plus#(s(x),y) -> plus#(x,y) ->
    plus#(s(x),y) -> plus#(x,y)
    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))) -> plus#(x,y) ->
    plus#(s(x),y) -> plus#(x,y)
    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))
    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)))) -> 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#(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#(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#(plus(cons(0(),x),cons(y,l))) -> sum#(cons(s(x),cons(y,l)))
    sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) ->
    sum#(plus(cons(0(),x),cons(y,l))) -> pred#(sum(cons(s(x),cons(y,l))))
    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)
   SCC Processor:
    #sccs: 4
    #rules: 4
    #arcs: 17/81
    DPs:
     sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k)))))
    TRS:
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     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)))))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
     pred(cons(s(x),nil())) -> cons(x,nil())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [sum#](x0) = x0,
      
      [pred](x0) = 1,
      
      [s](x0) = 1,
      
      [0] = 0,
      
      [plus](x0, x1) = x1 + 1,
      
      [sum](x0) = 1,
      
      [cons](x0, x1) = x1 + 1,
      
      [app](x0, x1) = x0 + x1 + 1,
      
      [nil] = 0
     orientation:
      sum#(app(l,cons(x,cons(y,k)))) = k + l + 3 >= l + 2 = sum#(app(l,sum(cons(x,cons(y,k)))))
      
      app(nil(),k) = k + 1 >= k = k
      
      app(l,nil()) = l + 1 >= l = l
      
      app(cons(x,l),k) = k + l + 2 >= k + l + 2 = cons(x,app(l,k))
      
      sum(cons(x,nil())) = 1 >= 1 = cons(x,nil())
      
      sum(cons(x,cons(y,l))) = 1 >= 1 = sum(cons(plus(x,y),l))
      
      sum(app(l,cons(x,cons(y,k)))) = 1 >= 1 = sum(app(l,sum(cons(x,cons(y,k)))))
      
      plus(0(),y) = y + 1 >= y = y
      
      plus(s(x),y) = y + 1 >= 1 = s(plus(x,y))
      
      sum(plus(cons(0(),x),cons(y,l))) = 1 >= 1 = pred(sum(cons(s(x),cons(y,l))))
      
      pred(cons(s(x),nil())) = 1 >= 1 = cons(x,nil())
     problem:
      DPs:
       
      TRS:
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       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)))))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
       pred(cons(s(x),nil())) -> cons(x,nil())
     Qed
    
    DPs:
     app#(cons(x,l),k) -> app#(l,k)
    TRS:
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     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)))))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
     pred(cons(s(x),nil())) -> cons(x,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       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)))))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
       pred(cons(s(x),nil())) -> cons(x,nil())
     Qed
    
    DPs:
     sum#(cons(x,cons(y,l))) -> sum#(cons(plus(x,y),l))
    TRS:
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     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)))))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
     pred(cons(s(x),nil())) -> cons(x,nil())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [sum#](x0) = x0 + 1,
      
      [pred](x0) = 1,
      
      [s](x0) = x0,
      
      [0] = 0,
      
      [plus](x0, x1) = x1 + 1,
      
      [sum](x0) = 1,
      
      [cons](x0, x1) = x1 + 1,
      
      [app](x0, x1) = x0 + x1,
      
      [nil] = 0
     orientation:
      sum#(cons(x,cons(y,l))) = l + 3 >= l + 2 = sum#(cons(plus(x,y),l))
      
      app(nil(),k) = k >= k = k
      
      app(l,nil()) = l >= l = l
      
      app(cons(x,l),k) = k + l + 1 >= k + l + 1 = cons(x,app(l,k))
      
      sum(cons(x,nil())) = 1 >= 1 = cons(x,nil())
      
      sum(cons(x,cons(y,l))) = 1 >= 1 = sum(cons(plus(x,y),l))
      
      sum(app(l,cons(x,cons(y,k)))) = 1 >= 1 = sum(app(l,sum(cons(x,cons(y,k)))))
      
      plus(0(),y) = y + 1 >= y = y
      
      plus(s(x),y) = y + 1 >= y + 1 = s(plus(x,y))
      
      sum(plus(cons(0(),x),cons(y,l))) = 1 >= 1 = pred(sum(cons(s(x),cons(y,l))))
      
      pred(cons(s(x),nil())) = 1 >= 1 = cons(x,nil())
     problem:
      DPs:
       
      TRS:
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       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)))))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
       pred(cons(s(x),nil())) -> cons(x,nil())
     Qed
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
     sum(cons(x,nil())) -> cons(x,nil())
     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)))))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
     pred(cons(s(x),nil())) -> cons(x,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       app(nil(),k) -> k
       app(l,nil()) -> l
       app(cons(x,l),k) -> cons(x,app(l,k))
       sum(cons(x,nil())) -> cons(x,nil())
       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)))))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
       pred(cons(s(x),nil())) -> cons(x,nil())
     Qed