(STRATEGY INNERMOST) (VAR X XS) (DATATYPES A = µX.< cons(X, X), 0 >) (SIGNATURES zeros :: [] -> A tail :: [A] -> A) (RULES zeros() -> cons(0(),zeros()) tail(cons(X,XS)) -> XS)