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))

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