(VAR X Y Z) (RULES fst(0,Z) -> nil fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z)) from(X) -> cons(X,from(s(X))) add(0,X) -> X add(s(X),Y) -> s(add(X,Y)) len(nil) -> 0 len(cons(X,Z)) -> s(len(Z)) )