Let us note that proof-structures can be defined inductively. A proof-structure with only one hyperedge is necessarily an axiom with two conclusions. Then a proof-structure with $n$ hyperedges is either built from the union of two proof-structures with respectively $k$ and $n-k$ hyperedges, or from a proof-structure with $n-1$ hyperedges extended by either a $\otimes$, $\parr$, or $cut$ hyperedge on two of its conclusions. In the following we use this inductive definition to define the *address* of occurrences of atoms in a proof-structure.

A vertex $v$ is *above* another vertex $u$ in a proof-structure if there exists a directed path from $v$ to $u$ going through only $\otimes$ and $\parr$ hyperedges.

\[def:loc\] We now consider a signature in which there exists at least two unary function symbols $\mathtt{r},\mathtt{l}$ and unary functions symbols $p_A$ for all occurrences[^6] of MLL formulas $A$. We define the partial address $\ploc_\mathcal{S}(d,x)$ of an occurrence of atom $d$ in a MLL proof-structure $\mathcal{S}$, with respect to the variable $x$, inductively:

-   $\ploc_\mathcal{S}(d,x)=x$ when $\mathcal{S}$ consists only of an axiom hyperedge;

-   $\ploc_\mathcal{S}(d,x)=\ploc_{\mathcal{S}_i}(d,x)$ if $\mathcal{S}$ is the union of two smaller proof-structures $\mathcal{S}_1, \mathcal{S}_2$ and $d$ appears in $\mathcal{S}_i$;

-   $\ploc_\mathcal{S}(d,x)=\mathtt{l}(\ploc_{\mathcal{S}'}(d,x)$ (resp. $\ploc_\mathcal{S}(d,x)=\mathtt{r}(\ploc_{\mathcal{S}'}(d,x)$) if $\mathcal{S}$ is obtained 