## 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 *M *Dv}`

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

`int.minN`

  > > `{FS.int.minN *M *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 *M *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`.