Deterministic Buchi automata.

theorem Cslib.Automata.DA.buchi_eq_finAcc_omegaLim {State : Type u_1} {Symbol : Type u_2} {da : DA State Symbol} {acc : Set State} : ωAcceptor.language { toDA := da, accept := acc } = (Acceptor.language { toDA := da, accept := acc })↗ω

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