(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR a b c k l x) (DATATYPES A = µX.< empty, cons(X, X) >) (SIGNATURES f :: [A x A] -> A g :: [A x A x A] -> A) (RULES f(empty(),l) -> l f(cons(x,k),l) -> g(k ,l ,cons(x,k)) g(a,b,c) -> f(a,cons(b,c)))