(from AG01 3.23) (VAR x y) (RULES f(0,y) -> 0 f(s(x),y) -> f(f(x,y),y) )