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.choueka_lang_omega_power_subset_omega_limit
Project documentation
If the language accepted by M is of the form V∗, then V^ω ⊆ V∗ * (M.ChouekaLang acc)↗ω. Note that this theorem does need to assume that M is finite-state.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_acc_lang_compl
Plain-language statement
For a DA, complementing the language it accepts can be achieved by simply complementing the set of accepting states.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_acc_lang_iff_run_acc
Plain-language statement
A finite word al is accepted by M if and only if M reaches an accepting state after running on al starting from the initial state.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_acc_omega_lang
Plain-language statement
The ω-language accepted by a deterministic Buchi automaton is the ω-limit of the language accepted by the same automaton.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_det_run_2
Plain-language statement
If any M2 copy in the second state component of M1.Concat acc1 M2 ever stabilizes (in the sense of never being deactivated from some point on), then it contains an infinite run of M2 starting from its activation.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_det_run_cnt2
Plain-language statement
The second state component of M1.Concat acc1 M2 always has at least one inactive copy of M2 available.
Source project: Automata Theory
Person-level attribution pending.