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 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 583 to 588 of 2,569 results.
Cslib.Automata.NA.loop_run_exists
Mathematical statement
For any infinite sequence xls of nonempty finite words from language na, there is an infinite run of na.loop corresponding to xls.flatten in which the state () marks the boundaries between the finite words in xls.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.loop_run_one_iter
Mathematical statement
A run of na.loop containing at least one non-initial () state is the concatenation of a nonempty finite run of na followed by a run of na.loop.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.totalize_run_mtr
Mathematical statement
In an infinite execution of NA.totalize, as long as the NA stays in a non-sink state, the execution so far corresponds to a finite execution of the original NA.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq
Mathematical statement
Correctness of toNAFinAcc.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.εNA.FinAcc.toSingleAccept_language_eq
Mathematical statement
toSingleAccept preserves the language of the input automaton.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_choice_assoc
Mathematical statement
P + (Q + R) ~ (P + Q) + R
Source project: Lean Computer Science Library
Person-level attribution pending.