YES(?,O(n^2))

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

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