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