(VAR X) (RULES active(f(f(a))) -> mark(f(g(f(a)))) mark(f(X)) -> active(f(mark(X))) mark(a) -> active(a) mark(g(X)) -> active(g(X)) f(mark(X)) -> f(X) f(active(X)) -> f(X) g(mark(X)) -> g(X) g(active(X)) -> g(X) )