I'm reviewing some notes about tree automata and I'm trying to conclude a proof that the professor left incomplete. The statement is:
Let $A = \{a,b\}$ and $T = \{t \in T_A^{\omega} \mid \text{every path in $t$ contains a finite number of $a$}\}$. Prove that $T$ isn't Buchi recognizable.
Now we can define the following subsets of trees $t_n \subseteq T$ where $t \in t_n$ has one $a$ at positions: $\epsilon, 1^{m_1}0, 1^{m_1}01^{m_2}0, \ldots, 1^{m_1}01^{m_2}0\ldots1^{m_n}0$ with $m_i > 0$.
Now assume that $\mathcal{A} = (Q, A, \Delta, q_0, F)$ is the Buchi automaton that recognizes $T$ with $|Q| = n+1$ and $q_0$ appears only at the root of its computations. Let $t \in t_n$ and $r$ be a successful run of $\mathcal{A}$ on $t$.
Claim: $\color{red}{\text{There exists $u \leq v < w$ such that $r(u) = r(w) = s \in F$ and $t(v) = a$.}}$
Obviously if we show that the claim is true we can prove the initial statement: take the subtree $t_v$ and obtain a $t' \in t_{n+1}$ by replacing the subtree $t_w$ with $t_v$. We have that there exist a run $r'$ which is identical to $r$ up to the position for $w$ and will follow the same sequence of states at $w$ as it did at $v$, and hence is accepting. Repeat the process and you obtain a branch with infinite $a$s that is accepted by $\mathcal{A}$. (This is just the rough idea, it requires a bit of formalism, but it's not the point of the question.)
My question is: how do I prove the claim?
I can show that there exist a $t' \in t_{2n}$ with that property (which is actually good enough for the rest of the proof), but not that given a fixed $t_n$ the statement holds for any successful run.
My idea is simply: given that $r$ is accepting there must exist a $s \in F$ repeated infinite times in a path passing through $1^{m_1}01^{m_2}0\ldots1^{m_n}0$. Then take a tree $t'' \in t_{n+1}$ that is identical to $t_n$ up to the position $x$ where $r(x) = s$ on that path, and add an $a$ below such position. Now this tree is still accepted by the automaton and there exist an accepting run $r'$ identical to $r$ up to the position $x$, but then $r'$ cannot reuse $s$ for accepting that same path (otherwise we have found the three states of the claim) and so it must use a different state $s'$. Repeat for all final states and you have that $t_{2n}$ must have a run with that property.
Is there any way to apply this kind of reasoning to $t_{n-1}$, $t_{n-2}$ etc to obtain the result for $t_n$? It looks like at most I may be able to prove that there exist a $t'' \in t_n$ with a run with that property, while the claim is stronger. Or am I going in the wrong direction?