(VAR X Y Z) (RULES sel(s(X),cons(Y,Z)) -> sel(X,Z) sel(0,cons(X,Z)) -> X first(0,Z) -> nil first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z)) from(X) -> cons(X,from(s(X))) sel1(s(X),cons(Y,Z)) -> sel1(X,Z) sel1(0,cons(X,Z)) -> quote(X) first1(0,Z) -> nil1 first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z)) quote(0) -> 01 quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z)) quote1(nil) -> nil1 quote(s(X)) -> s1(quote(X)) quote(sel(X,Z)) -> sel1(X,Z) quote1(first(X,Z)) -> first1(X,Z) unquote(01) -> 0 unquote(s1(X)) -> s(unquote(X)) unquote1(nil1) -> nil unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) fcons(X,Z) -> cons(X,Z) )