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