User Manual for Rodin v.2.3: About the notation that we use

3.2.1 About the notation that we use

We denote a sequence of identifiers with $\mathbf{x} = x_1,\ldots ,x_ n$ and $\mathbf{x}’ = x’_1,\ldots ,x’_ n$ . As a convention, we use

$\mathbf{c}$ for constants
$\mathbf{v}$ and $\mathbf{w}$ for variables of an abstract resp. concrete machine
$\mathbf{t}$ and $\mathbf{u}$ for parameters of an abstract resp. concrete machine
$A$ for axioms
$I$ and $J$ for the invariants of the abstract machines resp. concrete machine
$G$ and $H$ for the guards of the abstract events resp. concrete event