YES

---- CR(R)
---- [Knuth and Bendix, 1970]
R:
s(p(x)) -> x
p(s(x)) -> x
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(x,p(y)) -> p(+(x,y))
-(x,0()) -> x
-(x,s(y)) -> p(-(x,y))
-(x,p(y)) -> s(-(x,y))
CP(R):
p(___y3) -> p(___y3)
+(___y8,___y7) -> s(+(___y8,p(___y7)))
-(___y16,___y15) -> p(-(___y16,p(___y15)))
s(___y21) -> s(___y21)
+(___y31,___y30) -> p(+(___y31,s(___y30)))
-(___y39,___y38) -> s(-(___y39,s(___y38)))