YES

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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  +(s(x17),x16) -> s(+(x17,x16))
  s(s(x20)) -> x20
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [+](x0, x1) = 6x0 + x1 + 2,
    
    [s](x0) = x0 + 2
   orientation:
    +(s(x17),x16) = x16 + 6x17 + 14 >= x16 + 6x17 + 4 = s(+(x17,x16))
    
    s(s(x20)) = x20 + 4 >= x20 = x20
   problem:
    
   Qed