(VAR X) (RULES f(X,g(X)) -> f(1,g(X)) g(1) -> g(0) )