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())
  Usable Rule 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:
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
    sum(cons(x,nil())) -> cons(x,nil())
    app(nil(),k) -> k
    app(l,nil()) -> l
    app(cons(x,l),k) -> cons(x,app(l,k))
   Matrix Interpretation Processor: dim=3
    
    usable rules:
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
     sum(cons(x,nil())) -> cons(x,nil())
     app(nil(),k) -> k
     app(l,nil()) -> l
     app(cons(x,l),k) -> cons(x,app(l,k))
    interpretation:
     [pred#](x0) = [0],
     
     [plus#](x0, x1) = [0 1 0]x0,
     
     [sum#](x0) = [0 1 0]x0,
     
     [app#](x0, x1) = [0 1 0]x0 + [1],
     
               [0 0 0]     [0]
     [s](x0) = [0 1 0]x0 + [1]
               [0 0 0]     [0],
     
           [1]
     [0] = [1]
           [0],
     
                      [0 0 0]     [1 0 0]  
     [plus](x0, x1) = [0 1 0]x0 + [0 1 0]x1
                      [0 0 0]     [0 1 1]  ,
     
                 [0 0 0]     [1]
     [sum](x0) = [0 1 0]x0 + [0]
                 [0 1 0]     [0],
     
                      [0 0 0]     [0 1 1]     [1]
     [cons](x0, x1) = [1 1 0]x0 + [0 1 0]x1 + [1]
                      [1 1 0]     [0 0 0]     [0],
     
                     [1 1 0]     [1 1 1]     [1]
     [app](x0, x1) = [0 1 0]x0 + [1 1 0]x1 + [1]
                     [0 0 1]     [0 0 1]     [1],
     
             [0]
     [nil] = [0]
             [0]
    orientation:
     app#(cons(x,l),k) = [0 1 0]l + [1 1 0]x + [2] >= [0 1 0]l + [1] = app#(l,k)
     
     sum#(cons(x,cons(y,l))) = [0 1 0]l + [1 1 0]x + [1 1 0]y + [2] >= [0 1 0]x = plus#(x,y)
     
     sum#(cons(x,cons(y,l))) = [0 1 0]l + [1 1 0]x + [1 1 0]y + [2] >= [0 1 0]l + [0 1 0]x + [1 1 0]y + [1] = sum#(cons(plus(x,y),l))
     
     sum#(app(l,cons(x,cons(y,k)))) = [0 2 0]k + [0 1 0]l + [1 1 0]x + [3 3 0]y + [5] >= [0 1 0]k + [1 1 0]x + [1 1 0]y + [2] = sum#(cons(x,cons(y,k)))
     
     sum#(app(l,cons(x,cons(y,k)))) = [0 2 0]k + [0 1 0]l + [1 1 0]x + [3 3 0]y + [5] >= [0 1 0]l + [1] = app#(l,sum(cons(x,cons(y,k))))
     
     sum#(app(l,cons(x,cons(y,k)))) = [0 2 0]k + [0 1 0]l + [1 1 0]x + [3 3 0]y + [5] >= [0 1 0]k + [0 1 0]l + [1 1 0]x + [1 1 0]y + [4] = sum#(app(l,sum(cons(x,cons(y,k)))))
     
     plus#(s(x),y) = [0 1 0]x + [1] >= [0 1 0]x = plus#(x,y)
     
     sum#(plus(cons(0(),x),cons(y,l))) = [0 1 0]l + [0 1 0]x + [1 1 0]y + [4] >= [0 1 0]l + [0 1 0]x + [1 1 0]y + [3] = sum#(cons(s(x),cons(y,l)))
     
     sum#(plus(cons(0(),x),cons(y,l))) = [0 1 0]l + [0 1 0]x + [1 1 0]y + [4] >= [0] = pred#(sum(cons(s(x),cons(y,l))))
     
                   [1 0 0]    [0]         
     plus(0(),y) = [0 1 0]y + [1] >= y = y
                   [0 1 1]    [0]         
     
                    [0 0 0]    [1 0 0]    [0]    [0 0 0]    [0 0 0]    [0]               
     plus(s(x),y) = [0 1 0]x + [0 1 0]y + [1] >= [0 1 0]x + [0 1 0]y + [1] = s(plus(x,y))
                    [0 0 0]    [0 1 1]    [0]    [0 0 0]    [0 0 0]    [0]               
     
                              [0 0 0]    [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [0 0 0]    [1]                         
     sum(cons(x,cons(y,l))) = [0 1 0]l + [1 1 0]x + [1 1 0]y + [2] >= [0 1 0]l + [0 1 0]x + [1 1 0]y + [1] = sum(cons(plus(x,y),l))
                              [0 1 0]    [1 1 0]    [1 1 0]    [2]    [0 1 0]    [0 1 0]    [1 1 0]    [1]                         
     
                          [0 0 0]    [1]    [0 0 0]    [1]                
     sum(cons(x,nil())) = [1 1 0]x + [1] >= [1 1 0]x + [1] = cons(x,nil())
                          [1 1 0]    [1]    [1 1 0]    [0]                
     
                    [1 1 1]    [1]         
     app(nil(),k) = [1 1 0]k + [1] >= k = k
                    [0 0 1]    [1]         
     
                    [1 1 0]    [1]         
     app(l,nil()) = [0 1 0]l + [1] >= l = l
                    [0 0 1]    [1]         
     
                        [1 1 1]    [0 2 1]    [1 1 0]    [3]    [1 1 1]    [0 1 1]    [0 0 0]    [3]                   
     app(cons(x,l),k) = [1 1 0]k + [0 1 0]l + [1 1 0]x + [2] >= [1 1 0]k + [0 1 0]l + [1 1 0]x + [2] = cons(x,app(l,k))
                        [0 0 1]    [0 0 0]    [1 1 0]    [1]    [0 0 0]    [0 0 0]    [1 1 0]    [0]                   
    problem:
     DPs:
      
     TRS:
      plus(0(),y) -> y
      plus(s(x),y) -> s(plus(x,y))
      sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
      sum(cons(x,nil())) -> cons(x,nil())
      app(nil(),k) -> k
      app(l,nil()) -> l
      app(cons(x,l),k) -> cons(x,app(l,k))
    Qed