7.3 Standard Propagators

diff

{FS.diff $M1 $M2 $M3}

\codeinline{oz}{M3} = \codeinline{oz}{M1} \setminus \codeinline{oz}{M2}

intersect

{FS.intersect $M1 $M2 $M3}

\codeinline{oz}{M3} = \codeinline{oz}{M1} \cap \codeinline{oz}{M2}

intersectN

{FS.intersectN *Mv *M}

\codeinline{oz}{M} = \bigcap \{ \codeinline{oz}{M'} \mid \codeinline{oz}{M'} \in \codeinline{oz}{Mv}\}

union

{FS.union $M1 $M2 $M3}

\codeinline{oz}{M3} = \codeinline{oz}{M1} \cup \codeinline{oz}{M2}

unionN

{FS.unionN $Mv $M}

\codeinline{oz}{M} = \bigcup \{ \codeinline{oz}{S} \mid \codeinline{oz}{S} \in \codeinline{oz}{Mv}\}

subset

{FS.subset $M1 $M2}

\codeinline{oz}{M1} \subseteq \codeinline{oz}{M2}

disjoint

{FS.disjoint $M1 $M2}

\codeinline{oz}{M1} \| \codeinline{oz}{M2}

disjointN

{FS.disjointN *Mv}

All elements of the vector Mv are pairwise disjoint.

distinct

{FS.distinct $M1 $M2}

\codeinline{oz}{M1} \neq \codeinline{oz}{M2}

distinctN

{FS.distinctN *MV}

All elements of the vector Mv are pairwise distinct.

partition

{FS.partition $MV $M}

Mv is a partition of M; that is, Mv contains pairwise disjoint sets such that their union yields M.


Denys Duchier, Leif Kornstaedt, Martin Homik, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.4.0 (20080702)