--- Abstract Syntax Tree ------------------------
double(n)
    = add{2}(dup{3}(n{4}))
dup(Z)
    = Pair{8}(Z{9},Z{10})
dup(S(n))
    = dSuc{13}(dup{14}(n{15}))
dSuc(Pair(m,n))
    = Pair{20}(S{21}(m{22}),S{23}(n{24}))
add(Pair(Z,m))
    = m{30}
add(Pair(S(n),m))
    = S{35}(add{36}(Pair{37}(n{38},m{39})))
--- Tree Automata -------------------------------
E37 <-- Pair(E38, E39)
    { \v1{n} v2{m} -> v1{n}*v2{m} }
E20 <-- Pair(E21, E23)
    { \v1{m} v2{n} -> v1{m}*v2{n} }
E8  <-- Pair(E9, E10)
    { \v1{} v2{} -> v1{}*v2{} }
E35 <-- S(E36)
    { \v1{m,n} -> v1{m,n} }
E23 <-- S(E24)
    { \v1{n} -> v1{n} }
E21 <-- S(E22)
    { \v1{m} -> v1{m} }
E10 <-- Z
    { {} }
E9  <-- Z
    { {} }
E39 <-- __
    { {m:__} }
E38 <-- __
    { {n:__} }
E30 <-- __
    { {m:__} }
E24 <-- __
    { {n:__} }
E22 <-- __
    { {m:__} }
E15 <-- __
    { {n:__} }
E4  <-- __
    { {n:__} }
E36 <-- Fadd
    { \x{_1} -> let {v1{m,n} = @E37(x{_1}._1)} in v1{m,n} }
Fadd
    <-- E35
    { \v{m,n} -> {_1:Pair(S(v{m,n}.n),v{m,n}.m)} }
Fadd
    <-- E30
    { \v{m} -> {_1:Pair(Z,v{m}.m)} }
FdSuc
    <-- E20
    { \v{m,n} -> {_1:Pair(v{m,n}.m,v{m,n}.n)} }
E14 <-- Fdup
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
E13 <-- FdSuc
    { \x{_1} -> let {v1{n} = @E14(x{_1}._1)} in v1{n} }
Fdup
    <-- E13
    { \v{n} -> {_1:S(v{n}.n)} }
Fdup
    <-- E8
    { \v{} -> {_1:Z} }
E3  <-- Fdup
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
E2  <-- Fadd
    { \x{_1} -> let {v1{n} = @E3(x{_1}._1)} in v1{n} }
Fdouble
    <-- E2
    { \v{n} -> {_1:v{n}.n} }
--- Guided Tree Automata ------------------------
{Fdouble:
         INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> __()
             1 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- S(2)
                     { \x1_1->
                       (  (((\v{m} -> {_1:Pair(Z,v{m}.m)})
                            >>> (\x{_1} -> let {v1{n} = @E3(x{_1}._1)} in v1{n})
                            >>> (\v{n} -> {_1:v{n}.n})) $ ({m:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> ((\v{m,n} -> {_1:Pair(S(v{m,n}.n),v{m,n}.m)})
                                 >>> (\x{_1} -> let {v1{n} = @E3(x{_1}._1)} in v1{n}))
                            >>> (\v{n} -> {_1:v{n}.n}))
                           $
                           x1_1)) }
                 0   <-- __
                     { (((\v{m} -> {_1:Pair(Z,v{m}.m)})
                         >>> (\x{_1} -> let {v1{n} = @E3(x{_1}._1)} in v1{n})
                         >>> (\v{n} -> {_1:v{n}.n})) $ ({m:__})) }
             1:
                 2   <-- S(2)
                     { \x1_1->
                       (  (((\v{m} -> {_1:Pair(Z,v{m}.m)})
                            >>> (\x{_1} -> 
                                 let {v1{m,n} = @E37(x{_1}._1)} in v1{m,n})) $ ({m:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> (\v{m,n} -> {_1:Pair(S(v{m,n}.n),v{m,n}.m)})
                            >>> (\x{_1} -> let {v1{m,n} = @E37(x{_1}._1)} in v1{m,n}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{m} -> {_1:Pair(Z,v{m}.m)})
                         >>> (\x{_1} -> 
                              let {v1{m,n} = @E37(x{_1}._1)} in v1{m,n})) $ ({m:__})) }
 E3:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(3,1)
             1 --> S(2)
             1 --> Z()
             2 --> __()
             3 --> S(4)
             3 --> Z()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(12, 7)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 1   <-- Pair(13, 8)
                     { \x1_1 x2_1->
                       ((\v1{m} v2{n} -> v1{m}*v2{n} >2> (\v{m,n} -> 
                                                          {_1:Pair(v{m,n}.m,v{m,n}.n)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{n} = @E14(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 x2_1) }
                 11  <-- __
                     { _|_ }
             1:
                 8   <-- S(10)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 7   <-- Z
                     { ({}) }
                 11  <-- __
                     { _|_ }
             2:
                 10  <-- __
                     { ({n:__}) }
             3:
                 13  <-- S(15)
                     { \x1_1-> ((\v1{m} -> v1{m}) $ x1_1) }
                 12  <-- Z
                     { ({}) }
                 11  <-- __
                     { _|_ }
             4:
                 15  <-- __
                     { ({m:__}) }
 E4:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E14:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(3,1)
             1 --> S(2)
             1 --> Z()
             2 --> __()
             3 --> S(4)
             3 --> Z()
             4 --> __()
         GUIDED TRANSITIONS:
             0:
                 3   <-- Pair(12, 7)
                     { \x1_1 x2_1->
                       ((\v1{} v2{} -> v1{}*v2{} >2> (\v{} -> {_1:Z})
                                                     >>> (\x{_1} -> 
                                                          let {v1{n} = x{_1}._1} in v1{n}))
                        $
                        x1_1 x2_1) }
                 3   <-- Pair(13, 8)
                     { \x1_1 x2_1->
                       ((\v1{m} v2{n} -> v1{m}*v2{n} >2> (\v{m,n} -> 
                                                          {_1:Pair(v{m,n}.m,v{m,n}.n)})
                                                         >>> (\x{_1} -> 
                                                              let {v1{n} = @E14(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 x2_1) }
                 11  <-- __
                     { _|_ }
             1:
                 8   <-- S(10)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 7   <-- Z
                     { ({}) }
                 11  <-- __
                     { _|_ }
             2:
                 10  <-- __
                     { ({n:__}) }
             3:
                 13  <-- S(15)
                     { \x1_1-> ((\v1{m} -> v1{m}) $ x1_1) }
                 12  <-- Z
                     { ({}) }
                 11  <-- __
                     { _|_ }
             4:
                 15  <-- __
                     { ({m:__}) }
 E15:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E37:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> Pair(2,1)
             1 --> __()
             2 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- Pair(5, 4)
                     { \x1_1 x2_1-> ((\v1{n} v2{m} -> v1{n}*v2{m}) $ x1_1 x2_1) }
                 0   <-- __
                     { _|_ }
             1:
                 4   <-- __
                     { ({m:__}) }
             2:
                 5   <-- __
                     { ({n:__}) }}
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons: 
Possibly range-overlapping expressions: 
    at (10,18) -- (11,1)
        m
    at (11,21) -- (12,1)
        S(add{36}(Pair{37}(n{38},m{39})))
-- 0.03 seconds is elapsed.