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.loop_run_one_iter
Plain-language 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
Plain-language 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
Plain-language statement
Correctness of toNAFinAcc.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.εNA.FinAcc.toSingleAccept_language_eq
Plain-language statement
toSingleAccept preserves the language of the input automaton.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_choice_assoc
Plain-language statement
P + (Q + R) ~ (P + Q) + R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_congr_choice
Plain-language statement
P ~ Q → P + R ~ Q + R
Source project: Lean Computer Science Library
Person-level attribution pending.