--- Abstract Syntax Tree ------------------------
reverse(x)
    = rev{2}(x{3},Nil{4})
rev(Nil,y)
    = y{9}
rev(Cons(a,x),y)
    = rev{14}(x{15},Cons{16}(a{17},y{18}))
--- Tree Automata -------------------------------
E16 <-- Cons(E17, E18)
    { \v1{a} v2{y} -> v1{a}*v2{y} }
E4  <-- Nil
    { {} }
E18 <-- __
    { {y:__} }
E17 <-- __
    { {a:__} }
E15 <-- __
    { {x:__} }
E9  <-- __
    { {y:__} }
E3  <-- __
    { {x:__} }
E14 <-- Frev
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{a,y} = @E16(x{_1,_2}._2)}
      in v1{x}*v2{a,y} }
Frev
    <-- E14
    { \v{a,x,y} -> {_1:Cons(v{a,x,y}.a,v{a,x,y}.x), _2:v{a,x,y}.y} }
Frev
    <-- E9
    { \v{y} -> {_1:Nil, _2:v{y}.y} }
E2  <-- Frev
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{} }
Freverse
    <-- E2
    { \v{x} -> {_1:v{x}.x} }
--- Guided Tree Automata ------------------------
{Freverse:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { (  (((\v{y} -> {_1:Nil, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{})
                            >>> (\v{x} -> {_1:v{x}.x})) $ ({y:__}))
                        | (((\v{y} -> {_1:Nil, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{a,y} = @E16(x{_1,_2}._2)}
                                 in v1{x}*v2{a,y})
                            >>> ((\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{} = @E4(x{_1,_2}._2)}
                                      in v1{x}*v2{}))
                            >>> (\v{x} -> {_1:v{x}.x})) $ ({y:__}))
                        | (((\v{y} -> {_1:Nil, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{a,y} = @E16(x{_1,_2}._2)}
                                 in v1{x}*v2{a,y})
                            >>> (fixA[(\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{a,y} = @E16(x{_1,_2}._2)}
                                           in v1{x}*v2{a,y})])
                            >>> ((\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{} = @E4(x{_1,_2}._2)}
                                      in v1{x}*v2{}))
                            >>> (\v{x} -> {_1:v{x}.x})) $ ({y:__}))) }
 E3:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E4:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Nil()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Nil
                     { ({}) }
                 0   <-- __
                     { _|_ }
 E15:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E16:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> __()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(5, 4)
                     { \x1_1 x2_1-> ((\v1{a} v2{y} -> v1{a}*v2{y}) $ x1_1 x2_1) }
                 0   <-- __
                     { _|_ }
             1:
                 4   <-- __
                     { ({y:__}) }
             2:
                 5   <-- __
                     { ({a:__}) }}
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons: 
Possibly range-overlapping expressions: 
    at (5,20) -- (6,1)
        y
    at (6,20) -- (7,1)
        rev(x{15},Cons{16}(a{17},y{18}))
-- 0.01 seconds is elapsed.