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