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.SKI.isChurch_injective
Plain-language statement
Injectivity for Church numerals
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.List.headD_correct
Plain-language statement
General head-with-default correctness.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.parallelReduction_diamond
Plain-language statement
The key result: the Church-Rosser property holds for ⭢ₚ. The proof is a lengthy case analysis on the reductions a ⭢ₚ a₁ and a ⭢ₚ a₂, but is entirely mechanical.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.elimVar_correct
Plain-language statement
Correctness for the elimVar algorithm, which provides the inductive step of the bracket abstraction algorithm. We induct backwards on the list, corresponding to applying the transformation from the inside out. Since we haven't defined reduction for polynomials, we substitute arbitrary terms for the inner variables.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.toSKI_correct
Plain-language statement
Correctness for the toSKI (bracket abstraction) algorithm.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Red.le_parallelReduction
Plain-language statement
The inclusion (· ⭢ ·) ≤ (· ⭢ₚ ·).
Source project: Lean Computer Science Library
Person-level attribution pending.