(VAR y x) (RULES +(0,0) -> 0 +(s(0),y) -> s(+(0,y)) +(x,s(y)) -> s(+(y,x)) s(s(x)) -> x ) (COMMENT experiments for [36] submitted by: Takahito Aoto )