--- Abstract Syntax Tree ------------------------
add(Z,y)
    = y{4}
add(S(x),y)
    = S{8}(add{9}(x{10},y{11}))
--- Tree Automata -------------------------------
E8  <-- S(E9)
    { \v1{x,y} -> v1{x,y} }
E11 <-- __
    { {y:__} }
E10 <-- __
    { {x:__} }
E4  <-- __
    { {y:__} }
E9  <-- Fadd
    { \x{_1,_2} -> 
      let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y} }
Fadd
    <-- E8
    { \v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y} }
Fadd
    <-- E4
    { \v{y} -> {_1:Z, _2:v{y}.y} }
--- Guided Tree Automata ------------------------
{Fadd:   INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> S(1)
             0 --> __()
             1 --> S(1)
             1 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- S(2)
                     { \x1_1->
                       (  ((\v{y} -> {_1:Z, _2:v{y}.y}) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y}))
                           $
                           x1_1)) }
                 0   <-- __
                     { ((\v{y} -> {_1:Z, _2:v{y}.y}) $ ({y:__})) }
             1:
                 2   <-- S(2)
                     { \x1_1->
                       (  (((\v{y} -> {_1:Z, _2:v{y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2}
                                 in v1{x}*v2{y})) $ ({y:__}))
                        | (((\v1{x,y} -> v1{x,y})
                            >>> (\v{x,y} -> {_1:S(v{x,y}.x), _2:v{x,y}.y})
                            >>> (\x{_1,_2} -> 
                                 let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2} in v1{x}*v2{y}))
                           $
                           x1_1)) }
                 2   <-- __
                     { (((\v{y} -> {_1:Z, _2:v{y}.y})
                         >>> (\x{_1,_2} -> 
                              let {v1{x} = x{_1,_2}._1; v2{y} = x{_1,_2}._2}
                              in v1{x}*v2{y})) $ ({y:__})) }
 E10:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({x:__}) }
 E11:    INITIAL GUIDE:
             0
         GUIDE FUNCTION:
             0 --> __()
         GUIDED TRANSITIONS:
             0:
                 0   <-- __
                     { ({y:__}) }}
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons: 
Possibly range-overlapping expressions: 
    at (3,12) -- (4,1)
        y
    at (4,15) -- (5,1)
        S(add{9}(x{10},y{11}))
-- 0.01 seconds is elapsed.