TRS: {f(x, y) -> h(x, y), f(x, y) -> h(y, x), h(x, x) -> x} POP*: Precedence: f > h empty Normal: pi(f) = [1,2], pi(h) = [2] Safe: pi(h) = [1] Predicative System: {f(x,y;) -> h(y;x), f(x,y;) -> h(x;y), h(x;x) -> x} Qed