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