of colours $\mathcal{A}\subseteq\mathcal{C}$. An $\mathcal{A}$-diagram $\delta$ is correct if $\mathtt{free}(\delta)\neq\emptyset$ and the associated unification problem $\mathcal{P}(\delta)$ has a solution.

The actualisation of a correct diagram $\delta$ is the star $\actu \delta$ defined as $\abs{\actu \delta}=\mathtt{free}(\delta)$ and $\rho_{\actu \delta}: (e,r)\in\mathtt{free}(\delta)\mapsto \psi(\theta(e,r))$, where $\psi = \unifalgo{\mathcal{P}(\delta)}$ and $\theta(e,\_)$ is the renaming used in Definition \[def:underproblem\].

We write $\correctdiag{k}(\Sigma)$ (resp. $\correcttreediag{k}(\Sigma)$) for the set of correct $\mathcal{A}$-diagrams (resp. correct tree-like $\mathcal{A}$-diagrams) over $\Sigma$ with $k$ vertices, and $\saturateddiag{k}(\Sigma)$ (resp. $\saturatedtreediag{k}(\Sigma)$) the set of saturated $\mathcal{A}$-diagrams in $\correctdiag{k}(\Sigma)$ (resp. in $\correcttreediag{k}(\Sigma)$).

Note that the approach proposed by Girard used a step-by-step procedure merging two adjacent stars in a diagram. It is possible to prove that his approach and our lead to the same result, and more precisely that a sequence of merging coincides with a step-by-step execution of the Martelli-Montanari unification algorithm [@martelli1982efficient]. Stating and proving this refined result is however outside of the scope of this paper.

\[def:normalalization\] The normalisation or execution (resp. tree-like normalisation) of a constellation $\Sigma$ w.r.t. a set of colours $\mathcal{A}\subseteq\mathcal{C}$ is defined by $\exec^*_\mathcal{A}(\Sigma) = \bigcup_{k=0}^{\infty} \actu\saturatedstardiag{k}(\Sigma)$ ($*\in\{\emptyset,tree\}$), where $\actu\saturatedstardiag{k}(\delta)$ denotes the set $\{\actu\delta\mid \delta\in\saturatedstardiag{k}(\delta)\}$.

The constellation $\Sigma_{ex}$ is the only constellation from example \[ex:constellation\] which has saturated 