[HJ97] Hongde Hu and André Joyal. Coherence completions of categories and their enriched softness. *Electronic Notes in Theoretical Computer Science*, 6:174-190, 1997. MFPS XIII, Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference. URL: https://www.sciencedirect.com/science/article/pii/S1571066105801628, doi:10.1016/S1571-0661(05)80162-8.

[HJ99] Hongde Hu and Andre Joyal. Coherence completions of categories. *Theoretical Computer Science*, 227(1):153-184, 1999. URL: https://www.sciencedirect.com/science/article/pii/S0304397599000511, doi:10.1016/S0304-3975(99)00051-1.

[Hou08] Robin Houston. Finite products are biproducts in a compact closed category. *Journal of Pure and Applied Algebra*, 212(2):394-400, February 2008. URL: https://arxiv.org/abs/math/0604542, doi:10.1016/j.jpaa.2007.05.021.

[Hue80] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. *Journal of the ACM*, 27(4):797-821, October 1980. doi:10.1145/322217.322230.

[Hug12] Dominic Hughes. Simple free star-autonomous categories and full coherence. *Journal of Pure and Applied Algebra*, 216(11):2386-2410, 2012. URL: https://www.sciencedirect.com/science/article/pii/S0022404912001089, doi:10.1016/j.jpaa.2012.03.020.

[HvG05] Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. *ACM Transactions on Computational Logic*, 6(4):784-842, 2005. doi:10.1145/1094622.1094629.

[HvG16] Dominic Hughes and Rob van Glabbeek. MALL proof nets identify proofs modulo rule commutation, 2016. https://arxiv.org/abs/1609.04693.

[Joy95a] André Joyal. Free bicomplete categories. *Mathematical Reports of the Academy of Sciences*, 17(5):219-224, 1995.

[Joy95b] André Joyal. Free bicompletion of enriched categories. *Mathematical Reports of the Academy of Sciences*, 17(5):213-218, 1995.

[Lam96] François Lamarche. From proof nets to games: extended abstract. *Electronic Notes in Theoretical Computer Science*, 3:107-119, 1996. doi:10.1016/S1571-0661(05)80409-8.

[Lau05] Olivier Laurent. Classical isomorphisms of types. *Mathematical Structures in Computer Science*, 15(5):969-1004, October 2005.

[LM08] Olivier Laurent and Roberto Maieli. Cut elimination for monomial MALL proof nets. In *Proceedings of the twenty-third annual symposium on Logic In Computer Science*, pages 486-497. IEEE, IEEE Computer Society Press, June 2008.

[LS88] Joachim Lambek and Philip Scott. *Introduction to Higher-Order Categorical Logic*. Number 7 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1988.

[PTdF10] Michele Pagani and Lorenzo Tortora de Falco. Strong normalization property for second order linear logic. *Theoretical Computer Science*, 411(2):410-444, 2010.

[Rit91] Mikael Rittri. Using types as search keys in function libraries. *Journal of Functional Programming*, 1(1):71-89, 1991.

[RU02] Laurent Regnier and Pawel Urzyczyn. Retractions of types with many atoms, 2002. http://arxiv.org/abs/cs/0212005.

[See89] Robert Seely. Linear logic, *-autonomous categories and cofree coalgebras. Contemporary mathematics*, 92, 1989.

[Sol83] Sergei Soloviev. The category of finite sets and cartesian closed categories. *Journal of Soviet Mathematics*, 22(3):1387-1400, 1983.

[TdF01] Lorenzo Tortora de Falco. Additives of linear logic and normalization- part II: the additive standardization theorem. Unpublished note, September 2001.

[TdF03] Lorenzo Tortora de Falco. Additives of linear logic and normalization- part I: a (restricted) Church-Rosser property. *Theoretical Computer Science*, 294(3):489-524, February 2003. doi:10.1016/S0304-3975(01)00176-1.
# APPENDIX A. RULE COMMUTATION IS THE CORE OF CUT-ELIMINATION

In this appendix is given a complete proof of Theorem 4.2 (i.e. [CP05, Theorem 5.1]). We had no knowledge of [CP05] when writing the conference paper [DGL23] on which this journal paper is based. Our initial proof of this result (extended with the mix-rules) is given in the first author's PhD thesis [DG24, Theorem 2.47]. After comparing our work with the one of Cockett and Pastro, the core of the two proofs happens to be very similar. There are three main differences between them, in addition to the used formalism. The first one is the choice of the theorems from rewriting theory which are used: Cockett and Pastro apply a result [CP05, Proposition B.3] they proved that resembles [AT12, Theorem 2.2] while we used a simpler (but less powerful) theorem [Hue80]. In particular, we proved a stronger result when closing rewriting diagrams (known as local coherence) while their theorem allowed them to prove a weaker one, that needs less technical tools. The second difference is a simplification by Cockett and Pastro allowing not to consider *cut – cut* commutations [CP05, Lemma C.2]. The last one is the norm for normalization: while they provide one that decreases by cut-elimination and is stable through $\top$-free rule commutations, we provide a norm stable by all rule commutations as well as *cut – cut* commutations (and still decreasing for other cut-elimination steps). Furthermore, the proof of [CP05, Theorem 5.1] seems to contain a mistake due to a $\& - \otimes$ commutation duplicating a cut-rule (see more explanations in Section 4), and a critical pair is lacking when closing rewriting diagrams.

We present here a fusion of these two demonstrations, in the setting of sequent calculus, with as rewriting theorem [AT12, Theorem 2.2], with simplifications on *cut – cut* commutations, corrected diagrams and the lacking case from [CP05]. We also detail some arguments implicit in the work of Cockett and Pastro, e.g. why there are no more critical pairs than the ones provided (and the one they forgot). The main idea to patch the proof of [CP05] is to consider only rule commutations with no *cut*-rule above, as we did in our proof, and then to normalize above the considered rules before applying a commutation between them. Note also that, contrary to [CP05], we do not assume proofs to be axiom-expanded since it almost does not impact the reasoning.

We work in sequent calculus, hence by proof we mean a sequent calculus proof, never considering proof-nets. We use standard notations from relation algebra and rewriting theory: given a relation $\triangleleft$, $\triangleleft^*$ (resp. $\triangleleft^+$, resp. $\triangleleft^=$) is the transitive reflexive (resp. transitive, resp. reflexive) closure of $\triangleleft$, while $\triangleright$ is the converse relation – symmetric relations will correspond to symmetric symbols. We denote by $\cdot$ the composition of relations.

We deduce Theorem 4.2 from a Church-Rosser property, that will be found by applying a result from Aoto and Tomaya [AT12].

**Definition A.1.** Let $\sim$ and $\to$ be relations on a set $A$ such that $\sim$ is an equivalence relation. The relation $\to$ is *Church-Rosser modulo* $\sim$ if $(\to \cup \leftarrow \cup \sim)^* \subseteq \to^* \cdot \sim \cdot \to^*$ (see Figure 16).

**Theorem A.2** [AT12, Theorem 2.2]. Let $\mid\vdash$, $\to$ and $\rightsquigarrow$ be relations on a set $A$ such that $\mid\vdash$ is symmetric and $\rightsquigarrow \subseteq \mid\vdash$. Set $\Rightarrow \coloneqq \to \cup \rightsquigarrow$. Suppose:

(i) $\to \rightsquigarrow^*$ is strongly normalizing;

(ii) $\leftarrow \to \subseteq \Rightarrow^* \cdot \bar{\mid\vdash} \cdot \Rightarrow^* \leftarrow$;

(iii) $\mid\vdash \to \subseteq (\bar{\mid\vdash} \cdot \Rightarrow^* \leftarrow) \cup (\to \Rightarrow^* \cdot \mid\vdash \cdot \Rightarrow^* \leftarrow)$.

Then $\to$ is *Church-Rosser modulo* $\Rightarrow^* \mid\vdash$.
<figure><img src="image_31.png" /><figcaption>Figure 16: Diagram of Church-Rosser modulo $\sim$ (Definition A.1), with hypotheses in solid black and conclusions in dashed red</figcaption></figure>

We denote by $\xrightarrow{\bar{\beta}}$ a $\xrightarrow{\beta}$ step other than a *cut-cut* commutation, and call $\bar{\beta}$-equality $=_{\bar{\beta}}$ the equivalence closure of $\xrightarrow{\bar{\beta}}$ steps (as $\beta$-equality $=_{\beta}$ is the equivalence closure of $\xrightarrow{\beta}$ steps). Also note $\vdash^c$ the *cut-cut* commutation (which is a symmetric relation).

We recall $\vdash^r$ (defined in Definition 2.5) is one-step rule commutation of *cut-free MALL*, i.e. which is not a commutation involving a *cut-rule* nor having above the commuted rules a sub-proof with a *cut-rule* (but it may have a *cut-rule* in its external context); for instance in the $\top \otimes$ commutation creating or deleting a sub-proof $\pi$, $\pi$ is cut-free.<fnref n="6" /> As $\vdash^r$ is symmetric, $\vdash^r$ is an equivalence relation.

We will instantiate Theorem A.2 as follows.

**Corollary A.3.** *Suppose:*

(i) $\xrightarrow{\bar{\beta}} \cdot \vdash^r$ is strongly normalizing;

(ii) $\vdash^c \xrightarrow{\bar{\beta}} \vdash^c \xrightarrow{\bar{\beta}^*} \vdash^r$;

(iii) $\vdash^r \xrightarrow{\bar{\beta}} \vdash^c \xrightarrow{\bar{\beta}} \vdash^r \xrightarrow{\bar{\beta}^*} \vdash^c \xrightarrow{\bar{\beta}^*} \vdash^r$.

Then $\xrightarrow{\bar{\beta}}$ is *Church-Rosser modulo* $\vdash^r$.

*Proof.* Direct use of Theorem A.2 with $\vdash := \vdash^r$, $\rightsquigarrow := \vdash^r$ and $\to := \xrightarrow{\bar{\beta}}$. $\square$

We prove the first item in Section A.1, and the two other hypotheses in Section A.2. Finally, we show in Section A.3 that $\bar{\beta}$-equality and $\beta$-equality coincide, leading to a proof of Theorem 4.2.

**A.1. Strong normalization.** The goal of this section is proving the strong normalization of $\xrightarrow{\bar{\beta}} \cdot \vdash^r$, namely Proposition A.10. We do so by giving a measure which is preserved by $\vdash^r$ and decreases during a $\xrightarrow{\bar{\beta}}$ step. This measure is quite different from the one of Cockett and Pastro [CP05, Section B.1], for ours is stable by all rule commutations and not only $\top$-free ones. It is also quite original for it depends only on the sequents and formulas we apply the *cut*-rules to, as well as which *cut*-rules are above which other *cut*-rules, but nothing else about the surrounding proof. Such a measure is usually not good for cut-elimination, and seems hard to come by without a linear point of view.

**Definition A.4.** The *mass* $m(A)$ of a formula $A$ is a natural number defined by induction:

$$ \bullet m(X) = m(X^{\perp}) = m(1) = m(\perp) = m(\top) = m(0) = 2 $$

<footnote n="6">⁶Actually, we only need it for the $\top \otimes$ and $\& \otimes$ commutations, but ask it for all commutations to homogenize proofs.</footnote>
$$ \bullet m(A \otimes B) = m(A \not\cong B) = m(A \& B) = m(A \oplus B) = (m(A) + 1) \times (m(B) + 1) $$

We extend this notion to sequents by defining $m(A_1, \dots, A_n) = \prod_{i=1}^n m(A_i)$ (with the usual convention that the empty product equals 1).

The mass $m(c)$ of a cut-rule $c$ of the shape $\frac{\vdash A^{\perp}, \Gamma \quad \vdash A, \Delta}{\vdash \Gamma, \Delta}$ cut is defined as
$$ m(c) = m(A) \times m(\Gamma, \Delta). $$

**Fact A.5.** For any formula $A$, $m(A) = m(A^{\perp}) > 1$.

Taking the multiset of the masses of cut-rules as our measure is not enough when the cut-elimination step we apply is not on a top-most cut-rule. The problem comes from a $\&$-cut commutative case where the duplicated sub-proof contains a cut-rule, whose mass may be bigger than the one of the reduced cut-rule. A solution is to add to a cut-rule the masses of all cut-rules below it.

**Definition A.6.** In a proof $\pi$, we define a partial order $\preceq$ between cut-rules by $c' \preceq c$ when $c$ is in the sub-proof of $\pi$ of root $c'$. This relation is reflexive: $c \preceq c$.

The density $d(c)$ of a cut-rule $c$ in a proof $\pi$ is defined as $d(c) = \sum_{c' \preceq c} m(c')$.

The density $d(\pi)$ of a proof $\pi$ is the multiset of the densities of its cut-rules.

For example, consider the following proof $\pi$, with cut-rules $c_1$ to $c_5$:

$$ \frac{\frac{\frac{\overline{\vdash X^{\perp}, X}^{ax}}{\vdash X^{\perp}, X} \quad \overline{\vdash X^{\perp}, X}^{ax} \quad c_1}{\vdash X^{\perp}, X}^{ax} \quad \frac{\overline{\vdash X^{\perp}, X} \oplus_1 c_2}{\vdash X^{\perp}, X \oplus 0} \quad \overline{\vdash T, X}^{\top} \quad \overline{\vdash X^{\perp}, X}^{ax}}{\vdash X^{\perp}, X \oplus 0} \quad \frac{\overline{\vdash T, X}^{\top} \quad \overline{\vdash T \& X^{\perp}, X}^{ax} \quad c_3}{\vdash X^{\perp}, X} \quad \overline{\frac{\frac{\overline{\vdash X^{\perp}, X}^{ax}}{\vdash X^{\perp}, X} \oplus_1 c_4}{\vdash X^{\perp}, X}}$$

The masses of the cut-rules are $m(c_1) = m(c_4) = m(c_5) = 8$ and $m(c_2) = m(c_3) = 36$. The ordering of cut-rules is $c_5 \preceq c_3 \preceq c_2 \preceq c_1$ and $c_5 \preceq c_4$. Thus, $d(c_5) = m(c_5)$, $d(c_4) = m(c_5) + m(c_4)$, $d(c_3) = m(c_5) + m(c_3)$, $d(c_2) = m(c_5) + m(c_3) + m(c_2)$ and $d(c_1) = m(c_5) + m(c_3) + m(c_2) + m(c_1)$.

Proving that a cut-elimination step $\xrightarrow{\beta}$ decreases density is a matter of checking cases, while it is easy to show a rule commutation preserves it.

**Lemma A.7.** Consider a cut-elimination step $\tau \xrightarrow{\beta} \phi$ and call $c$ the (unique) cut-rule in $\tau$ involved in this step and $(c_i)_{i \in \{1; \dots; n\}}$ the $n \in \{0; 1; 2\}$ resulting cut-rules in $\phi$. Then $m(c) > \sum_{i=1}^n m(c_i)$.

*Proof.* It suffices to compute the masses before and after each cut-elimination step. In the following case study, we use implicitly Fact A.5.

ax key case Here

$$ \tau = \frac{\frac{\overline{\vdash A^{\perp}, A}^{ax}}{\vdash A, \Gamma} \quad \overline{\vdash A, \Gamma}^{\pi} \quad c}{\rho} \quad \phi = \frac{\overline{\vdash A, \Gamma}^{\pi}}{\rho} $$

We have $n = 0$ and $m(c) = m(A) \times m(A) \times m(\Gamma) > 0 = \sum_{i=1}^n m(c_i)$. $\not\cong - \otimes$ key case Here
$$ \tau = \frac{\pi_1 \quad \pi_2 \quad \pi_3}{\frac{\vdash A, \Gamma \quad \vdash B, \Delta \quad \vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash A \otimes B, \Gamma, \Delta} \otimes \frac{\vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash B^{\perp}, \mathcal{R} A^{\perp}, \Sigma}} c \quad \mathcal{R} \quad \phi = \frac{\pi_1 \quad \pi_2 \quad \pi_3}{\frac{\vdash B, \Delta \quad \vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash A^{\perp}, \Delta, \Sigma} c_2 \quad \vdash \Gamma, \Delta, \Sigma} \otimes \frac{\vdash B^{\perp} \oplus A^{\perp}, \Delta}{\vdash \Gamma, \Delta, \Sigma} c_1} \rho $$

$$ \phi = \frac{\pi_1 \quad \pi_2 \quad \pi_3}{\frac{\vdash B, \Delta \quad \vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash A^{\perp}, \Delta, \Sigma} c_2 \quad \vdash \Gamma, \Delta, \Sigma} \otimes \frac{\vdash B^{\perp} \oplus A^{\perp}, \Delta}{\vdash \Gamma, \Delta, \Sigma} c_1 \quad \rho $$

We have $n = 2$ and:

$$ \begin{aligned} m(c) - \sum_{i=1}^{n} m(c_i) &= m(A \otimes B) \times m(\Gamma, \Delta, \Sigma) - m(A) \times m(\Gamma, \Delta, \Sigma) - m(B) \times m(A^{\perp}, \Delta, \Sigma) \\ &\geq (m(A \otimes B) - m(A) - m(B) \times m(A)) \times m(\Gamma, \Delta, \Sigma) \\ &= (m(B) + 1) \times m(\Gamma, \Delta, \Sigma) > 0 \end{aligned} $$

& $\oplus_1$ key case Here

$$ \tau = \frac{\pi_1 \quad \pi_2}{\frac{\vdash A, \Gamma \quad \vdash B, \Gamma}{\vdash A \& B, \Gamma}} \& \frac{\vdash B^{\perp}, \Delta}{\vdash B^{\perp} \oplus A^{\perp}, \Delta} \oplus_1 c \quad \rho $$

$$ \phi = \frac{\pi_2 \quad \pi_3}{\frac{\vdash B, \Gamma \quad \vdash B^{\perp}, \Delta}{\vdash \Gamma, \Delta}} c_1 \quad \rho $$

We have $n = 1$ and $m(c) = m(A \& B) \times m(\Gamma, \Delta) > m(B) \times m(\Gamma, \Delta) = \sum_{i=1}^{n} m(c_i)$.

& $\oplus_2$ key case This case is very similar to the $\oplus_1$ key case.

$\perp - 1$ key case Here

$$ \tau = \frac{\pi}{\frac{\vdash 1}{\vdash \Gamma} 1 \quad \frac{\vdash \Gamma}{\vdash \Gamma, \perp} \perp c} \quad \phi = \frac{\pi}{\vdash \Gamma} \rho $$

We have $n = 0$ and $m(c) = 2 \times m(\Gamma) > 0 = \sum_{i=1}^{n} m(c_i)$.

$\mathcal{R}$ - cut commutative case Here

$$ \tau = \frac{\pi_1 \quad \pi_2}{\frac{\vdash A, B, C, \Gamma \quad \vdash B, C, \Gamma, \Delta}{\vdash A, B, \mathcal{R} C, \Gamma \quad \vdash A^{\perp}, \Delta}} c \quad \phi = \frac{\pi_1 \quad \pi_2}{\frac{\vdash B, C, \Gamma, \Delta \quad \vdash B, C, \Gamma, \Delta}{\vdash B, \mathcal{R} C, \Gamma, \Delta}} c_1 \quad \rho $$

We have $n = 1$ and:

$$ \begin{aligned} m(c) - \sum_{i=1}^{n} m(c_i) &= m(A) \times m(B, \mathcal{R} C) \times m(\Gamma, \Delta) - m(A) \times m(B) \times m(C) \times m(\Gamma, \Delta) \\ &= m(A) \times (m(B, \mathcal{R} C) - m(B) \times m(C)) \times m(\Gamma, \Delta) \\ &= m(A) \times (m(B) + m(C) + 1) \times m(\Gamma, \Delta) > 0 \end{aligned} $$

$\otimes$ - cut - 1, $\otimes$ - cut - 2, $\oplus_1$ - cut, $\oplus_2$ - cut and $\perp$ - cut commutative cases These cases are quite similar to the $\mathcal{R}$ - cut commutative case.

& - cut commutative case Here
Having a measure preserved not only by rule commutations, but also by cut-cut commutations, is doable but much more complicated [DG24].

### A.2. Reduction diagrams.
We prove here Items (ii) and (iii) of Corollary A.3.

In this section we denote graphically some proofs with the following convention. When writing proofs as in

$$ \frac{\rho}{r_1} \underset{r_2}{\stackrel{r}{\vdash}} \frac{\rho}{r_2} $$

we abuse notations in the cases where $r_1$ or $r_2$ is a &- or $\vdash$-rule. The meaning is that, if say $r_1$ is a &-rule, then $r_2$ is duplicated, and even possibly a whole sub-proof if $r_2$ is a $\otimes$-rule for instance. Similarly, if $r_1$ is a $\vdash$-rule, then this schema means that on the left hand-side $r_2$ and $\rho$ are not here, and are created by the $\vdash$-commutation.

We begin by proving Item (ii), corresponding to reduction diagrams 0, 1 and 2 of [CP05, Section B.2.1] (including all three versions of these diagrams, namely one without units, one for additive units and one for multiplicative units). The main difference compared to [CP05] is on the cases corresponding to their reduction diagram 2, which here corresponds to Figure 17: since rule commutations are allowed only in the absence of cut-rules above, we have to normalize the sub-proof(s) above the considered rules before commuting them.

**Lemma A.12.** Let $\pi$, $\pi_1$ and $\pi_2$ be MALL proofs such that $\pi_1 \stackrel{\bar{\beta}}{\leftarrow} \pi \stackrel{\bar{\beta}}{\rightarrow} \pi_2$. Then there exist $\pi'_1$ and $\pi'_2$ such that $\pi_1 \stackrel{\bar{\beta}^*}{\rightarrow} \pi'_1 \stackrel{r}{\stackrel{\bar{\beta}^*}{\vdash}} \pi'_2 \stackrel{\bar{\beta}^*}{\leftarrow} \pi_2$. Diagrammatically:

<figure><img src="image_32.png" /></figure>

More precisely, we need a step of $r$ exactly when both $\bar{\beta}$ steps are different commutative cases on the same cut-rule.

*Proof.* If the $\pi \stackrel{\bar{\beta}}{\rightarrow} \pi_1$ and $\pi \stackrel{\bar{\beta}}{\rightarrow} \pi_2$ steps involve only distinct rules then, taking into account that rules of one may be duplicated or erased by the other step, they commute and we have a proof $\pi'$ such that $\pi_1 \stackrel{\bar{\beta}^*}{\rightarrow} \pi' \stackrel{\bar{\beta}^*}{\leftarrow} \pi_2$, by applying one reduction after the other.

From now on, we assume both steps involve (at least) one common rule. If both reductions share all of their rules, then the two reductions are the same: $\pi_1 = \pi_2$ and we are done (recall Remark 2.4 for our convention on the $\mathcal{Y} \otimes \mathcal{Y}$ key case). Hence, we assume they do not share all of their rules. We distinguish cases according to the kinds of the $\bar{\beta}$ steps.

*If one step is a key case other than an ax one.* Remark that on the three rules of a non-ax key case, no other $\bar{\beta}$ step can be applied (only a cut-cut commutation could have been applied, but this case does not belong to $\bar{\beta}$). Whenceforth, this case cannot happen as it would lead to the two reductions sharing all of their rules.

*If both steps are ax key cases.* (This corresponds to the reduction diagram 0 of [CP05, Section B.2.1].) As the two reductions share one rule, but not all rules, the shared rule must be the cut-rule, with as premises two ax-rules. We can check that this critical pair leads to the same resulting proof from both choices of cut-elimination. Thus $\pi_1 = \pi_2$.
If one step is an ax key case and the other a commutative case. (This corresponds to the reduction diagram 1 of [CP05, Section B.2.1].) By symmetry, assume $\pi \xrightarrow{\bar{\beta}} \pi_2$ is the ax key case. For the two reductions share a rule, and the ax-rule cannot participate in a commutative step, the shared rule must be the cut-rule. We can still do this ax key step after the commutation (maybe twice in case of duplication, or zero time in case of erasure), recovering $\pi_2$. Thus:

• $\pi_1 \xrightarrow{\bar{\beta}} \pi_2$ (ax-key case and not a $\&$ - cut nor $\top$ - cut commutative case) or

• $\pi_1 \xrightarrow{\bar{\beta}} \pi_2$ ($\&$ - ax-key case and $\&$ - cut commutative case) or

• $\pi_1 = \pi_2$ (ax-key case and $\top$ - cut commutative case).

If both steps are commutative cases. (This corresponds to the reduction diagram 2 of [CP05, Section B.2.1], with a modification.) Here again, as the two reductions share a rule, it must be the cut-rule, because there is at most one cut-rule directly below a given rule. As the reductions do not share both of their rules, in $\pi \xrightarrow{\bar{\beta}} \pi_1$ we sent a rule $r_1$ from a branch of the cut below it, and in $\pi \xrightarrow{\bar{\beta}} \pi_2$ we do similarly on a rule $r_2$ in the other branch. This case, more complex than the previous ones, is depicted schematically on Figure 17. We can in $\pi_1$ commute the cut-rule and $r_2$ - maybe twice in case of a duplication, or zero in case of an erasure - obtaining $\pi'_1$, and similarly in $\pi_2$ the cut-rule and $r_1$, yielding $\pi'_2$. The two resulting proofs differ exactly by a commutation of $r_1$ and $r_2$ (even if both are $\top$-rules, they differ by a $\top$ - $\top$ commutation). For we apply rule commutation only on cut-free sub-proofs, we first eliminate all cut-rules above these two rules, in the same way in all sub-proofs (and in case of duplication, in the same way in all duplicates of the sub-proofs). This can be done thanks to weak normalization of $\xrightarrow{\bar{\beta}}$ (Corollary A.11). Finally, we commute $r_1$ and $r_2$, and thus $\pi_1 \xrightarrow{\bar{\beta}^*} \pi_2$ if both steps are commutative cases.

The only difficulty here is proving that (the normal forms of) the two proofs $\pi'_1$ and $\pi'_2$ differ by a commutation of $r_1$ and $r_2$ as claimed. This is a simple but tedious case analysis on the kind of rules $r_1$ and $r_2$ can be, and checking that in every case we indeed can apply an $\xrightarrow{\beta}^r$ step. As there are 8 possible commutative cases for $\xrightarrow{\bar{\beta}}$ and we have two such steps, this leads to $8^2 = 64$ cases. We give here only one of those, where $r_1$ is a $\&$-rule and $r_2$ is a $\mathfrak{R}$-rule. In this case, our proofs are:

$$ \pi = \frac{\rho_1 \quad \rho_2 \quad \rho_3}{\frac{\vdash A^{\perp}, B, \Gamma \quad \vdash A^{\perp}, C, \Gamma \quad \vdash A, D, E, \Delta}{\vdash A^{\perp}, B \& C, \Gamma \quad \vdash A, D \mathfrak{R} E, \Delta}} \mathfrak{R} \text{ cut} \quad \vdash B \& C, D \mathfrak{R} E, \Gamma, \Delta $$

$$ \pi_1 = \frac{\rho_1 \quad \rho_3}{\frac{\vdash A^{\perp}, B, \Gamma \quad \vdash A, D, E, \Delta \quad \vdash A, D \mathfrak{R} E, \Delta}{\vdash B, D \mathfrak{R} E, \Gamma, \Delta}} \mathfrak{R} \text{ cut} \quad \frac{\rho_2 \quad \rho_3}{\vdash A^{\perp}, C, \Gamma \quad \vdash A, D, E, \Delta \quad \vdash A, D \mathfrak{R} E, \Delta}} \mathfrak{R} \text{ cut} \quad \vdash C, D \mathfrak{R} E, \Gamma, \Delta \quad \& \quad \vdash B \& C, D \mathfrak{R} E, \Gamma, \Delta $$
<figure><img src="image_33.png" /><figcaption>Figure 17: Schematic representation of the last case of the proof of Lemma A.12</figcaption></figure>

$$ \pi_2 = \frac{\frac{\rho_1 \quad \rho_2}{\vdash A^{\perp}, B, \Gamma \quad \vdash A^{\perp}, C, \Gamma} \& \quad \frac{\rho_3}{\vdash A^{\perp}, B \& C, \Gamma}}{\frac{\vdash B \& C, D, E, \Gamma, \Delta}{\vdash B \& C, D \nparallel E, \Gamma, \Delta}} \text{cut} $$

Following the method described above, we apply two $\mathcal{R} \text{ - cut}$ commutative cases in $\pi_1$ and one $\& \text{ - cut}$ commutative case in $\pi_2$, obtaining:

$$ \pi'_1 = \frac{\frac{\rho_1 \quad \rho_3}{\vdash A^{\perp}, B, \Gamma \quad \vdash A, D, E, \Delta} \text{cut} \quad \frac{\rho_2 \quad \rho_3}{\vdash A^{\perp}, C, \Gamma \quad \vdash A, D, E, \Delta} \text{cut}}{\frac{\vdash B, D, E, \Gamma, \Delta}{\vdash B, D \nparallel E, \Gamma, \Delta} \mathcal{R} \quad \frac{\vdash C, D, E, \Gamma, \Delta}{\vdash C, D \nparallel E, \Gamma, \Delta} \mathcal{R} \quad \frac{\vdash B \& C, D \nparallel E, \Gamma, \Delta}{\vdash B \& C, D \nparallel E, \Gamma, \Delta} \mathcal{R}} \& $$

$$ \pi'_2 = \frac{\frac{\rho_1 \quad \rho_3}{\vdash A^{\perp}, B, \Gamma \quad \vdash A, D, E, \Delta} \text{cut} \quad \frac{\rho_2 \quad \rho_3}{\vdash A^{\perp}, C, \Gamma \quad \vdash A, D, E, \Delta} \text{cut}}{\frac{\vdash B, D, E, \Gamma, \Delta}{\vdash B \& C, D, E, \Gamma, \Delta} \mathcal{R} \quad \frac{\vdash C, D, E, \Gamma, \Delta}{\vdash B \& C, D \nparallel E, \Gamma, \Delta} \mathcal{R}} \& $$
Then, we eliminate all cut-rules above these & and $\mathfrak{N}$-rules, in the same way in both proofs (thanks to Corollary A.11), yielding:

$$ \pi_1'' = \frac{\tau_1^{\text{cut-free}} \quad \tau_2^{\text{cut-free}}}{\frac{\vdash B, D, E, \Gamma, \Delta \quad \vdash C, D, E, \Gamma, \Delta}{\vdash B, D \mathfrak{N} E, \Gamma, \Delta} \quad \vdash B \& C, D \mathfrak{N} E, \Gamma, \Delta} \quad \mathfrak{N} \quad \& $$

$$ \pi_2'' = \frac{\tau_1^{\text{cut-free}} \quad \tau_2^{\text{cut-free}}}{\frac{\vdash B, D, E, \Gamma, \Delta \quad \vdash C, D, E, \Gamma, \Delta}{\vdash B \& C, D, E, \Gamma, \Delta} \quad \mathfrak{N}} \quad \& $$

We observe these two last proofs are equal up to a $\& - \mathfrak{N}$ commutation, which gives us that
$$ \pi_1 \xrightarrow{\bar{\beta}} \cdot \xrightarrow{\bar{\beta}} \pi_1 \xrightarrow{\bar{\beta}^+} \pi_1'' \xrightarrow{r} \pi_2 \xrightarrow{\bar{\beta}^+} \pi_2' \xleftarrow{\bar{\beta}} \pi_2. \quad \square $$

Now, let us prove Item (iii) of Corollary A.3, corresponding to reduction diagrams 3 to 6 of [CP05, Section B.2.1] (again including all three versions of these diagrams). As for the previous lemma, the main difference with [CP05] is that we normalize above the rules we wish to commute, which is a new step to integrate in reduction diagrams 3 and 4 of [CP05, Section B.2.1]. We also consider a critical pair that was missing in [CP05, Section B.2.1].

**Lemma A.13.** Let $\pi_1, \pi_2$ and $\pi_3$ be proofs such that $\pi_1 \xrightarrow{r} \pi_2 \xrightarrow{\bar{\beta}} \pi_3$. Then, there exist $\pi'_1, \pi'_2, \pi'_3$ and $\pi'_4$ such that $\pi_1 \xrightarrow{\bar{\beta}} \pi'_1 \xrightarrow{r} \pi'_2 \xrightarrow{\bar{\beta}^*} \pi'_3 \xrightarrow{r} \pi'_4 \xleftarrow{\bar{\beta}^*} \pi_3$. Diagrammatically:

<figure><img src="image_34.png" /></figure>

*Proof.* An easily handled case is when the $\pi_1 \xrightarrow{r} \pi_2$ and $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ steps involve only distinct rules; assume for now this is the case. A first general sub-case is when rules of one step are neither erased nor duplicated by the other. Then these steps commute and $\pi_1 \xrightarrow{\bar{\beta}} \cdot \xrightarrow{r} \pi_3$, using the same steps in the other order (because these are local transformations).

Now, consider the case where the two steps still involve distinct rules, but the $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ step duplicates a sub-proof containing the rules of $\pi_1 \xrightarrow{r} \pi_2$ (which may happen if $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is a $\& - \text{cut}$ commutative case). We apply the corresponding $\xrightarrow{\bar{\beta}}$ step first in $\pi_1$, yielding $\pi_1 \xrightarrow{\bar{\beta}} \pi_1^1$, and then the $\xrightarrow{r}$ step twice, once for each occurrence, to recover $\pi_3$: we get $\pi_1 \xrightarrow{\bar{\beta}} \pi_1^1 \xrightarrow{r} \cdot \xrightarrow{r} \pi_3$.

Another general case is when the rules involved in the two steps are distinct, but the $\xrightarrow{\bar{\beta}}$ step eliminates a sub-proof containing the rules of the $\xrightarrow{r}$ step (this can arise when using a $\& - \oplus_i$ key case or a $\top - \text{cut}$ commutative case). In this case, doing in $\pi_1$ the $\xrightarrow{\bar{\beta}}$ step directly yields $\pi_3$: $\pi_1 \xrightarrow{\bar{\beta}} \pi_3$.
Remark that, if these steps use distinct rules, the $\pi_1 \dashv^r \pi_2$ step cannot duplicate nor erase the rules involved in $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$. Indeed, this may happen if the $\dashv^r$ step is a $\& - \otimes$ or $\top - \otimes$ commutative case, but we assumed that a sub-proof corresponding to a rule commutation is cut-free, and a $\stackrel{\bar{\beta}}{\longrightarrow}$ step involves a *cut-rule* by definition.

From now on, we suppose both steps involve at least one common rule, which cannot be a *cut* one for no commutation of $\dashv^r$ involves a *cut-rule*. In fact, there is exactly one shared rule. Indeed, commuting rules of an $\dashv^r$ step are made of one rule on top of another rule, so both cannot be above a *cut-rule*. We distinguish cases according to the kind of $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$.

1. If $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$ is an ax key case. As an ax-rule never commutes, the two steps share no rule, contradiction.

2. If $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$ is another key case. (This corresponds to the reduction diagrams 5 and 6 of [CP05, Section B.2.1].) We only treat the $\mathfrak{X} - \otimes$ key case. The cases where $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$ is a $\& - \oplus_i$ or $\top - 1$ key case are similar, and even simpler as less *cut-rules* result from the reduction. Here, $\pi_2$ and $\pi_3$ are the following proofs:

$$ \frac{\begin{array}{ccc} \rho_1 & \rho_2 & \rho_3 \\ \vdash A, \Gamma & \vdash B, \Delta & \vdash B^{\perp}, A^{\perp}, \Sigma \\ \vdash A \otimes B, \Gamma, \Delta & & \vdash B^{\perp} \mathfrak{X} A^{\perp}, \Sigma \end{array}}{\rho_4} \mathfrak{X} \frac{\begin{array}{ccc} \rho_1 & \rho_2 & \rho_3 \\ \vdash B, \Delta & \vdash B^{\perp}, A^{\perp}, \Sigma & \vdash A^{\perp}, \Delta, \Sigma \end{array}}{\rho_4} \text{cut} \frac{\begin{array}{ccc} \rho_1 & \rho_2 & \rho_3 \\ \vdash A, \Gamma & \vdash B^{\perp}, A^{\perp}, \Sigma & \vdash A^{\perp}, \Delta, \Sigma \end{array}}{\rho_4} \text{cut} $$

$$ \frac{\begin{array}{ccc} \rho_1 & \rho_2 & \rho_3 \\ \vdash B, \Delta & \vdash B^{\perp}, A^{\perp}, \Sigma & \vdash A^{\perp}, \Delta, \Sigma \end{array}}{\rho_4} \text{cut} \frac{\begin{array}{ccc} \rho_1 & \rho_2 & \rho_3 \\ \vdash A^{\perp}, \Delta, \Sigma & \vdash A^{\perp}, \Delta, \Sigma & \vdash A^{\perp}, \Sigma \end{array}}{\rho_4} \text{cut} $$

(up to symmetry of the *cut-rule*, the case where $\pi_2$ has a $\mathfrak{X}$-rule on the left and a $\otimes$ one on the right being symmetric and solved similarly; and up to the order of the formulas in each sequent).

By our assumption, $\pi_1 \dashv^r \pi_2$ was a step pushing down the $\otimes$ or $\mathfrak{X}$-rule, and up some non *cut-rule* $r$. On Figure 18 is depicted the reasoning we apply here, in the case where $r$ commutes with the $\otimes$-rule. We can in $\pi_1$ commute the *cut-rule* up and $r$ down (as $r$ cannot be the rule of the main connective of the formula on which we cut, nor an *ax-rule*). This yields a proof $\pi_1^1$ such that $\pi_1 \stackrel{\bar{\beta}}{\longrightarrow} \pi_1^1$ with this commutative step, with $\pi_1^1$ being $\pi_2$ except $r$ is below the *cut-rule* and not above the $\otimes$ or $\mathfrak{X}$-rule (by abuse, for if $r$ is a $\top$-rule then the *cut-rule* is not here anymore). Thus, $\pi_1^1 \stackrel{\bar{\beta}}{\longrightarrow} \pi_1^2$ using the same step as in $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$; unless if $r$ is a $\top$-rule, in which case there is nothing to do and we set $\pi_1^1 = \pi_1^2$; or if $r$ is a $\&$-rule, where we have to apply this step in both occurrences, obtaining $\pi_1^1 \stackrel{\bar{\beta}}{\longrightarrow} \pi_1^2$. In any case, $\pi_1^1 \stackrel{\bar{\beta}^*}{\longrightarrow} \pi_1^2$. Observe that $\pi_1^2$ is like $\pi_3$, except that $r$ is above some *cut-rule(s)* in $\pi_3$ and below in $\pi_1^2$. But, using $\stackrel{\bar{\beta}}{\longrightarrow}$ in $\pi_3$, $r$ can commute down one or two of the *cut-rules* created by the key case, yielding $\pi_1^2$ (including if $r$ is a $\&$ or $\top$-rule). Therefore, $\pi_1 \stackrel{\bar{\beta}}{\longrightarrow} \pi_1^1 \stackrel{\bar{\beta}^*}{\longrightarrow} \pi_1^2 \stackrel{\bar{\beta}^+}{\longleftrightarrow} \pi_3$, concluding this case.

3. If $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$ is a commutative case. As $\pi_1 \dashv^r \pi_2$ and $\pi_2 \stackrel{\bar{\beta}}{\longrightarrow} \pi_3$ have exactly one rule in common, the $\dashv^r$ step involves the rule $r$ that will be commuted down in the $\stackrel{\bar{\beta}}{\longrightarrow}$ step, and another rule that we call $s$ ($r$ and $s$ are not *cut-rules*). The proof $\pi_1$ has from top to bottom $r$, $s$ and *cut*, $\pi_2$ has $s$, $r$ and *cut*, and $\pi_3$ has $s$, *cut* and $r$. We will also consider the
rule $t$ on the other branch of the cut-rule. Schematically (and up to symmetry):

$$ \pi_1 = \frac{r}{s} - t $$

$$ \pi_2 = \frac{s}{r} - t $$

$$ \pi_3 = \frac{s}{r} - t $$

We have here different sub-cases, according to whether the cut-rule commutes with $s$ and/or $t$. More exactly, we consider the following exhaustive cases:

* $s$ commutes with the cut-rule;

* $s$ does not commute with the cut-rule but $t$ does;

* $s$ does not commute with the cut-rule and $t$ is an ax-rule;

* neither $s$ nor $t$ commute with the cut-rule and $t$ is not an ax-rule.

**3.a. If $s$ commutes with the cut-rule.** (This corresponds to the reduction diagram 3 of [CP05, Section B.2.1], with a modification.) Our reasoning for this case is depicted on Figure 19. In $\pi_1$, we commute $s$-cut then $r$-cut, yielding $\pi_1 \xrightarrow{\bar{\beta}} \pi_1 \xrightarrow{\bar{\beta}^*} \pi_1^2$ (the $\xrightarrow{\bar{\beta}^*}$ being of length one, except if $s$ is a &-rule, in which case we apply the $r$-cut commutation for both occurrences, or if $s$ is a $\vdash$-rule, in which case there is no commutation to apply). The proof $\pi_1^2$ has from top to bottom cut, $r$ and $s$. Meanwhile, in $\pi_3$ we commute $s$-cut (twice if $r$ is a &-rule, or zero time if it is a $\vdash$-rule), yielding $\pi_3^1$ having from top to bottom cut, $s$ and $r$. Now, both $\pi_1^2$ and $\pi_3^1$ have above $r$ and $s$ a same proof (maybe duplicated or erased). We use normalization of $\xrightarrow{\bar{\beta}}$ (Corollary A.11) to eliminate all cut-rules in this sub-proof, in the same way for all its occurrences in $\pi_1^2$ and $\pi_3^1$, obtaining proofs $\pi_1^3$ and $\pi_3^2$ equal up to the commutation of $r$ and $s$ (the very same one that was used in $\pi_1 \vdash \pi_2$). We thus obtain $\pi_1 \xrightarrow{\bar{\beta}} \pi_1 \xrightarrow{\bar{\beta}^*} \pi_1^2 \xrightarrow{\bar{\beta}^*} \pi_1^3 \vdash \pi_3^2 \xleftarrow{\bar{\beta}^*} \pi_1^3 \xleftarrow{\bar{\beta}^*} \pi_3$. To formally check that indeed we can apply a $\vdash$ step, we would have to check all cases depending on the kind of rules $r$ and $s$ are. We do not write this tedious case study; a motivated reader can easily check some of these cases.

**3.b. If $t$ commutes with the cut-rule whereas $s$ does not.** (This corresponds to the reduction diagram 4 of [CP05, Section B.2.1], with a modification.) Remark $s$ cannot be an ax-rule, for it commutes with $r$. This case is represented on Figure 20. On $\pi_1$, we apply a commutative $\xrightarrow{\bar{\beta}}$ step between $t$ and the cut-rule, giving $\pi_1^1 = \frac{s}{r} \text{ cut}$. We then apply the same rule commutation between $r$ and $s$ that was done in $\pi_1 \vdash \pi_2$, obtaining $\pi_1^2 = \frac{r}{s} \text{ cut}$ (as usual, we do it twice if $t$ is a &-rule and have nothing to do if $t$ is a $\vdash$-rule). After that, we apply a commutative step between $r$ and the cut-rule, the same one as in $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$, yielding $\pi_1^3 = \frac{r}{s} \text{ cut}$. On the other hand, applying in $\pi_3$ a commutative case with $t$ gives $\pi_3^1 = \frac{r}{s} \text{ cut}$. One can check that $\pi_1^3$ and $\pi_3^1$ differ only by a commutation between $r$ and $t$ - as usual, up to checking many cases depending on the kind of rules $r$ and $t$ are. We normalize the sub-proof(s) above $r$ and $t$ in the same way in $\pi_1^3$ and $\pi_3^1$ (using Corollary A.11), obtaining $\pi_1^4$ and $\pi_3^2$ such that $\pi_1^4 \vdash \pi_3^2$. This solves this case: $\pi_1 \xrightarrow{\bar{\beta}} \pi_1 \xrightarrow{r^*} \pi_1^2 \xrightarrow{\bar{\beta}^*} \pi_1^3 \xrightarrow{\bar{\beta}^*} \pi_1^4 \xrightarrow{r^*} \xleftarrow{\bar{\beta}^*} \pi_2^2 \xleftarrow{\bar{\beta}^*} \pi_3^1 \xleftarrow{\bar{\beta}^*} \pi_3$.

**3.c. If $s$ does not commute with the cut-rule and $t$ is an ax-rule.** (This is an absent case in [CP05, Section B.2.1] for they work with axiom-expanded proofs.) This case is represented on Figure 21. Observe that here both $s$ and $t$ introduce the cut formula. In both $\pi_1$ and $\pi_3$,
<figure><img src="image_35.png" /><figcaption>Figure 18: Schematic representation of case 2 in the proof of Lemma A.13</figcaption></figure>

we apply an *ax* key case using *t*, giving respectively $\pi_1^1 = \bar{r}$ and $\pi_3^1 = \bar{r}$ (as usual, in $\pi_3$ we do this key case twice if *r* is a `&-rule` and have nothing to do if *r* is a `⊥-rule`). One can check that $\pi_1^1 \dashv\vdash \pi_3^1$ through a commutation between *r* and *s*, with no *cut-rule* above *r* and *s* as there was a commutation $\pi_1 \dashv\vdash \pi_2$. Thus, we have $\pi_1 \xrightarrow{\bar{\beta}} \pi_1^1 \dashv\vdash \pi_3^1 \xleftarrow{\bar{\beta}^*} \pi_3$.

3.d. If *s* and *t* both do not commute with the cut-rule and *t* is not an *ax-rule*. (This is a missing case in [CP05, Section B.2.1].) This case is represented on Figure 22. In both $\pi_1$ and $\pi_3$ we apply the sole possible key case using *s* and *t*, obtaining respectively $\pi_1^1 = \bar{r}$ and $\pi_3^1 = \bar{r}$ (where $cut^*$ represents 0, 1 or 2 *cut-rules*). We remark that $\pi_3^1$ can be obtained from $\pi_1^1$ by commuting *r* with the produced *cut-rules* – except if the key case was a `&` $\to$ *i* one that erased *r*, in which case $\pi_1^1 = \pi_3^1$. Thus $\pi_1 \xrightarrow{\bar{\beta}} \pi_1^1 \xrightarrow{\bar{\beta}^*} \pi_3^1 \xleftarrow{\bar{\beta}^*} \pi_3$. $\square$

We can now prove the wished result.

**Proposition A.14.** In the sequent calculus of MALL, $\xrightarrow{\bar{\beta}}$ is Church-Rosser modulo $\bar{r}^* \dashv\vdash$.

*Proof.* By Corollary A.3, Proposition A.10 and Lemmas A.12 and A.13. $\square$

**A.3. Removing cut-cut commutations.** We prove here that $\beta$-equality and $\bar{\beta}$-equality coincide. This corresponds to [CP05, Lemmas C.2 and C.3], proven here with two considerations that were at best implicit in the proof of [CP05]. The first is that *cut* – *cut* commutations and *ax* key cases lead to proofs that are equal not directly up to *cut* – *cut* commutation but up to *symmetry of a cut-rule*. The second is that the demonstration of [CP05, Lemmas C.2 and C.3] proves an induction hypothesis on a single *cut* – *cut* commutation, but applies it on a sequence of such commutations.
<figure><img src="image_36.png" /><figcaption>Figure 19: Schematic representation of case 3.a in the proof of Lemma A.13</figcaption></figure>

<figure><img src="image_37.png" /><figcaption>Figure 20: Schematic representation of case 3.b in the proof of Lemma A.13</figcaption></figure>
<figure><img src="image_38.png" /><figcaption>Figure 21: Schematic representation of case 3.c in the proof of Lemma A.13</figcaption></figure>

<figure><img src="image_39.png" /><figcaption>Figure 22: Schematic representation of case 3.d in the proof of Lemma A.13</figcaption></figure>

**Definition A.15.** The symmetry of a cut-rule is the identification of the following (sub-) proofs:

$$ \pi_1 = \frac{\rho_1 \quad \rho_2}{\vdash A, \Gamma \quad \vdash A^{\perp}, \Delta \quad \vdash \Gamma, \Delta} \text{ cut} \quad \text{and} \quad \pi_2 = \frac{\rho_2}{\vdash A^{\perp}, \Delta \quad \vdash A, \Gamma} \text{ cut} $$

This relation is included in $=_{\beta}$, using a cut-cut commutation. Indeed, define respectively $\pi'_1$ and $\pi'_2$ the following two proofs, where $A_1$ and $A_2$ are both the formula A, with indices to follow their occurrences:
$$ \frac{\overline{\vdash A_1^\perp, A_2} \quad ax \quad \rho_1}{\overline{\vdash A_2, \Gamma} \quad cut \quad \rho_2 \quad \vdash A_2^\perp, \Delta} \quad \text{and} \quad \frac{\overline{\vdash A_1^\perp, A_2} \quad ax \quad \rho_2}{\overline{\vdash A_1^\perp, \Delta} \quad cut \quad \rho_1 \quad \vdash A_1, \Gamma} $$

Then $\pi_1 \stackrel{\bar{\beta}}{\leftarrow} \pi'_1 \stackrel{c}{\rvert} \pi'_2 \stackrel{\bar{\beta}}{\rightarrow} \pi_2$, these $\stackrel{\bar{\beta}}{\rightarrow}$ steps being $ax$ key cases.

We now prove this relation is in $\bar{\beta}$-equality.

**Lemma A.16.** Let $\pi_1$ and $\pi_2$ be two proofs equal up to symmetry of cut-rules. Then $\pi_1 \stackrel{\bar{\beta}^*}{\rightarrow} \pi_2$.

*Proof.* The idea is to eliminate any *cut-rule* in $\pi_1$ and $\pi_2$ in a symmetric way, and show the resulting proofs are equal up to symmetry of *cut-rules*. The result follows through weak normalization, as two cut-free proofs equal up to symmetry of *cut-rules* are simply equal.

We reason by induction on a sequence $\pi_1 \stackrel{\bar{\beta}^*}{\rightarrow} \rho$, with $\rho$ some cut-free proof found by weak normalization (Corollary A.11). If this sequence is empty, then $\pi_1$ is *cut-free* and so $\pi_1 = \pi_2$. Thus, take $\pi_1 \stackrel{\bar{\beta}}{\rightarrow} \pi'_1$ its first step. We apply the corresponding step in $\pi_2$, on the corresponding *cut-rule* which may be the symmetric version of $c$ (for if a $\stackrel{\bar{\beta}}{\rightarrow}$ step can be applied, then the one with switched premises can be applied on the symmetric version). We obtain a proof $\pi'_2$ with the *cut-rule* still permuted compared to $\pi'_1$ in case of a commutative case (or the *cut-rule* erased when commuting with a $\top$, or permuted and duplicated with a $\&$) and 0, 1 or 2 symmetric *cut-rules* resulting from a key case. In all cases, $\pi'_1$ and $\pi'_2$ are equal up to symmetry of *cut-rules*, allowing us to conclude by induction hypothesis. $\square$

**Lemma A.17** ([CP05, Lemmas C.2 and C.3], adapted). Let $\pi$ and $\tau$ be proofs such that $\pi \stackrel{c^*}{\rvert} \tau$. Then $\pi$ and $\tau$ are $\bar{\beta}$-equal.

*Proof.* We reason by induction on $(cr(\pi), n)$ where $cr(\pi)$ is the sum over slices of $\pi$ of the number of non-cut-rules in these slices, and $n$ the number of $\stackrel{c}{\rvert}$ steps in $\pi \stackrel{c^*}{\rvert} \tau$. Remark the number of non-cut-rules of a slice in a proof is preserved by *cut* – *cut* commutations, so that $cr(\pi) = cr(\tau)$.

If $n=0$ we are done as $\pi = \tau$. Otherwise, $\pi \stackrel{c^*}{\rvert} \tau$ is a non-empty sequence $\pi \stackrel{c}{\rvert} \phi \stackrel{c^*}{\rvert} \tau$. By induction hypothesis, $\phi = \bar{\beta} \tau$ (using $cr(\pi) = cr(\phi) = cr(\tau)$), so we have to prove $\pi = \bar{\beta} \phi$. As $\pi \stackrel{c}{\rvert} \phi$, we have:

$$ \pi = \frac{\mu_1 \quad \mu_2}{\frac{\vdash A^\perp, B^\perp, \Gamma_1 \quad \vdash B, \Gamma_2}{\vdash A^\perp, \Gamma_1, \Gamma_2 \quad \vdash A, \Gamma_3}} \text{cut} \quad \mu_3 \quad \frac{\mu_1 \quad \mu_3}{\frac{\vdash A^\perp, B^\perp, \Gamma_1 \quad \vdash A, \Gamma_3}{\vdash B^\perp, \Gamma_1, \Gamma_3 \quad \vdash B, \Gamma_2}} \text{cut} \quad \mu_2 \quad \frac{\mu_1 \quad \mu_3}{\frac{\vdash A^\perp, B^\perp, \Gamma_1 \quad \vdash A, \Gamma_3}{\vdash B^\perp, \Gamma_1, \Gamma_3 \quad \vdash B, \Gamma_2}} \text{cut} $$

and

$$ \phi = \frac{\mu_1 \quad \mu_3}{\frac{\vdash A^\perp, B^\perp, \Gamma_1 \quad \vdash A, \Gamma_3}{\vdash B^\perp, \Gamma_1, \Gamma_3 \quad \vdash B, \Gamma_2}} \text{cut} \quad \mu_2 \quad \frac{\mu_1 \quad \mu_3}{\frac{\vdash A^\perp, B^\perp, \Gamma_1 \quad \vdash A, \Gamma_3}{\vdash B^\perp, \Gamma_1, \Gamma_3 \quad \vdash B, \Gamma_2}} \text{cut} $$

(or one of the three other analogous situations, up to switching branches of the two *cut-rules*). Remark we use here that $\beta$-equality is contextual in order to assume the two commuted cut-rules are the last rules of $\pi$ and $\phi$. By eliminating cuts in $\mu_1$, $\mu_2$ and $\mu_3$ using $\stackrel{\bar{\beta}}{\rightarrow}$ (Corollary A.11), we can assume them cut-free. Remark that $cr(\mu_i) \le cr(\pi)$ for each $i$, as cut-elimination in MALL reduces the number of non-cut-rules in a slice. We conclude through a case study of the last rules of $\mu_1$, $\mu_2$ and $\mu_3$.

1. If the last rule of one of the $\mu_i$ is an ax-rule. If the last rule of $\mu_2$ or $\mu_3$ is an ax-rule, then using an $ax$ key case in $\pi$ and $\phi$ we obtain $\pi \stackrel{\bar{\beta}}{\rightarrow} \phi$. If the last rule of $\mu_1$ is an ax-rule, applying an $ax$ key case in $\pi$ and $\phi$ yield two proofs equal up to symmetry of a *cut-rule*, so $\bar{\beta}$-equal (Lemma A.16). Thus, we assume from now on that the last rule of each $\mu_i$ is not an ax-rule.
2. If the last rule of one of the $\mu_i$ commutes with both cut-rules. This case is represented on Figure 23. If the last rule $r$ of $\mu_1$ is not the rule introducing the formula $A^{\perp}$ nor the formula $B^{\perp}$, by applying in both $\pi$ and $\phi$ two commutative cases on $r$ with the two successive cut-rules below it, we obtain respectively

$$ \pi' = \frac{\frac{\mu_1' \quad \mu_2}{\vdash A^{\perp}, B^{\perp}, \Gamma_1' \quad \vdash B, \Gamma_2} \quad \mu_3}{\frac{\vdash A^{\perp}, \Gamma_1, \Gamma_2}{\vdash \Gamma_1', \Gamma_2, \Gamma_3} \quad \vdash A, \Gamma_3} \quad \text{cut} \quad \frac{\mu_1'}{\mu_1} \quad \text{and } \phi' = \frac{\frac{\mu_1' \quad \mu_3}{\vdash A^{\perp}, B^{\perp}, \Gamma_1' \quad \vdash A, \Gamma_3} \quad \mu_2}{\frac{\vdash B^{\perp}, \Gamma_1', \Gamma_3}{\vdash \Gamma_1', \Gamma_2, \Gamma_3} \quad \vdash B, \Gamma_2} \quad \text{cut} $$

with $\mu_1$ being $\frac{\vdash A^{\perp}, B^{\perp}, \Gamma_1'}{\vdash A^{\perp}, B^{\perp}, \Gamma_1}$, $\pi \xrightarrow{\bar{\beta}^+} \pi'$ and $\phi \xrightarrow{\bar{\beta}^+} \phi'$. We conclude by induction hypothesis

$$ \frac{\mu_1' \quad \mu_2}{\vdash A^{\perp}, B^{\perp}, \Gamma_1' \quad \vdash B, \Gamma_2} \quad \mu_3}{\vdash A^{\perp}, \Gamma_1', \Gamma_2 \quad \vdash A, \Gamma_3} \quad \text{cut} = \bar{\beta} \quad \frac{\mu_1' \quad \mu_3}{\vdash A^{\perp}, B^{\perp}, \Gamma_1' \quad \vdash A, \Gamma_3} \quad \mu_2}{\vdash B^{\perp}, \Gamma_1', \Gamma_3 \quad \vdash B, \Gamma_2} \quad \text{cut} $$

(which have at least the non-cut-rule $r$ removed with respect to $\pi$), so that $\pi \xrightarrow{\bar{\beta}^+} \pi' = \bar{\beta}$
$\phi' \xleftarrow{\bar{\beta}^+} \phi$. Remark that we apply the induction hypothesis two times in case $r$ is a $\&$-rule (once in each branch of $r$) and do not apply it if $r$ is a $\top$-rule. The cases where the last rule of $\mu_2$ is not the rule introducing the formula $B^{\perp}$, and where the last rule of $\mu_3$ is not the rule introducing the formula $A^{\perp}$, are similar.

3. If the last rule of all $\mu_i$ do not commute with the cut-rules. This case is represented on Figure 24. If the last rule $r_1$ of $\mu_1$ is the rule introducing the formula $B^{\perp}$, and the last rule $r_2$ of $\mu_2$ the one introducing $B$, we can apply a key case in $\pi$ and a commutative case on $r_1$ followed by a key case in $\phi$. The proofs we obtain are

$$ \pi' = \frac{\mu_1' \quad \mu_2'}{\frac{\vdash A^{\perp}, \Gamma_1' \quad \vdash \Gamma_2'}{\vdash A^{\perp}, \Gamma_1, \Gamma_2} \quad \mu_3} \quad \text{cut}^* \quad \frac{\mu_1'}{\mu_1} \quad \text{and } \phi' = \frac{\mu_1' \quad \mu_3}{\frac{\vdash A^{\perp}, \Gamma_1' \quad \vdash A, \Gamma_3}{\vdash \Gamma_1', \Gamma_3} \quad \mu_2} \quad \text{cut} $$

with $\mu_1 = \frac{\vdash A^{\perp}, \Gamma_1'}{\vdash A^{\perp}, B^{\perp}, \Gamma_1}$, $\mu_2 = \frac{\vdash \Gamma_2'}{\vdash B, \Gamma_2}$, $\pi \xrightarrow{\bar{\beta}} \pi'$ and $\phi \xrightarrow{\bar{\beta}^+} \phi'$. The notation $cut^*$

here means we have a number of cut-rules: 0 if the key case was a $\perp - 1$, 1 if it was a $\& - \oplus_1$ or $\& - \oplus_2$, 2 if it was a $\mathcal{N} - \otimes$. Remark that $\pi' \stackrel{c^*}{\longmapsto} \phi'$ (this sequence being of size the number of cut-rules represented by $cut^*$) with $cr(\pi') < cr(\pi)$ for we removed at least rules $r_1$ and $r_2$.

Hence, we conclude $\pi \xrightarrow{\bar{\beta}} \pi' = \bar{\beta} \phi' \xleftarrow{\bar{\beta}^+} \phi$. The case where the last rule of $\mu_1$ introduces $A^{\perp}$, and the last rule of $\mu_2$ introduces $A$, is similar. $\square$

The theorem claimed in the main part then follows.

**Theorem 4.2** (Rule commutation is the core of cut-elimination [CP05, Theorem 5.1]). If two proofs $\pi$ and $\tau$ are $\beta$-equal, then any of their normal forms by $\xrightarrow{\beta}$ are related by $\xrightarrow{r^*}$.

*Proof.* The normal forms are $\beta$-equal, so $\bar{\beta}$-equal (Lemma A.17). By Proposition A.14, they are related by $\xrightarrow{r^*}$ since no reduction $\xrightarrow{\bar{\beta}}$ can be applied to them. $\square$
<figure><img src="image_40.png" /><figcaption>Figure 23: Schematic representation of case 2 in the proof of Lemma A.17</figcaption></figure>

<figure><img src="image_41.png" /><figcaption>Figure 24: Schematic representation of case 3 in the proof of Lemma A.17</figcaption></figure>

## APPENDIX B. CONJECTURES ON ISOMORPHISMS OF SYMMETRIC MONOIDAL CLOSED CATEGORIES WITH FINITE (CO)PRODUCTS

As a follow-up of Section 9.3, we present here some conjectures about isomorphisms in SMCC with finite products and finite coproducts on one hand, and in SMCC with finite coproducts (but not finite products) on the other hand. We also give in these two cases formulas that are not isomorphic, while they are isomorphic in $\star$-autonomous categories with finite products.

We conjecture that isomorphisms in SMCC with both finite products and finite coproducts correspond to adding the equations of theory $\mathcal{C}$ (Section 10) to $\mathcal{S}$ (Table 7). However, our approach through $\star$-autonomous categories does not work since for example $\top \to (\top \oplus \top)$ and $(0 \& 0) \to 0$ are isomorphic in $\star$-autonomous categories but not in SMCC with finite products and coproducts. Indeed, in $\star$-autonomous categories one has:

$$ 
\begin{align*}
\top \to (\top \oplus \top) &= \mathcal{D} \to (((\top \to \bot) \& (\top \to \bot)) \to \bot) \\
&= \mathcal{D} (\top \otimes (0 \& 0)) \to \bot = \mathcal{D} ((0 \& 0) \otimes \top) \to \bot \\
&= \mathcal{D} (0 \& 0) \to (\top \to \bot) = \mathcal{D} (0 \& 0) \to 0
\end{align*}
$$
or directly by interpreting these formulas into MALL, one gets:

$$ \ell(\top \to (\top \oplus \top)) =_L 0 \mathfrak{R}(\top \oplus \top) =_L (\top \oplus \top) \mathfrak{R} 0 =_L \ell((0 \& 0) \to 0) $$

(the analogue of the non-ambiguity property, used in Section 9.3, does not hold). That this isomorphism is not valid in the SMCC setting follows from the succeeding necessary condition.

**Lemma B.1.** If $F \simeq G$ in symmetric monoidal closed categories with finite products and coproducts with $F$ and $G$ distributed (i.e. $\ell(F)$ and $\ell(G)$ are distributed) then there exist cut-free proofs of $F \vdash G$ and $G \vdash F$ in IMALL (intuitionistic multiplicative additive linear logic) [Bie95] whose left 0 rules introduce 0 sequents only and right $\top$ rules introduce $\top \vdash \top$ sequents only.

*Proof.* If $F$ and $G$ are isomorphic in SMCC with finite products and coproducts, the associated isomorphisms can be represented as IMALL proofs which we can assume to be cut-free. These proofs can be interpreted as MALL proofs (corresponding to the fact that MALL is an SMCC with finite products and coproducts). By Lemma 5.16, these MALL proofs have their $\top$ rules introducing $\vdash \top$, 0 sequents only which gives the required property on the IMALL proofs we started with. $\square$

We deduce that $\top \to (\top \oplus \top) \simeq (0 \& 0) \to 0$ is an isomorphism of MALL but not one of IMALL, using Lemma B.1 and since all cut-free proofs of $(0 \& 0) \to 0 \vdash \top \to (\top \oplus \top)$ in IMALL have the following shape:

$$ \frac{\frac{(0 \& 0) \to 0, \top \vdash \top}{(0 \& 0) \to 0, \top \vdash \top \oplus \top}}{\top R} \quad \frac{\oplus_i R}{(0 \& 0) \to 0 \vdash \top \to (\top \oplus \top)} \to R $$

Let us now investigate SMCC with finite coproducts only (without products). It is important to notice that an initial object 0 in a SMCC induces that $0 \to F$ is a terminal object for any $F$. This first means that we cannot uncorrelate completely products and coproducts. It also means that the theory of isomorphisms includes the equation $0 \to F \simeq 0 \to G$ even if it does not occur in $C$.<fnref n="7" /> It might be the only missing equation: we conjecture isomorphisms are characterized by the following equations:

$$ F \otimes (G \otimes H) = (F \otimes G) \otimes H $$

$$ F \otimes G = G \otimes F $$

$$ F \otimes 1 = F $$

$$ F \oplus (G \oplus H) = (F \oplus G) \oplus H $$

$$ F \oplus G = G \oplus F $$

$$ F \oplus 0 = F $$

$$ F \otimes (G \oplus H) = (F \otimes G) \oplus (F \otimes H) $$

$$ F \otimes 0 = 0 $$

$$ (F \otimes G) \to H = F \to (G \to H) $$

$$ 1 \to F = F $$

$$ 0 \to F = 0 \to G $$

Regarding a characterization through $\star$-autonomous categories, it is again not possible since, if we denote by $\top$ a terminal object, $(\top \to 0) \to 0$ and $\top \to (\top \otimes \top)$ are isomorphic

<footnote n="7">⁷Note this equation is derivable from $C$ through the use of $\top$, but $\top$ does not belong to the language here.</footnote>
in ★-autonomous categories (using $0 =_D \top \to \bot$):

$$ \begin{align*} (\top \to 0) \to 0 &=_D (\top \to (\top \to \bot)) \to (\top \to \bot) \\ &=_D (((\top \otimes \top) \to \bot) \to (\top \to \bot)) \\ &=_D (((((\top \otimes \top) \to \bot) \otimes \top) \to \bot) \\ &=_D (\top \otimes (((\top \otimes \top) \to \bot)) \to \bot) \\ &=_D \top \to (((((\top \otimes \top) \to \bot) \to \bot) \to \top) =_D \top \to (\top \otimes \top) \end{align*} $$

(or $\ell((\top \to 0) \to 0) =_L (\top \otimes \top) \to 0 =_L 0 \otimes (\top \to \top) =_L \ell(\top \to (\top \otimes \top))$ in MALL). But they are not isomorphic in SMCC with initial and terminal objects by Lemma B.1 since all cut-free proofs of $(\top \to 0) \to 0 \vdash \top \to (\top \otimes \top)$ in IMALL have the following shape (up to permuting the premises of the $(\otimes R)$-rule):

$$ \frac{(\top \to 0) \to 0 \vdash \top \quad \top R \qquad \top R}{(\top \to 0) \to 0, \top \vdash \top \otimes \top \qquad \otimes R} \quad \to R $$

or

$$ \frac{(\top \to 0) \to 0, \top \vdash \top \quad \top R \qquad \top R}{(\top \to 0) \to 0, \top \vdash \top \otimes \top \qquad \otimes R} \quad \to R $$