--- Abstract Syntax Tree ------------------------
diff(Nil,Nil)
    = Pair{6}(Nil{7},Nil{8})
diff(Cons(a,x),Cons(b,y))
    = letAt15{15}(diff{20}(x{21},Cons{22}(b{23},y{24})),a{32})
diff(Cons(a,x),Cons(b,y))
    = letAt40{40}(diff{47}(Cons{48}(a{49},x{50}),y{51}),b{60})
diff(Cons(a,x),Cons(b,y))
    = letAt68{68}(eqCheck{72}(a{73},b{74}),a{92},x{93},y{94})
letAt15(Pair(org,ops),a)
    = Pair{25}(Cons{26}(a{27},org{28}),Cons{29}(Del{30},ops{31}))
letAt40(Pair(Cons(a1,org),ops),b)
    = Pair{52}(Cons{53}(a1{54},org{55}),Cons{56}(Ins{57}(b{58}),ops{59}))
letAt68(Right(c),a,x,y)
    = letAt75{75}(diff{80}(x{81},y{82}),a{90})
letAt75(Pair(org,ops),a)
    = Pair{83}(Cons{84}(a{85},org{86}),Cons{87}(Keep{88},ops{89}))
eqCheck(B0,B1)
    = Left{104}(Pair{105}(B0{106},B1{107}))
eqCheck(B1,B0)
    = Left{110}(Pair{111}(B1{112},B0{113}))
eqCheck(B0,B0)
    = Right{116}(B0{117})
eqCheck(B1,B1)
    = Right{120}(B1{121})
--- Tree Automata -------------------------------
E117
    <-- B0
    { {} }
E113
    <-- B0
    { {} }
E106
    <-- B0
    { {} }
E121
    <-- B1
    { {} }
E112
    <-- B1
    { {} }
E107
    <-- B1
    { {} }
E87 <-- Cons(E88, E89)
    { \v1{} v2{ops} -> v1{}*v2{ops} }
E84 <-- Cons(E85, E86)
    { \v1{a} v2{org} -> v1{a}*v2{org} }
E56 <-- Cons(E57, E59)
    { \v1{b} v2{ops} -> v1{b}*v2{ops} }
E53 <-- Cons(E54, E55)
    { \v1{a1} v2{org} -> v1{a1}*v2{org} }
E29 <-- Cons(E30, E31)
    { \v1{} v2{ops} -> v1{}*v2{ops} }
E26 <-- Cons(E27, E28)
    { \v1{a} v2{org} -> v1{a}*v2{org} }
E48 <-- Cons(E49, E50)
    { \v1{a} v2{x} -> v1{a}*v2{x} }
E22 <-- Cons(E23, E24)
    { \v1{b} v2{y} -> v1{b}*v2{y} }
E30 <-- Del
    { {} }
E57 <-- Ins(E58)
    { \v1{b} -> v1{b} }
E88 <-- Keep
    { {} }
E110
    <-- Left(E111)
    { \v1{} -> v1{} }
E104
    <-- Left(E105)
    { \v1{} -> v1{} }
E8  <-- Nil
    { {} }
E7  <-- Nil
    { {} }
E111
    <-- Pair(E112, E113)
    { \v1{} v2{} -> v1{}*v2{} }
E105
    <-- Pair(E106, E107)
    { \v1{} v2{} -> v1{}*v2{} }
E83 <-- Pair(E84, E87)
    { \v1{a,org} v2{ops} -> v1{a,org}*v2{ops} }
E52 <-- Pair(E53, E56)
    { \v1{a1,org} v2{b,ops} -> v1{a1,org}*v2{b,ops} }
E25 <-- Pair(E26, E29)
    { \v1{a,org} v2{ops} -> v1{a,org}*v2{ops} }
E6  <-- Pair(E7, E8)
    { \v1{} v2{} -> v1{}*v2{} }
E120
    <-- Right(E121)
    { \v1{} -> v1{} }
E116
    <-- Right(E117)
    { \v1{} -> v1{} }
E89 <-- __
    { {ops:__} }
E86 <-- __
    { {org:__} }
E85 <-- __
    { {a:__} }
E90 <-- __
    { {a:__} }
E82 <-- __
    { {y:__} }
E81 <-- __
    { {x:__} }
E59 <-- __
    { {ops:__} }
E58 <-- __
    { {b:__} }
E55 <-- __
    { {org:__} }
E54 <-- __
    { {a1:__} }
E31 <-- __
    { {ops:__} }
E28 <-- __
    { {org:__} }
E27 <-- __
    { {a:__} }
E94 <-- __
    { {y:__} }
E93 <-- __
    { {x:__} }
E92 <-- __
    { {a:__} }
E74 <-- __
    { {b:__} }
E73 <-- __
    { {a:__} }
E60 <-- __
    { {b:__} }
E51 <-- __
    { {y:__} }
E50 <-- __
    { {x:__} }
E49 <-- __
    { {a:__} }
E32 <-- __
    { {a:__} }
E24 <-- __
    { {y:__} }
E23 <-- __
    { {b:__} }
E21 <-- __
    { {x:__} }
FeqCheck
    <-- E120
    { \v{} -> {_1:B1, _2:B1} }
FeqCheck
    <-- E116
    { \v{} -> {_1:B0, _2:B0} }
FeqCheck
    <-- E110
    { \v{} -> {_1:B1, _2:B0} }
FeqCheck
    <-- E104
    { \v{} -> {_1:B0, _2:B1} }
FletAt75
    <-- E83
    { \v{a,ops,org} -> 
      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops), _2:v{a,ops,org}.a} }
E80 <-- Fdiff
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
E75 <-- FletAt75
    { \x{_1,_2} -> 
      let {v1{x,y} = @E80(x{_1,_2}._1); v2{a} = x{_1,_2}._2}
      in v1{x,y}*v2{a} }
FletAt68
    <-- E75
    { \v{a,x,y} -> 
      {_1:Right(v{a,x,y}.c),
       _2:v{a,x,y}.a,
       _3:v{a,x,y}.x,
       _4:v{a,x,y}.y} }
FletAt40
    <-- E52
    { \v{a1,b,ops,org} -> 
      {_1:Pair(Cons(v{a1,b,ops,org}.a1,v{a1,b,ops,org}.org),v{a1,b,ops,org}.ops),
       _2:v{a1,b,ops,org}.b} }
FletAt15
    <-- E25
    { \v{a,ops,org} -> 
      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops), _2:v{a,ops,org}.a} }
E72 <-- FeqCheck
    { \x{_1,_2} -> 
      let {v1{a} = x{_1,_2}._1; v2{b} = x{_1,_2}._2} in v1{a}*v2{b} }
E68 <-- FletAt68
    { \x{_1,_2,_3,_4} -> 
      let {v1{a,b} = @E72(x{_1,_2,_3,_4}._1);
           v2{a} = x{_1,_2,_3,_4}._2;
           v3{x} = x{_1,_2,_3,_4}._3;
           v4{y} = x{_1,_2,_3,_4}._4}
      in v1{a,b}*v2{a}*v3{x}*v4{y} }
Fdiff
    <-- E68
    { \v{a,b,x,y} -> 
      {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
       _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)} }
E47 <-- Fdiff
    { \x{_1,_2} -> 
      let {v1{a,x} = @E48(x{_1,_2}._1); v2{y} = x{_1,_2}._2}
      in v1{a,x}*v2{y} }
E40 <-- FletAt40
    { \x{_1,_2} -> 
      let {v1{a,x,y} = @E47(x{_1,_2}._1); v2{b} = x{_1,_2}._2}
      in v1{a,x,y}*v2{b} }
Fdiff
    <-- E40
    { \v{a,b,x,y} -> 
      {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
       _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)} }
E20 <-- Fdiff
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{b,y} = @E22(x{_1,_2}._2)}
      in v1{x}*v2{b,y} }
E15 <-- FletAt15
    { \x{_1,_2} -> 
      let {v1{b,x,y} = @E20(x{_1,_2}._1); v2{a} = x{_1,_2}._2}
      in v1{b,x,y}*v2{a} }
Fdiff
    <-- E15
    { \v{a,b,x,y} -> 
      {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
       _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)} }
Fdiff
    <-- E6
    { \v{} -> {_1:Nil, _2:Nil} }
--- Guided Tree Automata ------------------------
{Fdiff:  INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(5,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> Del()
             3 --> Ins(4)
             3 --> Keep()
             4 --> __()
             5 --> Cons(7,6)
             5 --> Nil()
             6 --> __()
             7 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(26, 10)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{b,x,y} = @E20(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{b,x,y}*v2{a})
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(26, 13)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a1,org} v2{b,ops} -> 
                         v1{a1,org}*v2{b,ops} >2> (\v{a1,b,ops,org} -> 
                                                   {_1:Pair(Cons(v{a1,b,ops,org}.a1,v{a1,b,ops,org}.org),v{a1,b,ops,org}.ops),
                                                    _2:v{a1,b,ops,org}.b})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{a,x,y} = @E47(x{_1,_2}._1);
                                                            v2{b} = x{_1,_2}._2}
                                                       in v1{a,x,y}*v2{b})
                                                  >>> (\v{a,b,x,y} -> 
                                                       {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                        _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)}))
                        $
                        x1_2 x2_1) }
                 1   <-- Pair(26, 15)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x,y} = @E80(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{x,y}*v2{a})
                                                                     >>> ((\v{a,x,y} -> 
                                                                           {_1:Right(v{a,x,y}.c),
                                                                            _2:v{a,x,y}.a,
                                                                            _3:v{a,x,y}.x,
                                                                            _4:v{a,x,y}.y})
                                                                          >>> (\x{_1,_2,_3,_4} -> 
                                                                               let {v1{a,b} = @E72(x{_1,_2,_3,_4}._1);
                                                                                    v2{a} = x{_1,_2,_3,_4}._2;
                                                                                    v3{x} = x{_1,_2,_3,_4}._3;
                                                                                    v4{y} = x{_1,_2,_3,_4}._4}
                                                                               in v1{a,b}*v2{a}*v3{x}*v4{y}))
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)}))
                        $
                        x1_3 x2_1) }
                 1   <-- Pair(25, 9)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> \v{} -> {_1:Nil, _2:Nil})
                        $
                        x1_1 x2_1) }
                 24  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(19, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_1) }
                 13  <-- Cons(20, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{b} v2{ops} -> v1{b}*v2{ops}) $ x1_1 x2_2) }
                 15  <-- Cons(22, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_3) }
                 9   <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             2:
                 17  <-- __
                     { ({ops:__}, {ops:__}, {ops:__}) }
             3:
                 19  <-- Del
                     { ({}) }
                 20  <-- Ins(23)
                     { \x1_1-> ((\v1{b} -> v1{b}) $ x1_1) }
                 22  <-- Keep
                     { ({}) }
                 24  <-- __
                     { _|_ }
             4:
                 23  <-- __
                     { ({b:__}) }
             5:
                 26  <-- Cons(30, 29)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{a} v2{org} -> v1{a}*v2{org})
                        $
                        x1_1 x2_1, (\v1{a1} v2{org} -> v1{a1}*v2{org})
                                   $
                                   x1_2 x2_2, (\v1{a} v2{org} -> v1{a}*v2{org}) $ x1_3 x2_3) }
                 25  <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             6:
                 29  <-- __
                     { ({org:__}, {org:__}, {org:__}) }
             7:
                 30  <-- __
                     { ({a:__}, {a1:__}, {a:__}) }
 E20:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(5,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> Del()
             3 --> Ins(4)
             3 --> Keep()
             4 --> __()
             5 --> Cons(7,6)
             5 --> Nil()
             6 --> __()
             7 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Pair(26, 10)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{b,x,y} = @E20(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{b,x,y}*v2{a})
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x} = x{_1,_2}._1;
                                                                               v2{b,y} = @E22(x{_1,_2}._2)}
                                                                          in v1{x}*v2{b,y}))
                        $
                        x1_1 x2_1) }
                 3   <-- Pair(26, 13)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a1,org} v2{b,ops} -> 
                         v1{a1,org}*v2{b,ops} >2> (\v{a1,b,ops,org} -> 
                                                   {_1:Pair(Cons(v{a1,b,ops,org}.a1,v{a1,b,ops,org}.org),v{a1,b,ops,org}.ops),
                                                    _2:v{a1,b,ops,org}.b})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{a,x,y} = @E47(x{_1,_2}._1);
                                                            v2{b} = x{_1,_2}._2}
                                                       in v1{a,x,y}*v2{b})
                                                  >>> (\v{a,b,x,y} -> 
                                                       {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                        _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{x} = x{_1,_2}._1;
                                                            v2{b,y} = @E22(x{_1,_2}._2)}
                                                       in v1{x}*v2{b,y}))
                        $
                        x1_2 x2_1) }
                 3   <-- Pair(26, 15)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x,y} = @E80(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{x,y}*v2{a})
                                                                     >>> ((\v{a,x,y} -> 
                                                                           {_1:Right(v{a,x,y}.c),
                                                                            _2:v{a,x,y}.a,
                                                                            _3:v{a,x,y}.x,
                                                                            _4:v{a,x,y}.y})
                                                                          >>> (\x{_1,_2,_3,_4} -> 
                                                                               let {v1{a,b} = @E72(x{_1,_2,_3,_4}._1);
                                                                                    v2{a} = x{_1,_2,_3,_4}._2;
                                                                                    v3{x} = x{_1,_2,_3,_4}._3;
                                                                                    v4{y} = x{_1,_2,_3,_4}._4}
                                                                               in v1{a,b}*v2{a}*v3{x}*v4{y}))
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x} = x{_1,_2}._1;
                                                                               v2{b,y} = @E22(x{_1,_2}._2)}
                                                                          in v1{x}*v2{b,y}))
                        $
                        x1_3 x2_1) }
                 3   <-- Pair(25, 9)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil, _2:Nil})
                                                     >>> (\x{_1,_2} -> 
                                                          let {v1{x} = x{_1,_2}._1;
                                                               v2{b,y} = @E22(x{_1,_2}._2)}
                                                          in v1{x}*v2{b,y}))
                        $
                        x1_1 x2_1) }
                 24  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(19, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_1) }
                 13  <-- Cons(20, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{b} v2{ops} -> v1{b}*v2{ops}) $ x1_1 x2_2) }
                 15  <-- Cons(22, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_3) }
                 9   <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             2:
                 17  <-- __
                     { ({ops:__}, {ops:__}, {ops:__}) }
             3:
                 19  <-- Del
                     { ({}) }
                 20  <-- Ins(23)
                     { \x1_1-> ((\v1{b} -> v1{b}) $ x1_1) }
                 22  <-- Keep
                     { ({}) }
                 24  <-- __
                     { _|_ }
             4:
                 23  <-- __
                     { ({b:__}) }
             5:
                 26  <-- Cons(30, 29)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{a} v2{org} -> v1{a}*v2{org})
                        $
                        x1_1 x2_1, (\v1{a1} v2{org} -> v1{a1}*v2{org})
                                   $
                                   x1_2 x2_2, (\v1{a} v2{org} -> v1{a}*v2{org}) $ x1_3 x2_3) }
                 25  <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             6:
                 29  <-- __
                     { ({org:__}, {org:__}, {org:__}) }
             7:
                 30  <-- __
                     { ({a:__}, {a1:__}, {a:__}) }
 E21:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E22:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> __()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(5, 4)
                     { \x1_1 x2_1-> ((\v1{b} v2{y} -> v1{b}*v2{y}) $ x1_1 x2_1) }
                 0   <-- __
                     { _|_ }
             1:
                 4   <-- __
                     { ({y:__}) }
             2:
                 5   <-- __
                     { ({b:__}) }
 E32:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E47:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(5,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> Del()
             3 --> Ins(4)
             3 --> Keep()
             4 --> __()
             5 --> Cons(7,6)
             5 --> Nil()
             6 --> __()
             7 --> __()
         GUIDED TRANSITIONS:
             0:
                 5   <-- Pair(26, 10)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{b,x,y} = @E20(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{b,x,y}*v2{a})
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{a,x} = @E48(x{_1,_2}._1);
                                                                               v2{y} = x{_1,_2}._2}
                                                                          in v1{a,x}*v2{y}))
                        $
                        x1_1 x2_1) }
                 5   <-- Pair(26, 13)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a1,org} v2{b,ops} -> 
                         v1{a1,org}*v2{b,ops} >2> (\v{a1,b,ops,org} -> 
                                                   {_1:Pair(Cons(v{a1,b,ops,org}.a1,v{a1,b,ops,org}.org),v{a1,b,ops,org}.ops),
                                                    _2:v{a1,b,ops,org}.b})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{a,x,y} = @E47(x{_1,_2}._1);
                                                            v2{b} = x{_1,_2}._2}
                                                       in v1{a,x,y}*v2{b})
                                                  >>> (\v{a,b,x,y} -> 
                                                       {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                        _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{a,x} = @E48(x{_1,_2}._1);
                                                            v2{y} = x{_1,_2}._2}
                                                       in v1{a,x}*v2{y}))
                        $
                        x1_2 x2_1) }
                 5   <-- Pair(26, 15)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x,y} = @E80(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{x,y}*v2{a})
                                                                     >>> ((\v{a,x,y} -> 
                                                                           {_1:Right(v{a,x,y}.c),
                                                                            _2:v{a,x,y}.a,
                                                                            _3:v{a,x,y}.x,
                                                                            _4:v{a,x,y}.y})
                                                                          >>> (\x{_1,_2,_3,_4} -> 
                                                                               let {v1{a,b} = @E72(x{_1,_2,_3,_4}._1);
                                                                                    v2{a} = x{_1,_2,_3,_4}._2;
                                                                                    v3{x} = x{_1,_2,_3,_4}._3;
                                                                                    v4{y} = x{_1,_2,_3,_4}._4}
                                                                               in v1{a,b}*v2{a}*v3{x}*v4{y}))
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{a,x} = @E48(x{_1,_2}._1);
                                                                               v2{y} = x{_1,_2}._2}
                                                                          in v1{a,x}*v2{y}))
                        $
                        x1_3 x2_1) }
                 5   <-- Pair(25, 9)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil, _2:Nil})
                                                     >>> (\x{_1,_2} -> 
                                                          let {v1{a,x} = @E48(x{_1,_2}._1);
                                                               v2{y} = x{_1,_2}._2}
                                                          in v1{a,x}*v2{y}))
                        $
                        x1_1 x2_1) }
                 24  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(19, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_1) }
                 13  <-- Cons(20, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{b} v2{ops} -> v1{b}*v2{ops}) $ x1_1 x2_2) }
                 15  <-- Cons(22, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_3) }
                 9   <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             2:
                 17  <-- __
                     { ({ops:__}, {ops:__}, {ops:__}) }
             3:
                 19  <-- Del
                     { ({}) }
                 20  <-- Ins(23)
                     { \x1_1-> ((\v1{b} -> v1{b}) $ x1_1) }
                 22  <-- Keep
                     { ({}) }
                 24  <-- __
                     { _|_ }
             4:
                 23  <-- __
                     { ({b:__}) }
             5:
                 26  <-- Cons(30, 29)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{a} v2{org} -> v1{a}*v2{org})
                        $
                        x1_1 x2_1, (\v1{a1} v2{org} -> v1{a1}*v2{org})
                                   $
                                   x1_2 x2_2, (\v1{a} v2{org} -> v1{a}*v2{org}) $ x1_3 x2_3) }
                 25  <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             6:
                 29  <-- __
                     { ({org:__}, {org:__}, {org:__}) }
             7:
                 30  <-- __
                     { ({a:__}, {a1:__}, {a:__}) }
 E48:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> __()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(5, 4)
                     { \x1_1 x2_1-> ((\v1{a} v2{x} -> v1{a}*v2{x}) $ x1_1 x2_1) }
                 0   <-- __
                     { _|_ }
             1:
                 4   <-- __
                     { ({x:__}) }
             2:
                 5   <-- __
                     { ({a:__}) }
 E51:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }
 E60:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({b:__}) }
 E72:    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  <-- __
                     { _|_ }
 E73:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E74:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({b:__}) }
 E80:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(5,1)
             1 --> Cons(3,2)
             1 --> Nil()
             2 --> __()
             3 --> Del()
             3 --> Ins(4)
             3 --> Keep()
             4 --> __()
             5 --> Cons(7,6)
             5 --> Nil()
             6 --> __()
             7 --> __()
         GUIDED TRANSITIONS:
             0:
                 6   <-- Pair(26, 10)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{b,x,y} = @E20(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{b,x,y}*v2{a})
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x} = x{_1,_2}._1;
                                                                               v2{y} = x{_1,_2}._2}
                                                                          in v1{x}*v2{y}))
                        $
                        x1_1 x2_1) }
                 6   <-- Pair(26, 13)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a1,org} v2{b,ops} -> 
                         v1{a1,org}*v2{b,ops} >2> (\v{a1,b,ops,org} -> 
                                                   {_1:Pair(Cons(v{a1,b,ops,org}.a1,v{a1,b,ops,org}.org),v{a1,b,ops,org}.ops),
                                                    _2:v{a1,b,ops,org}.b})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{a,x,y} = @E47(x{_1,_2}._1);
                                                            v2{b} = x{_1,_2}._2}
                                                       in v1{a,x,y}*v2{b})
                                                  >>> (\v{a,b,x,y} -> 
                                                       {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                        _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                  >>> (\x{_1,_2} -> 
                                                       let {v1{x} = x{_1,_2}._1;
                                                            v2{y} = x{_1,_2}._2}
                                                       in v1{x}*v2{y}))
                        $
                        x1_2 x2_1) }
                 6   <-- Pair(26, 15)
                     { \(x1_1,x1_2,x1_3) x2_1->
                       ((\v1{a,org} v2{ops} -> v1{a,org}*v2{ops} >2> (\v{a,ops,org} -> 
                                                                      {_1:Pair(v{a,ops,org}.org,v{a,ops,org}.ops),
                                                                       _2:v{a,ops,org}.a})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x,y} = @E80(x{_1,_2}._1);
                                                                               v2{a} = x{_1,_2}._2}
                                                                          in v1{x,y}*v2{a})
                                                                     >>> ((\v{a,x,y} -> 
                                                                           {_1:Right(v{a,x,y}.c),
                                                                            _2:v{a,x,y}.a,
                                                                            _3:v{a,x,y}.x,
                                                                            _4:v{a,x,y}.y})
                                                                          >>> (\x{_1,_2,_3,_4} -> 
                                                                               let {v1{a,b} = @E72(x{_1,_2,_3,_4}._1);
                                                                                    v2{a} = x{_1,_2,_3,_4}._2;
                                                                                    v3{x} = x{_1,_2,_3,_4}._3;
                                                                                    v4{y} = x{_1,_2,_3,_4}._4}
                                                                               in v1{a,b}*v2{a}*v3{x}*v4{y}))
                                                                     >>> (\v{a,b,x,y} -> 
                                                                          {_1:Cons(v{a,b,x,y}.a,v{a,b,x,y}.x),
                                                                           _2:Cons(v{a,b,x,y}.b,v{a,b,x,y}.y)})
                                                                     >>> (\x{_1,_2} -> 
                                                                          let {v1{x} = x{_1,_2}._1;
                                                                               v2{y} = x{_1,_2}._2}
                                                                          in v1{x}*v2{y}))
                        $
                        x1_3 x2_1) }
                 6   <-- Pair(25, 9)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil, _2:Nil})
                                                     >>> (\x{_1,_2} -> 
                                                          let {v1{x} = x{_1,_2}._1;
                                                               v2{y} = x{_1,_2}._2}
                                                          in v1{x}*v2{y}))
                        $
                        x1_1 x2_1) }
                 24  <-- __
                     { _|_ }
             1:
                 10  <-- Cons(19, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_1) }
                 13  <-- Cons(20, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{b} v2{ops} -> v1{b}*v2{ops}) $ x1_1 x2_2) }
                 15  <-- Cons(22, 17)
                     { \x1_1 (x2_1,x2_2,x2_3)->
                       ((\v1{} v2{ops} -> v1{}*v2{ops}) $ x1_1 x2_3) }
                 9   <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             2:
                 17  <-- __
                     { ({ops:__}, {ops:__}, {ops:__}) }
             3:
                 19  <-- Del
                     { ({}) }
                 20  <-- Ins(23)
                     { \x1_1-> ((\v1{b} -> v1{b}) $ x1_1) }
                 22  <-- Keep
                     { ({}) }
                 24  <-- __
                     { _|_ }
             4:
                 23  <-- __
                     { ({b:__}) }
             5:
                 26  <-- Cons(30, 29)
                     { \(x1_1,x1_2,x1_3) (x2_1,x2_2,x2_3)->
                       ((\v1{a} v2{org} -> v1{a}*v2{org})
                        $
                        x1_1 x2_1, (\v1{a1} v2{org} -> v1{a1}*v2{org})
                                   $
                                   x1_2 x2_2, (\v1{a} v2{org} -> v1{a}*v2{org}) $ x1_3 x2_3) }
                 25  <-- Nil
                     { ({}) }
                 24  <-- __
                     { _|_ }
             6:
                 29  <-- __
                     { ({org:__}, {org:__}, {org:__}) }
             7:
                 30  <-- __
                     { ({a:__}, {a1:__}, {a:__}) }
 E81:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E82:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }
 E90:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E92:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({a:__}) }
 E93:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E94:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }}

-- 0.16 seconds is elapsed.