YES (VAR x) (RULES g(x) -> f(f(x)) ) (COMMENT Termination is shown by LPO with precedence: g > f )