Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
Automata.na_hist_inf_run_exists
Plain-language statement
Any infinite run of the original NA can be extended to an infinite run of the history NA, assuming that the history component can always "follow along".
Source project: Automata Theory
Person-level attribution pending.
Automata.na_loop_fin_run
Plain-language statement
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.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_loop_fin_run_exists
Plain-language statement
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.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_pset_run
Plain-language statement
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.
Source project: Automata Theory
Person-level attribution pending.
Automata.omega_reg_lang_finite_union_form
Plain-language statement
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.
Source project: Automata Theory
Person-level attribution pending.
Automata.pair_acc_lang_frequently_from_run
Plain-language statement
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.
Source project: Automata Theory
Person-level attribution pending.