(VAR x y) (RULES f(y,f(x,y)) -> f(f(a,y),f(a,x)) )