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