Glossary of Z notation

This page looks best when this and this X are about the same size: X. See these viewing tips.

`a == x`	`Abbreviation definition`
`a ::= b \| ...`	`Free type definition`
`[a]`	`Introduction of a given set (or [a,...])`
`a _`	`Prefix operator`
`_ a`	`Postfix operator`
`_ a _`	`Infix operator`

`true`	`Logical true constant`
`false`	`Logical false constant`
`p`	`Logical negation, not`
`p q`	`Logical conjunction, and`
`p q`	`Logical disjunction, or`
`p q`	`Logical implication`
`p q`	`Logical equivalence`
`X q`	`Universal quantification`
`X q`	`Existential quantification`
`(let a == x; ... p)`	`Local definition`

`x = y`	`Equality`
`x y`	`Inequality`
`x A`	`Set membership`
`x A`	`Non-membership`
	`Empty set`
`A B`	`Set inclusion`
`A B`	`Strict set inclusion`
`{ x, y, ... }`	`Set display`
`{ X x }`	`Set comprehension`
`( X x)`	`Lambda expression`
`(let a == x; ... y)`	`Local definition`
`if p then x else y`	`Conditional expression`
`(x,y, ...)`	`Tuple`
`(x,y)`	`Pair`
`A B ...`	`Cartesian product`
`A`	`Power set`
`A B`	`Set intersection`
`A B`	`Set union`
`A \ B`	`Set difference`
`first x`	`First element of an ordered pair`
`second x`	`Second element of an ordered pair`
`# A`	`Number of elements in a set`

`A B`	`Binary relation ( (A B))`
`a b`	`Maplet ((a,b))`
`dom R`	`Domain of a relation`
`ran R`	`Range of a relation`
`Q R`	`Forward relational composition`
`Q R`	`Backward relational composition (R Q)`
`A R`	`Domain restriction`
`A R`	`Domain anti-restriction`
`A R`	`Range restriction`
`A R`	`Range anti-restriction`
`R A`	`Relational image`
`R ^~`	`Inverse of relation`
`R ⁺`	`Transitive closure`
`Q R`	`Relational overriding`
`a R b`	`Infix relation`

	`Set of integers`
	`Set of natural numbers { 0, 1, 2, ... }`
`₁`	`Set of strictly positive numbers { 1, 2, ... }`
`m+n`	`Addition`
`m-n`	`Subtraction`
`m*n`	`Multiplication`
`m div n`	`Division`
`m mod n`	`Remainder (modulus)`
`m n`	`Less than or equal`
`m < n`	`Less than`
`m n`	`Greater than or equal`
`m > n`	`Greater than`
`m .. n`	`Number range`
`min A`	`Minimum of a set of numbers`
`max A`	`Maximum of a set of numbers`

`seq A`	`Set of finite sequences`
`seq₁ A`	`Set of non-empty finite sequences`
`iseq A`	`Set of finite injective sequences`
	`Empty sequence`
`x, y, ...`	`Sequence display`
`s t`	`Sequence concatenation`
`head s`	`First element of a sequence`
`tail s`	`All but the head element of a sequence`
`last s`	`Last element of a sequence`
`front s`	`All but the last element of a sequence`
`s in t`	`Sequence segment relation`

`S [ X ]`	`Horizontal schema`
`[ T; ... \| ... ]`	`Schema inclusion`
`z.a`	`Component selection (given z:S)`
`S`	`Binding`
`S`	`Schema negation`
`S T`	`Schema conjunction`
`S T`	`Schema disjunction`
`S T`	`Schema composition`
`S >> T`	`Schema piping`

`a?`	`Input to an operation`
`a!`	`Output from an operation`
`a`	`State component before an operation`
`a'`	`State component after an operation`
`S`	`State schema before an operation`
`S'`	`State schema after an operation`
`S`	`Change of state`
`S`	`No change of state`

Z2HTML tool for translating LaTeX documents with Z markup to HTML web pages.