(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))