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