(VAR x y) (RULES +(0,0) -> 0 +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) ) (COMMENT doi:10.4230/LIPIcs.FSCD.2016.33 [36] Example 1 submitted by: Takahito Aoto )