--- Abstract Syntax Tree ------------------------
treelist(BL)
    = Cons{3}(Nil{4},Nil{5})
treelist(BN(l,r))
    = lettreelist{9}(appn{10}(treelist{11}(l{12}),treelist{13}(r{14})))
lettreelist(Pair(n,Cons(r,rs)))
    = Cons{21}(n{22},Cons{23}(r{24},rs{25}))
incL(Nil)
    = Cons{30}(B0{31},Nil{32})
incL(Cons(B0,x))
    = Cons{36}(B1{37},x{38})
incL(Cons(B1,x))
    = Cons{42}(B0{43},incL{44}(x{45}))
appn(Nil,ys)
    = Pair{50}(Nil{51},ys{52})
appn(Cons(x,xs),ys)
    = letappend{57}(appn{58}(xs{59},ys{60}),x{61})
letappend(Pair(n,zs),x)
    = Pair{67}(incL{68}(n{69}),Cons{70}(x{71},zs{72}))
--- Tree Automata -------------------------------
E43 <-- B0
    { {} }
E31 <-- B0
    { {} }
E37 <-- B1
    { {} }
E70 <-- Cons(E71, E72)
    { \v1{x} v2{zs} -> v1{x}*v2{zs} }
E42 <-- Cons(E43, E44)
    { \v1{} v2{x} -> v1{}*v2{x} }
E36 <-- Cons(E37, E38)
    { \v1{} v2{x} -> v1{}*v2{x} }
E30 <-- Cons(E31, E32)
    { \v1{} v2{} -> v1{}*v2{} }
E23 <-- Cons(E24, E25)
    { \v1{r} v2{rs} -> v1{r}*v2{rs} }
E21 <-- Cons(E22, E23)
    { \v1{n} v2{r,rs} -> v1{n}*v2{r,rs} }
E3  <-- Cons(E4, E5)
    { \v1{} v2{} -> v1{}*v2{} }
E51 <-- Nil
    { {} }
E32 <-- Nil
    { {} }
E5  <-- Nil
    { {} }
E4  <-- Nil
    { {} }
E67 <-- Pair(E68, E70)
    { \v1{n} v2{x,zs} -> v1{n}*v2{x,zs} }
E50 <-- Pair(E51, E52)
    { \v1{} v2{ys} -> v1{}*v2{ys} }
E72 <-- __
    { {zs:__} }
E71 <-- __
    { {x:__} }
E69 <-- __
    { {n:__} }
E61 <-- __
    { {x:__} }
E60 <-- __
    { {ys:__} }
E59 <-- __
    { {xs:__} }
E52 <-- __
    { {ys:__} }
E45 <-- __
    { {x:__} }
E38 <-- __
    { {x:__} }
E25 <-- __
    { {rs:__} }
E24 <-- __
    { {r:__} }
E22 <-- __
    { {n:__} }
E14 <-- __
    { {r:__} }
E12 <-- __
    { {l:__} }
E68 <-- FincL
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
Fletappend
    <-- E67
    { \v{n,x,zs} -> 
      {_1:Pair(v{n,x,zs}.n,v{n,x,zs}.zs), _2:v{n,x,zs}.x} }
E58 <-- Fappn
    { \x{_1,_2} -> 
      let {v1{xs} = x{_1,_2}._1; v2{ys} = x{_1,_2}._2} in v1{xs}*v2{ys} }
E57 <-- Fletappend
    { \x{_1,_2} -> 
      let {v1{xs,ys} = @E58(x{_1,_2}._1); v2{x} = x{_1,_2}._2}
      in v1{xs,ys}*v2{x} }
Fappn
    <-- E57
    { \v{x,xs,ys} -> 
      {_1:Cons(v{x,xs,ys}.x,v{x,xs,ys}.xs), _2:v{x,xs,ys}.ys} }
Fappn
    <-- E50
    { \v{ys} -> {_1:Nil, _2:v{ys}.ys} }
E44 <-- FincL
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
FincL
    <-- E42
    { \v{x} -> {_1:Cons(B1,v{x}.x)} }
FincL
    <-- E36
    { \v{x} -> {_1:Cons(B0,v{x}.x)} }
FincL
    <-- E30
    { \v{} -> {_1:Nil} }
Flettreelist
    <-- E21
    { \v{n,r,rs} -> 
      {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))} }
E13 <-- Ftreelist
    { \x{_1} -> let {v1{r} = x{_1}._1} in v1{r} }
E11 <-- Ftreelist
    { \x{_1} -> let {v1{l} = x{_1}._1} in v1{l} }
E10 <-- Fappn
    { \x{_1,_2} -> 
      let {v1{l} = @E11(x{_1,_2}._1); v2{r} = @E13(x{_1,_2}._2)}
      in v1{l}*v2{r} }
E9  <-- Flettreelist
    { \x{_1} -> let {v1{l,r} = @E10(x{_1}._1)} in v1{l,r} }
Ftreelist
    <-- E9
    { \v{l,r} -> {_1:BN(v{l,r}.l,v{l,r}.r)} }
Ftreelist
    <-- E3
    { \v{} -> {_1:BL} }
--- Guided Tree Automata ------------------------
{Ftreelist:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> Nil()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(13, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> \v{} -> {_1:BL}) $ x1_1 x2_1) }
                 1   <-- Cons(13, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)}))
                        $
                        x1_2 x2_1) }
                 1   <-- Cons(14, 8)
                     { \x1_1 x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)}))
                        $
                        x1_1 x2_1) }
                 6   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(12, 11)
                     { \x1_1 x2_1-> ((\v1{r} v2{rs} -> v1{r}*v2{rs}) $ x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 6   <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({rs:__}) }
             3:
                 12  <-- __
                     { ({r:__}) }
             4:
                 13  <-- Nil
                     { ({}, {n:__}) }
                 14  <-- __
                     { ({n:__}) }
 E10:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> __()
             2 --> __()
             3 --> __()
             4 --> Cons(6,5)
             4 --> Nil()
             5 --> Cons(6,5)
             5 --> Nil()
             5 --> __()
             6 --> B0()
             6 --> B1()
             6 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(19, 7)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{n} v2{x,zs} -> v1{n}*v2{x,zs} >2> (\v{n,x,zs} -> 
                                                                {_1:Pair(v{n,x,zs}.n,v{n,x,zs}.zs),
                                                                 _2:v{n,x,zs}.x})
                                                               >>> (\x{_1,_2} -> 
                                                                    let {v1{xs,ys} = @E58(x{_1,_2}._1);
                                                                         v2{x} = x{_1,_2}._2}
                                                                    in v1{xs,ys}*v2{x})
                                                               >>> (\v{x,xs,ys} -> 
                                                                    {_1:Cons(v{x,xs,ys}.x,v{x,xs,ys}.xs),
                                                                     _2:v{x,xs,ys}.ys})
                                                               >>> (\x{_1,_2} -> 
                                                                    let {v1{l} = @E11(x{_1,_2}._1);
                                                                         v2{r} = @E13(x{_1,_2}._2)}
                                                                    in v1{l}*v2{r}))
                        $
                        x1_1 x2_2) }
                 1   <-- Pair(18, 6)
                     { \x1_1 x2_1->
                       ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:Nil, _2:v{ys}.ys})
                                                         >>> (\x{_1,_2} -> 
                                                              let {v1{l} = @E11(x{_1,_2}._1);
                                                                   v2{r} = @E13(x{_1,_2}._2)}
                                                              in v1{l}*v2{r}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(18, 7)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:Nil, _2:v{ys}.ys})
                                                         >>> (\x{_1,_2} -> 
                                                              let {v1{l} = @E11(x{_1,_2}._1);
                                                                   v2{r} = @E13(x{_1,_2}._2)}
                                                              in v1{l}*v2{r}))
                        $
                        x1_1 x2_1) }
                 26  <-- __
                     { _|_ }
             1:
                 7   <-- Cons(11, 10)
                     { \x1_1 x2_1->
                       ({ys:__}, (\v1{x} v2{zs} -> v1{x}*v2{zs}) $ x1_1 x2_1) }
                 6   <-- __
                     { ({ys:__}) }
             2:
                 10  <-- __
                     { ({zs:__}) }
             3:
                 11  <-- __
                     { ({x:__}) }
             4:
                 19  <-- Cons(27, 25)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B1,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_2) }
                 19  <-- Cons(28, 25)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 19  <-- Cons(27, 22)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 19  <-- Cons(28, 22)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_2) }
                 19  <-- Cons(28, 24)
                     { \x1_1 x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 18  <-- Nil
                     { ({}) }
                 26  <-- __
                     { _|_ }
             5:
                 24  <-- Cons(26, 25)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(27, 25)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B1,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_2 x2_2) }
                 25  <-- Cons(28, 25)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(26, 22)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(27, 22)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(27, 24)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(28, 22)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_2) }
                 25  <-- Cons(28, 24)
                     { \x1_1 x2_1->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(26, 24)
                     { \_ _-> ({x:__}) }
                 22  <-- Nil
                     { ({}, {x:__}) }
                 24  <-- __
                     { ({x:__}) }
             6:
                 27  <-- B0
                     { ({}, {}) }
                 28  <-- B1
                     { ({}) }
                 26  <-- __
                     { _|_ }
 E11:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> Nil()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Cons(13, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:BL})
                                                     >>> (\x{_1} -> 
                                                          let {v1{l} = x{_1}._1} in v1{l}))
                        $
                        x1_1 x2_1) }
                 3   <-- Cons(13, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l} = x{_1}._1}
                                                                    in v1{l}))
                        $
                        x1_2 x2_1) }
                 3   <-- Cons(14, 8)
                     { \x1_1 x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l} = x{_1}._1}
                                                                    in v1{l}))
                        $
                        x1_1 x2_1) }
                 6   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(12, 11)
                     { \x1_1 x2_1-> ((\v1{r} v2{rs} -> v1{r}*v2{rs}) $ x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 6   <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({rs:__}) }
             3:
                 12  <-- __
                     { ({r:__}) }
             4:
                 13  <-- Nil
                     { ({}, {n:__}) }
                 14  <-- __
                     { ({n:__}) }
 E12:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({l:__}) }
 E13:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(4,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> __()
             4 --> Nil()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Cons(13, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:BL})
                                                     >>> (\x{_1} -> 
                                                          let {v1{r} = x{_1}._1} in v1{r}))
                        $
                        x1_1 x2_1) }
                 3   <-- Cons(13, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{r} = x{_1}._1}
                                                                    in v1{r}))
                        $
                        x1_2 x2_1) }
                 3   <-- Cons(14, 8)
                     { \x1_1 x2_1->
                       ((\v1{n} v2{r,rs} -> v1{n}*v2{r,rs} >2> (\v{n,r,rs} -> 
                                                                {_1:Pair(v{n,r,rs}.n,Cons(v{n,r,rs}.r,v{n,r,rs}.rs))})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{l,r} = @E10(x{_1}._1)}
                                                                    in v1{l,r})
                                                               >>> (\v{l,r} -> 
                                                                    {_1:BN(v{l,r}.l,v{l,r}.r)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{r} = x{_1}._1}
                                                                    in v1{r}))
                        $
                        x1_1 x2_1) }
                 6   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(12, 11)
                     { \x1_1 x2_1-> ((\v1{r} v2{rs} -> v1{r}*v2{rs}) $ x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 6   <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({rs:__}) }
             3:
                 12  <-- __
                     { ({r:__}) }
             4:
                 13  <-- Nil
                     { ({}, {n:__}) }
                 14  <-- __
                     { ({n:__}) }
 E14:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({r:__}) }
 E45:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E58:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(4,1)
             1 --> Cons(3,2)
             1 --> __()
             2 --> __()
             3 --> __()
             4 --> Cons(6,5)
             4 --> Nil()
             5 --> Cons(6,5)
             5 --> Nil()
             5 --> __()
             6 --> B0()
             6 --> B1()
             6 --> __()
         GUIDED TRANSITIONS:
             0:
                 4   <-- Pair(19, 7)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{n} v2{x,zs} -> v1{n}*v2{x,zs} >2> (\v{n,x,zs} -> 
                                                                {_1:Pair(v{n,x,zs}.n,v{n,x,zs}.zs),
                                                                 _2:v{n,x,zs}.x})
                                                               >>> (\x{_1,_2} -> 
                                                                    let {v1{xs,ys} = @E58(x{_1,_2}._1);
                                                                         v2{x} = x{_1,_2}._2}
                                                                    in v1{xs,ys}*v2{x})
                                                               >>> (\v{x,xs,ys} -> 
                                                                    {_1:Cons(v{x,xs,ys}.x,v{x,xs,ys}.xs),
                                                                     _2:v{x,xs,ys}.ys})
                                                               >>> (\x{_1,_2} -> 
                                                                    let {v1{xs} = x{_1,_2}._1;
                                                                         v2{ys} = x{_1,_2}._2}
                                                                    in v1{xs}*v2{ys}))
                        $
                        x1_1 x2_2) }
                 4   <-- Pair(18, 6)
                     { \x1_1 x2_1->
                       ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:Nil, _2:v{ys}.ys})
                                                         >>> (\x{_1,_2} -> 
                                                              let {v1{xs} = x{_1,_2}._1;
                                                                   v2{ys} = x{_1,_2}._2}
                                                              in v1{xs}*v2{ys}))
                        $
                        x1_1 x2_1) }
                 4   <-- Pair(18, 7)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:Nil, _2:v{ys}.ys})
                                                         >>> (\x{_1,_2} -> 
                                                              let {v1{xs} = x{_1,_2}._1;
                                                                   v2{ys} = x{_1,_2}._2}
                                                              in v1{xs}*v2{ys}))
                        $
                        x1_1 x2_1) }
                 26  <-- __
                     { _|_ }
             1:
                 7   <-- Cons(11, 10)
                     { \x1_1 x2_1->
                       ({ys:__}, (\v1{x} v2{zs} -> v1{x}*v2{zs}) $ x1_1 x2_1) }
                 6   <-- __
                     { ({ys:__}) }
             2:
                 10  <-- __
                     { ({zs:__}) }
             3:
                 11  <-- __
                     { ({x:__}) }
             4:
                 19  <-- Cons(27, 25)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B1,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_2) }
                 19  <-- Cons(28, 25)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 19  <-- Cons(27, 22)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 19  <-- Cons(28, 22)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_2) }
                 19  <-- Cons(28, 24)
                     { \x1_1 x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> {_1:Cons(B0,v{x}.x)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 18  <-- Nil
                     { ({}) }
                 26  <-- __
                     { _|_ }
             5:
                 24  <-- Cons(26, 25)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(27, 25)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B1,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_2 x2_2) }
                 25  <-- Cons(28, 25)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(26, 22)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(27, 22)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(27, 24)
                     { \_ _-> ({x:__}) }
                 25  <-- Cons(28, 22)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_2) }
                 25  <-- Cons(28, 24)
                     { \x1_1 x2_1->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 24  <-- Cons(26, 24)
                     { \_ _-> ({x:__}) }
                 22  <-- Nil
                     { ({}, {x:__}) }
                 24  <-- __
                     { ({x:__}) }
             6:
                 27  <-- B0
                     { ({}, {}) }
                 28  <-- B1
                     { ({}) }
                 26  <-- __
                     { _|_ }
 E59:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({xs:__}) }
 E60:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({ys:__}) }
 E61:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E69:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }}

-- 0.10 seconds is elapsed.