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 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filtersCslib.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.Red.le_parallelReduction
Plain-language statement
The inclusion (· ⭢ ·) ≤ (· ⭢ₚ ·).
Source project: Lean Computer Science Library
Person-level attribution pending.
Relation.LocallyConfluent.Terminating_toConfluent
Project documentation
Newman's lemma: a terminating, locally confluent relation is confluent.
Source project: Lean Computer Science Library
Person-level attribution pending.