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