(VAR X Y) (RULES from(X) -> cons(X,from(s(X))) length(nil) -> 0 length(cons(X,Y)) -> s(length1(Y)) length1(X) -> length(X) )