--- Abstract Syntax Tree ------------------------
snoc(Nil,y)
    = Cons{4}(y{5},Nil{6})
snoc(Cons(a,x),y)
    = Cons{11}(a{12},snoc{13}(x{14},y{15}))
--- Tree Automata -------------------------------
E11 <-- Cons(E12, E13)
    { \v1{a} v2{x,y} -> v1{a}*v2{x,y} }
E4  <-- Cons(E5, E6)
    { \v1{y} v2{} -> v1{y}*v2{} }
E6  <-- Nil
    { {} }
E15 <-- __
    { {y:__} }
E14 <-- __
    { {x:__} }
E12 <-- __
    { {a:__} }
E5  <-- __
    { {y:__} }
E13 <-- Fsnoc
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
Fsnoc
    <-- E11
    { \v{a,x,y} -> {_1:Cons(v{a,x,y}.a,v{a,x,y}.x), _2:v{a,x,y}.y} }
Fsnoc
    <-- E4
    { \v{y} -> {_1:Nil, _2:v{y}.y} }
--- Guided Tree Automata ------------------------
{Fsnoc:  INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> Cons(2,1)
             1 --> Nil()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{x,y} -> v1{a}*v2{x,y} >2> \v{a,x,y} -> 
                                                             {_1:Cons(v{a,x,y}.a,v{a,x,y}.x),
                                                              _2:v{a,x,y}.y})
                        $
                        x1_2 x2_1) }
                 1   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{y} v2{} -> v1{y}*v2{} >2> \v{y} -> {_1:Nil, _2:v{y}.y})
                        $
                        x1_1 x2_1) }
                 5   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{x,y} -> v1{a}*v2{x,y} >2> (\v{a,x,y} -> 
                                                              {_1:Cons(v{a,x,y}.a,v{a,x,y}.x),
                                                               _2:v{a,x,y}.y})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = x{_1,_2}._1;
                                                                       v2{y} = x{_1,_2}._2}
                                                                  in v1{x}*v2{y}))
                        $
                        x1_2 x2_1) }
                 8   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{y} v2{} -> v1{y}*v2{} >2> (\v{y} -> {_1:Nil, _2:v{y}.y})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{x} = x{_1,_2}._1;
                                                                 v2{y} = x{_1,_2}._2}
                                                            in v1{x}*v2{y}))
                        $
                        x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 9   <-- __
                     { ({y:__}, {a:__}) }
 E14:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E15:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }}

-- 0.01 seconds is elapsed.