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