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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
           [15]
   [add] = [8 ],
   
             [12]
   [curry] = [0 ],
   
         [0]
   [s] = [0],
   
                   [1 2]          [0]
   [app](x0, x1) = [0 1]x0 + x1 + [1],
   
         [2]
   [0] = [1],
   
            [2]
   [plus] = [5]
  orientation:
                                [28]         
   app(app(plus(),0()),y) = y + [8 ] >= y = y
   
                                   [1 2]        [26]    [1 2]        [24]                                
   app(app(plus(),app(s(),x)),y) = [0 1]x + y + [8 ] >= [0 1]x + y + [8 ] = app(s(),app(app(plus(),x),y))
   
                                  [1 4]    [1 2]        [18]    [1 4]    [1 2]        [2]                  
   app(app(app(curry(),f),x),y) = [0 1]f + [0 1]x + y + [3 ] >= [0 1]f + [0 1]x + y + [2] = app(app(f,x),y)
   
           [15]    [14]                      
   add() = [8 ] >= [6 ] = app(curry(),plus())
  problem:
   
  Qed