--- Abstract Syntax Tree ------------------------
zip(Nil,y)
    = Nil{5}
zip(Cons(a,x),Nil)
    = Nil{10}
zip(Cons(a,x),Cons(b,y))
    = Cons{17}(Pair{18}(a{19},b{20}),zip{21}(x{22},y{23}))
--- Tree Automata -------------------------------
E17 <-- Cons(E18, E21)
    { \v1{a,b} v2{x,y} -> v1{a,b}*v2{x,y} }
E10 <-- Nil
    { {} }
E5  <-- Nil
    { {} }
E18 <-- Pair(E19, E20)
    { \v1{a} v2{b} -> v1{a}*v2{b} }
E23 <-- __
    { {y:__} }
E22 <-- __
    { {x:__} }
E20 <-- __
    { {b:__} }
E19 <-- __
    { {a:__} }
E21 <-- Fzip
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
Fzip
    <-- E17
    { \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)} }
Fzip
    <-- E10
    { \v{} -> {_1:Cons(v{}.a,v{}.x), _2:Nil} }
Fzip
    <-- E5
    { \v{} -> {_1:Nil, _2:v{}.y} }
--- Guided Tree Automata ------------------------
{Fzip:   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:Cons(v{}.a,v{}.x), _2:Nil}) $ ({}))
                        | ((\v{} -> {_1:Nil, _2:v{}.y}) $ ({}))) }
                 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:Cons(v{}.a,v{}.x), _2:Nil})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2}
                                 in v1{x}*v2{y})) $ ({}))
                        | (((\v{} -> {_1:Nil, _2:v{}.y})
                            >>> (\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:__}) }
 E22:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E23:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }}
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons: 
Possibly range-overlapping expressions: 
    at (3,22) -- (4,1)
        Nil
    at (4,22) -- (5,1)
        Nil
-- 0.02 seconds is elapsed.