YES(?,O(n^2))

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:
 Complexity Transformation Processor:
  strict:
   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())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [add] = 1,
     
     [curry] = 0,
     
     [s] = 0,
     
     [app](x0, x1) = x0 + x1,
     
     [0] = 0,
     
     [plus] = 0
    orientation:
     app(app(plus(),0()),y) = y >= y = y
     
     app(app(plus(),app(s(),x)),y) = x + y >= x + y = app(s(),app(app(plus(),x),y))
     
     app(app(app(curry(),f),x),y) = f + x + y >= f + x + y = app(app(f,x),y)
     
     add() = 1 >= 0 = app(curry(),plus())
    problem:
     strict:
      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)
     weak:
      add() -> app(curry(),plus())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [add] = 0,
       
       [curry] = 0,
       
       [s] = 0,
       
       [app](x0, x1) = x0 + x1,
       
       [0] = 1,
       
       [plus] = 0
      orientation:
       app(app(plus(),0()),y) = y + 1 >= y = y
       
       app(app(plus(),app(s(),x)),y) = x + y >= x + y = app(s(),app(app(plus(),x),y))
       
       app(app(app(curry(),f),x),y) = f + x + y >= f + x + y = app(app(f,x),y)
       
       add() = 0 >= 0 = app(curry(),plus())
      problem:
       strict:
        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)
       weak:
        app(app(plus(),0()),y) -> y
        add() -> app(curry(),plus())
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [add] = 1,
         
         [curry] = 1,
         
         [s] = 0,
         
         [app](x0, x1) = x0 + x1,
         
         [0] = 0,
         
         [plus] = 0
        orientation:
         app(app(plus(),app(s(),x)),y) = x + y >= x + y = app(s(),app(app(plus(),x),y))
         
         app(app(app(curry(),f),x),y) = f + x + y + 1 >= f + x + y = app(app(f,x),y)
         
         app(app(plus(),0()),y) = y >= y = y
         
         add() = 1 >= 1 = app(curry(),plus())
        problem:
         strict:
          app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
         weak:
          app(app(app(curry(),f),x),y) -> app(app(f,x),y)
          app(app(plus(),0()),y) -> y
          add() -> app(curry(),plus())
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                   [0]
           [add] = [1],
           
                     [0]
           [curry] = [0],
           
                 [1]
           [s] = [1],
           
                           [1 1]       
           [app](x0, x1) = [0 1]x0 + x1,
           
                 [0]
           [0] = [1],
           
                    [0]
           [plus] = [0]
          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 2]    [1 1]         [1 2]    [1 1]                       
           app(app(app(curry(),f),x),y) = [0 1]f + [0 1]x + y >= [0 1]f + [0 1]x + y = app(app(f,x),y)
           
                                        [1]         
           app(app(plus(),0()),y) = y + [1] >= y = y
           
                   [0]    [0]                      
           add() = [1] >= [0] = app(curry(),plus())
          problem:
           strict:
            
           weak:
            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)
            app(app(plus(),0()),y) -> y
            add() -> app(curry(),plus())
          Qed