--- Abstract Syntax Tree ------------------------
double(Z)
    = Z{3}
double(S(x))
    = S{6}(S{7}(double{8}(x{9})))
--- Tree Automata -------------------------------
E7  <-- S(E8)
    { \v1{x} -> v1{x} }
E6  <-- S(E7)
    { \v1{x} -> v1{x} }
E3  <-- Z
    { {} }
E9  <-- __
    { {x:__} }
E8  <-- Fdouble
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Fdouble
    <-- E6
    { \v{x} -> {_1:S(v{x}.x)} }
Fdouble
    <-- E3
    { \v{} -> {_1:Z} }
--- Guided Tree Automata ------------------------
{Fdouble:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> Z()
             1 --> S(2)
             2 --> S(1)
             2 --> Z()
         GUIDED TRANSITIONS:
             0:
                 1   <-- S(7)
                     { \x1_1->
                       (((\v1{x} -> v1{x}) >>> (\v{x} -> {_1:S(v{x}.x)})) $ x1_1) }
                 1   <-- Z
                     { ((\v{} -> {_1:Z}) $ ({})) }
                 6   <-- __
                     { _|_ }
             1:
                 7   <-- S(8)
                     { \x1_1-> ((\v1{x} -> v1{x}) $ x1_1) }
                 6   <-- __
                     { _|_ }
             2:
                 8   <-- S(7)
                     { \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) }
                 8   <-- Z
                     { (((\v{} -> {_1:Z})
                         >>> (\x{_1} -> let {v1{x} = x{_1}._1} in v1{x})) $ ({})) }
                 6   <-- __
                     { _|_ }
 E9:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }}

-- 0.01 seconds is elapsed.