YES(?,O(n^2))

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

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