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()}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(len) = [1], pi(from) = [1], pi(fst) = [1,2]
  
Safe:
   
  
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