(VAR X Y Z ) (STRATEGY CONTEXTSENSITIVE (and 1) (true ) (false ) (if 1) (add 1) (0 ) (s ) (first 1 2) (nil ) (cons ) (from ) ) (RULES and(true, X) -> X and(false, Y) -> false if(true, X, Y) -> X if(false, X, Y) -> Y add(0, X) -> X add(s(X), Y) -> s(add(X, Y)) first(0, X) -> nil first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) from(X) -> cons(X, from(s(X))) )