YES(?,O(n^2))

Problem:
 app(id(),x) -> x
 app(plus(),0()) -> id()
 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))

Proof:
 Complexity Transformation Processor:
  strict:
   app(id(),x) -> x
   app(plus(),0()) -> id()
   app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s] = 0,
     
     [0] = 0,
     
     [plus] = 0,
     
     [app](x0, x1) = x0 + x1,
     
     [id] = 1
    orientation:
     app(id(),x) = x + 1 >= x = x
     
     app(plus(),0()) = 0 >= 1 = id()
     
     app(app(plus(),app(s(),x)),y) = x + y >= x + y = app(s(),app(app(plus(),x),y))
    problem:
     strict:
      app(plus(),0()) -> id()
      app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
     weak:
      app(id(),x) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [s] = 0,
       
       [0] = 1,
       
       [plus] = 0,
       
       [app](x0, x1) = x0 + x1,
       
       [id] = 0
      orientation:
       app(plus(),0()) = 1 >= 0 = id()
       
       app(app(plus(),app(s(),x)),y) = x + y >= x + y = app(s(),app(app(plus(),x),y))
       
       app(id(),x) = x >= x = x
      problem:
       strict:
        app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
       weak:
        app(plus(),0()) -> id()
        app(id(),x) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
               [1]
         [s] = [1],
         
               [1]
         [0] = [1],
         
                  [0]
         [plus] = [0],
         
                         [1 1]       
         [app](x0, x1) = [0 1]x0 + x1,
         
                [1]
         [id] = [1]
        orientation:
                                         [1 1]        [3]    [1 1]        [2]                                
         app(app(plus(),app(s(),x)),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = app(s(),app(app(plus(),x),y))
         
                           [1]    [1]       
         app(plus(),0()) = [1] >= [1] = id()
         
                           [2]         
         app(id(),x) = x + [1] >= x = x
        problem:
         strict:
          
         weak:
          app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
          app(plus(),0()) -> id()
          app(id(),x) -> x
        Qed