--- Abstract Syntax Tree ------------------------
doubleList(Nil)
    = Nil{3}
doubleList(Cons(a,x))
    = Cons{7}(a{8},Cons{9}(a{10},doubleList{11}(x{12})))
--- Tree Automata -------------------------------
E9  <-- Cons(E10, E11)
    { \v1{a} v2{x} -> v1{a}*v2{x} }
E7  <-- Cons(E8, E9)
    { \v1{a} v2{a,x} -> v1{a}*v2{a,x} }
E3  <-- Nil
    { {} }
E12 <-- __
    { {x:__} }
E10 <-- __
    { {a:__} }
E8  <-- __
    { {a:__} }
E11 <-- FdoubleList
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
FdoubleList
    <-- E7
    { \v{a,x} -> {_1:Cons(v{a,x}.a,v{a,x}.x)} }
FdoubleList
    <-- E3
    { \v{} -> {_1:Nil} }
--- Guided Tree Automata ------------------------
{FdoubleList:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(3,1)
             0 --> Nil()
             1 --> Cons(4,2)
             2 --> Cons(3,1)
             2 --> Nil()
             3 --> __()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(12, 10)
                     { \x1_1 x2_1->
                       ((\v1{a} v2{a,x} -> v1{a}*v2{a,x} >2> \v{a,x} -> 
                                                             {_1:Cons(v{a,x}.a,v{a,x}.x)})
                        $
                        x1_1 x2_1) }
                 1   <-- Nil
                     { ((\v{} -> {_1:Nil}) $ ({})) }
                 8   <-- __
                     { _|_ }
             1:
                 10  <-- Cons(13, 11)
                     { \x1_1 x2_1-> ((\v1{a} v2{x} -> v1{a}*v2{x}) $ x1_1 x2_1) }
                 8   <-- __
                     { _|_ }
             2:
                 11  <-- Cons(12, 10)
                     { \x1_1 x2_1->
                       ((\v1{a} v2{a,x} -> v1{a}*v2{a,x} >2> (\v{a,x} -> 
                                                              {_1:Cons(v{a,x}.a,v{a,x}.x)})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 11  <-- Nil
                     { (((\v{} -> {_1:Nil})
                         >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) }
                 8   <-- __
                     { _|_ }
             3:
                 12  <-- __
                     { ({a:__}) }
             4:
                 13  <-- __
                     { ({a:__}) }
 E12:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }}

-- 0.01 seconds is elapsed.