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