also satisfies the additional constraint that each vertex must be (1) the target of exactly one hyperedge, and (2) the source of at most one hyperedge. When needed, a proof-structure will be defined as a 6-tuple $(V,E,s,t,\ell_V,\ell_E)$, where $(V,E,s,t)$ is a directed hypergraph (see Definition \[ex:graphencoding\]) and $\ell_V: V\rightarrow \mathcal{F}_{\mathrm{MLL}}$, $\ell_E: E\rightarrow\{\otimes,\parr,\mathrm{ax},\mathrm{cut}\}$ are labelling maps.

The cut-elimination procedure, which is defined in the natural way for MLL sequent calculus, becomes a graph-rewriting system on proof-structures, defined by the two rewriting rules (figure \[subfig:cutelimination\]). The following definition explains how sequent calculus proofs can be represented as proof-structures.

\[def:translation\] We define a translation $\interp{\cdot}$ from MLL sequent calculus derivations to proof-structures. The proof-structures of the domain of $\interp{\cdot}$ are called the *proof-nets*.

Note that this translation is not surjective, and some proof-structures do not represent sequent calculus proofs. This is tackled by the *correctness criterion* which characterises those proof-structures that do translate sequent calculus proofs through topological properties. This is discussed in the next section but for the time being we define the notion of proof-net.

A *proof-net* is a proof-structure $\mathcal{S}$ such that there exists a MLL sequent calculus proof $\pi$ with $\mathcal{S}=\interp{\pi}$.

Reconstruction of proof-structures and their dynamics {#subsec:proofs}
-----------------------------------------------------

