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