YES

Problem:
 app(app(plus(),0()),y) -> y
 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
 app(app(app(curry(),f),x),y) -> app(app(f,x),y)
 add() -> app(curry(),plus())

Proof:
 DP Processor:
  DPs:
   app#(app(plus(),app(s(),x)),y) -> app#(plus(),x)
   app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y)
   app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y))
   app#(app(app(curry(),f),x),y) -> app#(f,x)
   app#(app(app(curry(),f),x),y) -> app#(app(f,x),y)
   add#() -> app#(curry(),plus())
  TRS:
   app(app(plus(),0()),y) -> y
   app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
   app(app(app(curry(),f),x),y) -> app(app(f,x),y)
   add() -> app(curry(),plus())
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [add#] = 4,
    
    [app#](x0, x1) = 2x0 + x1 + 1,
    
    [add] = 3,
    
    [curry] = 1,
    
    [s] = 0,
    
    [app](x0, x1) = 2x0 + x1 + 1,
    
    [0] = 4,
    
    [plus] = 0
   orientation:
    app#(app(plus(),app(s(),x)),y) = 2x + y + 5 >= x + 1 = app#(plus(),x)
    
    app#(app(plus(),app(s(),x)),y) = 2x + y + 5 >= 2x + y + 3 = app#(app(plus(),x),y)
    
    app#(app(plus(),app(s(),x)),y) = 2x + y + 5 >= 2x + y + 4 = app#(s(),app(app(plus(),x),y))
    
    app#(app(app(curry(),f),x),y) = 4f + 2x + y + 15 >= 2f + x + 1 = app#(f,x)
    
    app#(app(app(curry(),f),x),y) = 4f + 2x + y + 15 >= 4f + 2x + y + 3 = app#(app(f,x),y)
    
    add#() = 4 >= 3 = app#(curry(),plus())
    
    app(app(plus(),0()),y) = y + 11 >= y = y
    
    app(app(plus(),app(s(),x)),y) = 2x + y + 5 >= 2x + y + 4 = app(s(),app(app(plus(),x),y))
    
    app(app(app(curry(),f),x),y) = 4f + 2x + y + 15 >= 4f + 2x + y + 3 = app(app(f,x),y)
    
    add() = 3 >= 3 = app(curry(),plus())
   problem:
    DPs:
     
    TRS:
     app(app(plus(),0()),y) -> y
     app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
     app(app(app(curry(),f),x),y) -> app(app(f,x),y)
     add() -> app(curry(),plus())
   Qed