YES

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

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