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