YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
-(0(),x) -> 0()
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
CP(R):
0() -> 0()
0() -> 0()