--- Abstract Syntax Tree ------------------------
fib(Z)
    = S{3}(Z{4})
fib(S(n))
    = fib2{7}(n{8})
fib2(Z)
    = S{12}(S{13}(Z{14}))
fib2(S(m))
    = add{17}(fib{18}(S{19}(m{20})),fib{21}(m{22}))
add(Z,y)
    = y{27}
add(S(x),y)
    = S{31}(add{32}(x{33},y{34}))
--- Tree Automata -------------------------------
E31 <-- S(E32)
    { \v1{x,y} -> v1{x,y} }
E19 <-- S(E20)
    { \v1{m} -> v1{m} }
E13 <-- S(E14)
    { \v1{} -> v1{} }
E12 <-- S(E13)
    { \v1{} -> v1{} }
E3  <-- S(E4)
    { \v1{} -> v1{} }
E14 <-- Z
    { {} }
E4  <-- Z
    { {} }
E34 <-- __
    { {y:__} }
E33 <-- __
    { {x:__} }
E27 <-- __
    { {y:__} }
E22 <-- __
    { {m:__} }
E20 <-- __
    { {m:__} }
E8  <-- __
    { {n:__} }
E32 <-- Fadd
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
Fadd
    <-- E31
    { \v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y} }
Fadd
    <-- E27
    { \v{y} -> {_1:Z, _2:v{y}.y} }
E21 <-- Ffib
    { \x{_1} -> let {v1{m} = x{_1}._1} in v1{m} }
E18 <-- Ffib
    { \x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m} }
E17 <-- Fadd
    { \x{_1,_2} -> 
      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
      in v1{m}*v2{m} }
Ffib2
    <-- E17
    { \v{m} -> {_1:S(v{m}.m)} }
Ffib2
    <-- E12
    { \v{} -> {_1:Z} }
E7  <-- Ffib2
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
Ffib
    <-- E7
    { \v{n} -> {_1:S(v{n}.n)} }
Ffib
    <-- E3
    { \v{} -> {_1:Z} }
--- Guided Tree Automata ------------------------
{Ffib:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> __()
             1 --> S(2)
             1 --> Z()
             1 --> __()
             2 --> S(3)
             2 --> Z()
             2 --> __()
             3 --> S(3)
             3 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- S(5)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({y:__}))
                        | (((\v1{} -> v1{})
                            >>> ((\v{} -> {_1:Z})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)}))
                           $
                           x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)}))
                           $
                           x1_2)) }
                 0   <-- S(4)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({y:__}))
                        | (((\v1{} -> v1{}) >>> (\v{} -> {_1:Z})) $ x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)}))
                           $
                           x1_2)) }
                 0   <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)}))
                           $
                           x1_1)) }
                 0   <-- __
                     { (((\v{y} -> {_1:Z, _2:v{y}.y})
                         >>> (\x{_1,_2} -> 
                              let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                              in v1{m}*v2{m})
                         >>> ((\v{m} -> {_1:S(v{m}.m)})
                              >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                         >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({y:__})) }
             1:
                 5   <-- S(8)
                     { \(x1_1,x1_2)->
                       ((\v1{} -> v1{}) $ x1_1,   (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                                                | (((\v1{x,y} -> v1{x,y})
                                                    >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 4   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             2:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 8   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             3:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
 E8:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E18:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> __()
             1 --> S(2)
             1 --> Z()
             1 --> __()
             2 --> S(3)
             2 --> Z()
             2 --> __()
             3 --> S(3)
             3 --> __()
         GUIDED TRANSITIONS:
             0:
                 2   <-- S(5)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m})) $ ({y:__}))
                        | (((\v1{} -> v1{})
                            >>> ((\v{} -> {_1:Z})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m}))
                           $
                           x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m}))
                           $
                           x1_2)) }
                 2   <-- S(4)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m})) $ ({y:__}))
                        | (((\v1{} -> v1{})
                            >>> (\v{} -> {_1:Z})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m}))
                           $
                           x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m}))
                           $
                           x1_2)) }
                 2   <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = @E19(x{_1}._1)} in v1{m}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{y} -> {_1:Z, _2:v{y}.y})
                         >>> (\x{_1,_2} -> 
                              let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                              in v1{m}*v2{m})
                         >>> ((\v{m} -> {_1:S(v{m}.m)})
                              >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> 
                              let {v1{m} = @E19(x{_1}._1)} in v1{m})) $ ({y:__})) }
             1:
                 5   <-- S(8)
                     { \(x1_1,x1_2)->
                       ((\v1{} -> v1{}) $ x1_1,   (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                                                | (((\v1{x,y} -> v1{x,y})
                                                    >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 4   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             2:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 8   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             3:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
 E19:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- S(3)
                     { \x1_1-> ((\v1{m} -> v1{m}) $ x1_1) }
                 0   <-- __
                     { _|_ }
             1:
                 3   <-- __
                     { ({m:__}) }
 E21:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> __()
             1 --> S(2)
             1 --> Z()
             1 --> __()
             2 --> S(3)
             2 --> Z()
             2 --> __()
             3 --> S(3)
             3 --> __()
         GUIDED TRANSITIONS:
             0:
                 2   <-- S(5)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m})) $ ({y:__}))
                        | (((\v1{} -> v1{})
                            >>> ((\v{} -> {_1:Z})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m}))
                           $
                           x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m}))
                           $
                           x1_2)) }
                 2   <-- S(4)
                     { \(x1_1,x1_2)->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m})) $ ({y:__}))
                        | (((\v1{} -> v1{})
                            >>> (\v{} -> {_1:Z})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m}))
                           $
                           x1_1)
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m}))
                           $
                           x1_2)) }
                 2   <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                 in v1{m}*v2{m})
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> ((\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                                      in v1{m}*v2{m}))
                            >>> ((\v{m} -> {_1:S(v{m}.m)})
                                 >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{y} -> {_1:Z, _2:v{y}.y})
                         >>> (\x{_1,_2} -> 
                              let {v1{m} = @E18(x{_1,_2}._1); v2{m} = @E21(x{_1,_2}._2)}
                              in v1{m}*v2{m})
                         >>> ((\v{m} -> {_1:S(v{m}.m)})
                              >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{m} = x{_1}._1} in v1{m})) $ ({y:__})) }
             1:
                 5   <-- S(8)
                     { \(x1_1,x1_2)->
                       ((\v1{} -> v1{}) $ x1_1,   (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                                                | (((\v1{x,y} -> v1{x,y})
                                                    >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 4   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             2:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 8   <-- Z
                     { ({}, ((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
             3:
                 10  <-- S(10)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _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})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{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)) }
                 10  <-- __
                     { (((\v{y} -> {_1:Z, _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})) $ ({y:__})) }
 E22:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({m:__}) }
 E33:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E34:    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 (5,10) -- (6,1)
        S(Z{4})
    at (6,13) -- (8,1)
        fib2(n{8})
-- 0.11 seconds is elapsed.