define the core objects of our model.

\[def:colouredsignature\] A *coloured signature* is a 4-tuple $\mathbb{S} = (\mathcal{V}, \mathcal{F}, \mathcal{C}, \mathtt{ar})$ where $ (\mathcal{V}, \mathcal{F}, \mathtt{ar})$ is a signature and $\mathcal{C} \subseteq \mathcal{F}$ is a specified set of *colours*. The set of terms $\mathcal{T}_\mathbb{S}$ is defined as the set of terms over the signature $(\mathcal{V}, \mathcal{F}, \mathtt{ar})$.

We will now work with the coloured signature $\mathbb{S} = (\mathcal{V}, \mathcal{F}, \mathcal{C}, \mathtt{ar})$ unless specified otherwise.

\[def:ray\] A ray is a term in the grammar $r ::= +c(t_1, ..., t_n) \mid -c(t_1, ..., t_n) \mid t$, where $\{t_1, ..., t_n\} \subseteq \mathcal{T}_\mathbb{S}$ and $c \in \mathcal{C}$ with $\mathtt{ar}(c) = n$. The underlying term of a ray is defined by $\floor{+c(t_1, ..., t_n)} = \floor{-c(t_1, ..., t_n)} = c(t_1, ..., t_n)$ and $\floor{t}=t$.

\[not:ray\] We will sometimes write $+c.t$ (resp. $-c.t$) instead of $+c(t)$ (resp. $-c(t)$) for unary colours when it is convenient.

\[def:star\] A star $\sigma$ over a coloured signature $\mathbb{S}$ is a finite and non-empty multiset of rays, i.e. a finite set $\abs{\sigma}$ together with a map $\rho_\sigma:\abs{\sigma}\rightarrow\rays{\mathbb{S}}$. The set of variables appearing in $\sigma$ is written $\mathtt{vars}(\sigma)$. Stars are written as multisets $\sigma=\gstar{r_1, ..., r_n}$.

\[def:alphaeq\] Given a substitution $\theta$, its 