TRS: { first(0(), X) -> nil(), first(s(X), cons(Y)) -> cons(Y), from(X) -> cons(X)} MPO: Prec: first > nil, from > cons empty Strict: {} Weak: {} Qed