--- Abstract Syntax Tree ------------------------
peano2bin(x)
    = testHalve{2}(halve{3}(x{4}))
testHalve(Pair(b,Z))
    = Cons{10}(b{11},Nil{12})
testHalve(Pair(b,S(x)))
    = Cons{17}(b{18},peano2bin{19}(S{20}(x{21})))
halve(Z)
    = Pair{26}(B0{27},Z{28})
halve(S(Z))
    = Pair{31}(B1{32},Z{33})
halve(S(S(x)))
    = letAt37{37}(halve{42}(x{43}))
letAt37(Pair(b,s))
    = Pair{44}(b{45},S{46}(s{47}))
--- Tree Automata -------------------------------
E27 <-- B0
    { {} }
E32 <-- B1
    { {} }
E17 <-- Cons(E18, E19)
    { \v1{b} v2{x} -> v1{b}*v2{x} }
E10 <-- Cons(E11, E12)
    { \v1{b} v2{} -> v1{b}*v2{} }
E12 <-- Nil
    { {} }
E44 <-- Pair(E45, E46)
    { \v1{b} v2{s} -> v1{b}*v2{s} }
E31 <-- Pair(E32, E33)
    { \v1{} v2{} -> v1{}*v2{} }
E26 <-- Pair(E27, E28)
    { \v1{} v2{} -> v1{}*v2{} }
E46 <-- S(E47)
    { \v1{s} -> v1{s} }
E20 <-- S(E21)
    { \v1{x} -> v1{x} }
E33 <-- Z
    { {} }
E28 <-- Z
    { {} }
E47 <-- __
    { {s:__} }
E45 <-- __
    { {b:__} }
E43 <-- __
    { {x:__} }
E21 <-- __
    { {x:__} }
E18 <-- __
    { {b:__} }
E11 <-- __
    { {b:__} }
E4  <-- __
    { {x:__} }
FletAt37
    <-- E44
    { \v{b,s} -> {_1:Pair(v{b,s}.b,v{b,s}.s)} }
E42 <-- Fhalve
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E37 <-- FletAt37
    { \x{_1} -> let {v1{x} = @E42(x{_1}._1)} in v1{x} }
Fhalve
    <-- E37
    { \v{x} -> {_1:S(S(v{x}.x))} }
Fhalve
    <-- E31
    { \v{} -> {_1:S(Z)} }
Fhalve
    <-- E26
    { \v{} -> {_1:Z} }
E19 <-- Fpeano2bin
    { \x{_1} -> let {v1{x} = @E20(x{_1}._1)} in v1{x} }
FtestHalve
    <-- E17
    { \v{b,x} -> {_1:Pair(v{b,x}.b,S(v{b,x}.x))} }
FtestHalve
    <-- E10
    { \v{b} -> {_1:Pair(v{b}.b,Z)} }
E3  <-- Fhalve
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
E2  <-- FtestHalve
    { \x{_1} -> let {v1{x} = @E3(x{_1}._1)} in v1{x} }
Fpeano2bin
    <-- E2
    { \v{x} -> {_1:v{x}.x} }
--- Guided Tree Automata ------------------------
{Fpeano2bin:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> Cons(2,1)
             1 --> Nil()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{x} -> v1{b}*v2{x} >2> (\v{b,x} -> 
                                                          {_1:Pair(v{b,x}.b,S(v{b,x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E3(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:v{x}.x}))
                        $
                        x1_2 x2_1) }
                 1   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Pair(v{b}.b,Z)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{x} = @E3(x{_1}._1)} in v1{x})
                                                       >>> (\v{x} -> {_1:v{x}.x}))
                        $
                        x1_1 x2_1) }
                 5   <-- __
                     { _|_ }
             1:
                 8   <-- Cons(9, 8)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{x} -> v1{b}*v2{x} >2> (\v{b,x} -> 
                                                          {_1:Pair(v{b,x}.b,S(v{b,x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E3(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:v{x}.x})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E20(x{_1}._1)}
                                                              in v1{x}))
                        $
                        x1_2 x2_1) }
                 8   <-- Cons(9, 7)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{} -> v1{b}*v2{} >2> (\v{b} -> {_1:Pair(v{b}.b,Z)})
                                                       >>> (\x{_1} -> 
                                                            let {v1{x} = @E3(x{_1}._1)} in v1{x})
                                                       >>> (\v{x} -> {_1:v{x}.x})
                                                       >>> (\x{_1} -> 
                                                            let {v1{x} = @E20(x{_1}._1)} in v1{x}))
                        $
                        x1_1 x2_1) }
                 7   <-- Nil
                     { ({}) }
                 5   <-- __
                     { _|_ }
             2:
                 9   <-- __
                     { ({b:__}, {b:__}) }
 E3:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(3,1)
             1 --> S(2)
             1 --> Z()
             2 --> __()
             3 --> B0()
             3 --> B1()
             3 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(12, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(12, 9)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_2 x2_1) }
                 1   <-- Pair(13, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:S(Z)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_2) }
                 1   <-- Pair(13, 9)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_2 x2_1) }
                 1   <-- Pair(14, 9)
                     { \x1_1 x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 7   <-- __
                     { _|_ }
             1:
                 9   <-- S(11)
                     { \x1_1-> ((\v1{s} -> v1{s}) $ x1_1) }
                 8   <-- Z
                     { ({}, {}) }
                 7   <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({s:__}) }
             3:
                 12  <-- B0
                     { ({}, {b:__}) }
                 13  <-- B1
                     { ({}, {b:__}) }
                 14  <-- __
                     { ({b:__}) }
 E4:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E20:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- S(3)
                     { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) }
                 0   <-- __
                     { _|_ }
             1:
                 3   <-- __
                     { ({x:__}) }
 E42:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(3,1)
             1 --> S(2)
             1 --> Z()
             2 --> __()
             3 --> B0()
             3 --> B1()
             3 --> __()
         GUIDED TRANSITIONS:
             0:
                 4   <-- Pair(12, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 4   <-- Pair(12, 9)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_2 x2_1) }
                 4   <-- Pair(13, 8)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:S(Z)})
                                                     >>> (\x{_1} -> 
                                                          let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_2) }
                 4   <-- Pair(13, 9)
                     { \(x1_1,x1_2) x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_2 x2_1) }
                 4   <-- Pair(14, 9)
                     { \x1_1 x2_1->
                       ((\v1{b} v2{s} -> v1{b}*v2{s} >2> (\v{b,s} -> 
                                                          {_1:Pair(v{b,s}.b,v{b,s}.s)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = @E42(x{_1}._1)} in v1{x})
                                                         >>> (\v{x} -> {_1:S(S(v{x}.x))})
                                                         >>> (\x{_1} -> 
                                                              let {v1{x} = x{_1}._1} in v1{x}))
                        $
                        x1_1 x2_1) }
                 7   <-- __
                     { _|_ }
             1:
                 9   <-- S(11)
                     { \x1_1-> ((\v1{s} -> v1{s}) $ x1_1) }
                 8   <-- Z
                     { ({}, {}) }
                 7   <-- __
                     { _|_ }
             2:
                 11  <-- __
                     { ({s:__}) }
             3:
                 12  <-- B0
                     { ({}, {b:__}) }
                 13  <-- B1
                     { ({}, {b:__}) }
                 14  <-- __
                     { ({b:__}) }
 E43:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }}

-- 0.06 seconds is elapsed.