(VAR X Y Z ) (RULES dbl(0) -> 0 dbl(s(X)) -> s(s(dbl(X))) dbls(nil) -> nil dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) sel(0, cons(X, Y)) -> X sel(s(X), cons(Y, Z)) -> sel(X, Z) indx(nil, X) -> nil indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) from(X) -> cons(X, from(s(X))) )