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?