--- Abstract Syntax Tree ------------------------
myzip(Nil,Nil)
    = Nil{4}
myzip(Cons(a,x),Cons(b,y))
    = Cons{11}(Pair{12}(a{13},b{14}),myzip{15}(x{16},y{17}))
--- Tree Automata -------------------------------
E11 <-- Cons(E12, E15)
    { \v1{a,b} v2{x,y} -> v1{a,b}*v2{x,y} }
E4  <-- Nil
    { {} }
E12 <-- Pair(E13, E14)
    { \v1{a} v2{b} -> v1{a}*v2{b} }
E17 <-- __
    { {y:__} }
E16 <-- __
    { {x:__} }
E14 <-- __
    { {b:__} }
E13 <-- __
    { {a:__} }
E15 <-- Fmyzip
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
Fmyzip
    <-- E11
    { \v{a,b,x,y} -> 
      {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
       _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)} }
Fmyzip
    <-- E4
    { \v{} -> {_1:Nil, _2:Nil} }
--- Guided Tree Automata ------------------------
{Fmyzip: INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             0 --> Nil()
             1 --> Cons(2,1)
             1 --> Nil()
             2 --> Pair(4,3)
             3 --> __()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(8, 6)
                     { \x1_1 x2_1->
                       ((\v1{a,b} v2{x,y} -> v1{a,b}*v2{x,y} >2> \v{a,b,x,y} -> 
                                                                 {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                  _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                        $
                        x1_1 x2_1) }
                 1   <-- Nil
                     { ((\v{} -> {_1:Nil, _2:Nil}) $ ({})) }
                 7   <-- __
                     { _|_ }
             1:
                 6   <-- Cons(8, 6)
                     { \x1_1 x2_1->
                       ((\v1{a,b} v2{x,y} -> v1{a,b}*v2{x,y} >2> (\v{a,b,x,y} -> 
                                                                  {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                   _2:Cons(v{a,b,x,y}.b,v{a,b,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_1 x2_1) }
                 6   <-- Nil
                     { (((\v{} -> {_1:Nil, _2:Nil})
                         >>> (\x{_1,_2} -> 
                              let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2}
                              in v1{x}*v2{y})) $ ({})) }
                 7   <-- __
                     { _|_ }
             2:
                 8   <-- Pair(12, 11)
                     { \x1_1 x2_1-> ((\v1{a} v2{b} -> v1{a}*v2{b}) $ x1_1 x2_1) }
                 7   <-- __
                     { _|_ }
             3:
                 11  <-- __
                     { ({b:__}) }
             4:
                 12  <-- __
                     { ({a:__}) }
 E16:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E17:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }}

-- 0.02 seconds is elapsed.