Notation

v : τ means value v has type τ.
X = a means that a type or a value X is an alias for a.
X := [something] means that X is defined to be [something]
A percent sign % preceded only by spaces starts a line comment % [comment]
We use · to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math] we may use a [math]\displaystyle{ (x, \cdot) }[/math] to express that we do not care about the value [math]\displaystyle{ y }[/math] takes in each of the tuples.
Let X be a set or a sequence. We use |X| to denote the size/length of the set/sequence.
Let X be a sequence. We use X[i] to access the element in X at index i and X[u…v] to refer to a slice of the sequence starting at index u and ending at index v. For example, for a sequence X := (a, b, c, d), the slice X[2…3] = (b, c).
We define the concatenation of two ordered sequences [math]\displaystyle{ a := (x_1, …, x_m) }[/math] and [math]\displaystyle{ b := (y_1, …, y_n) }[/math] as [math]\displaystyle{ (x_1, …, x_m, y_1, …, y_n) }[/math].
We often work with partial maps [math]\displaystyle{ M: X \mapsto Y }[/math], which we write as [math]\displaystyle{ \{ (x_1 \mapsto y_1), \dots, (x_n \mapsto y_n) \} }[/math], where [math]\displaystyle{ \forall~ i, 1 \leq i \leq n : x_i \in X \land y_i \in Y }[/math] and [math]\displaystyle{ \nexists~ i, j, 1 \leq i, j \leq n: x_i = x_j \land i \neq j }[/math]. We note that partial maps can be nested, i.e., the set [math]\displaystyle{ Y }[/math] could again be a partial map