Consider the definition of a constraint C containing a
propagating indexical `X in R`

. Let
\TV(X,C,S) denote the set of values for X that can make
C true in some ground extension of the store S.
Then the indexical should obey the following coding rules:

- all arguments of C except X should occur in R
- if R is ground in S, S(R) = \TV(X,C,S)

If the coding rules are observed, S(R) can be proven to contain
\TV(X,C,S) for all stores in which R is monotone. Hence
it is natural for the implementation to wait until R becomes
monotone before admitting the propagating indexical for execution. The
execution of `X in R`

thus involves the following:

- If D(X,S) is disjoint from S(R), a contradiction is detected.
- If D(X,S) is contained in S(R), D(X,S) does not contain any values known to be incompatible with C, and the indexical suspends, unless R is ground in S, in which case C is detected as entailed.
- Otherwise, D(X,S) contains some values that are known to be
incompatible with C. Hence,
`X::S(R)`

is added to the store (X is pruned), and the indexical suspends, unless R is ground in S, in which case C is detected as entailed.

A propagating indexical is scheduled for execution as follows:

- it is evaluated initially as soon as it has become monotone
- it is re-evaluated when one of the following conditions occurs:
- the domain of a variable Y that occurs as
`dom(Y)`

or`card(Y)`

in R has been updated - the lower bound of a variable Y that occurs as
`min(Y)`

in R has been updated - the upper bound of a variable Y that occurs as
`max(Y)`

in R has been updated

- the domain of a variable Y that occurs as