YES

---- CR(R)
---- Rule Labeling [van Oostrom, RTA 2008].
R:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
inc(x) -> s(x)
+(x,y) -> +(y,x)
inc(+(x,y)) -> +(inc(x),y)

Label:
[+(x,0()) -> x] = 4
[+(x,s(y)) -> s(+(x,y))] = 4
[+(0(),y) -> y] = 4
[+(s(x),y) -> s(+(x,y))] = 4
[inc(x) -> s(x)] = 0
[+(x,y) -> +(y,x)] = 8
[inc(+(x,y)) -> +(inc(x),y)] = 7