Proving that a (tree) language is not Buchi recognizable

Question

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?

Answer 1

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.