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