NO

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

Proof:
 Nonconfluence Processor:
  terms: +(f5(),f6()) *<- +(f5(),s(s(f6()))) ->* s(+(s(f6()),f5()))
  Qed
  
  first automaton:
   final states: {3}
   transitions:
    f6() -> 4*
    +(5,4) -> 3*
    f5() -> 5*
  
  second automaton:
   final states: {6}
   transitions:
    f6() -> 8*
    +(9,7) -> 10*
    s(8) -> 9*
    s(10) -> 6*
    f5() -> 7*