--- Abstract Syntax Tree ------------------------ bin2peano(Cons(B0,Nil)) = Z{7} bin2peano(Cons(B1,Nil)) = S{11}(Z{12}) bin2peano(Cons(B0,Cons(a,x))) = doubleP{18}(bin2peano1{19}(Cons{20}(a{21},x{22}))) bin2peano(Cons(B1,Cons(a,x))) = S{28}(doubleP{29}(bin2peano1{30}(Cons{31}(a{32},x{33})))) bin2peano1(Cons(B0,x)) = doubleP{39}(bin2peano1{40}(x{41})) bin2peano1(Cons(B1,x)) = S{45}(double{46}(bin2peano2{47}(x{48}))) bin2peano2(Nil) = Z{53} bin2peano2(Cons(B0,x)) = doubleP{57}(bin2peano1{58}(x{59})) bin2peano2(Cons(B1,x)) = S{63}(double{64}(bin2peano2{65}(x{66}))) double(Z) = Z{70} double(S(x)) = S{73}(S{74}(double{75}(x{76}))) doubleP(S(Z)) = S{81}(S{82}(Z{83})) doubleP(S(S(x))) = S{87}(S{88}(S{89}(S{90}(double{91}(x{92}))))) --- Tree Automata ------------------------------- E31 <-- Cons(E32, E33) { \v1{a} v2{x} -> v1{a}*v2{x} } E20 <-- Cons(E21, E22) { \v1{a} v2{x} -> v1{a}*v2{x} } E90 <-- S(E91) { \v1{x} -> v1{x} } E89 <-- S(E90) { \v1{x} -> v1{x} } E88 <-- S(E89) { \v1{x} -> v1{x} } E87 <-- S(E88) { \v1{x} -> v1{x} } E82 <-- S(E83) { \v1{} -> v1{} } E81 <-- S(E82) { \v1{} -> v1{} } E74 <-- S(E75) { \v1{x} -> v1{x} } E73 <-- S(E74) { \v1{x} -> v1{x} } E63 <-- S(E64) { \v1{x} -> v1{x} } E45 <-- S(E46) { \v1{x} -> v1{x} } E28 <-- S(E29) { \v1{a,x} -> v1{a,x} } E11 <-- S(E12) { \v1{} -> v1{} } E83 <-- Z { {} } E70 <-- Z { {} } E53 <-- Z { {} } E12 <-- Z { {} } E7 <-- Z { {} } E92 <-- __ { {x:__} } E76 <-- __ { {x:__} } E66 <-- __ { {x:__} } E59 <-- __ { {x:__} } E48 <-- __ { {x:__} } E41 <-- __ { {x:__} } E33 <-- __ { {x:__} } E32 <-- __ { {a:__} } E22 <-- __ { {x:__} } E21 <-- __ { {a:__} } E91 <-- Fdouble { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } FdoubleP <-- E87 { \v{x} -> {_1:S(S(v{x}.x))} } FdoubleP <-- E81 { \v{} -> {_1:S(Z)} } E75 <-- Fdouble { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } Fdouble <-- E73 { \v{x} -> {_1:S(v{x}.x)} } Fdouble <-- E70 { \v{} -> {_1:Z} } E65 <-- Fbin2peano2 { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } E64 <-- Fdouble { \x{_1} -> let {v1{x} = @E65(x{_1}._1)} in v1{x} } Fbin2peano2 <-- E63 { \v{x} -> {_1:Cons(B1,v{x}.x)} } E58 <-- Fbin2peano1 { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } E57 <-- FdoubleP { \x{_1} -> let {v1{x} = @E58(x{_1}._1)} in v1{x} } Fbin2peano2 <-- E57 { \v{x} -> {_1:Cons(B0,v{x}.x)} } Fbin2peano2 <-- E53 { \v{} -> {_1:Nil} } E47 <-- Fbin2peano2 { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } E46 <-- Fdouble { \x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x} } Fbin2peano1 <-- E45 { \v{x} -> {_1:Cons(B1,v{x}.x)} } E40 <-- Fbin2peano1 { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} } E39 <-- FdoubleP { \x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x} } Fbin2peano1 <-- E39 { \v{x} -> {_1:Cons(B0,v{x}.x)} } E30 <-- Fbin2peano1 { \x{_1} -> let {v1{a,x} = @E31(x{_1}._1)} in v1{a,x} } E29 <-- FdoubleP { \x{_1} -> let {v1{a,x} = @E30(x{_1}._1)} in v1{a,x} } Fbin2peano <-- E28 { \v{a,x} -> {_1:Cons(B1,Cons(v{a,x}.a,v{a,x}.x))} } E19 <-- Fbin2peano1 { \x{_1} -> let {v1{a,x} = @E20(x{_1}._1)} in v1{a,x} } E18 <-- FdoubleP { \x{_1} -> let {v1{a,x} = @E19(x{_1}._1)} in v1{a,x} } Fbin2peano <-- E18 { \v{a,x} -> {_1:Cons(B0,Cons(v{a,x}.a,v{a,x}.x))} } Fbin2peano <-- E11 { \v{} -> {_1:Cons(B1,Nil)} } Fbin2peano <-- E7 { \v{} -> {_1:Cons(B0,Nil)} } --- Guided Tree Automata ------------------------ {Fbin2peano: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 0 --> Z() 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(6) 5 --> Z() 6 --> S(6) 6 --> Z() GUIDED TRANSITIONS: 0: 1 <-- S(16) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{a,x} = @E19(x{_1}._1)} in v1{a,x})) >>> (\v{a,x} -> {_1:Cons(B0,Cons(v{a,x}.a,v{a,x}.x))})) $ x1_1) } 1 <-- S(8) { \x1_1-> (((\v1{a,x} -> v1{a,x}) >>> (\v{a,x} -> {_1:Cons(B1,Cons(v{a,x}.a,v{a,x}.x))})) $ x1_1) } 1 <-- S(14) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{a,x} = @E19(x{_1}._1)} in v1{a,x})) >>> (\v{a,x} -> {_1:Cons(B0,Cons(v{a,x}.a,v{a,x}.x))})) $ x1_1) } 1 <-- S(7) { \x1_1-> (((\v1{} -> v1{}) >>> (\v{} -> {_1:Cons(B1,Nil)})) $ x1_1) } 1 <-- Z { ((\v{} -> {_1:Cons(B0,Nil)}) $ ({})) } 32 <-- __ { _|_ } 1: 8 <-- S(16) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{a,x} = @E30(x{_1}._1)} in v1{a,x})) $ x1_1) } 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 8 <-- S(14) { \x1_1-> (((\v1{} -> v1{}) >>> (\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{a,x} = @E30(x{_1}._1)} in v1{a,x})) $ x1_1) } 14 <-- S(20) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 7 <-- Z { ({}) } 32 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 14 <-- S(20) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 20 <-- Z { ({}) } 32 <-- __ { _|_ } 3: 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- S(31) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 20 <-- Z { ({}) } 32 <-- __ { _|_ } 4: 31 <-- S(33) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 26 <-- S(31) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 31 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 32 <-- __ { _|_ } 5: 31 <-- S(33) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 33 <-- S(34) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 31 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 32 <-- __ { _|_ } 6: 34 <-- S(33) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 33 <-- S(34) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 34 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 32 <-- __ { _|_ } E19: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 1 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E20(x{_1}._1)} in v1{a,x})) $ x1_1) } 1 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E20(x{_1}._1)} in v1{a,x})) $ x1_1) } 1 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E20(x{_1}._1)} in v1{a,x})) $ x1_1) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E20: 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:__}) } E30: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 1 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E31(x{_1}._1)} in v1{a,x})) $ x1_1) } 1 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E31(x{_1}._1)} in v1{a,x})) $ x1_1) } 1 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{a,x} = @E31(x{_1}._1)} in v1{a,x})) $ x1_1) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E31: 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:__}) } E40: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 1 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 1 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 1 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E41: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E47: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 0 --> Z() 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 1 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E58(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 1 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E58(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 1 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 1 <-- Z { (((\v{} -> {_1:Nil}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E65(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E65(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E48: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E58: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 2 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 2 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E40(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 2 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E47(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E59: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E65: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> S(1) 0 --> Z() 1 --> S(2) 1 --> Z() 2 --> S(3) 2 --> Z() 3 --> S(4) 3 --> Z() 4 --> S(5) 4 --> Z() 5 --> S(5) 5 --> Z() GUIDED TRANSITIONS: 0: 2 <-- S(10) { \x1_1-> (((\v1{x} -> v1{x}) >>> ((\v{x} -> {_1:S(S(v{x}.x))}) >>> (\x{_1} -> let {v1{x} = @E58(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 2 <-- S(8) { \x1_1-> (((\v1{} -> v1{}) >>> ((\v{} -> {_1:S(Z)}) >>> (\x{_1} -> let {v1{x} = @E58(x{_1}._1)} in v1{x})) >>> (\v{x} -> {_1:Cons(B0,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 2 <-- S(6) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:Cons(B1,v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 2 <-- Z { (((\v{} -> {_1:Nil}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 1: 10 <-- S(16) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 6 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = @E65(x{_1}._1)} in v1{x})) $ x1_1) } 8 <-- S(15) { \x1_1-> ((\v1{} -> v1{}) $ x1_1) } 6 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = @E65(x{_1}._1)} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 2: 16 <-- S(21) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 15 <-- Z { ({}) } 27 <-- __ { _|_ } 3: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 21 <-- S(26) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 4: 26 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 26 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } 5: 29 <-- S(28) { \x1_1-> (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ x1_1) } 28 <-- S(29) { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) } 29 <-- Z { (((\v{} -> {_1:Z}) >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) } 27 <-- __ { _|_ } E66: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E76: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) } E92: INITIAL GUIDE: 0 GUIDE FUNCTION: 0 --> __() GUIDED TRANSITIONS: 0: 0 <-- __ { ({x:__}) }} -- 0.13 seconds is elapsed.