(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR accu l orig x y) (DATATYPES A = µX.< nil, 0, cons(X, X), s(X), false, true, undefined >) (SIGNATURES length :: [A] -> A lt :: [A x A] -> A head :: [A] -> A tail :: [A] -> A reverse :: [A] -> A rev :: [A x A x A x A] -> A if :: [A x A x A x A x A] -> A) (RULES length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) head(cons(x,l)) -> x head(nil()) -> undefined() tail(nil()) -> nil() tail(cons(x,l)) -> l reverse(l) -> rev(0(),l,nil(),l) rev(x,l,accu,orig) -> if(lt(x ,length(orig)) ,x ,l ,accu ,orig) if(true(),x,l,accu,orig) -> rev(s(x) ,tail(l) ,cons(head(l),accu) ,orig) if(false(),x,l,accu,orig) -> accu)