Research proof index

A diamond property for CanReachVia. This theorem formalizes Proposition 1 of [Volzer2004].

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...

The correctness of d.scheduleMsgs ps s under the assumption a.FairDeliverMsg d ps q.

Given an infinite sequence of non-empty finite executions of algorithm a, if all messages with destinations in ps that are in-flight at the beginning of each finite execution are delivered in that finite execution, then those finite executions can be concatenated into an infinite execution of a in which every process in ps is fair.

Whenever the message carrying the input value for process 0 is enabled in a state, a message carrying that value is eventually sent to every process p by process 0.

Whenever a message carrying a value sent by process 0 is enabled at a process p, p eventually decides on that value.