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