from a graph $D$ of $D_{\delta'}$ to $D_{\delta}$ such that $\delta=\delta'\circ\varphi$.

A maximal $\mathcal{A}$-diagram w.r.t. $\sqsubseteq$ is called *saturated*.

For the constellations from example \[ex:constellation\] and their unfication graph in example \[ex:ugraph\], $\Sigma_\nat$ has no saturated diagram since it is always possible to extend any star $\gstar{-nat.s^n(0), +nat.s^{n+1}(0)}$ by connecting it to $$\gstar{-nat.s^{n+1}(0), +nat.s^{n+2}(0)} \in \Sigma_\nat.$$ Similarly, $\Sigma_a$ can always connect any star with a new copy of itself so no saturated diagram can be constructed. The star $\gstar{x, -b(g(x))} \in \Sigma_{ex}$ can be connected to either $\gstar{g(x), f(x), +a(f(x))}+\gstar{-a(y), +b(y)}$ or just $\gstar{+b(x), x}$ and these two connexions can’t be extended. Therefore, they form saturated diagrams.

Evaluation and Normal form {#subsec:evaluation}
--------------------------

Diagrams can be evaluated by confronting and annihilating the rays connected together similarly to a chemical reaction between molecules which will have an effect on the remaining free rays. This reaction defines a unification problem. When a solution (a substitution) to this problem exists, one can apply it to all the free rays involved in the diagram. Edges in the diagram then represent equalities and the diagram can be *contracted* into a single star. This operation is called *actualisation*.

\[def:correctdiagram\] Consider a constellation $\Sigma$ and a set 