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.FLP.Algorithm.omega_notRcvd_enabled
Plain-language 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
Plain-language 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
Plain-language 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
Plain-language 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.
Cslib.FLP.FairScheduler.fairDeliverMsg_scheduleMsgs
Plain-language statement
The correctness of d.scheduleMsgs ps s under the assumption a.FairDeliverMsg d ps q.
Source project: Lean Computer Science Library
Person-level attribution pending.