7.2 Sets over Integers

int.min

{FS.int.min *M $D}

D is the minimal element within M.

int.max

{FS.int.max *M $D}

D is the maximal element within M.

int.convex

{FS.int.convex *M}

Whenever I1 and I2 are elements of M, then every I between I1 and I2, I1 < I < I2, is also in M.

int.match

{FS.int.match **Dv}

Dv is a vector of integer variables that denotes the elements of M in ascending order.

int.minN

{FS.int.minN **Dv}

Dv is a vector of n integer variables that denotes the n minimal elements of M in ascending order.

int.maxN

{FS.int.maxN **Dv}

Dv is a vector of n integer variables that denotes the n maximal elements of M in ascending order.

int.seq

{FS.int.seq *Mv}

Mv is a vector of disjoint sets such that for distinct sets M1 and M2, where M1 precedes M2 in Mv, all elements of M1 are smaller than any element of M2.


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