--- Abstract Syntax Tree ------------------------
inc(Nil)
    = Cons{4}(B0{5},Nil{6})
inc(Cons(B0,x))
    = Cons{10}(B1{11},x{12})
inc(Cons(B1,x))
    = Cons{16}(B0{17},inc{18}(x{19}))
--- Tree Automata -------------------------------
E17 <-- B0
    { {} }
E5  <-- B0
    { {} }
E11 <-- B1
    { {} }
E16 <-- Cons(E17, E18)
    { \v1{} v2{x} -> v1{}*v2{x} }
E10 <-- Cons(E11, E12)
    { \v1{} v2{x} -> v1{}*v2{x} }
E4  <-- Cons(E5, E6)
    { \v1{} v2{} -> v1{}*v2{} }
E6  <-- Nil
    { {} }
E19 <-- __
    { {x:__} }
E12 <-- __
    { {x:__} }
E18 <-- Finc
    { \x{_1} -> let {v1{x} = x{_1}._1} in v1{x} }
Finc
    <-- E16
    { \v{x} -> {_1:Cons(B1,v{x}.x)} }
Finc
    <-- E10
    { \v{x} -> {_1:Cons(B0,v{x}.x)} }
Finc
    <-- E4
    { \v{} -> {_1:Nil} }
--- Guided Tree Automata ------------------------
{Finc:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Cons(2,1)
             1 --> Cons(2,1)
             1 --> Nil()
             1 --> __()
             2 --> B0()
             2 --> B1()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Cons(14, 12)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> \v{x} -> {_1:Cons(B1,v{x}.x)})
                        $
                        x1_2 x2_2) }
                 1   <-- Cons(15, 12)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> \v{x} -> {_1:Cons(B0,v{x}.x)})
                        $
                        x1_1 x2_1) }
                 1   <-- Cons(14, 9)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ((\v1{} v2{} -> v1{}*v2{} >2> \v{} -> {_1:Nil}) $ x1_1 x2_1) }
                 1   <-- Cons(15, 9)
                     { \x1_1 (x2_1,x2_2)->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> \v{x} -> {_1:Cons(B0,v{x}.x)})
                        $
                        x1_1 x2_2) }
                 1   <-- Cons(15, 11)
                     { \x1_1 x2_1->
                       ((\v1{} v2{x} -> v1{}*v2{x} >2> \v{x} -> {_1:Cons(B0,v{x}.x)})
                        $
                        x1_1 x2_1) }
                 13  <-- __
                     { _|_ }
             1:
                 11  <-- Cons(13, 12)
                     { \_ _-> ({x:__}) }
                 12  <-- Cons(14, 12)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B1,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_2 x2_2) }
                 12  <-- Cons(15, 12)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 11  <-- Cons(13, 9)
                     { \_ _-> ({x:__}) }
                 12  <-- Cons(14, 9)
                     { \(x1_1,x1_2) (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Nil})
                                                             >>> (\x{_1} -> 
                                                                  let {v1{x} = x{_1}._1} in v1{x}))
                                $
                                x1_1 x2_1) }
                 11  <-- Cons(14, 11)
                     { \_ _-> ({x:__}) }
                 12  <-- Cons(15, 9)
                     { \x1_1 (x2_1,x2_2)->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_2) }
                 12  <-- Cons(15, 11)
                     { \x1_1 x2_1->
                       ({x:__}, (\v1{} v2{x} -> v1{}*v2{x} >2> (\v{x} -> 
                                                                {_1:Cons(B0,v{x}.x)})
                                                               >>> (\x{_1} -> 
                                                                    let {v1{x} = x{_1}._1}
                                                                    in v1{x}))
                                $
                                x1_1 x2_1) }
                 11  <-- Cons(13, 11)
                     { \_ _-> ({x:__}) }
                 9   <-- Nil
                     { ({}, {x:__}) }
                 11  <-- __
                     { ({x:__}) }
             2:
                 14  <-- B0
                     { ({}, {}) }
                 15  <-- B1
                     { ({}) }
                 13  <-- __
                     { _|_ }
 E19:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }}

-- 0.03 seconds is elapsed.