YES
(VAR x y)
(RULES
plus(x,s(y)) -> s(plus(x,y))
plus(x,z()) -> x
)