YES(?,O(n^2))

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

Proof:
 Complexity Transformation Processor:
  strict:
   f(+(x,0())) -> f(x)
   +(x,+(y,z)) -> +(+(x,y),z)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [f](x0) = x0 + 1,
     
     [+](x0, x1) = x0 + x1,
     
     [0] = 1
    orientation:
     f(+(x,0())) = x + 2 >= x + 1 = f(x)
     
     +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
    problem:
     strict:
      +(x,+(y,z)) -> +(+(x,y),z)
     weak:
      f(+(x,0())) -> f(x)
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                 [1 0]  
       [f](x0) = [0 0]x0,
       
                          [1 1]     [0]
       [+](x0, x1) = x0 + [0 1]x1 + [1],
       
             [0]
       [0] = [0]
      orientation:
                         [1 1]    [1 2]    [1]        [1 1]    [1 1]    [0]              
       +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z)
       
                     [1 0]     [1 0]        
       f(+(x,0())) = [0 0]x >= [0 0]x = f(x)
      problem:
       strict:
        
       weak:
        +(x,+(y,z)) -> +(+(x,y),z)
        f(+(x,0())) -> f(x)
      Qed