TRS: { fst(0(), Z) -> nil(), fst(s(), cons(Y)) -> cons(Y), from(X) -> cons(X), add(0(), X) -> X, add(s(), Y) -> s(), len(nil()) -> 0(), len(cons(X)) -> s()} POP*: Quasi-Precedence: len > 0 ~ nil, len > s, from > cons 0 ~ nil Normal: pi(len) = [1], pi(from) = [1], pi(fst) = [1,2] Safe: pi(cons) = [1] Predicative System: { fst(0(),Z;) -> nil(), fst(s(),cons(;Y);) -> cons(;Y), from(X;) -> cons(;X), add(0(),X;) -> X, add(s(),Y;) -> s(), len(nil();) -> 0(), len(cons(;X);) -> s()} Qed