2. A conjunctive predicate = iNi, where i is a predicate defined on variables local to...

2. A conjunctive predicate φ = ∧i∈Nφi, where φi is a predicate defined on variables local to process Pi.

In a distributed execution (E,≺), let First_Cut(φ) be denote the earliest or smallest consistent cut in which the global conjunctive predicate φ becomes true.

Recall that in different equivalent executions, a different “path” may be traced through the state lattice. Therefore, for different re-executions of this (deterministic) distributed program, is the state First_Cut(φ) well-defined? i.e., is it uniquely identified? Worded equivalently, is the set of cuts C(φ) closed under intersection?