(VAR x y)
(RULES
  +(0,y) -> y
  +(s(x),y) -> s(+(x,y))
  +(x,0) -> x
  +(x,s(y)) -> s(+(x,y))
)
(COMMENT
doi:10.1017/CBO9781139172752
[4] Exercise 6.5(b)
submitted by: Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama
)