YES
TRS:
 {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                      app(id(), x) -> x,
                  app(plus(), 0()) -> id()}
 RUF:
  Strict:
   {app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                        app(id(), x) -> x}
  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#(s(), 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#(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