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