--- Abstract Syntax Tree ------------------------
sigma(Z)
    = Z{3}
sigma(S(n))
    = add{6}(S{7}(n{8}),sigma{9}(n{10}))
add(Z,n)
    = n{15}
add(S(m),n)
    = S{19}(add{20}(m{21},n{22}))
--- Tree Automata -------------------------------
E19 <-- S(E20)
    { \v1{m,n} -> v1{m,n} }
E7  <-- S(E8)
    { \v1{n} -> v1{n} }
E3  <-- Z
    { {} }
E22 <-- __
    { {n:__} }
E21 <-- __
    { {m:__} }
E15 <-- __
    { {n:__} }
E10 <-- __
    { {n:__} }
E8  <-- __
    { {n:__} }
E20 <-- Fadd
    { \x{_1,_2} -> 
      let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n} }
Fadd
    <-- E19
    { \v{m,n} -> {_1:S(v{m,n}.m), _2:v{m,n}.n} }
Fadd
    <-- E15
    { \v{n} -> {_1:Z, _2:v{n}.n} }
E9  <-- Fsigma
    { \x{_1} -> let {v1{n} = x{_1}._1} in v1{n} }
E6  <-- Fadd
    { \x{_1,_2} -> 
      let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
      in v1{n}*v2{n} }
Fsigma
    <-- E6
    { \v{n} -> {_1:S(v{n}.n)} }
Fsigma
    <-- E3
    { \v{} -> {_1:Z} }
--- Guided Tree Automata ------------------------
{Fsigma: INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> Z()
             0 --> __()
             1 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- S(2)
                     { \x1_1->
                       (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                 in v1{n}*v2{n})
                            >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({n:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> ((\v{m,n} -> {_1:S(v{m,n}.m), _2:v{m,n}.n})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                      in v1{n}*v2{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)}))
                           $
                           x1_1)) }
                 0   <-- Z
                     { (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                 in v1{n}*v2{n})
                            >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({n:__}))
                        | ((\v{} -> {_1:Z}) $ ({}))) }
                 0   <-- __
                     { (((\v{n} -> {_1:Z, _2:v{n}.n})
                         >>> (\x{_1,_2} -> 
                              let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                              in v1{n}*v2{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})) $ ({n:__})) }
             1:
                 2   <-- S(2)
                     { \x1_1->
                       (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2}
                                 in v1{m}*v2{n})) $ ({n:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> (\v{m,n} -> {_1:S(v{m,n}.m), _2:v{m,n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{n} -> {_1:Z, _2:v{n}.n})
                         >>> (\x{_1,_2} -> 
                              let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2}
                              in v1{m}*v2{n})) $ ({n:__})) }
 E7:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 1   <-- S(3)
                     { \x1_1-> ((\v1{n} -> v1{n}) $ x1_1) }
                 0   <-- __
                     { _|_ }
             1:
                 3   <-- __
                     { ({n:__}) }
 E9:     INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> Z()
             0 --> __()
             1 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- S(2)
                     { \x1_1->
                       (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                 in v1{n}*v2{n})
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({n:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> ((\v{m,n} -> {_1:S(v{m,n}.m), _2:v{m,n}.n})
                                 >>> (\x{_1,_2} -> 
                                      let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                      in v1{n}*v2{n}))
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n}))
                           $
                           x1_1)) }
                 0   <-- Z
                     { (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                                 in v1{n}*v2{n})
                            >>> (\v{n} -> {_1:S(v{n}.n)})
                            >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({n:__}))
                        | (((\v{} -> {_1:Z})
                            >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({}))) }
                 0   <-- __
                     { (((\v{n} -> {_1:Z, _2:v{n}.n})
                         >>> (\x{_1,_2} -> 
                              let {v1{n} = @E7(x{_1,_2}._1); v2{n} = @E9(x{_1,_2}._2)}
                              in v1{n}*v2{n})
                         >>> (\v{n} -> {_1:S(v{n}.n)})
                         >>> (\x{_1} -> let {v1{n} = x{_1}._1} in v1{n})) $ ({n:__})) }
             1:
                 2   <-- S(2)
                     { \x1_1->
                       (  (((\v{n} -> {_1:Z, _2:v{n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2}
                                 in v1{m}*v2{n})) $ ({n:__}))
                        | (((\v1{m,n} -> v1{m,n})
                            >>> (\v{m,n} -> {_1:S(v{m,n}.m), _2:v{m,n}.n})
                            >>> (\x{_1,_2} -> 
                                 let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2} in v1{m}*v2{n}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{n} -> {_1:Z, _2:v{n}.n})
                         >>> (\x{_1,_2} -> 
                              let {v1{m} = x{_1,_2}._1; v2{n} = x{_1,_2}._2}
                              in v1{m}*v2{n})) $ ({n:__})) }
 E10:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }
 E21:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({m:__}) }
 E22:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({n:__}) }}
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons: 
Possibly range-overlapping expressions: 
    at (3,12) -- (4,1)
        Z
    at (4,15) -- (6,1)
        add(S{7}(n{8}),sigma{9}(n{10}))
-- 0.03 seconds is elapsed.