Consider the definition of a constraint `C` containing a checking
indexical

. Let `X` in `R``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:

- 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, then `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

thus involves the following:
`X` in `R`

- If
`D(X,S)`is contained in`S(R)`, then none of the possible values for`X`can make`C`false, and so`C`is detected as entailed. - Otherwise, if
`D(X,S)`is disjoint from`S(R)`and`R`is ground in`S`, then all possible values for`X`will make`C`false, and so`C`is detected as disentailed. - Otherwise,
`D(X,S)`contains some values that could make`C`true and some that could make`C`false, and the indexical suspends.

A checking indexical is scheduled for execution as follows:

- it is evaluated initially as soon as it has become anti-monotone
- it is re-evaluated when one of the following conditions occurs:
- the domain of
`X`has been pruned, or`X`has been assigned - the domain of a variable
`Y`that occurs as`dom(`

or`Y`)`card(`

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

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

in`Y`)`R`has been decreased

- the domain of

Send feedback on this subject.