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