(STRATEGY
    INNERMOST)

(VAR
    x1 x2 x3 x4 x5 x7 x9)
(DATATYPES
    A = µX.< Leaf(X), cons_x(X), Node(X, X), comp_f_g(X, X), Cons(X, X), Nil >)
(SIGNATURES
    walk#1 :: [A] -> A
    comp_f_g#1 :: [A x A x A] -> A
    main :: [A] -> A)
(RULES
    walk#1(Leaf(x2)) -> cons_x(x2)
    walk#1(Node(x5,x3)) ->
      comp_f_g(walk#1(x5),walk#1(x3))
    comp_f_g#1(comp_f_g(x4,x5)
              ,comp_f_g(x2,x3)
              ,x1) -> comp_f_g#1(x4
                                ,x5
                                ,comp_f_g#1(x2,x3,x1))
    comp_f_g#1(comp_f_g(x7,x9)
              ,cons_x(x2)
              ,x4) -> comp_f_g#1(x7
                                ,x9
                                ,Cons(x2,x4))
    comp_f_g#1(cons_x(x2)
              ,comp_f_g(x5,x7)
              ,x3) -> Cons(x2
                          ,comp_f_g#1(x5,x7,x3))
    comp_f_g#1(cons_x(x5)
              ,cons_x(x2)
              ,x4) -> Cons(x5,Cons(x2,x4))
    main(Leaf(x4)) -> Cons(x4,Nil())
    main(Node(x9,x5)) ->
      comp_f_g#1(walk#1(x9)
                ,walk#1(x5)
                ,Nil()))