--- Abstract Syntax Tree ------------------------
twopower(Z)
    = S{3}(S{4}(Z{5}))
twopower(S(n))
    = double2{8}(twopower{9}(n{10}))
double2(S(S(n)))
    = S{15}(S{16}(S{17}(S{18}(double{19}(n{20})))))
double(Z)
    = Z{24}
double(S(n))
    = S{27}(S{28}(double{29}(n{30})))
--- Tree Automata -------------------------------
E28 <-- S(E29)
    { \v1{n} -> v1{n} }
E27 <-- S(E28)
    { \v1{n} -> v1{n} }
E18 <-- S(E19)
    { \v1{n} -> v1{n} }
E17 <-- S(E18)
    { \v1{n} -> v1{n} }
E16 <-- S(E17)
    { \v1{n} -> v1{n} }
E15 <-- S(E16)
    { \v1{n} -> v1{n} }
E4  <-- S(E5)
    { \v1{} -> v1{} }
E3  <-- S(E4)
    { \v1{} -> v1{} }
E24 <-- Z
    { {} }
E5  <-- Z
    { {} }
E30 <-- __
    { {n:__} }
E20 <-- __
    { {n:__} }
E10 <-- __
    { {n:__} }
E29 <-- Fdouble
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
Fdouble
    <-- E27
    { \v{n} -> {_1:S(v{n}.n)} }
Fdouble
    <-- E24
    { \v{} -> {_1:Z} }
E19 <-- Fdouble
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
Fdouble2
    <-- E15
    { \v{n} -> {_1:S(S(v{n}.n))} }
E9  <-- Ftwopower
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
E8  <-- Fdouble2
    { \x{_1} -> let {v1{n} = @E9(x{_1}._1)} in v1{n} }
Ftwopower
    <-- E8
    { \v{n} -> {_1:S(v{n}.n)} }
Ftwopower
    <-- E3
    { \v{} -> {_1:Z} }
--- Guided Tree Automata ------------------------
{Ftwopower:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             1 --> S(2)
             2 --> S(3)
             2 --> Z()
             3 --> S(4)
             4 --> S(5)
             4 --> Z()
             5 --> S(6)
             6 --> S(5)
             6 --> Z()
         GUIDED TRANSITIONS:
             0:
                 1   <-- S(7)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> ((\v{n} -> {_1:S(S(v{n}.n))})
                              >>> (\x{_1} -> let {v1{n} = @E9(x{_1}._1)} in v1{n}))
                         >>> (\v{n} -> {_1:S(v{n}.n)}))
                        $
                        x1_1) }
                 1   <-- S(5)
                     { \x1_1-> (((\v1{} -> v1{}) >>> (\v{} -> {_1:Z})) $ x1_1) }
                 22  <-- __
                     { _|_ }
             1:
                 7   <-- S(11)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 5   <-- S(10)
                     { \x1_1-> ((\v1{} -> v1{}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             2:
                 11  <-- S(14)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 10  <-- Z
                     { ({}) }
                 22  <-- __
                     { _|_ }
             3:
                 14  <-- S(17)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             4:
                 17  <-- S(23)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 17  <-- Z
                     { (((\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({})) }
                 22  <-- __
                     { _|_ }
             5:
                 23  <-- S(24)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             6:
                 24  <-- S(23)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 24  <-- Z
                     { (((\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({})) }
                 22  <-- __
                     { _|_ }
 E9:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             1 --> S(2)
             2 --> S(3)
             2 --> Z()
             3 --> S(4)
             4 --> S(5)
             4 --> Z()
             5 --> S(6)
             6 --> S(5)
             6 --> Z()
         GUIDED TRANSITIONS:
             0:
                 2   <-- S(7)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> ((\v{n} -> {_1:S(S(v{n}.n))})
                              >>> (\x{_1} -> let {v1{n} = @E9(x{_1}._1)} in v1{n}))
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 2   <-- S(5)
                     { \x1_1->
                       (((\v1{} -> v1{})
                         >>> (\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 22  <-- __
                     { _|_ }
             1:
                 7   <-- S(11)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 5   <-- S(10)
                     { \x1_1-> ((\v1{} -> v1{}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             2:
                 11  <-- S(14)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 10  <-- Z
                     { ({}) }
                 22  <-- __
                     { _|_ }
             3:
                 14  <-- S(17)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             4:
                 17  <-- S(23)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 17  <-- Z
                     { (((\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({})) }
                 22  <-- __
                     { _|_ }
             5:
                 23  <-- S(24)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 22  <-- __
                     { _|_ }
             6:
                 24  <-- S(23)
                     { \x1_1->
                       (((\v1{n} -> v1{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1) }
                 24  <-- Z
                     { (((\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({})) }
                 22  <-- __
                     { _|_ }
 E10:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E20:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E30:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }}

-- 0.03 seconds is elapsed.