YES

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