Lasso Trace Exists

Lemma 1. For any non-empty Buchi automaton $$A = (Q, \delta, q_0, F)$$, there is $$w \in L (A)$$ s.t. $$w = u v^{\omega}$$ where $$u, v \in \Sigma^{\ast}$$.

Proof.

Since A is non-empty, we take an arbitrary infinite word $$w \in L (A)$$. Suppose $$w = a_1 a_2 \cdots$$.

From the acceptance condition of Buchi automaton, we know there must be at least one final state $$q_f \in F$$ that occurs in $$w$$ infinitely often. Assume at position i, after reading prefix $$a_1 \cdots a_i$$, $$q_f$$ is reached for the first time, and at position j it is reached for the second time.

Then consider the infinite word $$w' = a_1 \cdots a_i (a_{i + 1} \cdots a_j)^{\omega}$$. Obviously $$w' \in L (A)$$ and it satisfies the condition.