YES
TRS:
 { app(app(app(curry(), f), x), y) -> app(app(f, x), y),
  app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
          app(app(plus(), 0()), y) -> y,
                             add() -> app(curry(), plus())}
 RUF:
  Strict:
   { app(app(app(curry(), f), x), y) -> app(app(f, x), y),
    app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y))}
  Weak:
   {}
  RUF:
   Strict:
    {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y))}
   Weak:
    {}
   DP:
    Strict:
     {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y),
      app#(app(plus(), app(s(), x)), y) -> app#(plus(), x),
      app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))}
    Weak:
    {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y))}
    EDG:
     {(app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
      (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), 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)))}
     SCCS:
      Scc:
       {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)}
      SCC:
       Strict:
        {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)}
       Weak:
       {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y))}
       POLY:
        Argument Filtering:
         pi(s) = [], pi(plus) = [], pi(app#) = 0, pi(app) = [0,1]
        Usable Rules:
         {}
        Interpretation:
         [app](x0, x1) = x0 + x1,
         [s] = 1,
         [plus] = 0
        Strict:
         {}
        Weak:
         {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y))}
        Qed