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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersCslib.Automata.NA.Buchi.concat_language_eq
Plain-language statement
The Buchi automaton formed from concat na1 na2 accepts the ω-language that is the concatenation of the language of na1 and the ω-language of na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_acc_freq_acc
Plain-language statement
If the intersection automaton sees one accepting condition infinitely many times, then it sees the other accepting condition infinitely many times as well.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_comp_acc_freq_acc
Plain-language statement
If the intersection automaton sees the accepting conditions of both component automata infinitely many times, then its own accepting condition also happens infinitely many times.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_language_eq
Plain-language statement
The language accepted by the intersection automaton is the intersection of the languages accepted by the two component automata.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow
Plain-language statement
The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages of the form L * M^ω, where all Ls and Ms are regular languages.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.concat_run_exists
Plain-language statement
Given an accepting finite run of na1 and a run of na2, there exists a run of concat na1 na2 that is the concatenation of the two runs.
Source project: Lean Computer Science Library
Person-level attribution pending.