s(s^n(t))$, $nat$ is a colour and $s$ and $0$ are function symbols.

Diagrams and Reduction {#subsec:diagrams}
----------------------

Constellations are gatherings of stars destined to be connected together through their rays of opposite polarities. We define the unification graph of a constellation which is a multigraph specifying which stars can be connected together through the unification of their rays.

\[def:duality\] Two rays $r, r'$ are dual w.r.t. a set of colours $\mathcal{A}\subseteq\mathcal{C}$, written $r \poll_{\mathcal{A}} r'$, if there exists $c\in\mathcal{A}$ such that either $r=+c.t$ and $r'=-c.t'$, or $r=-c.t$ and $r'=+c.t'$, where $t,t'$ are matchable.

\[def:ugraph\] The unification graph $\ugraph{\mathcal{A}}{\Sigma}$ of a constellation $\Sigma$ w.r.t. a set of colours $\mathcal{A}\subseteq\mathcal{C}$ is the undirected multigraph $(V^{\ugraph{\mathcal{A}}{\Sigma}},E^{\ugraph{\mathcal{A}}{\Sigma}},s^{\ugraph{\mathcal{A}}{\Sigma}})$ where $V^{\ugraph{\mathcal{A}}{\Sigma}}=\abs{\Sigma}$, $E^{\ugraph{\mathcal{A}}{\Sigma}}$ is the set of unordered pairs $\{ ((s,r),(s',r')) \in\rays{\Sigma} \mid  r \poll_{\mathcal{A}} r' \}$, and $s^{\ugraph{\mathcal{A}}{\Sigma}}$ is the function defined by $s^{\ugraph{\mathcal{A}}{\Sigma}}((s,r),(s',r'))=\{s,s'\}$.

\[ex:ugraph\] If we take the constellations from example \[ex:constellation\], the unification graph $\ugraph{nat}{\Sigma_\nat}$ is an infinite linear graph and $\ugraph{b, c, d, e}{\Sigma_{ex}}$ is a linear graph

at (0, 0) (a) ; at (0.5, 0) (b) ; at (1, 0) (c) ; at (1.5, 0) (d) ; (a) – (b); (b) – (c); (c) – (d);

of $4$ vertices. The graph $\ugraph{a, 