YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
CP(R):
0() -> 0()
s(___y10) -> s(+(0(),___y10))
s(+(___y18,0())) -> s(___y18)
s(+(___y21,s(___y24))) -> s(+(s(___y21),___y24))
0() -> 0()
s(___y28) -> s(+(___y28,0()))
s(+(0(),___y36)) -> s(___y36)
s(+(s(___y40),___y39)) -> s(+(___y40,s(___y39)))