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 673 to 678 of 2,569 results.
Cslib.SKI.Red.le_parallelReduction
Mathematical statement
The inclusion (· ⭢ ·) ≤ (· ⭢ₚ ·).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.rice
Project documentation
Rice's theorem: no SKI term is a non-trivial predicate. More specifically, say a term P is a predicate if, for every term x, P · x reduces to either TT or FF. A predicate P is trivial if either it always reduces to true, or always to false. This version of Rice's theorem derives a contradiction from the existence of a predicate P and...
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.sqrt_correct
Mathematical statement
Sqrt correctly computes Nat.sqrt.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.URM.evalState_toStandardForm_regs
Mathematical statement
Registers preservation: both reach states with the same registers.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.URM.haltsWithResult_iff_eval
Mathematical statement
A program halts with result a iff evaluation returns Part.some a.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.URM.isHalted_iff_normal
Mathematical statement
A state is halted iff it is normal (has no successor) in the reduction system.
Source project: Lean Computer Science Library
Person-level attribution pending.