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