--- Abstract Syntax Tree ------------------------ inpre(x) = inprePrim{2}(x{3},Nil{4}) inprePrim(BLeaf,ys) = Pair{9}(Nil{10},ys{11}) inprePrim(BNode(v,l,r),ys2) = letAt17{17}(inprePrim{22}(r{23},ys2{24}),l{69},v{70}) letAt17(Pair(rs,ys1),l,v) = letAt25{25}(inprePrim{30}(l{31},ys1{32}),rs{65},v{66}) letAt25(Pair(ls,ys),rs,v) = letAt33{33}(unSplitXs{39}(ls{40},v{41},rs{42}),ys{63}) letAt33(Pair3(xs,y,bs),ys) = letAt43{43}(isEquiv{50}(xs{51},y{52},bs{53}),ys{61}) letAt43(Pair(Cons(x2,xs2),y2),ys) = Pair{54}(Cons{55}(x2{56},xs2{57}),Cons{58}(y2{59},ys{60})) letUSX(Pair(xs2,bs),y) = Pair3{78}(Cons{79}(y{80},xs2{81}),y{82},Cons{83}(True{84},bs{85})) unSplitXs(Nil,y,xs) = letUSX{91}(copyFalses{92}(xs{93}),y{94}) unSplitXs(Cons(x,l),z,r) = letAt100{100}(unSplitXs{106}(l{107},z{108},r{109}),x{118}) letAt100(Pair3(xs,y,bs),x) = Pair3{110}(Cons{111}(x{112},xs{113}),y{114},Cons{115}(False{116},bs{117})) copyFalses(Nil) = Pair{123}(Nil{124},Nil{125}) copyFalses(Cons(x,xs)) = letAt129{129}(copyFalses{134}(xs{135}),x{143}) letAt129(Pair(s,t),x) = Pair{136}(Cons{137}(x{138},s{139}),Cons{140}(False{141},t{142})) isEquiv(Nil,y,Nil) = Pair{150}(Nil{151},y{152}) isEquiv(Cons(x,xs),y,Cons(b,bs)) = letAt160{160}(checkEquiv{165}(x{166},y{167},b{168}),bs{185},xs{186}) letAt160(Pair(x1,y1),bs,xs) = letAt169{169}(isEquiv{174}(xs{175},y1{176},bs{177}),x1{183}) letAt169(Pair(xs1,y2),x1) = Pair{178}(Cons{179}(x1{180},xs1{181}),y2{182}) checkEquiv(Z,Z,True) = Pair{196}(Z{197},Z{198}) checkEquiv(S(x),Z,False) = Pair{203}(S{204}(x{205}),Z{206}) checkEquiv(Z,S(y),False) = Pair{211}(Z{212},S{213}(y{214})) checkEquiv(S(x),S(y),b) = letAt220{220}(checkEquiv{225}(x{226},y{227},b{228})) letAt220(Pair(x1,y1)) = Pair{229}(S{230}(x1{231}),S{232}(y1{233})) --- Tree Automata ------------------------------- E179 <-- Cons(E180, E181) { \v1{x1} v2{xs1} -> v1{x1}*v2{xs1} } E140 <-- Cons(E141, E142) { \v1{} v2{t} -> v1{}*v2{t} } E137 <-- Cons(E138, E139) { \v1{x} v2{s} -> v1{x}*v2{s} } E115 <-- Cons(E116, E117) { \v1{} v2{bs} -> v1{}*v2{bs} } E111 <-- Cons(E112, E113) { \v1{x} v2{xs} -> v1{x}*v2{xs} } E83 <-- Cons(E84, E85) { \v1{} v2{bs} -> v1{}*v2{bs} } E79 <-- Cons(E80, E81) { \v1{y} v2{xs2} -> v1{y}*v2{xs2} } E58 <-- Cons(E59, E60) { \v1{y2} v2{ys} -> v1{y2}*v2{ys} } E55 <-- Cons(E56, E57) { \v1{x2} v2{xs2} -> v1{x2}*v2{xs2} } E141 <-- False { {} } E116 <-- False { {} } E151 <-- Nil { {} } E125 <-- Nil { {} } E124 <-- Nil { {} } E10 <-- Nil { {} } E4 <-- Nil { {} } E229 <-- Pair(E230, E232) { \v1{x1} v2{y1} -> v1{x1}*v2{y1} } E211 <-- Pair(E212, E213) { \v1{} v2{y} -> v1{}*v2{y} } E203 <-- Pair(E204, E206) { \v1{x} v2{} -> v1{x}*v2{} } E196 <-- Pair(E197, E198) { \v1{} v2{} -> v1{}*v2{} } E178 <-- Pair(E179, E182) { \v1{x1,xs1} v2{y2} -> v1{x1,xs1}*v2{y2} } E150 <-- Pair(E151, E152) { \v1{} v2{y} -> v1{}*v2{y} } E136 <-- Pair(E137, E140) { \v1{s,x} v2{t} -> v1{s,x}*v2{t} } E123 <-- Pair(E124, E125) { \v1{} v2{} -> v1{}*v2{} } E54 <-- Pair(E55, E58) { \v1{x2,xs2} v2{y2,ys} -> v1{x2,xs2}*v2{y2,ys} } E9 <-- Pair(E10, E11) { \v1{} v2{ys} -> v1{}*v2{ys} } E110 <-- Pair3(E111, E114, E115) { \v1{x,xs} v2{y} v3{bs} -> v1{x,xs}*v2{y}*v3{bs} } E78 <-- Pair3(E79, E82, E83) { \v1{xs2,y} v2{y} v3{bs} -> v1{xs2,y}*v2{y}*v3{bs} } E232 <-- S(E233) { \v1{y1} -> v1{y1} } E230 <-- S(E231) { \v1{x1} -> v1{x1} } E213 <-- S(E214) { \v1{y} -> v1{y} } E204 <-- S(E205) { \v1{x} -> v1{x} } E84 <-- True { {} } E212 <-- Z { {} } E206 <-- Z { {} } E198 <-- Z { {} } E197 <-- Z { {} } E233 <-- __ { {y1:__} } E231 <-- __ { {x1:__} } E228 <-- __ { {b:__} } E227 <-- __ { {y:__} } E226 <-- __ { {x:__} } E214 <-- __ { {y:__} } E205 <-- __ { {x:__} } E182 <-- __ { {y2:__} } E181 <-- __ { {xs1:__} } E180 <-- __ { {x1:__} } E183 <-- __ { {x1:__} } E177 <-- __ { {bs:__} } E176 <-- __ { {y1:__} } E175 <-- __ { {xs:__} } E186 <-- __ { {xs:__} } E185 <-- __ { {bs:__} } E168 <-- __ { {b:__} } E167 <-- __ { {y:__} } E166 <-- __ { {x:__} } E152 <-- __ { {y:__} } E142 <-- __ { {t:__} } E139 <-- __ { {s:__} } E138 <-- __ { {x:__} } E143 <-- __ { {x:__} } E135 <-- __ { {xs:__} } E117 <-- __ { {bs:__} } E114 <-- __ { {y:__} } E113 <-- __ { {xs:__} } E112 <-- __ { {x:__} } E118 <-- __ { {x:__} } E109 <-- __ { {r:__} } E108 <-- __ { {z:__} } E107 <-- __ { {l:__} } E94 <-- __ { {y:__} } E93 <-- __ { {xs:__} } E85 <-- __ { {bs:__} } E82 <-- __ { {y:__} } E81 <-- __ { {xs2:__} } E80 <-- __ { {y:__} } E60 <-- __ { {ys:__} } E59 <-- __ { {y2:__} } E57 <-- __ { {xs2:__} } E56 <-- __ { {x2:__} } E61 <-- __ { {ys:__} } E53 <-- __ { {bs:__} } E52 <-- __ { {y:__} } E51 <-- __ { {xs:__} } E63 <-- __ { {ys:__} } E42 <-- __ { {rs:__} } E41 <-- __ { {v:__} } E40 <-- __ { {ls:__} } E66 <-- __ { {v:__} } E65 <-- __ { {rs:__} } E32 <-- __ { {ys1:__} } E31 <-- __ { {l:__} } E70 <-- __ { {v:__} } E69 <-- __ { {l:__} } E24 <-- __ { {ys2:__} } E23 <-- __ { {r:__} } E11 <-- __ { {ys:__} } E3 <-- __ { {x:__} } FletAt220 <-- E229 { \v{x1,y1} -> {_1:Pair(v{x1,y1}.x1,v{x1,y1}.y1)} } E225 <-- FcheckEquiv { \x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b} } E220 <-- FletAt220 { \x{_1} -> let {v1{b,x,y} = @E225(x{_1}._1)} in v1{b,x,y} } FcheckEquiv <-- E220 { \v{b,x,y} -> {_1:S(v{b,x,y}.x), _2:S(v{b,x,y}.y), _3:v{b,x,y}.b} } FcheckEquiv <-- E211 { \v{y} -> {_1:Z, _2:S(v{y}.y), _3:False} } FcheckEquiv <-- E203 { \v{x} -> {_1:S(v{x}.x), _2:Z, _3:False} } FcheckEquiv <-- E196 { \v{} -> {_1:Z, _2:Z, _3:True} } FletAt169 <-- E178 { \v{x1,xs1,y2} -> {_1:Pair(v{x1,xs1,y2}.xs1,v{x1,xs1,y2}.y2), _2:v{x1,xs1,y2}.x1} } E174 <-- FisEquiv { \x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y1} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y1}*v3{bs} } E169 <-- FletAt169 { \x{_1,_2} -> let {v1{bs,xs,y1} = @E174(x{_1,_2}._1); v2{x1} = x{_1,_2}._2} in v1{bs,xs,y1}*v2{x1} } FletAt160 <-- E169 { \v{bs,x1,xs,y1} -> {_1:Pair(v{bs,x1,xs,y1}.x1,v{bs,x1,xs,y1}.y1), _2:v{bs,x1,xs,y1}.bs, _3:v{bs,x1,xs,y1}.xs} } E165 <-- FcheckEquiv { \x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b} } E160 <-- FletAt160 { \x{_1,_2,_3} -> let {v1{b,x,y} = @E165(x{_1,_2,_3}._1); v2{bs} = x{_1,_2,_3}._2; v3{xs} = x{_1,_2,_3}._3} in v1{b,x,y}*v2{bs}*v3{xs} } FisEquiv <-- E160 { \v{b,bs,x,xs,y} -> {_1:Cons(v{b,bs,x,xs,y}.x,v{b,bs,x,xs,y}.xs), _2:v{b,bs,x,xs,y}.y, _3:Cons(v{b,bs,x,xs,y}.b,v{b,bs,x,xs,y}.bs)} } FisEquiv <-- E150 { \v{y} -> {_1:Nil, _2:v{y}.y, _3:Nil} } FletAt129 <-- E136 { \v{s,t,x} -> {_1:Pair(v{s,t,x}.s,v{s,t,x}.t), _2:v{s,t,x}.x} } E134 <-- FcopyFalses { \x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs} } E129 <-- FletAt129 { \x{_1,_2} -> let {v1{xs} = @E134(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{xs}*v2{x} } FcopyFalses <-- E129 { \v{x,xs} -> {_1:Cons(v{x,xs}.x,v{x,xs}.xs)} } FcopyFalses <-- E123 { \v{} -> {_1:Nil} } FletAt100 <-- E110 { \v{bs,x,xs,y} -> {_1:Pair3(v{bs,x,xs,y}.xs,v{bs,x,xs,y}.y,v{bs,x,xs,y}.bs), _2:v{bs,x,xs,y}.x} } E106 <-- FunSplitXs { \x{_1,_2,_3} -> let {v1{l} = x{_1,_2,_3}._1; v2{z} = x{_1,_2,_3}._2; v3{r} = x{_1,_2,_3}._3} in v1{l}*v2{z}*v3{r} } E100 <-- FletAt100 { \x{_1,_2} -> let {v1{l,r,z} = @E106(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{l,r,z}*v2{x} } FunSplitXs <-- E100 { \v{l,r,x,z} -> {_1:Cons(v{l,r,x,z}.x,v{l,r,x,z}.l), _2:v{l,r,x,z}.z, _3:v{l,r,x,z}.r} } E92 <-- FcopyFalses { \x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs} } E91 <-- FletUSX { \x{_1,_2} -> let {v1{xs} = @E92(x{_1,_2}._1); v2{y} = x{_1,_2}._2} in v1{xs}*v2{y} } FunSplitXs <-- E91 { \v{xs,y} -> {_1:Nil, _2:v{xs,y}.y, _3:v{xs,y}.xs} } FletUSX <-- E78 { \v{bs,xs2,y} -> {_1:Pair(v{bs,xs2,y}.xs2,v{bs,xs2,y}.bs), _2:v{bs,xs2,y}.y} } FletAt43 <-- E54 { \v{x2,xs2,y2,ys} -> {_1:Pair(Cons(v{x2,xs2,y2,ys}.x2,v{x2,xs2,y2,ys}.xs2),v{x2,xs2,y2,ys}.y2), _2:v{x2,xs2,y2,ys}.ys} } E50 <-- FisEquiv { \x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y}*v3{bs} } E43 <-- FletAt43 { \x{_1,_2} -> let {v1{bs,xs,y} = @E50(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{bs,xs,y}*v2{ys} } FletAt33 <-- E43 { \v{bs,xs,y,ys} -> {_1:Pair3(v{bs,xs,y,ys}.xs,v{bs,xs,y,ys}.y,v{bs,xs,y,ys}.bs), _2:v{bs,xs,y,ys}.ys} } E39 <-- FunSplitXs { \x{_1,_2,_3} -> let {v1{ls} = x{_1,_2,_3}._1; v2{v} = x{_1,_2,_3}._2; v3{rs} = x{_1,_2,_3}._3} in v1{ls}*v2{v}*v3{rs} } E33 <-- FletAt33 { \x{_1,_2} -> let {v1{ls,rs,v} = @E39(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{ls,rs,v}*v2{ys} } FletAt25 <-- E33 { \v{ls,rs,v,ys} -> {_1:Pair(v{ls,rs,v,ys}.ls,v{ls,rs,v,ys}.ys), _2:v{ls,rs,v,ys}.rs, _3:v{ls,rs,v,ys}.v} } E30 <-- FinprePrim { \x{_1,_2} -> let {v1{l} = x{_1,_2}._1; v2{ys1} = x{_1,_2}._2} in v1{l}*v2{ys1} } E25 <-- FletAt25 { \x{_1,_2,_3} -> let {v1{l,ys1} = @E30(x{_1,_2,_3}._1); v2{rs} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{l,ys1}*v2{rs}*v3{v} } FletAt17 <-- E25 { \v{l,rs,v,ys1} -> {_1:Pair(v{l,rs,v,ys1}.rs,v{l,rs,v,ys1}.ys1), _2:v{l,rs,v,ys1}.l, _3:v{l,rs,v,ys1}.v} } E22 <-- FinprePrim { \x{_1,_2} -> let {v1{r} = x{_1,_2}._1; v2{ys2} = x{_1,_2}._2} in v1{r}*v2{ys2} } E17 <-- FletAt17 { \x{_1,_2,_3} -> let {v1{r,ys2} = @E22(x{_1,_2,_3}._1); v2{l} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{r,ys2}*v2{l}*v3{v} } FinprePrim <-- E17 { \v{l,r,v,ys2} -> {_1:BNode(v{l,r,v,ys2}.v,v{l,r,v,ys2}.l,v{l,r,v,ys2}.r), _2:v{l,r,v,ys2}.ys2} } FinprePrim <-- E9 { \v{ys} -> {_1:BLeaf, _2:v{ys}.ys} } E2 <-- FinprePrim { \x{_1,_2} -> let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{} } Finpre <-- E2 { \v{x} -> {_1:v{x}.x} } --- Guided Tree Automata ------------------------ {Finpre: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> __() 2 --> __() 3 --> __() 4 --> Cons(6,5) 4 --> Nil() 5 --> __() 6 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(13, 6) { \x1_1 x2_1-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{}) >>> (\v{x} -> {_1:v{x}.x})) $ x1_1 x2_1) } 1 <-- Pair(13, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{}) >>> (\v{x} -> {_1:v{x}.x})) $ x1_1 x2_1) } 1 <-- Pair(14, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{x2,xs2} v2{y2,ys} -> v1{x2,xs2}*v2{y2,ys} >2> (\v{x2,xs2,y2,ys} -> {_1:Pair(Cons(v{x2,xs2,y2,ys}.x2,v{x2,xs2,y2,ys}.xs2),v{x2,xs2,y2,ys}.y2), _2:v{x2,xs2,y2,ys}.ys}) >>> (\x{_1,_2} -> let {v1{bs,xs,y} = @E50(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{bs,xs,y}*v2{ys}) >>> ((\v{bs,xs,y,ys} -> {_1:Pair3(v{bs,xs,y,ys}.xs,v{bs,xs,y,ys}.y,v{bs,xs,y,ys}.bs), _2:v{bs,xs,y,ys}.ys}) >>> (\x{_1,_2} -> let {v1{ls,rs,v} = @E39(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{ls,rs,v}*v2{ys})) >>> ((\v{ls,rs,v,ys} -> {_1:Pair(v{ls,rs,v,ys}.ls,v{ls,rs,v,ys}.ys), _2:v{ls,rs,v,ys}.rs, _3:v{ls,rs,v,ys}.v}) >>> (\x{_1,_2,_3} -> let {v1{l,ys1} = @E30(x{_1,_2,_3}._1); v2{rs} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{l,ys1}*v2{rs}*v3{v})) >>> ((\v{l,rs,v,ys1} -> {_1:Pair(v{l,rs,v,ys1}.rs,v{l,rs,v,ys1}.ys1), _2:v{l,rs,v,ys1}.l, _3:v{l,rs,v,ys1}.v}) >>> (\x{_1,_2,_3} -> let {v1{r,ys2} = @E22(x{_1,_2,_3}._1); v2{l} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{r,ys2}*v2{l}*v3{v})) >>> ((\v{l,r,v,ys2} -> {_1:BNode(v{l,r,v,ys2}.v,v{l,r,v,ys2}.l,v{l,r,v,ys2}.r), _2:v{l,r,v,ys2}.ys2}) >>> (\x{_1,_2} -> let {v1{x} = x{_1,_2}._1; v2{} = @E4(x{_1,_2}._2)} in v1{x}*v2{})) >>> (\v{x} -> {_1:v{x}.x})) $ x1_1 x2_2) } 12 <-- __ { _|_ } 1: 7 <-- Cons(11, 10) { \x1_1 x2_1-> ({ys:__}, (\v1{y2} v2{ys} -> v1{y2}*v2{ys}) $ x1_1 x2_1) } 6 <-- __ { ({ys:__}) } 2: 10 <-- __ { ({ys:__}) } 3: 11 <-- __ { ({y2:__}) } 4: 14 <-- Cons(18, 17) { \x1_1 x2_1-> ((\v1{x2} v2{xs2} -> v1{x2}*v2{xs2}) $ x1_1 x2_1) } 13 <-- Nil { ({}) } 12 <-- __ { _|_ } 5: 17 <-- __ { ({xs2:__}) } 6: 18 <-- __ { ({x2:__}) } E3: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E4: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Nil() GUIDED TRANSITIONS: 0: 1 <-- Nil { ({}) } 0 <-- __ { _|_ } E22: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> __() 2 --> __() 3 --> __() 4 --> Cons(6,5) 4 --> Nil() 5 --> __() 6 --> __() GUIDED TRANSITIONS: 0: 4 <-- Pair(13, 6) { \x1_1 x2_1-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{r} = x{_1,_2}._1; v2{ys2} = x{_1,_2}._2} in v1{r}*v2{ys2})) $ x1_1 x2_1) } 4 <-- Pair(13, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{r} = x{_1,_2}._1; v2{ys2} = x{_1,_2}._2} in v1{r}*v2{ys2})) $ x1_1 x2_1) } 4 <-- Pair(14, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{x2,xs2} v2{y2,ys} -> v1{x2,xs2}*v2{y2,ys} >2> (\v{x2,xs2,y2,ys} -> {_1:Pair(Cons(v{x2,xs2,y2,ys}.x2,v{x2,xs2,y2,ys}.xs2),v{x2,xs2,y2,ys}.y2), _2:v{x2,xs2,y2,ys}.ys}) >>> (\x{_1,_2} -> let {v1{bs,xs,y} = @E50(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{bs,xs,y}*v2{ys}) >>> ((\v{bs,xs,y,ys} -> {_1:Pair3(v{bs,xs,y,ys}.xs,v{bs,xs,y,ys}.y,v{bs,xs,y,ys}.bs), _2:v{bs,xs,y,ys}.ys}) >>> (\x{_1,_2} -> let {v1{ls,rs,v} = @E39(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{ls,rs,v}*v2{ys})) >>> ((\v{ls,rs,v,ys} -> {_1:Pair(v{ls,rs,v,ys}.ls,v{ls,rs,v,ys}.ys), _2:v{ls,rs,v,ys}.rs, _3:v{ls,rs,v,ys}.v}) >>> (\x{_1,_2,_3} -> let {v1{l,ys1} = @E30(x{_1,_2,_3}._1); v2{rs} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{l,ys1}*v2{rs}*v3{v})) >>> ((\v{l,rs,v,ys1} -> {_1:Pair(v{l,rs,v,ys1}.rs,v{l,rs,v,ys1}.ys1), _2:v{l,rs,v,ys1}.l, _3:v{l,rs,v,ys1}.v}) >>> (\x{_1,_2,_3} -> let {v1{r,ys2} = @E22(x{_1,_2,_3}._1); v2{l} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{r,ys2}*v2{l}*v3{v})) >>> (\v{l,r,v,ys2} -> {_1:BNode(v{l,r,v,ys2}.v,v{l,r,v,ys2}.l,v{l,r,v,ys2}.r), _2:v{l,r,v,ys2}.ys2}) >>> (\x{_1,_2} -> let {v1{r} = x{_1,_2}._1; v2{ys2} = x{_1,_2}._2} in v1{r}*v2{ys2})) $ x1_1 x2_2) } 12 <-- __ { _|_ } 1: 7 <-- Cons(11, 10) { \x1_1 x2_1-> ({ys:__}, (\v1{y2} v2{ys} -> v1{y2}*v2{ys}) $ x1_1 x2_1) } 6 <-- __ { ({ys:__}) } 2: 10 <-- __ { ({ys:__}) } 3: 11 <-- __ { ({y2:__}) } 4: 14 <-- Cons(18, 17) { \x1_1 x2_1-> ((\v1{x2} v2{xs2} -> v1{x2}*v2{xs2}) $ x1_1 x2_1) } 13 <-- Nil { ({}) } 12 <-- __ { _|_ } 5: 17 <-- __ { ({xs2:__}) } 6: 18 <-- __ { ({x2:__}) } E23: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({r:__}) } E24: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ys2:__}) } E30: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> __() 2 --> __() 3 --> __() 4 --> Cons(6,5) 4 --> Nil() 5 --> __() 6 --> __() GUIDED TRANSITIONS: 0: 4 <-- Pair(13, 6) { \x1_1 x2_1-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{l} = x{_1,_2}._1; v2{ys1} = x{_1,_2}._2} in v1{l}*v2{ys1})) $ x1_1 x2_1) } 4 <-- Pair(13, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{ys} -> v1{}*v2{ys} >2> (\v{ys} -> {_1:BLeaf, _2:v{ys}.ys}) >>> (\x{_1,_2} -> let {v1{l} = x{_1,_2}._1; v2{ys1} = x{_1,_2}._2} in v1{l}*v2{ys1})) $ x1_1 x2_1) } 4 <-- Pair(14, 7) { \x1_1 (x2_1,x2_2)-> ((\v1{x2,xs2} v2{y2,ys} -> v1{x2,xs2}*v2{y2,ys} >2> (\v{x2,xs2,y2,ys} -> {_1:Pair(Cons(v{x2,xs2,y2,ys}.x2,v{x2,xs2,y2,ys}.xs2),v{x2,xs2,y2,ys}.y2), _2:v{x2,xs2,y2,ys}.ys}) >>> (\x{_1,_2} -> let {v1{bs,xs,y} = @E50(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{bs,xs,y}*v2{ys}) >>> ((\v{bs,xs,y,ys} -> {_1:Pair3(v{bs,xs,y,ys}.xs,v{bs,xs,y,ys}.y,v{bs,xs,y,ys}.bs), _2:v{bs,xs,y,ys}.ys}) >>> (\x{_1,_2} -> let {v1{ls,rs,v} = @E39(x{_1,_2}._1); v2{ys} = x{_1,_2}._2} in v1{ls,rs,v}*v2{ys})) >>> ((\v{ls,rs,v,ys} -> {_1:Pair(v{ls,rs,v,ys}.ls,v{ls,rs,v,ys}.ys), _2:v{ls,rs,v,ys}.rs, _3:v{ls,rs,v,ys}.v}) >>> (\x{_1,_2,_3} -> let {v1{l,ys1} = @E30(x{_1,_2,_3}._1); v2{rs} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{l,ys1}*v2{rs}*v3{v})) >>> ((\v{l,rs,v,ys1} -> {_1:Pair(v{l,rs,v,ys1}.rs,v{l,rs,v,ys1}.ys1), _2:v{l,rs,v,ys1}.l, _3:v{l,rs,v,ys1}.v}) >>> (\x{_1,_2,_3} -> let {v1{r,ys2} = @E22(x{_1,_2,_3}._1); v2{l} = x{_1,_2,_3}._2; v3{v} = x{_1,_2,_3}._3} in v1{r,ys2}*v2{l}*v3{v})) >>> (\v{l,r,v,ys2} -> {_1:BNode(v{l,r,v,ys2}.v,v{l,r,v,ys2}.l,v{l,r,v,ys2}.r), _2:v{l,r,v,ys2}.ys2}) >>> (\x{_1,_2} -> let {v1{l} = x{_1,_2}._1; v2{ys1} = x{_1,_2}._2} in v1{l}*v2{ys1})) $ x1_1 x2_2) } 12 <-- __ { _|_ } 1: 7 <-- Cons(11, 10) { \x1_1 x2_1-> ({ys:__}, (\v1{y2} v2{ys} -> v1{y2}*v2{ys}) $ x1_1 x2_1) } 6 <-- __ { ({ys:__}) } 2: 10 <-- __ { ({ys:__}) } 3: 11 <-- __ { ({y2:__}) } 4: 14 <-- Cons(18, 17) { \x1_1 x2_1-> ((\v1{x2} v2{xs2} -> v1{x2}*v2{xs2}) $ x1_1 x2_1) } 13 <-- Nil { ({}) } 12 <-- __ { _|_ } 5: 17 <-- __ { ({xs2:__}) } 6: 18 <-- __ { ({x2:__}) } E31: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({l:__}) } E32: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ys1:__}) } E39: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair3(5,4,1) 1 --> Cons(3,2) 2 --> __() 3 --> False() 3 --> True() 4 --> __() 5 --> Cons(7,6) 6 --> __() 7 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair3(18, 16, 7) { \(x1_1,x1_2) (x2_1,x2_2) x3_1-> ((\v1{xs2,y} v2{y} v3{bs} -> v1{xs2,y}*v2{y}*v3{bs} >3> (\v{bs,xs2,y} -> {_1:Pair(v{bs,xs2,y}.xs2,v{bs,xs2,y}.bs), _2:v{bs,xs2,y}.y}) >>> (\x{_1,_2} -> let {v1{xs} = @E92(x{_1,_2}._1); v2{y} = x{_1,_2}._2} in v1{xs}*v2{y}) >>> (\v{xs,y} -> {_1:Nil, _2:v{xs,y}.y, _3:v{xs,y}.xs}) >>> (\x{_1,_2,_3} -> let {v1{ls} = x{_1,_2,_3}._1; v2{v} = x{_1,_2,_3}._2; v3{rs} = x{_1,_2,_3}._3} in v1{ls}*v2{v}*v3{rs})) $ x1_1 x2_1 x3_1) } 1 <-- Pair3(18, 16, 10) { \(x1_1,x1_2) (x2_1,x2_2) x3_1-> ((\v1{x,xs} v2{y} v3{bs} -> v1{x,xs}*v2{y}*v3{bs} >3> (\v{bs,x,xs,y} -> {_1:Pair3(v{bs,x,xs,y}.xs,v{bs,x,xs,y}.y,v{bs,x,xs,y}.bs), _2:v{bs,x,xs,y}.x}) >>> (\x{_1,_2} -> let {v1{l,r,z} = @E106(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{l,r,z}*v2{x}) >>> (\v{l,r,x,z} -> {_1:Cons(v{l,r,x,z}.x,v{l,r,x,z}.l), _2:v{l,r,x,z}.z, _3:v{l,r,x,z}.r}) >>> (\x{_1,_2,_3} -> let {v1{ls} = x{_1,_2,_3}._1; v2{v} = x{_1,_2,_3}._2; v3{rs} = x{_1,_2,_3}._3} in v1{ls}*v2{v}*v3{rs})) $ x1_2 x2_2 x3_1) } 17 <-- __ { _|_ } 1: 7 <-- Cons(14, 12) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{bs} -> v1{}*v2{bs}) $ x1_1 x2_1) } 10 <-- Cons(15, 12) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{bs} -> v1{}*v2{bs}) $ x1_1 x2_2) } 17 <-- __ { _|_ } 2: 12 <-- __ { ({bs:__}, {bs:__}) } 3: 15 <-- False { ({}) } 14 <-- True { ({}) } 17 <-- __ { _|_ } 4: 16 <-- __ { ({y:__}, {y:__}) } 5: 18 <-- Cons(22, 21) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{y} v2{xs2} -> v1{y}*v2{xs2}) $ x1_1 x2_1, (\v1{x} v2{xs} -> v1{x}*v2{xs}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 6: 21 <-- __ { ({xs2:__}, {xs:__}) } 7: 22 <-- __ { ({y:__}, {x:__}) } E40: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ls:__}) } E41: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E42: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({rs:__}) } E50: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> Cons(4,3) 2 --> Nil() 3 --> __() 4 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(7, 5) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{y} -> v1{}*v2{y} >2> (\v{y} -> {_1:Nil, _2:v{y}.y, _3:Nil}) >>> (\x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y}*v3{bs})) $ x1_1 x2_1) } 1 <-- Pair(8, 5) { \x1_1 (x2_1,x2_2)-> ((\v1{x1,xs1} v2{y2} -> v1{x1,xs1}*v2{y2} >2> (\v{x1,xs1,y2} -> {_1:Pair(v{x1,xs1,y2}.xs1,v{x1,xs1,y2}.y2), _2:v{x1,xs1,y2}.x1}) >>> (\x{_1,_2} -> let {v1{bs,xs,y1} = @E174(x{_1,_2}._1); v2{x1} = x{_1,_2}._2} in v1{bs,xs,y1}*v2{x1}) >>> ((\v{bs,x1,xs,y1} -> {_1:Pair(v{bs,x1,xs,y1}.x1,v{bs,x1,xs,y1}.y1), _2:v{bs,x1,xs,y1}.bs, _3:v{bs,x1,xs,y1}.xs}) >>> (\x{_1,_2,_3} -> let {v1{b,x,y} = @E165(x{_1,_2,_3}._1); v2{bs} = x{_1,_2,_3}._2; v3{xs} = x{_1,_2,_3}._3} in v1{b,x,y}*v2{bs}*v3{xs})) >>> (\v{b,bs,x,xs,y} -> {_1:Cons(v{b,bs,x,xs,y}.x,v{b,bs,x,xs,y}.xs), _2:v{b,bs,x,xs,y}.y, _3:Cons(v{b,bs,x,xs,y}.b,v{b,bs,x,xs,y}.bs)}) >>> (\x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y}*v3{bs})) $ x1_1 x2_2) } 6 <-- __ { _|_ } 1: 5 <-- __ { ({y:__}, {y2:__}) } 2: 8 <-- Cons(12, 11) { \x1_1 x2_1-> ((\v1{x1} v2{xs1} -> v1{x1}*v2{xs1}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 6 <-- __ { _|_ } 3: 11 <-- __ { ({xs1:__}) } 4: 12 <-- __ { ({x1:__}) } E51: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({xs:__}) } E52: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E53: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({bs:__}) } E61: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ys:__}) } E63: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ys:__}) } E65: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({rs:__}) } E66: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E69: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({l:__}) } E70: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E92: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> Nil() 2 --> __() 3 --> False() 4 --> Cons(6,5) 4 --> Nil() 5 --> __() 6 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(16, 8) { \x1_1 x2_1-> ((\v1{s,x} v2{t} -> v1{s,x}*v2{t} >2> (\v{s,t,x} -> {_1:Pair(v{s,t,x}.s,v{s,t,x}.t), _2:v{s,t,x}.x}) >>> (\x{_1,_2} -> let {v1{xs} = @E134(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{xs}*v2{x}) >>> (\v{x,xs} -> {_1:Cons(v{x,xs}.x,v{x,xs}.xs)}) >>> (\x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs})) $ x1_1 x2_1) } 1 <-- Pair(15, 7) { \x1_1 x2_1-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil}) >>> (\x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs})) $ x1_1 x2_1) } 14 <-- __ { _|_ } 1: 8 <-- Cons(13, 11) { \x1_1 x2_1-> ((\v1{} v2{t} -> v1{}*v2{t}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 14 <-- __ { _|_ } 2: 11 <-- __ { ({t:__}) } 3: 13 <-- False { ({}) } 14 <-- __ { _|_ } 4: 16 <-- Cons(20, 19) { \x1_1 x2_1-> ((\v1{x} v2{s} -> v1{x}*v2{s}) $ x1_1 x2_1) } 15 <-- Nil { ({}) } 14 <-- __ { _|_ } 5: 19 <-- __ { ({s:__}) } 6: 20 <-- __ { ({x:__}) } E93: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({xs:__}) } E94: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E106: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair3(5,4,1) 1 --> Cons(3,2) 2 --> __() 3 --> False() 3 --> True() 4 --> __() 5 --> Cons(7,6) 6 --> __() 7 --> __() GUIDED TRANSITIONS: 0: 4 <-- Pair3(18, 16, 7) { \(x1_1,x1_2) (x2_1,x2_2) x3_1-> ((\v1{xs2,y} v2{y} v3{bs} -> v1{xs2,y}*v2{y}*v3{bs} >3> (\v{bs,xs2,y} -> {_1:Pair(v{bs,xs2,y}.xs2,v{bs,xs2,y}.bs), _2:v{bs,xs2,y}.y}) >>> (\x{_1,_2} -> let {v1{xs} = @E92(x{_1,_2}._1); v2{y} = x{_1,_2}._2} in v1{xs}*v2{y}) >>> (\v{xs,y} -> {_1:Nil, _2:v{xs,y}.y, _3:v{xs,y}.xs}) >>> (\x{_1,_2,_3} -> let {v1{l} = x{_1,_2,_3}._1; v2{z} = x{_1,_2,_3}._2; v3{r} = x{_1,_2,_3}._3} in v1{l}*v2{z}*v3{r})) $ x1_1 x2_1 x3_1) } 4 <-- Pair3(18, 16, 10) { \(x1_1,x1_2) (x2_1,x2_2) x3_1-> ((\v1{x,xs} v2{y} v3{bs} -> v1{x,xs}*v2{y}*v3{bs} >3> (\v{bs,x,xs,y} -> {_1:Pair3(v{bs,x,xs,y}.xs,v{bs,x,xs,y}.y,v{bs,x,xs,y}.bs), _2:v{bs,x,xs,y}.x}) >>> (\x{_1,_2} -> let {v1{l,r,z} = @E106(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{l,r,z}*v2{x}) >>> (\v{l,r,x,z} -> {_1:Cons(v{l,r,x,z}.x,v{l,r,x,z}.l), _2:v{l,r,x,z}.z, _3:v{l,r,x,z}.r}) >>> (\x{_1,_2,_3} -> let {v1{l} = x{_1,_2,_3}._1; v2{z} = x{_1,_2,_3}._2; v3{r} = x{_1,_2,_3}._3} in v1{l}*v2{z}*v3{r})) $ x1_2 x2_2 x3_1) } 17 <-- __ { _|_ } 1: 7 <-- Cons(14, 12) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{bs} -> v1{}*v2{bs}) $ x1_1 x2_1) } 10 <-- Cons(15, 12) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{bs} -> v1{}*v2{bs}) $ x1_1 x2_2) } 17 <-- __ { _|_ } 2: 12 <-- __ { ({bs:__}, {bs:__}) } 3: 15 <-- False { ({}) } 14 <-- True { ({}) } 17 <-- __ { _|_ } 4: 16 <-- __ { ({y:__}, {y:__}) } 5: 18 <-- Cons(22, 21) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{y} v2{xs2} -> v1{y}*v2{xs2}) $ x1_1 x2_1, (\v1{x} v2{xs} -> v1{x}*v2{xs}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 6: 21 <-- __ { ({xs2:__}, {xs:__}) } 7: 22 <-- __ { ({y:__}, {x:__}) } E107: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({l:__}) } E108: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({z:__}) } E109: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({r:__}) } E118: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E134: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> Nil() 2 --> __() 3 --> False() 4 --> Cons(6,5) 4 --> Nil() 5 --> __() 6 --> __() GUIDED TRANSITIONS: 0: 3 <-- Pair(16, 8) { \x1_1 x2_1-> ((\v1{s,x} v2{t} -> v1{s,x}*v2{t} >2> (\v{s,t,x} -> {_1:Pair(v{s,t,x}.s,v{s,t,x}.t), _2:v{s,t,x}.x}) >>> (\x{_1,_2} -> let {v1{xs} = @E134(x{_1,_2}._1); v2{x} = x{_1,_2}._2} in v1{xs}*v2{x}) >>> (\v{x,xs} -> {_1:Cons(v{x,xs}.x,v{x,xs}.xs)}) >>> (\x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs})) $ x1_1 x2_1) } 3 <-- Pair(15, 7) { \x1_1 x2_1-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil}) >>> (\x{_1} -> let {v1{xs} = x{_1}._1} in v1{xs})) $ x1_1 x2_1) } 14 <-- __ { _|_ } 1: 8 <-- Cons(13, 11) { \x1_1 x2_1-> ((\v1{} v2{t} -> v1{}*v2{t}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 14 <-- __ { _|_ } 2: 11 <-- __ { ({t:__}) } 3: 13 <-- False { ({}) } 14 <-- __ { _|_ } 4: 16 <-- Cons(20, 19) { \x1_1 x2_1-> ((\v1{x} v2{s} -> v1{x}*v2{s}) $ x1_1 x2_1) } 15 <-- Nil { ({}) } 14 <-- __ { _|_ } 5: 19 <-- __ { ({s:__}) } 6: 20 <-- __ { ({x:__}) } E135: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({xs:__}) } E143: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E165: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(3,1) 1 --> S(2) 1 --> Z() 2 --> __() 3 --> S(4) 3 --> Z() 4 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(12, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z, _2:Z, _3:True}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_1 x2_1) } 1 <-- Pair(12, 8) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{} v2{y} -> v1{}*v2{y} >2> (\v{y} -> {_1:Z, _2:S(v{y}.y), _3:False}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_2 x2_1) } 1 <-- Pair(13, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{x} v2{} -> v1{x}*v2{} >2> (\v{x} -> {_1:S(v{x}.x), _2:Z, _3:False}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_1 x2_2) } 1 <-- Pair(13, 8) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{x1} v2{y1} -> v1{x1}*v2{y1} >2> (\v{x1,y1} -> {_1:Pair(v{x1,y1}.x1,v{x1,y1}.y1)}) >>> (\x{_1} -> let {v1{b,x,y} = @E225(x{_1}._1)} in v1{b,x,y}) >>> (\v{b,x,y} -> {_1:S(v{b,x,y}.x), _2:S(v{b,x,y}.y), _3:v{b,x,y}.b}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_2 x2_2) } 11 <-- __ { _|_ } 1: 8 <-- S(10) { \(x1_1,x1_2)-> ((\v1{y} -> v1{y}) $ x1_1, (\v1{y1} -> v1{y1}) $ x1_2) } 7 <-- Z { ({}, {}) } 11 <-- __ { _|_ } 2: 10 <-- __ { ({y:__}, {y1:__}) } 3: 13 <-- S(15) { \(x1_1,x1_2)-> ((\v1{x} -> v1{x}) $ x1_1, (\v1{x1} -> v1{x1}) $ x1_2) } 12 <-- Z { ({}, {}) } 11 <-- __ { _|_ } 4: 15 <-- __ { ({x:__}, {x1:__}) } E166: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E167: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E168: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({b:__}) } E174: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> Cons(4,3) 2 --> Nil() 3 --> __() 4 --> __() GUIDED TRANSITIONS: 0: 3 <-- Pair(7, 5) { \x1_1 (x2_1,x2_2)-> ((\v1{} v2{y} -> v1{}*v2{y} >2> (\v{y} -> {_1:Nil, _2:v{y}.y, _3:Nil}) >>> (\x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y1} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y1}*v3{bs})) $ x1_1 x2_1) } 3 <-- Pair(8, 5) { \x1_1 (x2_1,x2_2)-> ((\v1{x1,xs1} v2{y2} -> v1{x1,xs1}*v2{y2} >2> (\v{x1,xs1,y2} -> {_1:Pair(v{x1,xs1,y2}.xs1,v{x1,xs1,y2}.y2), _2:v{x1,xs1,y2}.x1}) >>> (\x{_1,_2} -> let {v1{bs,xs,y1} = @E174(x{_1,_2}._1); v2{x1} = x{_1,_2}._2} in v1{bs,xs,y1}*v2{x1}) >>> ((\v{bs,x1,xs,y1} -> {_1:Pair(v{bs,x1,xs,y1}.x1,v{bs,x1,xs,y1}.y1), _2:v{bs,x1,xs,y1}.bs, _3:v{bs,x1,xs,y1}.xs}) >>> (\x{_1,_2,_3} -> let {v1{b,x,y} = @E165(x{_1,_2,_3}._1); v2{bs} = x{_1,_2,_3}._2; v3{xs} = x{_1,_2,_3}._3} in v1{b,x,y}*v2{bs}*v3{xs})) >>> (\v{b,bs,x,xs,y} -> {_1:Cons(v{b,bs,x,xs,y}.x,v{b,bs,x,xs,y}.xs), _2:v{b,bs,x,xs,y}.y, _3:Cons(v{b,bs,x,xs,y}.b,v{b,bs,x,xs,y}.bs)}) >>> (\x{_1,_2,_3} -> let {v1{xs} = x{_1,_2,_3}._1; v2{y1} = x{_1,_2,_3}._2; v3{bs} = x{_1,_2,_3}._3} in v1{xs}*v2{y1}*v3{bs})) $ x1_1 x2_2) } 6 <-- __ { _|_ } 1: 5 <-- __ { ({y:__}, {y2:__}) } 2: 8 <-- Cons(12, 11) { \x1_1 x2_1-> ((\v1{x1} v2{xs1} -> v1{x1}*v2{xs1}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 6 <-- __ { _|_ } 3: 11 <-- __ { ({xs1:__}) } 4: 12 <-- __ { ({x1:__}) } E175: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({xs:__}) } E176: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y1:__}) } E177: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({bs:__}) } E183: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x1:__}) } E185: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({bs:__}) } E186: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({xs:__}) } E225: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(3,1) 1 --> S(2) 1 --> Z() 2 --> __() 3 --> S(4) 3 --> Z() 4 --> __() GUIDED TRANSITIONS: 0: 5 <-- Pair(12, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z, _2:Z, _3:True}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_1 x2_1) } 5 <-- Pair(12, 8) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{} v2{y} -> v1{}*v2{y} >2> (\v{y} -> {_1:Z, _2:S(v{y}.y), _3:False}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_2 x2_1) } 5 <-- Pair(13, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{x} v2{} -> v1{x}*v2{} >2> (\v{x} -> {_1:S(v{x}.x), _2:Z, _3:False}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_1 x2_2) } 5 <-- Pair(13, 8) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{x1} v2{y1} -> v1{x1}*v2{y1} >2> (\v{x1,y1} -> {_1:Pair(v{x1,y1}.x1,v{x1,y1}.y1)}) >>> (\x{_1} -> let {v1{b,x,y} = @E225(x{_1}._1)} in v1{b,x,y}) >>> (\v{b,x,y} -> {_1:S(v{b,x,y}.x), _2:S(v{b,x,y}.y), _3:v{b,x,y}.b}) >>> (\x{_1,_2,_3} -> let {v1{x} = x{_1,_2,_3}._1; v2{y} = x{_1,_2,_3}._2; v3{b} = x{_1,_2,_3}._3} in v1{x}*v2{y}*v3{b})) $ x1_2 x2_2) } 11 <-- __ { _|_ } 1: 8 <-- S(10) { \(x1_1,x1_2)-> ((\v1{y} -> v1{y}) $ x1_1, (\v1{y1} -> v1{y1}) $ x1_2) } 7 <-- Z { ({}, {}) } 11 <-- __ { _|_ } 2: 10 <-- __ { ({y:__}, {y1:__}) } 3: 13 <-- S(15) { \(x1_1,x1_2)-> ((\v1{x} -> v1{x}) $ x1_1, (\v1{x1} -> v1{x1}) $ x1_2) } 12 <-- Z { ({}, {}) } 11 <-- __ { _|_ } 4: 15 <-- __ { ({x:__}, {x1:__}) } E226: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E227: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E228: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({b:__}) }} -- 0.26 seconds is elapsed.