feat: prove the existence of an omega-regular language not accepted by any deterministic Buchi automaton

[ctchou]

This patch exhibits an omega-regular language (that is, it is accepted by a finite-state nondeterministic Buchi automaton) that is not accepted by any deterministic Buchi automaton which is not even required to be finite-state.

Some code reorg in OmegaSequence is also done.

This PR now includes #150 (which is closed) as well, whose main results are:

• The ω-language accepted by a deterministic Buchi automaton is the ω-limit of the language accepted by the same automaton.
• The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular.
• The ω-limit of a regular language is ω-regular.

[ctchou]

Since Chris reviewed #150 as part of this PR, I'll close #150.