(STRATEGY
    INNERMOST)

(VAR
    m n x x' xs xs')
(DATATYPES
    A = µX.< Cons(X, X), Nil >)
(SIGNATURES
    ack :: [A x A] -> A
    goal :: [A x A] -> A)
(RULES
    ack(Cons(x,xs),Nil()) -> ack(xs
                                ,Cons(Nil(),Nil()))
    ack(Cons(x',xs'),Cons(x,xs)) ->
      ack(xs',ack(Cons(x',xs'),xs))
    ack(Nil(),n) -> Cons(Cons(Nil()
                             ,Nil())
                        ,n)
    goal(m,n) -> ack(m,n))