YES(?,O(n^2))

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

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