Provando que um idioma (árvore) não é reconhecível pelo Buchi

Estou revendo algumas anotações sobre autômatos de árvores e estou tentando concluir uma prova de que o professor deixou incompleto. A afirmação é:

Deixei $A = \{a,b\}$ e $T = \{t \in T_A^{\omega} \mid \text{every path in $t$ contains a finite number of $a$}\}$. Prove que$T$ Buchi não é reconhecível.

Agora podemos definir os seguintes subconjuntos de árvores $t_n \subseteq T$ Onde $t \in t_n$ tem um $a$ nas posições: $\epsilon, 1^{m_1}0, 1^{m_1}01^{m_2}0, \ldots, 1^{m_1}01^{m_2}0\ldots1^{m_n}0$ com $m_i > 0$.

Agora assuma que $\mathcal{A} = (Q, A, \Delta, q_0, F)$ é o autômato Buchi que reconhece $T$ com $|Q| = n+1$ e $q_0$aparece apenas na raiz de seus cálculos. Deixei$t \in t_n$ e $r$ ser uma corrida bem sucedida de $\mathcal{A}$ em $t$.

Afirmação: $\color{red}{\text{There exists $u \leq v < w$ such that $r(u) = r(w) = s \in F$ and $t(v) = a$.}}$

Obviamente, se mostrarmos que a afirmação é verdadeira, podemos provar a afirmação inicial: pegue a subárvore $t_v$ e obter um $t' \in t_{n+1}$ substituindo a subárvore $t_w$ com $t_v$. Temos que existe uma corrida$r'$ que é idêntico ao $r$ até a posição de $w$ e seguirá a mesma sequência de estados em $w$ como fez em $v$e, portanto, está aceitando. Repita o processo e você obterá um ramo com infinito$a$s que é aceito por $\mathcal{A}$. (Essa é apenas a idéia aproximada, requer um pouco de formalismo, mas não é o ponto da questão.)

Minha pergunta é: como faço para provar a reivindicação?

Eu posso mostrar que existe uma $t' \in t_{2n}$ com essa propriedade (que é realmente boa o suficiente para o restante da prova), mas não com um determinado valor $t_n$ a declaração vale para qualquer execução bem-sucedida.

Minha ideia é simplesmente: dado que $r$ está aceitando deve existir um $s \in F$ repetidas vezes infinitas em um caminho que passa $1^{m_1}01^{m_2}0\ldots1^{m_n}0$. Então pegue uma árvore$t'' \in t_{n+1}$que é idêntico a até a posição que nesse caminho e adicione um abaixo dessa posição. Agora, essa árvore ainda é aceita pelo autômato e existe uma execução de aceitação idêntica a até a posição , mas então não pode reutilizar para aceitar o mesmo caminho (caso contrário, encontramos os três estados da reivindicação) e, portanto, deve usar um estado diferente . Repita para todos os estados finais e você tem que deve ter uma execução com essa propriedade.$t_n$$x$$r(x) = s$$a$$r'$$r$$x$$r'$$s$$s'$$t_{2n}$

Existe alguma maneira de aplicar esse tipo de raciocínio a , etc, para obter o resultado para ? Parece que, no máximo, posso provar que existe um com uma execução com essa propriedade, enquanto a reivindicação é mais forte. Ou estou indo na direção errada?$t_{n-1}$$t_{n-2}$$t_n$ $t'' \in t_n$

A idéia é brincar com os 's, como segue.$m_i$

Considere uma árvore , que tem no , e em nenhum outro lugar. Veja o caminho - uma execução de aceitação nele tem infinitos estados de aceitação. Aguardar até que um estado de aceitação foi atingido, e só então colocar em , em que é grande o suficiente.$t_1$$a$$\epsilon$$1^\omega$$a$$1^{m_1}0$$m_1$

Agora observe o caminho , novamente, ele possui um estado de aceitação eventualmente, denote o comprimento até , coloque em e veja em . Até agora você tem quase o que queria - dois estados aceitantes com um entre eles (falando informalmente). Mas você ainda não tem garantia de que ambos os estados aceitantes sejam iguais. Para impor esse último, repetimos o processo por vezes, esgotando assim o número de estados aceitantes e, pelo princípio do pigeonhole, dois estados aceitantes devem ser iguais.$1^{m_1}01^\omega$$m_2$$a$$1^{m_1}01^{m_2}0$$1^{m_1}01^{m_2}01^\omega$$a$$n$