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 $(x, y)$ we may use a $(x, \cdot)$ to express that we do not care about the value $y$ 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 $a := (x_{1}, \dots , x_{m})$ and $b := (y_{1}, \dots , y_{n})$
We often work with partial maps $M : X \mapsto Y$ , which we write as ${(x_{1} \mapsto y_{1}), \dots, (x_{n} \mapsto y_{n})}$ , where $\forall i, 1 \leq i \leq n : x_{i} \in X \land y_{i} \in Y$ and $∄ i, j, 1 \leq i, j \leq n : x_{i} = x_{j} \land i \neq j$ . We note that partial maps can be nested, i.e., the set $Y$ could again be a partial map