(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x xs ys) (DATATYPES A = µX.< Cons(X, X), Nil >) (SIGNATURES shuffle :: [A] -> A reverse :: [A] -> A append :: [A x A] -> A goal :: [A] -> A) (RULES shuffle(Cons(x,xs)) -> Cons(x ,shuffle(reverse(xs))) reverse(Cons(x,xs)) -> append(reverse(xs) ,Cons(x,Nil())) append(Cons(x,xs),ys) -> Cons(x ,append(xs,ys)) shuffle(Nil()) -> Nil() reverse(Nil()) -> Nil() append(Nil(),ys) -> ys goal(xs) -> shuffle(xs))