Note that
instead of equipping the automaton model with a parity acceptance condition, we could
equip it with an MSO acceptance condition, i.e. an MSO formula \(\phi \) 
using two binary predicates: \(s_1\)  and \(s_2\) , standing for left and right successor (in the binary tree), and for each \(q\in Q\)  a unary predicate \(\lambda _q\) , holding at nodes labeled with \(q\) .
This would not change the expressive power of the tree automata, since parity tree automata have the same expressive power as MSO over infinite binary trees [1]}, [2]}.
