Integer grids

Uses Integer intervals

Integer grids have sort ℤ⧺ℕ.nz⧺ℤ and are defined using the operator
 ℤ⧺ℕ.nz ⧺ ℤ : ℤ⧺ℕ.nz⧺ℤ
The first argument of this operator is constructed using the auxiliary operator
 ℤ ⧺ ℕ.nz : ℤ⧺ℕ.nz
of sort ℤ⧺ℕ.nz.

An integer interval is a special case of an integer grid with a grid spacing of 1, thus: ℤ⋯ℤ ⊆ ℤ⧺ℕ.nz⧺ℤ.

Special cases for grids:
- ℕ⧺ℕ.nz ⧺ ℕ : ℕ⧺ℕ.nz⧺ℕ
with ℕ ⧺ ℕ.nz : ℕ⧺ℕ.nz, ℕ⋯ℕ ⊆ ℕ⧺ℕ.nz⧺ℕ,
ℕ⧺ℕ.nz⧺ℕ ⊆ ℤ⧺ℕ.nz⧺ℤ, and ℕ⧺ℕ.nz ⊆ ℤ⧺ℕ.nz
- ℕ.nz⧺ℕ.nz ⧺ ℕ.nz : ℕ.nz⧺ℕ.nz⧺ℕ.nz
with ℕ.nz ⧺ ℕ.nz : ℕ.nz⧺ℕ.nz, ℕ.nz⋯ℕ.nz ⊆ ℕ.nz⧺ℕ.nz⧺ℕ.nz,
ℕ.nz⧺ℕ.nz⧺ℕ.nz ⊆ ℕ⧺ℕ.nz⧺ℕ, and ℕ.nz⧺ℕ.nz ⊆ ℕ⧺ℕ.nz