YES

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

Proof:
 Church Rosser Transformation Processor (chew):
  The clusters for
   r1 = if(0(),y,z) -> y
   r2 = if(x,y,y) -> y
  have a trivial peak:
   x206 <- if(0(),x206,x207) -> x206
  The clusters for
   r1 = if(s(x),y,z) -> z
   r2 = if(x,y,y) -> y
  have a trivial peak:
   x207 <- if(s(x202),x206,x207) -> x207
  UNC by Chew's theorem.
  Qed