34.9.7 Execution of Checking Indexicals

Consider the definition of a constraint C containing a checking indexical X in R. Let \FV(X,C,S) denote the set of values for X that can make C false in some ground extension of the store S. Then the indexical should obey the following coding rules:

If the coding rules are observed, S(R) can be proven to exclude \FV(X,C,S) for all stores in which R is anti-monotone. Hence it is natural for the implementation to wait until R becomes anti-monotone before admitting the checking indexical for execution. The execution of X in R thus involves the following:

A checking indexical is scheduled for execution as follows: