--- Abstract Syntax Tree ------------------------
reverse(Nil)
    = Nil{3}
reverse(Cons(a,x))
    = snoc{7}(reverse{8}(x{9}),a{10})
snoc(Nil,b)
    = Cons{15}(b{16},Nil{17})
snoc(Cons(a,x),b)
    = Cons{22}(a{23},snoc{24}(x{25},b{26}))
--- Tree Automata -------------------------------
E22 <-- Cons(E23, E24)
    { \v1{a} v2{b,x} -> v1{a}*v2{b,x} }
E15 <-- Cons(E16, E17)
    { \v1{b} v2{} -> v1{b}*v2{} }
E17 <-- Nil
    { {} }
E3  <-- Nil
    { {} }
E26 <-- __
    { {b:__} }
E25 <-- __
    { {x:__} }
E23 <-- __
    { {a:__} }
E16 <-- __
    { {b:__} }
E10 <-- __
    { {a:__} }
E9  <-- __
    { {x:__} }
E24 <-- Fsnoc
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{x}*v2{b} }
Fsnoc
    <-- E22
    { \v{a,b,x} -> {_1:Cons(v{a,b,x}.a,v{a,b,x}.x), _2:v{a,b,x}.b} }
Fsnoc
    <-- E15
    { \v{b} -> {_1:Nil, _2:v{b}.b} }
E8  <-- Freverse
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E7  <-- Fsnoc
    { \x{_1,_2} -> 
      let {v1{x} = @E8(x{_1,_2}._1); v2{a} = x{_1,_2}._2}
      in v1{x}*v2{a} }
Freverse
    <-- E7
    { \v{a,x} -> {_1:Cons(v{a,x}.a,v{a,x}.x)} }
Freverse
    <-- E3
    { \v{} -> {_1:Nil} }
--- Guided Tree Automata ------------------------
{Freverse:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             0 --> Nil()
             1 --> Cons(2,1)
             1 --> Nil()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{b,x} -> v1{a}*v2{b,x} >2> (\v{a,b,x} -> 
                                                              {_1:Cons(v{a,b,x}.a,v{a,b,x}.x),
                                                               _2:v{a,b,x}.b})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = @E8(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)}))
                        $
                        x1_2 x2_1) }
                 1   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Nil, _2:v{b}.b})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{x} = @E8(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)}))
                        $
                        x1_1 x2_1) }
                 1   <-- Nil
                     { ((\v{} -> {_1:Nil}) $ ({})) }
                 5   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{b,x} -> v1{a}*v2{b,x} >2> (\v{a,b,x} -> 
                                                              {_1:Cons(v{a,b,x}.a,v{a,b,x}.x),
                                                               _2:v{a,b,x}.b})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = x{_1,_2}._1;
                                                                       v2{b} = x{_1,_2}._2}
                                                                  in v1{x}*v2{b}))
                        $
                        x1_2 x2_1) }
                 8   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Nil, _2:v{b}.b})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{x} = x{_1,_2}._1;
                                                                 v2{b} = x{_1,_2}._2}
                                                            in v1{x}*v2{b}))
                        $
                        x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 9   <-- __
                     { ({b:__}, {a:__}) }
 E8:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             0 --> Nil()
             1 --> Cons(2,1)
             1 --> Nil()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{b,x} -> v1{a}*v2{b,x} >2> (\v{a,b,x} -> 
                                                              {_1:Cons(v{a,b,x}.a,v{a,b,x}.x),
                                                               _2:v{a,b,x}.b})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = @E8(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_2 x2_1) }
                 1   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Nil, _2:v{b}.b})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{x} = @E8(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) }
                 1   <-- Nil
                     { (((\v{} -> {_1:Nil})
                         >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) }
                 5   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{a} v2{b,x} -> v1{a}*v2{b,x} >2> (\v{a,b,x} -> 
                                                              {_1:Cons(v{a,b,x}.a,v{a,b,x}.x),
                                                               _2:v{a,b,x}.b})
                                                             >>> (\x{_1,_2} -> 
                                                                  let {v1{x} = x{_1,_2}._1;
                                                                       v2{b} = x{_1,_2}._2}
                                                                  in v1{x}*v2{b}))
                        $
                        x1_2 x2_1) }
                 8   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Nil, _2:v{b}.b})
                                                       >>> (\x{_1,_2} -> 
                                                            let {v1{x} = x{_1,_2}._1;
                                                                 v2{b} = x{_1,_2}._2}
                                                            in v1{x}*v2{b}))
                        $
                        x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 9   <-- __
                     { ({b:__}, {a:__}) }
 E9:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E10:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E25:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E26:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({b:__}) }}

-- 0.03 seconds is elapsed.