--- Abstract Syntax Tree ------------------------
runlength(Nil)
    = Nil{3}
runlength(Cons(a,x))
    = f{7}(runlength{8}(x{9}),a{10})
f(Nil,a)
    = Cons{15}(Pair{16}(a{17},Cons{18}(B0{19},Nil{20})),Nil{21})
f(Cons(Pair(b,n),r),a)
    = g{28}(eq{29}(a{30},b{31}),n{32},r{33})
g(Right(a),n,r)
    = Cons{40}(Pair{41}(a{42},inc{43}(n{44})),r{45})
g(Left(Pair(a,b)),n,r)
    = Cons{52}(Pair{53}(a{54},Cons{55}(B0{56},Nil{57})),Cons{58}(Pair{59}(b{60},n{61}),r{62}))
inc(Cons(B1,Nil))
    = Cons{72}(B0{73},Cons{74}(B1{75},Nil{76}))
inc(Cons(B0,Nil))
    = Cons{80}(B1{81},Nil{82})
inc(Cons(B0,Cons(B0,x)))
    = Cons{88}(B1{89},Cons{90}(B0{91},nonemp{92}(x{93})))
inc(Cons(B0,Cons(B1,x)))
    = Cons{99}(B1{100},Cons{101}(B1{102},x{103}))
inc(Cons(B1,Cons(B0,x)))
    = Cons{109}(B0{110},Cons{111}(B1{112},nonemp{113}(x{114})))
inc(Cons(B1,Cons(B1,x)))
    = Cons{120}(B0{121},Cons{122}(B0{123},inc2{124}(x{125})))
inc2(Nil)
    = Cons{130}(B1{131},Nil{132})
inc2(Cons(B0,x))
    = Cons{136}(B1{137},nonemp{138}(x{139}))
inc2(Cons(B1,x))
    = Cons{143}(B0{144},inc2{145}(x{146}))
nonemp(Cons(B0,x))
    = Cons{152}(B0{153},x{154})
nonemp(Cons(B1,x))
    = Cons{158}(B1{159},x{160})
eq(B0,B0)
    = Right{167}(B0{168})
eq(B1,B1)
    = Right{171}(B1{172})
eq(B0,B1)
    = Left{175}(Pair{176}(B0{177},B1{178}))
eq(B1,B0)
    = Left{181}(Pair{182}(B1{183},B0{184}))
--- Tree Automata -------------------------------
E184
    <-- B0
    { {} }
E177
    <-- B0
    { {} }
E168
    <-- B0
    { {} }
E153
    <-- B0
    { {} }
E144
    <-- B0
    { {} }
E123
    <-- B0
    { {} }
E121
    <-- B0
    { {} }
E110
    <-- B0
    { {} }
E91 <-- B0
    { {} }
E73 <-- B0
    { {} }
E56 <-- B0
    { {} }
E19 <-- B0
    { {} }
E183
    <-- B1
    { {} }
E178
    <-- B1
    { {} }
E172
    <-- B1
    { {} }
E159
    <-- B1
    { {} }
E137
    <-- B1
    { {} }
E131
    <-- B1
    { {} }
E112
    <-- B1
    { {} }
E102
    <-- B1
    { {} }
E100
    <-- B1
    { {} }
E89 <-- B1
    { {} }
E81 <-- B1
    { {} }
E75 <-- B1
    { {} }
E158
    <-- Cons(E159, E160)
    { \v1{} v2{x} -> v1{}*v2{x} }
E152
    <-- Cons(E153, E154)
    { \v1{} v2{x} -> v1{}*v2{x} }
E143
    <-- Cons(E144, E145)
    { \v1{} v2{x} -> v1{}*v2{x} }
E136
    <-- Cons(E137, E138)
    { \v1{} v2{x} -> v1{}*v2{x} }
E130
    <-- Cons(E131, E132)
    { \v1{} v2{} -> v1{}*v2{} }
E122
    <-- Cons(E123, E124)
    { \v1{} v2{x} -> v1{}*v2{x} }
E120
    <-- Cons(E121, E122)
    { \v1{} v2{x} -> v1{}*v2{x} }
E111
    <-- Cons(E112, E113)
    { \v1{} v2{x} -> v1{}*v2{x} }
E109
    <-- Cons(E110, E111)
    { \v1{} v2{x} -> v1{}*v2{x} }
E101
    <-- Cons(E102, E103)
    { \v1{} v2{x} -> v1{}*v2{x} }
E99 <-- Cons(E100, E101)
    { \v1{} v2{x} -> v1{}*v2{x} }
E90 <-- Cons(E91, E92)
    { \v1{} v2{x} -> v1{}*v2{x} }
E88 <-- Cons(E89, E90)
    { \v1{} v2{x} -> v1{}*v2{x} }
E80 <-- Cons(E81, E82)
    { \v1{} v2{} -> v1{}*v2{} }
E74 <-- Cons(E75, E76)
    { \v1{} v2{} -> v1{}*v2{} }
E72 <-- Cons(E73, E74)
    { \v1{} v2{} -> v1{}*v2{} }
E58 <-- Cons(E59, E62)
    { \v1{b,n} v2{r} -> v1{b,n}*v2{r} }
E55 <-- Cons(E56, E57)
    { \v1{} v2{} -> v1{}*v2{} }
E52 <-- Cons(E53, E58)
    { \v1{a} v2{b,n,r} -> v1{a}*v2{b,n,r} }
E40 <-- Cons(E41, E45)
    { \v1{a,n} v2{r} -> v1{a,n}*v2{r} }
E18 <-- Cons(E19, E20)
    { \v1{} v2{} -> v1{}*v2{} }
E15 <-- Cons(E16, E21)
    { \v1{a} v2{} -> v1{a}*v2{} }
E181
    <-- Left(E182)
    { \v1{} -> v1{} }
E175
    <-- Left(E176)
    { \v1{} -> v1{} }
E132
    <-- Nil
    { {} }
E82 <-- Nil
    { {} }
E76 <-- Nil
    { {} }
E57 <-- Nil
    { {} }
E21 <-- Nil
    { {} }
E20 <-- Nil
    { {} }
E3  <-- Nil
    { {} }
E182
    <-- Pair(E183, E184)
    { \v1{} v2{} -> v1{}*v2{} }
E176
    <-- Pair(E177, E178)
    { \v1{} v2{} -> v1{}*v2{} }
E59 <-- Pair(E60, E61)
    { \v1{b} v2{n} -> v1{b}*v2{n} }
E53 <-- Pair(E54, E55)
    { \v1{a} v2{} -> v1{a}*v2{} }
E41 <-- Pair(E42, E43)
    { \v1{a} v2{n} -> v1{a}*v2{n} }
E16 <-- Pair(E17, E18)
    { \v1{a} v2{} -> v1{a}*v2{} }
E171
    <-- Right(E172)
    { \v1{} -> v1{} }
E167
    <-- Right(E168)
    { \v1{} -> v1{} }
E160
    <-- __
    { {x:__} }
E154
    <-- __
    { {x:__} }
E146
    <-- __
    { {x:__} }
E139
    <-- __
    { {x:__} }
E125
    <-- __
    { {x:__} }
E114
    <-- __
    { {x:__} }
E103
    <-- __
    { {x:__} }
E93 <-- __
    { {x:__} }
E62 <-- __
    { {r:__} }
E61 <-- __
    { {n:__} }
E60 <-- __
    { {b:__} }
E54 <-- __
    { {a:__} }
E45 <-- __
    { {r:__} }
E44 <-- __
    { {n:__} }
E42 <-- __
    { {a:__} }
E33 <-- __
    { {r:__} }
E32 <-- __
    { {n:__} }
E31 <-- __
    { {b:__} }
E30 <-- __
    { {a:__} }
E17 <-- __
    { {a:__} }
E10 <-- __
    { {a:__} }
E9  <-- __
    { {x:__} }
Feq <-- E181
    { \v{} -> {_1:B1, _2:B0} }
Feq <-- E175
    { \v{} -> {_1:B0, _2:B1} }
Feq <-- E171
    { \v{} -> {_1:B1, _2:B1} }
Feq <-- E167
    { \v{} -> {_1:B0, _2:B0} }
Fnonemp
    <-- E158
    { \v{x} -> {_1:Cons(B1,v{x}.x)} }
Fnonemp
    <-- E152
    { \v{x} -> {_1:Cons(B0,v{x}.x)} }
E145
    <-- Finc2
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc2
    <-- E143
    { \v{x} -> {_1:Cons(B1,v{x}.x)} }
E138
    <-- Fnonemp
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc2
    <-- E136
    { \v{x} -> {_1:Cons(B0,v{x}.x)} }
Finc2
    <-- E130
    { \v{} -> {_1:Nil} }
E124
    <-- Finc2
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc
    <-- E120
    { \v{x} -> {_1:Cons(B1,Cons(B1,v{x}.x))} }
E113
    <-- Fnonemp
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc
    <-- E109
    { \v{x} -> {_1:Cons(B1,Cons(B0,v{x}.x))} }
Finc
    <-- E99
    { \v{x} -> {_1:Cons(B0,Cons(B1,v{x}.x))} }
E92 <-- Fnonemp
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc
    <-- E88
    { \v{x} -> {_1:Cons(B0,Cons(B0,v{x}.x))} }
Finc
    <-- E80
    { \v{} -> {_1:Cons(B0,Nil)} }
Finc
    <-- E72
    { \v{} -> {_1:Cons(B1,Nil)} }
Fg  <-- E52
    { \v{a,b,n,r} -> 
      {_1:Left(Pair(v{a,b,n,r}.a,v{a,b,n,r}.b)),
       _2:v{a,b,n,r}.n,
       _3:v{a,b,n,r}.r} }
E43 <-- Finc
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
Fg  <-- E40
    { \v{a,n,r} -> 
      {_1:Right(v{a,n,r}.a), _2:v{a,n,r}.n, _3:v{a,n,r}.r} }
E29 <-- Feq
    { \x{_1,_2} -> 
      let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b} }
E28 <-- Fg
    { \x{_1,_2,_3} -> 
      let {v1{a,b} = @E29(x{_1,_2,_3}._1);
           v2{n} = x{_1,_2,_3}._2;
           v3{r} = x{_1,_2,_3}._3}
      in v1{a,b}*v2{n}*v3{r} }
Ff  <-- E28
    { \v{a,b,n,r} -> 
      {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
       _2:v{a,b,n,r}.a} }
Ff  <-- E15
    { \v{a} -> {_1:Nil, _2:v{a}.a} }
E8  <-- Frunlength
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E7  <-- Ff
    { \x{_1,_2} -> 
      let {v1{x} = @E8(x{_1,_2}._1); v2{a} = x{_1,_2}._2}
      in v1{x}*v2{a} }
Frunlength
    <-- E7
    { \v{a,x} -> {_1:Cons(v{a,x}.a,v{a,x}.x)} }
Frunlength
    <-- E3
    { \v{} -> {_1:Nil} }
--- Guided Tree Automata ------------------------
{Frunlength:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(6,1)
             0 --> Nil()
             1 --> Cons(3,2)
             1 --> Nil()
             1 --> __()
             2 --> __()
             3 --> Pair(5,4)
             3 --> __()
             4 --> __()
             5 --> __()
             6 --> Pair(14,7)
             7 --> Cons(13,8)
             8 --> Cons(12,9)
             8 --> Nil()
             9 --> Cons(11,10)
             9 --> Nil()
             9 --> __()
             10 --> Cons(11,10)
             10 --> Nil()
             10 --> __()
             11 --> B0()
             11 --> B1()
             11 --> __()
             12 --> B0()
             12 --> B1()
             13 --> B0()
             13 --> B1()
             14 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(21, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{a} v2{} -> v1{a}*v2{} >2> (\v{a} -> {_1:Nil, _2:v{a}.a})
                                                       >>> (\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   <-- Cons(21, 10)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{a} v2{b,n,r} -> v1{a}*v2{b,n,r} >2> (\v{a,b,n,r} -> 
                                                                  {_1:Left(Pair(v{a,b,n,r}.a,v{a,b,n,r}.b)),
                                                                   _2:v{a,b,n,r}.n,
                                                                   _3:v{a,b,n,r}.r})
                                                                 >>> (\x{_1,_2,_3} -> 
                                                                      let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                           v2{n} = x{_1,_2,_3}._2;
                                                                           v3{r} = x{_1,_2,_3}._3}
                                                                      in v1{a,b}*v2{n}*v3{r})
                                                                 >>> ((\v{a,b,n,r} -> 
                                                                       {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                        _2:v{a,b,n,r}.a})
                                                                      >>> (\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_2) }
                 1   <-- Cons(24, 8)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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_2) }
                 1   <-- Cons(24, 9)
                     { \x1_1 x2_1->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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   <-- Cons(24, 10)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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}) $ ({})) }
                 74  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(15, 13)
                     { \x1_1 x2_1->
                       ({r:__}, (\v1{b,n} v2{r} -> v1{b,n}*v2{r}) $ x1_1 x2_1) }
                 9   <-- Cons(74, 13)
                     { \_ _-> ({r:__}) }
                 8   <-- Nil
                     { ({}, {r:__}) }
                 9   <-- __
                     { ({r:__}) }
             2:
                 13  <-- __
                     { ({r:__}) }
             3:
                 15  <-- Pair(19, 18)
                     { \x1_1 x2_1-> ((\v1{b} v2{n} -> v1{b}*v2{n}) $ x1_1 x2_1) }
                 74  <-- __
                     { _|_ }
             4:
                 18  <-- __
                     { ({n:__}) }
             5:
                 19  <-- __
                     { ({b:__}) }
             6:
                 21  <-- Pair(77, 27)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{a} v2{} -> v1{a}*v2{}) $ x1_1 x2_1, (\v1{a} v2{} -> 
                                                                  v1{a}*v2{})
                                                                 $
                                                                 x1_3 x2_2) }
                 24  <-- Pair(77, 30)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a} v2{n} -> v1{a}*v2{n}) $ x1_2 x2_1) }
                 74  <-- __
                     { _|_ }
             7:
                 30  <-- Cons(75, 43)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B1,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_5 x2_2) }
                 30  <-- Cons(75, 48)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B1,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_4 x2_2) }
                 30  <-- Cons(76, 42)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_1) }
                 30  <-- Cons(76, 43)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_1) }
                 30  <-- Cons(76, 48)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 30  <-- Cons(75, 39)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Cons(B1,Nil)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 30  <-- Cons(76, 39)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_2) }
                 30  <-- Cons(76, 47)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 27  <-- Cons(75, 38)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1, (\v1{} v2{} -> v1{}*v2{})
                                                               $
                                                               x1_2 x2_2) }
                 30  <-- Cons(76, 38)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Cons(B0,Nil)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_3) }
                 74  <-- __
                     { _|_ }
             8:
                 48  <-- Cons(72, 52)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_2, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_3 x2_3) }
                 48  <-- Cons(72, 53)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_2, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_3 x2_3) }
                 42  <-- Cons(73, 52)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_1 x2_1) }
                 43  <-- Cons(73, 53)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_1 x2_1, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_2 x2_4) }
                 39  <-- Cons(72, 51)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1, (\v1{} v2{x} -> v1{}*v2{x})
                                                               $
                                                               x1_2 x2_2) }
                 47  <-- Cons(72, 54)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_1) }
                 38  <-- Nil
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             9:
                 54  <-- Cons(74, 64)
                     { \_ _-> ({x:__}) }
                 54  <-- Cons(74, 65)
                     { \_ _-> ({x:__}) }
                 53  <-- Cons(69, 64)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_3 x2_4, {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_3 x2_4, (\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_2 x2_1) }
                 53  <-- Cons(69, 65)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, {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_3 x2_3, (\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_2 x2_1) }
                 53  <-- Cons(70, 64)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_2 x2_3, {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_2 x2_3, (\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_1 x2_2) }
                 52  <-- Cons(70, 65)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 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_2 x2_2) }
                 54  <-- Cons(74, 63)
                     { \_ _-> ({x:__}) }
                 53  <-- Cons(69, 63)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, {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_3 x2_3, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> 
                                                                                    {_1:Nil})
                                                                                   >>> (\x{_1} -> 
                                                                                        let {v1{x} = x{_1}._1}
                                                                                        in v1{x}))
                                                      $
                                                      x1_1 x2_1) }
                 52  <-- Cons(69, 67)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\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_3 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_3 x2_2) }
                 52  <-- Cons(70, 63)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 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_2 x2_2) }
                 52  <-- Cons(70, 67)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\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_2 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_2 x2_1) }
                 54  <-- Cons(74, 67)
                     { \_ _-> ({x:__}) }
                 51  <-- Nil
                     { ({}, {x:__}) }
                 54  <-- __
                     { ({x:__}) }
             10:
                 67  <-- Cons(74, 64)
                     { \_ _-> ({x:__}, {x:__}) }
                 67  <-- Cons(74, 65)
                     { \_ _-> ({x:__}, {x:__}) }
                 64  <-- Cons(69, 64)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_3 x2_4, (\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_2 x2_1, {x:__}, {x:__}) }
                 64  <-- Cons(69, 65)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, (\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_2 x2_1, {x:__}, {x:__}) }
                 64  <-- Cons(70, 64)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_2 x2_3, (\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_1 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 65)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 x2_2, {x:__}, {x:__}) }
                 67  <-- Cons(74, 63)
                     { \_ _-> ({x:__}, {x:__}) }
                 64  <-- Cons(69, 63)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                                >>> (\x{_1} -> 
                                                                     let {v1{x} = x{_1}._1}
                                                                     in v1{x}))
                                   $
                                   x1_1 x2_1, {x:__}, {x:__}) }
                 65  <-- Cons(69, 67)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\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_3 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 63)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 67)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\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_2 x2_1, {x:__}, {x:__}) }
                 67  <-- Cons(74, 67)
                     { \_ _-> ({x:__}, {x:__}) }
                 63  <-- Nil
                     { ({}, {x:__}, {x:__}) }
                 67  <-- __
                     { ({x:__}, {x:__}) }
             11:
                 70  <-- B0
                     { ({}, {}) }
                 69  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             12:
                 73  <-- B0
                     { ({}, {}) }
                 72  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             13:
                 75  <-- B0
                     { ({}, {}, {}, {}, {}) }
                 76  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             14:
                 77  <-- __
                     { ({a:__}, {a:__}, {a:__}) }
 E8:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(6,1)
             0 --> Nil()
             1 --> Cons(3,2)
             1 --> Nil()
             1 --> __()
             2 --> __()
             3 --> Pair(5,4)
             3 --> __()
             4 --> __()
             5 --> __()
             6 --> Pair(14,7)
             7 --> Cons(13,8)
             8 --> Cons(12,9)
             8 --> Nil()
             9 --> Cons(11,10)
             9 --> Nil()
             9 --> __()
             10 --> Cons(11,10)
             10 --> Nil()
             10 --> __()
             11 --> B0()
             11 --> B1()
             11 --> __()
             12 --> B0()
             12 --> B1()
             13 --> B0()
             13 --> B1()
             14 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(21, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{a} v2{} -> v1{a}*v2{} >2> (\v{a} -> {_1:Nil, _2:v{a}.a})
                                                       >>> (\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   <-- Cons(21, 10)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{a} v2{b,n,r} -> v1{a}*v2{b,n,r} >2> (\v{a,b,n,r} -> 
                                                                  {_1:Left(Pair(v{a,b,n,r}.a,v{a,b,n,r}.b)),
                                                                   _2:v{a,b,n,r}.n,
                                                                   _3:v{a,b,n,r}.r})
                                                                 >>> (\x{_1,_2,_3} -> 
                                                                      let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                           v2{n} = x{_1,_2,_3}._2;
                                                                           v3{r} = x{_1,_2,_3}._3}
                                                                      in v1{a,b}*v2{n}*v3{r})
                                                                 >>> ((\v{a,b,n,r} -> 
                                                                       {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                        _2:v{a,b,n,r}.a})
                                                                      >>> (\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_2) }
                 1   <-- Cons(24, 8)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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_2) }
                 1   <-- Cons(24, 9)
                     { \x1_1 x2_1->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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   <-- Cons(24, 10)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{a,n} v2{r} -> v1{a,n}*v2{r} >2> (\v{a,n,r} -> 
                                                              {_1:Right(v{a,n,r}.a),
                                                               _2:v{a,n,r}.n,
                                                               _3:v{a,n,r}.r})
                                                             >>> (\x{_1,_2,_3} -> 
                                                                  let {v1{a,b} = @E29(x{_1,_2,_3}._1);
                                                                       v2{n} = x{_1,_2,_3}._2;
                                                                       v3{r} = x{_1,_2,_3}._3}
                                                                  in v1{a,b}*v2{n}*v3{r})
                                                             >>> ((\v{a,b,n,r} -> 
                                                                   {_1:Cons(Pair(v{a,b,n,r}.b,v{a,b,n,r}.n),v{a,b,n,r}.r),
                                                                    _2:v{a,b,n,r}.a})
                                                                  >>> (\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})) $ ({})) }
                 74  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(15, 13)
                     { \x1_1 x2_1->
                       ({r:__}, (\v1{b,n} v2{r} -> v1{b,n}*v2{r}) $ x1_1 x2_1) }
                 9   <-- Cons(74, 13)
                     { \_ _-> ({r:__}) }
                 8   <-- Nil
                     { ({}, {r:__}) }
                 9   <-- __
                     { ({r:__}) }
             2:
                 13  <-- __
                     { ({r:__}) }
             3:
                 15  <-- Pair(19, 18)
                     { \x1_1 x2_1-> ((\v1{b} v2{n} -> v1{b}*v2{n}) $ x1_1 x2_1) }
                 74  <-- __
                     { _|_ }
             4:
                 18  <-- __
                     { ({n:__}) }
             5:
                 19  <-- __
                     { ({b:__}) }
             6:
                 21  <-- Pair(77, 27)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{a} v2{} -> v1{a}*v2{}) $ x1_1 x2_1, (\v1{a} v2{} -> 
                                                                  v1{a}*v2{})
                                                                 $
                                                                 x1_3 x2_2) }
                 24  <-- Pair(77, 30)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a} v2{n} -> v1{a}*v2{n}) $ x1_2 x2_1) }
                 74  <-- __
                     { _|_ }
             7:
                 30  <-- Cons(75, 43)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B1,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_5 x2_2) }
                 30  <-- Cons(75, 48)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B1,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_4 x2_2) }
                 30  <-- Cons(76, 42)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_1) }
                 30  <-- Cons(76, 43)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B0,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_2 x2_1) }
                 30  <-- Cons(76, 48)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 30  <-- Cons(75, 39)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Cons(B1,Nil)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 30  <-- Cons(76, 39)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_2) }
                 30  <-- Cons(76, 47)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                        {_1:Cons(B0,Cons(B1,v{x}.x))})
                                                       >>> (\x{_1} -> 
                                                            let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_3 x2_1) }
                 27  <-- Cons(75, 38)
                     { \(x1_1,x1_2,x1_3,x1_4,x1_5) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1, (\v1{} v2{} -> v1{}*v2{})
                                                               $
                                                               x1_2 x2_2) }
                 30  <-- Cons(76, 38)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Cons(B0,Nil)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_3) }
                 74  <-- __
                     { _|_ }
             8:
                 48  <-- Cons(72, 52)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_2, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_3 x2_3) }
                 48  <-- Cons(72, 53)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_2, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_3 x2_3) }
                 42  <-- Cons(73, 52)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_1 x2_1) }
                 43  <-- Cons(73, 53)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_1 x2_1, (\v1{} v2{x} -> 
                                                                  v1{}*v2{x})
                                                                 $
                                                                 x1_2 x2_4) }
                 39  <-- Cons(72, 51)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1, (\v1{} v2{x} -> v1{}*v2{x})
                                                               $
                                                               x1_2 x2_2) }
                 47  <-- Cons(72, 54)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x}) $ x1_2 x2_1) }
                 38  <-- Nil
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             9:
                 54  <-- Cons(74, 64)
                     { \_ _-> ({x:__}) }
                 54  <-- Cons(74, 65)
                     { \_ _-> ({x:__}) }
                 53  <-- Cons(69, 64)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_3 x2_4, {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_3 x2_4, (\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_2 x2_1) }
                 53  <-- Cons(69, 65)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, {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_3 x2_3, (\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_2 x2_1) }
                 53  <-- Cons(70, 64)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_2 x2_3, {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_2 x2_3, (\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_1 x2_2) }
                 52  <-- Cons(70, 65)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 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_2 x2_2) }
                 54  <-- Cons(74, 63)
                     { \_ _-> ({x:__}) }
                 53  <-- Cons(69, 63)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, {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_3 x2_3, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> 
                                                                                    {_1:Nil})
                                                                                   >>> (\x{_1} -> 
                                                                                        let {v1{x} = x{_1}._1}
                                                                                        in v1{x}))
                                                      $
                                                      x1_1 x2_1) }
                 52  <-- Cons(69, 67)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\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_3 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_3 x2_2) }
                 52  <-- Cons(70, 63)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 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_2 x2_2) }
                 52  <-- Cons(70, 67)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\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_2 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_2 x2_1) }
                 54  <-- Cons(74, 67)
                     { \_ _-> ({x:__}) }
                 51  <-- Nil
                     { ({}, {x:__}) }
                 54  <-- __
                     { ({x:__}) }
             10:
                 67  <-- Cons(74, 64)
                     { \_ _-> ({x:__}, {x:__}) }
                 67  <-- Cons(74, 65)
                     { \_ _-> ({x:__}, {x:__}) }
                 64  <-- Cons(69, 64)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_3 x2_4, (\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_2 x2_1, {x:__}, {x:__}) }
                 64  <-- Cons(69, 65)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, (\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_2 x2_1, {x:__}, {x:__}) }
                 64  <-- Cons(70, 64)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3,x2_4)->
                       ((\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_2 x2_3, (\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_1 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 65)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 x2_2, {x:__}, {x:__}) }
                 67  <-- Cons(74, 63)
                     { \_ _-> ({x:__}, {x:__}) }
                 64  <-- Cons(69, 63)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\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_3 x2_3, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                                >>> (\x{_1} -> 
                                                                     let {v1{x} = x{_1}._1}
                                                                     in v1{x}))
                                   $
                                   x1_1 x2_1, {x:__}, {x:__}) }
                 65  <-- Cons(69, 67)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2)->
                       ((\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_3 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 63)
                     { \(x1_1,x1_2) (x2_1,x2_2,x2_3)->
                       ((\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_2 x2_2, {x:__}, {x:__}) }
                 65  <-- Cons(70, 67)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\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_2 x2_1, {x:__}, {x:__}) }
                 67  <-- Cons(74, 67)
                     { \_ _-> ({x:__}, {x:__}) }
                 63  <-- Nil
                     { ({}, {x:__}, {x:__}) }
                 67  <-- __
                     { ({x:__}, {x:__}) }
             11:
                 70  <-- B0
                     { ({}, {}) }
                 69  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             12:
                 73  <-- B0
                     { ({}, {}) }
                 72  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             13:
                 75  <-- B0
                     { ({}, {}, {}, {}, {}) }
                 76  <-- B1
                     { ({}, {}, {}) }
                 74  <-- __
                     { _|_ }
             14:
                 77  <-- __
                     { ({a:__}, {a:__}, {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:__}) }
 E29:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Left(2)
             0 --> Right(1)
             1 --> B0()
             1 --> B1()
             2 --> Pair(4,3)
             3 --> B0()
             3 --> B1()
             4 --> B0()
             4 --> B1()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Left(10)
                     { \x1_1->
                       (((\v1{} -> v1{})
                         >>> (\v{} -> {_1:B0, _2:B1})
                         >>> (\x{_1,_2} -> 
                              let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b}))
                        $
                        x1_1) }
                 1   <-- Left(13)
                     { \x1_1->
                       (((\v1{} -> v1{})
                         >>> (\v{} -> {_1:B1, _2:B0})
                         >>> (\x{_1,_2} -> 
                              let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b}))
                        $
                        x1_1) }
                 1   <-- Right(7)
                     { \x1_1->
                       (((\v1{} -> v1{})
                         >>> (\v{} -> {_1:B0, _2:B0})
                         >>> (\x{_1,_2} -> 
                              let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b}))
                        $
                        x1_1) }
                 1   <-- Right(8)
                     { \x1_1->
                       (((\v1{} -> v1{})
                         >>> (\v{} -> {_1:B1, _2:B1})
                         >>> (\x{_1,_2} -> 
                              let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b}))
                        $
                        x1_1) }
                 19  <-- __
                     { _|_ }
             1:
                 7   <-- B0
                     { ({}) }
                 8   <-- B1
                     { ({}) }
                 19  <-- __
                     { _|_ }
             2:
                 10  <-- Pair(20, 17)
                     { \x1_1 x2_1-> ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1) }
                 13  <-- Pair(21, 18)
                     { \x1_1 x2_1-> ((\v1{} v2{} -> v1{}*v2{}) $ x1_1 x2_1) }
                 19  <-- __
                     { _|_ }
             3:
                 18  <-- B0
                     { ({}) }
                 17  <-- B1
                     { ({}) }
                 19  <-- __
                     { _|_ }
             4:
                 20  <-- B0
                     { ({}) }
                 21  <-- B1
                     { ({}) }
                 19  <-- __
                     { _|_ }
 E30:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E31:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({b:__}) }
 E32:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E33:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({r:__}) }
 E44:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E93:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E114:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E125:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E139:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E146:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }}

-- 0.26 seconds is elapsed.