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