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 601 to 606 of 2,569 results.
Cslib.FLP.AdmissibleRun.fault_zero
Mathematical statement
Specialize the definition of Algorithm.AdmissibleRun to the case of zero fault.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.omega_notRcvd_enabled
Mathematical statement
A message that is in-flight stays in-flight as long as it is not received (infinite execution version).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.recvMsg_comm
Mathematical statement
If m1 and m2 are both inflight and they have different destinations, then receiving them in either order produces the same end state.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.tr_diamond
Mathematical statement
A diamond property for the transition relation a.lts.Tr.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.CanReachVia.diamond
Project documentation
A diamond property for CanReachVia. This theorem formalizes Proposition 1 of [Volzer2004].
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.CanReachVia.subset_inp
Mathematical statement
If inputs inp1 and inp2 agree on all processes in ps and state s is reachable from the initial state determined by inp1 by receiving messages with destinations in ps only, then there exists a state s2 that agrees with s on the states of all processes and is reachable from the initial state determined by inp2 by receiving messages with de...
Source project: Lean Computer Science Library
Person-level attribution pending.