(VAR x1 x2 y1 y2 ) (RULES f(x1,g(x2)) -> f(x1,g(x1)) f(g(y1),y2) -> f(g(y1),g(y1)) g(a) -> g(b) b -> a f(g(b),y2) -> f(g(a),g(a)) )