This paper explores the question: How can we exploit the information
that a state predicate p holds at some point in a computation in reasoning
about the remainder of the computation? This question is relevant because
partial global snapshots of distributed systems can determine that
a predicate holds at a point in the computation, even though the partial
snapshot does not determine the complete global state. This question is
also relevant in extending the substitution axiom of UNITY.