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:

- 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 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:

- If
`D(X,S)`is contained in`S(R)`, 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`, 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(`

`Y``)`

or`card(`

`Y``)`

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

`Y``)`

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

`Y``)`

in`R`has been decreased

- the domain of

Send feedback on this subject.