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