feat: prove basic properties of deterministic Buchi automata

[ctchou]

This patch proves some basic properties of deterministic Buchi automata. The 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.

Some code reorg is also done.

[ctchou]

Merge in the current upstream/main.

[ctchou]

Merge in the current upstream/main.