(VAR X Y Z) (STRATEGY CONTEXTSENSITIVE (dbl 1) (0) (s) (dbls 1) (nil) (cons) (sel 1 2) (indx 1) (from) (dbl1 1) (01) (s1 1) (sel1 1 2) (quote 1) ) (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))) dbl1(0) -> 01 dbl1(s(X)) -> s1(s1(dbl1(X))) sel1(0,cons(X,Y)) -> X sel1(s(X),cons(Y,Z)) -> sel1(X,Z) quote(0) -> 01 quote(s(X)) -> s1(quote(X)) quote(dbl(X)) -> dbl1(X) quote(sel(X,Y)) -> sel1(X,Y) )