YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(s(x),y) -> +(x,s(y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [s](x0) = x0 + 4,
    
    [+](x0, x1) = x0 + x1 + 29,
    
    [0] = 2
   orientation:
    +(0(),y) = y + 31 >= y = y
    
    +(s(x),y) = x + y + 33 >= x + y + 33 = s(+(x,y))
    
    +(s(x),y) = x + y + 33 >= x + y + 33 = +(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
    interpretation:
                    [0]
     [s](x0) = x0 + [1],
     
                   [1 1]     [1 1]  
     [+](x0, x1) = [0 1]x0 + [0 1]x1,
     
           [0]
     [0] = [0]
    orientation:
                 [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]            
     +(s(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = s(+(x,y))
     
                 [1 1]    [1 1]    [1]    [1 1]    [1 1]    [1]            
     +(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
     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