YES

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

Proof:
 Church Rosser Transformation Processor:
  
  critical peaks: joinable
  Qed