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