Proving that a (tree) language is not Buchi recognizable

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?

The idea is to play with the $m_i$'s, as follows.
Consider a tree $t_1$, which has $a$ in $\epsilon$, and nowhere else. Look at the path $1^\omega$ — an accepting run on it has infinitely many accepting states. Wait until such an accepting state was reached, and only then put $a$ at $1^{m_1}0$, where $m_1$ is large enough.
Now look at the path $1^{m_1}01^\omega$, again, it has an accepting state eventually, denote the length up to it by $m_2$, put an $a$ at $1^{m_1}01^{m_2}0$ and look at $1^{m_1}01^{m_2}01^\omega$. By now you have almost what you wanted - two accepting states with an $a$ between them (informally speaking). But you are not yet guaranteed that both accepting states are equal. To enforce the latter, we repeat the process for $n$ times, thus exhausting the number of accepting states, and by the pigeonhole principle, two accepting states must be equal.
• You don't even need to consider the number of states - just note that this approach gives you (for any given automaton $A$) an infinite sequence $m_1,m_2,\ldots$ such that for each $k$, $A$ reaches an accepting state $k$ times on $1^{m_1}01^{m_2}0\ldots 1^{m_k}0$, and therefore the limit $1^{m_1}01^{m_2}0\ldots$ will be accepted despite having infinitely many $0$s. – Klaus Draeger Feb 28 '16 at 10:47
• Right, but the OP specifically wanted to bound the number of $m_i$'s by $n+1$, for which you do need the number of states. – Shaull Feb 28 '16 at 11:00
• This is more or less what I was thinking about, however it proves something a little weaker than the claim. With this you prove that $\exists t \in t_n$ and $\exists r$ succesful run of $\mathcal{A}$ on $t$ such that <claim>. While in the proof as stated by the professor you have $\forall t \in t_n$ and $\forall r$ succesful run of $\mathcal{A}$ over $t$ ti holds <claim>. The problem is that if you have $t$ fixed you cannot really play with those $m_i$s as you wish. Now I wonder whether the claim as stated by the professor is actually true or whether this is the best we can achieve. – Bakuriu Feb 28 '16 at 14:19
• For every successful run the claim is clearly false, since the automaton can have a component which guesses a point from which $a$ is never encountered again. Clearly every $t\in t_n$ will have at least one such accepting run... – Shaull Feb 28 '16 at 14:35