(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x y z) (DATATYPES A = µX.< nil, .(X, X), true, false >) (SIGNATURES rev :: [A] -> A car :: [A] -> A cdr :: [A] -> A null :: [A] -> A ++ :: [A x A] -> A) (RULES rev(nil()) -> nil() rev(.(x,y)) -> ++(rev(y) ,.(x,nil())) car(.(x,y)) -> x cdr(.(x,y)) -> y null(nil()) -> true() null(.(x,y)) -> false() ++(nil(),y) -> y ++(.(x,y),z) -> .(x,++(y,z)))