YES(?,O(n^2))

Problem:
 f(+(x,0())) -> f(x)
 +(x,+(y,z)) -> +(+(x,y),z)

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 1]     [0 ]
   [f](x0) = [0 1]x0 + [12],
   
                      [1 1]     [0]
   [+](x0, x1) = x0 + [0 1]x1 + [2],
   
         [4]
   [0] = [9]
  orientation:
                 [1 1]    [24]    [1 1]    [0 ]       
   f(+(x,0())) = [0 1]x + [23] >= [0 1]x + [12] = f(x)
   
                     [1 1]    [1 2]    [2]        [1 1]    [1 1]    [0]              
   +(x,+(y,z)) = x + [0 1]y + [0 1]z + [4] >= x + [0 1]y + [0 1]z + [4] = +(+(x,y),z)
  problem:
   
  Qed