--- Abstract Syntax Tree ------------------------
taba_reverse_let(x)
    = letAt2{2}(h{7}(idshape{8}(x{9})))
letAt2(Pair(Nil,y))
    = y{10}
h(Pair(n,x))
    = hImpl{15}(n{16},x{17})
hImpl(Z,y)
    = Pair{22}(y{23},Nil{24})
hImpl(S(x),y)
    = letAt28{28}(hImpl{35}(x{36},y{37}))
letAt28(Pair(Cons(a,x1),y1))
    = Pair{38}(x1{39},Cons{40}(a{41},y1{42}))
idshape(Nil)
    = Pair{46}(Z{47},Nil{48})
idshape(Cons(a,x))
    = letAt52{52}(idshape{57}(x{58}),a{65})
letAt52(Pair(n,x),a)
    = Pair{59}(S{60}(n{61}),Cons{62}(a{63},x{64}))
--- Tree Automata -------------------------------
E62 <-- Cons(E63, E64)
    { \v1{a} v2{x} -> v1{a}*v2{x} }
E40 <-- Cons(E41, E42)
    { \v1{a} v2{y1} -> v1{a}*v2{y1} }
E48 <-- Nil
    { {} }
E24 <-- Nil
    { {} }
E59 <-- Pair(E60, E62)
    { \v1{n} v2{a,x} -> v1{n}*v2{a,x} }
E46 <-- Pair(E47, E48)
    { \v1{} v2{} -> v1{}*v2{} }
E38 <-- Pair(E39, E40)
    { \v1{x1} v2{a,y1} -> v1{x1}*v2{a,y1} }
E22 <-- Pair(E23, E24)
    { \v1{y} v2{} -> v1{y}*v2{} }
E60 <-- S(E61)
    { \v1{n} -> v1{n} }
E47 <-- Z
    { {} }
E64 <-- __
    { {x:__} }
E63 <-- __
    { {a:__} }
E61 <-- __
    { {n:__} }
E65 <-- __
    { {a:__} }
E58 <-- __
    { {x:__} }
E42 <-- __
    { {y1:__} }
E41 <-- __
    { {a:__} }
E39 <-- __
    { {x1:__} }
E37 <-- __
    { {y:__} }
E36 <-- __
    { {x:__} }
E23 <-- __
    { {y:__} }
E17 <-- __
    { {x:__} }
E16 <-- __
    { {n:__} }
E10 <-- __
    { {y:__} }
E9  <-- __
    { {x:__} }
FletAt52
    <-- E59
    { \v{a,n,x} -> {_1:Pair(v{a,n,x}.n,v{a,n,x}.x), _2:v{a,n,x}.a} }
E57 <-- Fidshape
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E52 <-- FletAt52
    { \x{_1,_2} -> 
      let {v1{x} = @E57(x{_1,_2}._1); v2{a} = x{_1,_2}._2}
      in v1{x}*v2{a} }
Fidshape
    <-- E52
    { \v{a,x} -> {_1:Cons(v{a,x}.a,v{a,x}.x)} }
Fidshape
    <-- E46
    { \v{} -> {_1:Nil} }
FletAt28
    <-- E38
    { \v{a,x1,y1} -> 
      {_1:Pair(Cons(v{a,x1,y1}.a,v{a,x1,y1}.x1),v{a,x1,y1}.y1)} }
E35 <-- FhImpl
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
E28 <-- FletAt28
    { \x{_1} -> let {v1{x,y} = @E35(x{_1}._1)} in v1{x,y} }
FhImpl
    <-- E28
    { \v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y} }
FhImpl
    <-- E22
    { \v{y} -> {_1:Z, _2:v{y}.y} }
E15 <-- FhImpl
    { \x{_1,_2} -> 
      let {v1{n} = x{_1,_2}._1; v2{x} = x{_1,_2}._2} in v1{n}*v2{x} }
Fh  <-- E15
    { \v{n,x} -> {_1:Pair(v{n,x}.n,v{n,x}.x)} }
FletAt2
    <-- E10
    { \v{y} -> {_1:Pair(Nil,v{y}.y)} }
E8  <-- Fidshape
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E7  <-- Fh
    { \x{_1} -> let {v1{x} = @E8(x{_1}._1)} in v1{x} }
E2  <-- FletAt2
    { \x{_1} -> let {v1{x} = @E7(x{_1}._1)} in v1{x} }
Ftaba_reverse_let
    <-- E2
    { \v{x} -> {_1:v{x}.x} }
--- Guided Tree Automata ------------------------
{Ftaba_reverse_let:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { (((\v{y} -> {_1:Pair(Nil,v{y}.y)})
                         >>> (\x{_1} -> let {v1{x} = @E7(x{_1}._1)} in v1{x})
                         >>> (\v{x} -> {_1:v{x}.x})) $ ({y:__})) }
 E7:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(12, 6)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{y} v2{} -> v1{y}*v2{} >2> (\v{y} -> {_1:Z, _2:v{y}.y})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{n} = x{_1,_2}._1;
                                                                 v2{x} = x{_1,_2}._2}
                                                            in v1{n}*v2{x})
                                                       >>> (\v{n,x} -> {_1:Pair(v{n,x}.n,v{n,x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{x} = @E8(x{_1}._1)} in v1{x}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(12, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{x1} v2{a,y1} -> v1{x1}*v2{a,y1} >2> (\v{a,x1,y1} -> 
                                                                  {_1:Pair(Cons(v{a,x1,y1}.a,v{a,x1,y1}.x1),v{a,x1,y1}.y1)})
                                                                 >>> (\x{_1} -> 
                                                                      let {v1{x,y} = @E35(x{_1}._1)}
                                                                      in v1{x,y})
                                                                 >>> ((\v{x,y} -> 
                                                                       {_1:S(v{x,y}.x),
                                                                        _2:v{x,y}.y})
                                                                      >>> (\x{_1,_2} -> 
                                                                           let {v1{n} = x{_1,_2}._1;
                                                                                v2{x} = x{_1,_2}._2}
                                                                           in v1{n}*v2{x}))
                                                                 >>> (\v{n,x} -> 
                                                                      {_1:Pair(v{n,x}.n,v{n,x}.x)})
                                                                 >>> (\x{_1} -> 
                                                                      let {v1{x} = @E8(x{_1}._1)}
                                                                      in v1{x}))
                        $
                        x1_2 x2_1) }
                 5   <-- __
                     { _|_ }
             1:
                 7   <-- Cons(11, 10)
                     { \x1_1 x2_1-> ((\v1{a} v2{y1} -> v1{a}*v2{y1}) $ x1_1 x2_1) }
                 6   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 10  <-- __
                     { ({y1:__}) }
             3:
                 11  <-- __
                     { ({a:__}) }
             4:
                 12  <-- __
                     { ({y:__}, {x1:__}) }
 E8:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> S(5)
             4 --> Z()
             5 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(14, 7)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(15, 8)
                     { \x1_1 x2_1->
                       ((\v1{n} v2{a,x} -> v1{n}*v2{a,x} >2> (\v{a,n,x} -> 
                                                              {_1:Pair(v{a,n,x}.n,v{a,n,x}.x),
                                                               _2:v{a,n,x}.a})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = @E57(x{_1,_2}._1);
                                                                       v2{a} = x{_1,_2}._2}
                                                                  in v1{x}*v2{a})
                                                             >>> (\v{a,x} -> 
                                                                  {_1:Cons(v{a,x}.a,v{a,x}.x)})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 13  <-- __
                     { _|_ }
             1:
                 8   <-- Cons(12, 11)
                     { \x1_1 x2_1-> ((\v1{a} v2{x} -> v1{a}*v2{x}) $ x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 13  <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({x:__}) }
             3:
                 12  <-- __
                     { ({a:__}) }
             4:
                 15  <-- S(17)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 14  <-- Z
                     { ({}) }
                 13  <-- __
                     { _|_ }
             5:
                 17  <-- __
                     { ({n:__}) }
 E9:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E16:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E17:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E35:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Pair(12, 6)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{y} v2{} -> v1{y}*v2{} >2> (\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}))
                        $
                        x1_1 x2_1) }
                 3   <-- Pair(12, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{x1} v2{a,y1} -> v1{x1}*v2{a,y1} >2> (\v{a,x1,y1} -> 
                                                                  {_1:Pair(Cons(v{a,x1,y1}.a,v{a,x1,y1}.x1),v{a,x1,y1}.y1)})
                                                                 >>> (\x{_1} -> 
                                                                      let {v1{x,y} = @E35(x{_1}._1)}
                                                                      in 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 x2_1) }
                 5   <-- __
                     { _|_ }
             1:
                 7   <-- Cons(11, 10)
                     { \x1_1 x2_1-> ((\v1{a} v2{y1} -> v1{a}*v2{y1}) $ x1_1 x2_1) }
                 6   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 10  <-- __
                     { ({y1:__}) }
             3:
                 11  <-- __
                     { ({a:__}) }
             4:
                 12  <-- __
                     { ({y:__}, {x1:__}) }
 E36:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E37:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }
 E57:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> S(5)
             4 --> Z()
             5 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Pair(14, 7)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 3   <-- Pair(15, 8)
                     { \x1_1 x2_1->
                       ((\v1{n} v2{a,x} -> v1{n}*v2{a,x} >2> (\v{a,n,x} -> 
                                                              {_1:Pair(v{a,n,x}.n,v{a,n,x}.x),
                                                               _2:v{a,n,x}.a})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = @E57(x{_1,_2}._1);
                                                                       v2{a} = x{_1,_2}._2}
                                                                  in v1{x}*v2{a})
                                                             >>> (\v{a,x} -> 
                                                                  {_1:Cons(v{a,x}.a,v{a,x}.x)})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 13  <-- __
                     { _|_ }
             1:
                 8   <-- Cons(12, 11)
                     { \x1_1 x2_1-> ((\v1{a} v2{x} -> v1{a}*v2{x}) $ x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 13  <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({x:__}) }
             3:
                 12  <-- __
                     { ({a:__}) }
             4:
                 15  <-- S(17)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 14  <-- Z
                     { ({}) }
                 13  <-- __
                     { _|_ }
             5:
                 17  <-- __
                     { ({n:__}) }
 E58:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E65:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }}

-- 0.06 seconds is elapsed.