temp.tex<2>

Theorem A set of words are \(\omega\)-regular iff they are Büchi-recognisable.
Proof
(\(\Rightarrow\)) Let \(L\) be the set of words and \(L\) is \(\omega\)-regular, i.e.$\backslash$, \(L\) is a finite union of \(\omega\)-languages of the form \(\sqcup \cdot V ^\omega\).

Let \(A\) be the Büchi automaton that accepts \(L(V)^\omega\) (Lemma2), \(A=(Q, Q_0, R, F)\)
and let A' be the finite word Automaton for \(L(\sqcup)\)
We construct \(A''=(Q'',Q_0'',R'',F'')\)
\begin{itemize}
\item \(Q'' = Q \sqcup Q'\)
\item \(Q''_0 = Q_0\)
\item \(R'' = R \sqcup R' \sqcup {(q, \delta, q'') \mid (q, \delta, q') \in R, q' \in F, q'' \in Q_0'}\)
\item \(F'' = F'\)
\end{itemize}

Let \(xy^\omega \in \sqcup \cdot V^\omega\), there is a run on \(A\) for \(x, r = q_0 \dots q_{R-1}q_n\) where
\(q_n \in F\), and there is a run on \(A'\) for \(y^\omega, r=q'_0q'_1 \dots\) where \(q \in F'\) occurs infinitely often,
there is a run on \(A''\) for \(xy^\omega, q_0 \dots q_{n-1} q'_0q'_1 \dots\) where \(q\) occurs infinitely often.
\(xy^\omega \in L(A'')\)

(\(\Leftarrow\)) Let \(L\) be the set of words and \(L\) is Büchi-recognisable. We need to show \(L\) is \(\omega\)-regular.

BLANK

\(q_n \in F\), and there is a run on \(A'\) for \(y^\omega, r = q'_0q'_1 \dots\) where \(q \in F'\) occurs infinitely often,
there is a run on \(A''\) for \$xy\^{}\(\omega\),q\textsubscript{0} \dots{} q\textsubscript{n-1} q'\textsubscript{0q};\textsubscript{1} \dots{} where \(q\) occurs infinitely often,
\(xy^\omega \in L(A'')\)
(\(\Leftarrow\)) Let \(L\) bet he set of words and \(L\) is Büchi-recognisable.
We need to show \(L\) is \(\omega\)-regular.

Let \(A\) be the Büchi automaton that accepts \(L\). \(A=(Q,Q_0,R,F)\)
\(S_{q,q'}=\{\omega \in L \mid (Q, \{S\}, R, \{s'\})\) accepts \(u\}\)

\(L(A)=\bigcup\limits_{q_0 \in Q_0, q_F \in F} S_{q_0, q_F} \cdot S_{q_F,q_F}^\omega\)

1 \(L(A) \subseteq \bigcup S \cdot S^\omega\)

\begin{itemize}
\item Let \(\omega\) be the word for which there's an accepting run on \(A\)
\end{itemize}

\(r=q_0q_1 \dots q_R\) where \(q \in F\) occurs infinitely often.

BLANK

Let \(n_1, \dots, n_i\) be the indices of \(q_F\).
\(\omega(n_i) \dots \omega(n_{i+1BLANK}) \in S_{q_F,q_F}\) for \(i \geq 1\).
\(\omega \in \bigcup S \cdot S ^\omega\).

2 \(\bigcup S \cdot S ^\omega \subseteq L(A)\) let \(\omega=\omega_0 \omega_1 \dots \omega_0 \in S_{q_0 q_F}\) and \(\omega_i \in S=_{q_F, q_F}\)

BLANK
\end{document}