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