YES

1 decompositions
 #1 -----------
   1: +(0(),x1) -> x1
   2: +(s(x2),x3) -> s(+(x2,x3))
   3: s(s(x4)) -> x4

@Knuth and Bendix' criterion
--- R
   1: +(0(),x1) -> x1
   2: +(s(x2),x3) -> s(+(x2,x3))
   3: s(s(x4)) -> x4

--- S
   1: +(0(),x1) -> x1
   2: +(s(x2),x3) -> s(+(x2,x3))
   3: s(s(x4)) -> x4