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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
         [7]
   [s] = [0],
   
         [12]
   [0] = [13],
   
            [0]
   [plus] = [0],
   
                   [1 1]          [2]
   [app](x0, x1) = [0 1]x0 + x1 + [8],
   
          [7]
   [id] = [1]
  orientation:
                     [10]         
   app(id(),x) = x + [9 ] >= x = x
   
                     [14]    [7]       
   app(plus(),0()) = [21] >= [1] = id()
   
                                   [1 1]        [29]    [1 1]        [21]                                
   app(app(plus(),app(s(),x)),y) = [0 1]x + y + [24] >= [0 1]x + y + [24] = app(s(),app(app(plus(),x),y))
  problem:
   
  Qed