YES(?,O(n^2))

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

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