TRS: { first(0(), X) -> nil(), first(s(X), cons(Y)) -> cons(Y), from(X) -> cons(X)} LMPO: Quasi-Precedence: empty Normal: pi(from) = [1], pi(first) = [1,2] Safe: Predicative System: { first(0(),X;) -> nil(), first(s(X;),cons(Y;);) -> cons(Y;), from(X;) -> cons(X;)} Qed