YES

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

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [s](x0) = x0,
   
   [+](x0, x1) = x0 + x1 + 6,
   
   [0] = 1
  orientation:
   +(0(),y) = y + 7 >= y = y
   
   +(s(x),y) = x + y + 6 >= x + y + 6 = s(+(x,y))
   
   +(s(x),y) = x + y + 6 >= x + y + 6 = +(x,s(y))
  problem:
   +(s(x),y) -> s(+(x,y))
   +(s(x),y) -> +(x,s(y))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [s](x0) = x0 + 1,
    
    [+](x0, x1) = 2x0 + x1
   orientation:
    +(s(x),y) = 2x + y + 2 >= 2x + y + 1 = s(+(x,y))
    
    +(s(x),y) = 2x + y + 2 >= 2x + y + 1 = +(x,s(y))
   problem:
    
   Qed