YES

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

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