(STRATEGY
    INNERMOST)

(VAR
    rest revprefix x x' xs)
(DATATYPES
    A = µX.< Cons(X, X), Nil >)
(SIGNATURES
    select :: [A x A x A] -> A
    revapp :: [A x A] -> A
    permute :: [A] -> A
    mapconsapp :: [A x A x A] -> A
    goal :: [A] -> A)
(RULES
    select(x'
          ,revprefix
          ,Cons(x,xs)) -> mapconsapp(x'
                                    ,permute(revapp(revprefix
                                                   ,Cons(x,xs)))
                                    ,select(x
                                           ,Cons(x',revprefix)
                                           ,xs))
    revapp(Cons(x,xs),rest) ->
      revapp(xs,Cons(x,rest))
    permute(Cons(x,xs)) -> select(x
                                 ,Nil()
                                 ,xs)
    mapconsapp(x'
              ,Cons(x,xs)
              ,rest) -> Cons(Cons(x',x)
                            ,mapconsapp(x',xs,rest))
    select(x,revprefix,Nil()) ->
      mapconsapp(x
                ,permute(revapp(revprefix
                               ,Nil()))
                ,Nil())
    revapp(Nil(),rest) -> rest
    permute(Nil()) -> Cons(Nil()
                          ,Nil())
    mapconsapp(x,Nil(),rest) -> rest
    goal(xs) -> permute(xs))