(STRATEGY
    INNERMOST)

(VAR
    x1 x16 x2 x4 x6 x8)
(DATATYPES
    A = µX.< Nil, Cons(X, X), Leaf(X), Node(X, X) >)
(SIGNATURES
    revApp#2 :: [A x A] -> A
    dfsAcc#3 :: [A x A] -> A
    main :: [A] -> A)
(RULES
    revApp#2(Nil(),x16) -> x16
    revApp#2(Cons(x6,x4),x2) ->
      revApp#2(x4,Cons(x6,x2))
    dfsAcc#3(Leaf(x8),x16) ->
      Cons(x8,x16)
    dfsAcc#3(Node(x6,x4),x2) ->
      dfsAcc#3(x4,dfsAcc#3(x6,x2))
    main(x1) -> revApp#2(dfsAcc#3(x1
                                 ,Nil())
                        ,Nil()))