YES(?,O(n^2))

Problem:
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(0(),s(y)) -> s(y)
 s(+(0(),y)) -> s(y)

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                  [8]
   [s](x0) = x0 + [1],
   
                      [1 1]     [8]
   [+](x0, x1) = x0 + [0 1]x1 + [0],
   
         [7]
   [0] = [9]
  orientation:
                  [24]         
   +(x,0()) = x + [9 ] >= x = x
   
                   [1 1]    [17]        [1 1]    [16]            
   +(x,s(y)) = x + [0 1]y + [1 ] >= x + [0 1]y + [1 ] = s(+(x,y))
   
                 [1 1]    [24]        [8]       
   +(0(),s(y)) = [0 1]y + [10] >= y + [1] = s(y)
   
                 [1 1]    [23]        [8]       
   s(+(0(),y)) = [0 1]y + [10] >= y + [1] = s(y)
  problem:
   
  Qed