(STRATEGY INNERMOST) (VAR ) (DATATYPES A = µX.< 0, cons(X, X), s(X) >) (SIGNATURES f :: [A] -> A p :: [A] -> A) (RULES f(0()) -> cons(0(),f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0())