(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x) (DATATYPES A = µX.< s(X) >) (SIGNATURES f :: [A] -> A) (RULES f(x) -> s(x) f(s(s(x))) -> s(f(f(x))))