--- Abstract Syntax Tree ------------------------ inpre(BLeaf) = Pair{3}(Nil{4},Nil{5}) inpre(BNode(v,l,r)) = dappend{10}(v{11},inpre{12}(l{13}),inpre{14}(r{15})) dappend(v,Pair(li,lp),Pair(ri,rp)) = letAt24{24}(dapp_body{31}(v{32},Pair{33}(li{34},lp{35}),Pair{36}(ri{37},rp{38}))) letAt24(Pair(v,Pair(i,p))) = Pair{39}(i{40},Cons{41}(v{42},p{43})) dapp_body(v,Pair(Nil,Nil),Pair(ri,rp)) = Pair{53}(v{54},Pair{55}(Cons{56}(v{57},ri{58}),rp{59})) dapp_body(v,Pair(Cons(x,li),Cons(y,lp)),Pair(ri,rp)) = letAt71{71}(neq{76}(v{77},x{78}),li{107},lp{108},ri{109},rp{110},y{111}) letAt71(Pair(v1,x1),li,lp,ri,rp,y) = letAt79{79}(dapp_body{86}(v1{87},Pair{88}(li{89},lp{90}),Pair{91}(ri{92},rp{93})),x1{103},y{104}) letAt79(Pair(v2,Pair(i,p)),x1,y) = Pair{94}(v2{95},Pair{96}(Cons{97}(x1{98},i{99}),Cons{100}(y{101},p{102}))) neq(Z,S(n)) = Pair{123}(Z{124},S{125}(n{126})) neq(S(m),Z) = Pair{130}(S{131}(m{132}),Z{133}) neq(S(m),S(n)) = letAt138{138}(neq{143}(m{144},n{145})) letAt138(Pair(m1,n1)) = Pair{146}(S{147}(m1{148}),S{149}(n1{150})) --- Tree Automata ------------------------------- E100 <-- Cons(E101, E102) { \v1{y} v2{p} -> v1{y}*v2{p} } E97 <-- Cons(E98, E99) { \v1{x1} v2{i} -> v1{x1}*v2{i} } E56 <-- Cons(E57, E58) { \v1{v} v2{ri} -> v1{v}*v2{ri} } E41 <-- Cons(E42, E43) { \v1{v} v2{p} -> v1{v}*v2{p} } E5 <-- Nil { {} } E4 <-- Nil { {} } E146 <-- Pair(E147, E149) { \v1{m1} v2{n1} -> v1{m1}*v2{n1} } E130 <-- Pair(E131, E133) { \v1{m} v2{} -> v1{m}*v2{} } E123 <-- Pair(E124, E125) { \v1{} v2{n} -> v1{}*v2{n} } E96 <-- Pair(E97, E100) { \v1{i,x1} v2{p,y} -> v1{i,x1}*v2{p,y} } E94 <-- Pair(E95, E96) { \v1{v2} v2{i,p,x1,y} -> v1{v2}*v2{i,p,x1,y} } E91 <-- Pair(E92, E93) { \v1{ri} v2{rp} -> v1{ri}*v2{rp} } E88 <-- Pair(E89, E90) { \v1{li} v2{lp} -> v1{li}*v2{lp} } E55 <-- Pair(E56, E59) { \v1{ri,v} v2{rp} -> v1{ri,v}*v2{rp} } E53 <-- Pair(E54, E55) { \v1{v} v2{ri,rp,v} -> v1{v}*v2{ri,rp,v} } E39 <-- Pair(E40, E41) { \v1{i} v2{p,v} -> v1{i}*v2{p,v} } E36 <-- Pair(E37, E38) { \v1{ri} v2{rp} -> v1{ri}*v2{rp} } E33 <-- Pair(E34, E35) { \v1{li} v2{lp} -> v1{li}*v2{lp} } E3 <-- Pair(E4, E5) { \v1{} v2{} -> v1{}*v2{} } E149 <-- S(E150) { \v1{n1} -> v1{n1} } E147 <-- S(E148) { \v1{m1} -> v1{m1} } E131 <-- S(E132) { \v1{m} -> v1{m} } E125 <-- S(E126) { \v1{n} -> v1{n} } E133 <-- Z { {} } E124 <-- Z { {} } E150 <-- __ { {n1:__} } E148 <-- __ { {m1:__} } E145 <-- __ { {n:__} } E144 <-- __ { {m:__} } E132 <-- __ { {m:__} } E126 <-- __ { {n:__} } E102 <-- __ { {p:__} } E101 <-- __ { {y:__} } E99 <-- __ { {i:__} } E98 <-- __ { {x1:__} } E95 <-- __ { {v2:__} } E104 <-- __ { {y:__} } E103 <-- __ { {x1:__} } E93 <-- __ { {rp:__} } E92 <-- __ { {ri:__} } E90 <-- __ { {lp:__} } E89 <-- __ { {li:__} } E87 <-- __ { {v1:__} } E111 <-- __ { {y:__} } E110 <-- __ { {rp:__} } E109 <-- __ { {ri:__} } E108 <-- __ { {lp:__} } E107 <-- __ { {li:__} } E78 <-- __ { {x:__} } E77 <-- __ { {v:__} } E59 <-- __ { {rp:__} } E58 <-- __ { {ri:__} } E57 <-- __ { {v:__} } E54 <-- __ { {v:__} } E43 <-- __ { {p:__} } E42 <-- __ { {v:__} } E40 <-- __ { {i:__} } E38 <-- __ { {rp:__} } E37 <-- __ { {ri:__} } E35 <-- __ { {lp:__} } E34 <-- __ { {li:__} } E32 <-- __ { {v:__} } E15 <-- __ { {r:__} } E13 <-- __ { {l:__} } E11 <-- __ { {v:__} } FletAt138 <-- E146 { \v{m1,n1} -> {_1:Pair(v{m1,n1}.m1,v{m1,n1}.n1)} } E143 <-- Fneq { \x{_1,_2} -> let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n} } E138 <-- FletAt138 { \x{_1} -> let {v1{m,n} = @E143(x{_1}._1)} in v1{m,n} } Fneq <-- E138 { \v{m,n} -> {_1:S(v{m,n}.m), _2:S(v{m,n}.n)} } Fneq <-- E130 { \v{m} -> {_1:S(v{m}.m), _2:Z} } Fneq <-- E123 { \v{n} -> {_1:Z, _2:S(v{n}.n)} } FletAt79 <-- E94 { \v{i,p,v2,x1,y} -> {_1:Pair(v{i,p,v2,x1,y}.v2,Pair(v{i,p,v2,x1,y}.i,v{i,p,v2,x1,y}.p)), _2:v{i,p,v2,x1,y}.x1, _3:v{i,p,v2,x1,y}.y} } E86 <-- Fdapp_body { \x{_1,_2,_3} -> let {v1{v1} = x{_1,_2,_3}._1; v2{li,lp} = @E88(x{_1,_2,_3}._2); v3{ri,rp} = @E91(x{_1,_2,_3}._3)} in v1{v1}*v2{li,lp}*v3{ri,rp} } E79 <-- FletAt79 { \x{_1,_2,_3} -> let {v1{li,lp,ri,rp,v1} = @E86(x{_1,_2,_3}._1); v2{x1} = x{_1,_2,_3}._2; v3{y} = x{_1,_2,_3}._3} in v1{li,lp,ri,rp,v1}*v2{x1}*v3{y} } FletAt71 <-- E79 { \v{li,lp,ri,rp,v1,x1,y} -> {_1:Pair(v{li,lp,ri,rp,v1,x1,y}.v1,v{li,lp,ri,rp,v1,x1,y}.x1), _2:v{li,lp,ri,rp,v1,x1,y}.li, _3:v{li,lp,ri,rp,v1,x1,y}.lp, _4:v{li,lp,ri,rp,v1,x1,y}.ri, _5:v{li,lp,ri,rp,v1,x1,y}.rp, _6:v{li,lp,ri,rp,v1,x1,y}.y} } E76 <-- Fneq { \x{_1,_2} -> let {v1{v} = x{_1,_2}._1; v2{x} = x{_1,_2}._2} in v1{v}*v2{x} } E71 <-- FletAt71 { \x{_1,_2,_3,_4,_5,_6} -> let {v1{v,x} = @E76(x{_1,_2,_3,_4,_5,_6}._1); v2{li} = x{_1,_2,_3,_4,_5,_6}._2; v3{lp} = x{_1,_2,_3,_4,_5,_6}._3; v4{ri} = x{_1,_2,_3,_4,_5,_6}._4; v5{rp} = x{_1,_2,_3,_4,_5,_6}._5; v6{y} = x{_1,_2,_3,_4,_5,_6}._6} in v1{v,x}*v2{li}*v3{lp}*v4{ri}*v5{rp}*v6{y} } Fdapp_body <-- E71 { \v{li,lp,ri,rp,v,x,y} -> {_1:v{li,lp,ri,rp,v,x,y}.v, _2:Pair(Cons(v{li,lp,ri,rp,v,x,y}.x,v{li,lp,ri,rp,v,x,y}.li),Cons(v{li,lp,ri,rp,v,x,y}.y,v{li,lp,ri,rp,v,x,y}.lp)), _3:Pair(v{li,lp,ri,rp,v,x,y}.ri,v{li,lp,ri,rp,v,x,y}.rp)} } Fdapp_body <-- E53 { \v{ri,rp,v} -> {_1:v{ri,rp,v}.v, _2:Pair(Nil,Nil), _3:Pair(v{ri,rp,v}.ri,v{ri,rp,v}.rp)} } FletAt24 <-- E39 { \v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))} } E31 <-- Fdapp_body { \x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{li,lp} = @E33(x{_1,_2,_3}._2); v3{ri,rp} = @E36(x{_1,_2,_3}._3)} in v1{v}*v2{li,lp}*v3{ri,rp} } E24 <-- FletAt24 { \x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v} } Fdappend <-- E24 { \v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)} } E14 <-- Finpre { \x{_1} -> let {v1{r} = x{_1}._1} in v1{r} } E12 <-- Finpre { \x{_1} -> let {v1{l} = x{_1}._1} in v1{l} } E10 <-- Fdappend { \x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r} } Finpre <-- E10 { \v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)} } Finpre <-- E3 { \v{} -> {_1:BLeaf} } --- Guided Tree Automata ------------------------ {Finpre: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> Nil() 2 --> __() 3 --> __() 4 --> Nil() 4 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(13, 7) { \(x1_1,x1_2) x2_1-> ((\v1{} v2{} -> v1{}*v2{} >2> \v{} -> {_1:BLeaf}) $ x1_1 x2_1) } 1 <-- Pair(13, 8) { \(x1_1,x1_2) x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)})) $ x1_2 x2_1) } 1 <-- Pair(14, 8) { \x1_1 x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)})) $ x1_1 x2_1) } 6 <-- __ { _|_ } 1: 8 <-- Cons(12, 11) { \x1_1 x2_1-> ((\v1{v} v2{p} -> v1{v}*v2{p}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 6 <-- __ { _|_ } 2: 11 <-- __ { ({p:__}) } 3: 12 <-- __ { ({v:__}) } 4: 13 <-- Nil { ({}, {i:__}) } 14 <-- __ { ({i:__}) } E11: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E12: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> Nil() 2 --> __() 3 --> __() 4 --> Nil() 4 --> __() GUIDED TRANSITIONS: 0: 3 <-- Pair(13, 7) { \(x1_1,x1_2) x2_1-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:BLeaf}) >>> (\x{_1} -> let {v1{l} = x{_1}._1} in v1{l})) $ x1_1 x2_1) } 3 <-- Pair(13, 8) { \(x1_1,x1_2) x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)}) >>> (\x{_1} -> let {v1{l} = x{_1}._1} in v1{l})) $ x1_2 x2_1) } 3 <-- Pair(14, 8) { \x1_1 x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)}) >>> (\x{_1} -> let {v1{l} = x{_1}._1} in v1{l})) $ x1_1 x2_1) } 6 <-- __ { _|_ } 1: 8 <-- Cons(12, 11) { \x1_1 x2_1-> ((\v1{v} v2{p} -> v1{v}*v2{p}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 6 <-- __ { _|_ } 2: 11 <-- __ { ({p:__}) } 3: 12 <-- __ { ({v:__}) } 4: 13 <-- Nil { ({}, {i:__}) } 14 <-- __ { ({i:__}) } E13: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({l:__}) } E14: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(4,1) 1 --> Cons(3,2) 1 --> Nil() 2 --> __() 3 --> __() 4 --> Nil() 4 --> __() GUIDED TRANSITIONS: 0: 3 <-- Pair(13, 7) { \(x1_1,x1_2) x2_1-> ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:BLeaf}) >>> (\x{_1} -> let {v1{r} = x{_1}._1} in v1{r})) $ x1_1 x2_1) } 3 <-- Pair(13, 8) { \(x1_1,x1_2) x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)}) >>> (\x{_1} -> let {v1{r} = x{_1}._1} in v1{r})) $ x1_2 x2_1) } 3 <-- Pair(14, 8) { \x1_1 x2_1-> ((\v1{i} v2{p,v} -> v1{i}*v2{p,v} >2> (\v{i,p,v} -> {_1:Pair(v{i,p,v}.v,Pair(v{i,p,v}.i,v{i,p,v}.p))}) >>> (\x{_1} -> let {v1{li,lp,ri,rp,v} = @E31(x{_1}._1)} in v1{li,lp,ri,rp,v}) >>> ((\v{li,lp,ri,rp,v} -> {_1:v{li,lp,ri,rp,v}.v, _2:Pair(v{li,lp,ri,rp,v}.li,v{li,lp,ri,rp,v}.lp), _3:Pair(v{li,lp,ri,rp,v}.ri,v{li,lp,ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{l} = @E12(x{_1,_2,_3}._2); v3{r} = @E14(x{_1,_2,_3}._3)} in v1{v}*v2{l}*v3{r})) >>> (\v{l,r,v} -> {_1:BNode(v{l,r,v}.v,v{l,r,v}.l,v{l,r,v}.r)}) >>> (\x{_1} -> let {v1{r} = x{_1}._1} in v1{r})) $ x1_1 x2_1) } 6 <-- __ { _|_ } 1: 8 <-- Cons(12, 11) { \x1_1 x2_1-> ((\v1{v} v2{p} -> v1{v}*v2{p}) $ x1_1 x2_1) } 7 <-- Nil { ({}) } 6 <-- __ { _|_ } 2: 11 <-- __ { ({p:__}) } 3: 12 <-- __ { ({v:__}) } 4: 13 <-- Nil { ({}, {i:__}) } 14 <-- __ { ({i:__}) } E15: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({r:__}) } E31: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(8,1) 1 --> Pair(5,2) 2 --> Cons(4,3) 2 --> __() 3 --> __() 4 --> __() 5 --> Cons(7,6) 6 --> __() 7 --> __() 8 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(23, 6) { \(x1_1,x1_2) x2_1-> ((\v1{v} v2{ri,rp,v} -> v1{v}*v2{ri,rp,v} >2> (\v{ri,rp,v} -> {_1:v{ri,rp,v}.v, _2:Pair(Nil,Nil), _3:Pair(v{ri,rp,v}.ri,v{ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{li,lp} = @E33(x{_1,_2,_3}._2); v3{ri,rp} = @E36(x{_1,_2,_3}._3)} in v1{v}*v2{li,lp}*v3{ri,rp})) $ x1_1 x2_1) } 1 <-- Pair(23, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ( ((\v1{v} v2{ri,rp,v} -> v1{v}*v2{ri,rp,v} >2> (\v{ri,rp,v} -> {_1:v{ri,rp,v}.v, _2:Pair(Nil,Nil), _3:Pair(v{ri,rp,v}.ri,v{ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{li,lp} = @E33(x{_1,_2,_3}._2); v3{ri,rp} = @E36(x{_1,_2,_3}._3)} in v1{v}*v2{li,lp}*v3{ri,rp})) $ x1_1 x2_1) | ((\v1{v2} v2{i,p,x1,y} -> v1{v2}*v2{i,p,x1,y} >2> (\v{i,p,v2,x1,y} -> {_1:Pair(v{i,p,v2,x1,y}.v2,Pair(v{i,p,v2,x1,y}.i,v{i,p,v2,x1,y}.p)), _2:v{i,p,v2,x1,y}.x1, _3:v{i,p,v2,x1,y}.y}) >>> (\x{_1,_2,_3} -> let {v1{li,lp,ri,rp,v1} = @E86(x{_1,_2,_3}._1); v2{x1} = x{_1,_2,_3}._2; v3{y} = x{_1,_2,_3}._3} in v1{li,lp,ri,rp,v1}*v2{x1}*v3{y}) >>> ((\v{li,lp,ri,rp,v1,x1,y} -> {_1:Pair(v{li,lp,ri,rp,v1,x1,y}.v1,v{li,lp,ri,rp,v1,x1,y}.x1), _2:v{li,lp,ri,rp,v1,x1,y}.li, _3:v{li,lp,ri,rp,v1,x1,y}.lp, _4:v{li,lp,ri,rp,v1,x1,y}.ri, _5:v{li,lp,ri,rp,v1,x1,y}.rp, _6:v{li,lp,ri,rp,v1,x1,y}.y}) >>> (\x{_1,_2,_3,_4,_5,_6} -> let {v1{v,x} = @E76(x{_1,_2,_3,_4,_5,_6}._1); v2{li} = x{_1,_2,_3,_4,_5,_6}._2; v3{lp} = x{_1,_2,_3,_4,_5,_6}._3; v4{ri} = x{_1,_2,_3,_4,_5,_6}._4; v5{rp} = x{_1,_2,_3,_4,_5,_6}._5; v6{y} = x{_1,_2,_3,_4,_5,_6}._6} in v1{v,x}*v2{li}*v3{lp}*v4{ri}*v5{rp}*v6{y})) >>> (\v{li,lp,ri,rp,v,x,y} -> {_1:v{li,lp,ri,rp,v,x,y}.v, _2:Pair(Cons(v{li,lp,ri,rp,v,x,y}.x,v{li,lp,ri,rp,v,x,y}.li),Cons(v{li,lp,ri,rp,v,x,y}.y,v{li,lp,ri,rp,v,x,y}.lp)), _3:Pair(v{li,lp,ri,rp,v,x,y}.ri,v{li,lp,ri,rp,v,x,y}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v} = x{_1,_2,_3}._1; v2{li,lp} = @E33(x{_1,_2,_3}._2); v3{ri,rp} = @E36(x{_1,_2,_3}._3)} in v1{v}*v2{li,lp}*v3{ri,rp})) $ x1_2 x2_2)) } 17 <-- __ { _|_ } 1: 6 <-- Pair(18, 11) { \(x1_1,x1_2) x2_1-> ((\v1{ri,v} v2{rp} -> v1{ri,v}*v2{rp}) $ x1_1 x2_1) } 7 <-- Pair(18, 12) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{ri,v} v2{rp} -> v1{ri,v}*v2{rp}) $ x1_1 x2_1, (\v1{i,x1} v2{p,y} -> v1{i,x1}*v2{p,y}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 2: 12 <-- Cons(16, 15) { \x1_1 x2_1-> ({rp:__}, (\v1{y} v2{p} -> v1{y}*v2{p}) $ x1_1 x2_1) } 11 <-- __ { ({rp:__}) } 3: 15 <-- __ { ({p:__}) } 4: 16 <-- __ { ({y:__}) } 5: 18 <-- Cons(22, 21) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{v} v2{ri} -> v1{v}*v2{ri}) $ x1_1 x2_1, (\v1{x1} v2{i} -> v1{x1}*v2{i}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 6: 21 <-- __ { ({ri:__}, {i:__}) } 7: 22 <-- __ { ({v:__}, {x1:__}) } 8: 23 <-- __ { ({v:__}, {v2:__}) } E32: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E33: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(5, 4) { \x1_1 x2_1-> ((\v1{li} v2{lp} -> v1{li}*v2{lp}) $ x1_1 x2_1) } 0 <-- __ { _|_ } 1: 4 <-- __ { ({lp:__}) } 2: 5 <-- __ { ({li:__}) } E36: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(5, 4) { \x1_1 x2_1-> ((\v1{ri} v2{rp} -> v1{ri}*v2{rp}) $ x1_1 x2_1) } 0 <-- __ { _|_ } 1: 4 <-- __ { ({rp:__}) } 2: 5 <-- __ { ({ri:__}) } E76: 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 (x2_1,x2_2)-> ((\v1{} v2{n} -> v1{}*v2{n} >2> (\v{n} -> {_1:Z, _2:S(v{n}.n)}) >>> (\x{_1,_2} -> let {v1{v} = x{_1,_2}._1; v2{x} = x{_1,_2}._2} in v1{v}*v2{x})) $ x1_1 x2_1) } 1 <-- Pair(13, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{m1} v2{n1} -> v1{m1}*v2{n1} >2> (\v{m1,n1} -> {_1:Pair(v{m1,n1}.m1,v{m1,n1}.n1)}) >>> (\x{_1} -> let {v1{m,n} = @E143(x{_1}._1)} in v1{m,n}) >>> (\v{m,n} -> {_1:S(v{m,n}.m), _2:S(v{m,n}.n)}) >>> (\x{_1,_2} -> let {v1{v} = x{_1,_2}._1; v2{x} = x{_1,_2}._2} in v1{v}*v2{x})) $ x1_2 x2_2) } 1 <-- Pair(13, 9) { \(x1_1,x1_2) x2_1-> ((\v1{m} v2{} -> v1{m}*v2{} >2> (\v{m} -> {_1:S(v{m}.m), _2:Z}) >>> (\x{_1,_2} -> let {v1{v} = x{_1,_2}._1; v2{x} = x{_1,_2}._2} in v1{v}*v2{x})) $ x1_1 x2_1) } 11 <-- __ { _|_ } 1: 7 <-- S(10) { \(x1_1,x1_2)-> ((\v1{n} -> v1{n}) $ x1_1, (\v1{n1} -> v1{n1}) $ x1_2) } 9 <-- Z { ({}) } 11 <-- __ { _|_ } 2: 10 <-- __ { ({n:__}, {n1:__}) } 3: 13 <-- S(15) { \(x1_1,x1_2)-> ((\v1{m} -> v1{m}) $ x1_1, (\v1{m1} -> v1{m1}) $ x1_2) } 12 <-- Z { ({}) } 11 <-- __ { _|_ } 4: 15 <-- __ { ({m:__}, {m1:__}) } E77: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v:__}) } E78: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E86: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(8,1) 1 --> Pair(5,2) 2 --> Cons(4,3) 2 --> __() 3 --> __() 4 --> __() 5 --> Cons(7,6) 6 --> __() 7 --> __() 8 --> __() GUIDED TRANSITIONS: 0: 4 <-- Pair(23, 6) { \(x1_1,x1_2) x2_1-> ((\v1{v} v2{ri,rp,v} -> v1{v}*v2{ri,rp,v} >2> (\v{ri,rp,v} -> {_1:v{ri,rp,v}.v, _2:Pair(Nil,Nil), _3:Pair(v{ri,rp,v}.ri,v{ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v1} = x{_1,_2,_3}._1; v2{li,lp} = @E88(x{_1,_2,_3}._2); v3{ri,rp} = @E91(x{_1,_2,_3}._3)} in v1{v1}*v2{li,lp}*v3{ri,rp})) $ x1_1 x2_1) } 4 <-- Pair(23, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ( ((\v1{v} v2{ri,rp,v} -> v1{v}*v2{ri,rp,v} >2> (\v{ri,rp,v} -> {_1:v{ri,rp,v}.v, _2:Pair(Nil,Nil), _3:Pair(v{ri,rp,v}.ri,v{ri,rp,v}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v1} = x{_1,_2,_3}._1; v2{li,lp} = @E88(x{_1,_2,_3}._2); v3{ri,rp} = @E91(x{_1,_2,_3}._3)} in v1{v1}*v2{li,lp}*v3{ri,rp})) $ x1_1 x2_1) | ((\v1{v2} v2{i,p,x1,y} -> v1{v2}*v2{i,p,x1,y} >2> (\v{i,p,v2,x1,y} -> {_1:Pair(v{i,p,v2,x1,y}.v2,Pair(v{i,p,v2,x1,y}.i,v{i,p,v2,x1,y}.p)), _2:v{i,p,v2,x1,y}.x1, _3:v{i,p,v2,x1,y}.y}) >>> (\x{_1,_2,_3} -> let {v1{li,lp,ri,rp,v1} = @E86(x{_1,_2,_3}._1); v2{x1} = x{_1,_2,_3}._2; v3{y} = x{_1,_2,_3}._3} in v1{li,lp,ri,rp,v1}*v2{x1}*v3{y}) >>> ((\v{li,lp,ri,rp,v1,x1,y} -> {_1:Pair(v{li,lp,ri,rp,v1,x1,y}.v1,v{li,lp,ri,rp,v1,x1,y}.x1), _2:v{li,lp,ri,rp,v1,x1,y}.li, _3:v{li,lp,ri,rp,v1,x1,y}.lp, _4:v{li,lp,ri,rp,v1,x1,y}.ri, _5:v{li,lp,ri,rp,v1,x1,y}.rp, _6:v{li,lp,ri,rp,v1,x1,y}.y}) >>> (\x{_1,_2,_3,_4,_5,_6} -> let {v1{v,x} = @E76(x{_1,_2,_3,_4,_5,_6}._1); v2{li} = x{_1,_2,_3,_4,_5,_6}._2; v3{lp} = x{_1,_2,_3,_4,_5,_6}._3; v4{ri} = x{_1,_2,_3,_4,_5,_6}._4; v5{rp} = x{_1,_2,_3,_4,_5,_6}._5; v6{y} = x{_1,_2,_3,_4,_5,_6}._6} in v1{v,x}*v2{li}*v3{lp}*v4{ri}*v5{rp}*v6{y})) >>> (\v{li,lp,ri,rp,v,x,y} -> {_1:v{li,lp,ri,rp,v,x,y}.v, _2:Pair(Cons(v{li,lp,ri,rp,v,x,y}.x,v{li,lp,ri,rp,v,x,y}.li),Cons(v{li,lp,ri,rp,v,x,y}.y,v{li,lp,ri,rp,v,x,y}.lp)), _3:Pair(v{li,lp,ri,rp,v,x,y}.ri,v{li,lp,ri,rp,v,x,y}.rp)}) >>> (\x{_1,_2,_3} -> let {v1{v1} = x{_1,_2,_3}._1; v2{li,lp} = @E88(x{_1,_2,_3}._2); v3{ri,rp} = @E91(x{_1,_2,_3}._3)} in v1{v1}*v2{li,lp}*v3{ri,rp})) $ x1_2 x2_2)) } 17 <-- __ { _|_ } 1: 6 <-- Pair(18, 11) { \(x1_1,x1_2) x2_1-> ((\v1{ri,v} v2{rp} -> v1{ri,v}*v2{rp}) $ x1_1 x2_1) } 7 <-- Pair(18, 12) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{ri,v} v2{rp} -> v1{ri,v}*v2{rp}) $ x1_1 x2_1, (\v1{i,x1} v2{p,y} -> v1{i,x1}*v2{p,y}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 2: 12 <-- Cons(16, 15) { \x1_1 x2_1-> ({rp:__}, (\v1{y} v2{p} -> v1{y}*v2{p}) $ x1_1 x2_1) } 11 <-- __ { ({rp:__}) } 3: 15 <-- __ { ({p:__}) } 4: 16 <-- __ { ({y:__}) } 5: 18 <-- Cons(22, 21) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{v} v2{ri} -> v1{v}*v2{ri}) $ x1_1 x2_1, (\v1{x1} v2{i} -> v1{x1}*v2{i}) $ x1_2 x2_2) } 17 <-- __ { _|_ } 6: 21 <-- __ { ({ri:__}, {i:__}) } 7: 22 <-- __ { ({v:__}, {x1:__}) } 8: 23 <-- __ { ({v:__}, {v2:__}) } E87: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({v1:__}) } E88: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(5, 4) { \x1_1 x2_1-> ((\v1{li} v2{lp} -> v1{li}*v2{lp}) $ x1_1 x2_1) } 0 <-- __ { _|_ } 1: 4 <-- __ { ({lp:__}) } 2: 5 <-- __ { ({li:__}) } E91: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> Pair(2,1) 1 --> __() 2 --> __() GUIDED TRANSITIONS: 0: 1 <-- Pair(5, 4) { \x1_1 x2_1-> ((\v1{ri} v2{rp} -> v1{ri}*v2{rp}) $ x1_1 x2_1) } 0 <-- __ { _|_ } 1: 4 <-- __ { ({rp:__}) } 2: 5 <-- __ { ({ri:__}) } E103: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x1:__}) } E104: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E107: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({li:__}) } E108: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({lp:__}) } E109: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({ri:__}) } E110: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({rp:__}) } E111: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({y:__}) } E143: 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 (x2_1,x2_2)-> ((\v1{} v2{n} -> v1{}*v2{n} >2> (\v{n} -> {_1:Z, _2:S(v{n}.n)}) >>> (\x{_1,_2} -> let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n})) $ x1_1 x2_1) } 5 <-- Pair(13, 7) { \(x1_1,x1_2) (x2_1,x2_2)-> ((\v1{m1} v2{n1} -> v1{m1}*v2{n1} >2> (\v{m1,n1} -> {_1:Pair(v{m1,n1}.m1,v{m1,n1}.n1)}) >>> (\x{_1} -> let {v1{m,n} = @E143(x{_1}._1)} in v1{m,n}) >>> (\v{m,n} -> {_1:S(v{m,n}.m), _2:S(v{m,n}.n)}) >>> (\x{_1,_2} -> let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n})) $ x1_2 x2_2) } 5 <-- Pair(13, 9) { \(x1_1,x1_2) x2_1-> ((\v1{m} v2{} -> v1{m}*v2{} >2> (\v{m} -> {_1:S(v{m}.m), _2:Z}) >>> (\x{_1,_2} -> let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n})) $ x1_1 x2_1) } 11 <-- __ { _|_ } 1: 7 <-- S(10) { \(x1_1,x1_2)-> ((\v1{n} -> v1{n}) $ x1_1, (\v1{n1} -> v1{n1}) $ x1_2) } 9 <-- Z { ({}) } 11 <-- __ { _|_ } 2: 10 <-- __ { ({n:__}, {n1:__}) } 3: 13 <-- S(15) { \(x1_1,x1_2)-> ((\v1{m} -> v1{m}) $ x1_1, (\v1{m1} -> v1{m1}) $ x1_2) } 12 <-- Z { ({}) } 11 <-- __ { _|_ } 4: 15 <-- __ { ({m:__}, {m1:__}) } E144: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({m:__}) } E145: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({n:__}) }} --- Ambiguity Info ------------------------------ System failed to prove the injectivity because of following reasons: Possibly range-overlapping expressions: at (19,3) -- (20,1) Pair(v{54},Pair{55}(Cons{56}(v{57},ri{58}),rp{59})) at (21,3) -- (27,1) let Pair(v1,x1) neq(v,x) in Pair(v2,Pair(i,p)) = dapp_body(v1,Pair(li,lp),Pair(ri,rp)) Pair(v2,Pair(Cons(x1,i),Cons(y,p))) -- 0.16 seconds is elapsed.