Research proof index

A finite run of the loop NA that contains the inl () marker only at the beginning and at the end is an accepting run of M.

Conversely, for any finite accepting run of M, there is a finite run of the loop NA that contains the inl () marker only at the beginning and at the end.

For any input as, running M.Pset on as ends in the unique state that is exact the set of states reachable by running M on as.

The ω-regular language accepted by a finite-state NA M is the union of ω-languages of the form (M.PairLang s0 sa) * (M.PairLang sa sa)^ω, where s0 and sa range over initial and accepting states respectively.

If accepting states appear infinitely often in a run and φ : Stream' ℕ is StrictMono, then there exist infinitely many m such that the segment of the run from φ(m) to φ(m + 1) contains at least one accepting state.

The following result is technical and used to prove the saturation property of the Buchi congruence. Its main purpose is to "fill in" the states between the successive ss' m to produce a well-formed run in which the accepting states appear infinitely often. Note that ss needs to agree with ss' only at positions φ m: ∀ m, ss (φ m) = ss' m.