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 136 research declarations. Search 10,000 more complete Mathlib declarations.
136 results
Clear filtersCslib.URM.Steps.toStandardForm_halts
Plain-language statement
Forward halting: if p reaches a halted state, p.toStandardForm reaches a halted state with the same registers.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.URM.straight_line_halts_from_regs
Plain-language statement
Straight-line programs halt from any starting registers, not just State.init. Useful for chaining: after running one program, we can run the next straight-line segment from whatever registers we're in.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.compl
Plain-language statement
The complementation of an ω-regular language is ω-regular.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.eq_fin_iSup_hmul_omegaPow
Plain-language statement
An ω-language is regular iff it 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.ωLanguage.IsRegular.fin_cover_saturates
Plain-language statement
If an ω-language has a finite saturating cover made of ω-regular languages, then it is an ω-regular language.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.inf
Plain-language statement
The intersection of two ω-regular languages is ω-regular.
Source project: Lean Computer Science Library
Person-level attribution pending.