-b(x)}$ as we want.

The notion of diagram suggested by Girard [@girard2017transcendental] coincides with the notion of *tree-like diagram* in this work. However, as we will explain below, the more general notion of diagram considered here allows for the representation of interesting models of computation, such as Wang tilings [@wang1961proving].

As mentioned above, we consider the underlying graphs of diagrams to have natural numbers as vertices. This is used here to produce a family of substitutions $(\theta(v,\_))_{v\in\nat}$ of pairwise disjoint codomains. This is used in the following definition to rename all occurrences of stars in diagrams with pairwise disjoint sets of free variables.

\[def:underproblem\] The underlying unification problem $\mathcal{P}(\delta)$ of an $\mathcal{A}$-diagram $\delta$ over a constellation $\Sigma$ is defined as $$\{\theta(v,\floor{r}) \doteq \theta(v',\floor{r'}) \mid f\in E^{D_\delta}, s^{D_\delta}(f)=\{v,v'\}\wedge \delta(f)=((\delta(v),r),(\delta(v'),r')) \}.$$

In some ways, diagrams generalise trails in a graph. Where paths describe a possible trajectory for a particle, diagrams describe the possible trajectories of a wave that can simultaneously spread in several directions when encountering forks. We now introduce the notion of *saturated diagrams*, which correspond to *maximal paths*.

\[def:diagramorder\] We define a preorder $\sqsubseteq$ on $\mathcal{A}$-diagrams over a constellation $\Sigma$ by: $\delta \sqsubseteq \delta'$ if there exists an isomorphism $\varphi$ 