# Proving Termination With CPO –Full Version

Alejandro Díaz-Caro, Gilles Dowek, Jean-Pierre Jouannaud

► To cite this version:

Alejandro Díaz-Caro, Gilles Dowek, Jean-Pierre Jouannaud. Proving Termination With CPO –Full Version. 2025. hal-05146299v2

HAL Id: hal-05146299

https://inria.hal.science/hal-05146299v2

Submitted on 11 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Termination

Alejandro Díaz-Caro<fnref n="1" />,<fnref n="2" />, Gilles Dowek<fnref n="3" />,<fnref n="4" />, and Jean-Pierre Jouannaud<fnref n="4" />

**Abstract.** In this paper, we show how to use the computability path ordering for proving termination of complex cut-elimination calculi aiming at providing a basis for quantum computations. A new CPO rule for CPO is introduced which allows to overcome the lack of transitivity of CPO –whose transitive closure is an order while CPO is not.

# 1 Introduction

A popular, effective simplification ordering for proving termination of rewrite rules in a first-order setting is the recursive path ordering (RPO, [Der82]). Its higher-order generalization, the computability path ordering (CPO, [BJR15]) is as effective, but much less popular. In this paper, we show that it can indeed be used in practice to save lots of complex termination arguments. Our examples originate from the work of the first two authors [DCD24,DCD25].

The computability path ordering (CPO) is a well-founded relation over typed lambda terms that compares two terms by comparing their heads first, before recursing on their subterms. As RPO, it uses a precedence on function symbols –including abstraction and application. Since the lambda calculus is non-terminating while its typed versions are terminating, CPO must also include type comparisons. Of course, CPO decreases when beta reducing a term, a rule common to all lambda calculi.

Applying CPO comparisons is easy once the precedence on function symbols and order on types are given, which makes it very easy to use. A difficulty, however, is that CPO is not transitive, hence is not an order, even if we call it CPO. In practice, it is sometimes necessary, when comparing two terms *u*, *v* to invent some *middle term* *w* and compare *u* with *w* and *w* with *v*. We propose an additional CPO rule here that improves transitivity in practice.

# 2 Terms

We use here the language of simply typed λ-terms enriched with a set of function symbols having a fixed arity.

<footnote n="1">¹ Universidad Nacional de Quilmes, Argentina</footnote>

<footnote n="2">² ICC, Universidad de Buenos Aires & CONICET, Argentina
adiazcaro@conicet.gov.ar</footnote>

<footnote n="3">³ Inria, France
gilles.dowek@ens-paris-saclay.fr</footnote>

<footnote n="4">⁴ ENS Paris-Saclay, France
jeanpierre.jouannaud@gmail.com</footnote>
## 3 Types and admissible type orderings

In this section, we first recall the definition of (simple) types. Then, we define the (strict) ordering on types that will be used in CPO.

**Definition 1 (Types)** Let $S$ be a set of sorts. The set $\mathcal{T}$ of types is defined by the following grammar rules:

$$s, t := b \mid c(\bar{t}) \mid s \to t$$

where $b$ belongs to the set of base types and $c$ to the set of type constructors

Given a term $u$, we denote by $\tau(u)$ its type, assumed to uniquely exist.

In order to compare terms in the next section, we will need a specific kind of well-founded order on types, called *admissible* [JR07]. It is shown in [BJR15] that an admissible order on types $>_{\tau}$ can be generated from a well-founded order $>_{S}$ on sorts, as the smallest order on types containing $>_{S}$ that satisfies

1. the right-subterm property: $s \to t >_{\tau} t$;

2. the right-monotonicity property: $s >_{\tau} t$ implies $u \to s >_{\tau} u \to t$.

This order is actually included into any instance of the recursive path ordering for which the precedence contains $>_{S}$, and indeed, RPO itself is an admissible order on types that we will use in our examples.

## 4 The computability path ordering

The absence of infinite derivations in a calculus defined by rewrite rules is in general undecidable.

When the calculus is first-order, the property is usually called *termination*. A standard method for proving termination is to show that its rules decrease in some well-founded rewrite ordering, that is, an order stable under substitution (stability) and context application (monotonicity). Rewrite ordering that satisfy the subterm property, called *simplification orderings* are well-founded [Der82]. A popular simplification ordering is the *recursive path ordering* which compares two terms by comparing their head function symbol in some well-founded ordering on those symbols, called *the precedence*, before to recurse on their subterms.

When the calculus is higher-order, terms that do not originate an infinite derivation are called *strongly normalizing*, and the property that no such term exists is then called *termination* or *strong normalization*. For example, the lambda calculus contains terms that are not strongly normalizing while its typed versions are strongly normalizing. A standard method for proving strong normalization is to build a so called *strongly normalizing model* using Girard's method based on the definition of a *computability predicate*. This method is systematic but quite complex: it necessitates to invent such a predicate characterizing whose terms are strongly normalizing, before to (painfully) prove that all terms belong to the predicate, resulting in strong normalization.
The computability path ordering (CPO) is a well-founded relation over typed lambda terms that generalizes Dershowitz's recursive path ordering (RPO), hence compares two terms by comparing their heads first, before to recurse on their subterms [BJR15]. As RPO, it uses a precedence on function symbols, that now include two specific operators for building our lambda calculus, one for building abstractions written $[x]u$ and one for applications written $@(u, v)$. Since the lambda calculus is non-terminating while its typed versions are terminating, CPO must also include type comparisons for some admissible order on types. Of course, CPO should decrease when beta reducing a term, a rule common to all lambda calculi.

Applying CPO comparisons is easy once the precedence on function symbols and order on types are given, which makes it very easy to use. A difficulty, however, is that CPO is not transitive, hence is not an order. In practice, it is sometimes necessary, when comparing two terms $u, v$ to invent some *middle term* $w$ and compare $u$ with $w$ and $w$ with $v$. Inventing one middle term will always be enough for the calculi that we investigate here. So, Girard's method has been swept under the carpet, it is used once and for all to show that CPO is a well-founded relationship, hence allowing us to check termination by performing (decidable) ordering comparisons. We present next the definition of CPO, restricting ourselves to the comparisons that are necessary to carry out the termination proofs of the calculi we investigate.

## 4.1 Definition of CPO

While the recursive path ordering RPO operates on a term algebra generated from a first-order signature, the computability path ordering CPO operates on a simply typed lambda calculus generated from a higher-order signature. So, the recursive path ordering happens to be the restriction of the computability path ordering to the first-order sub-algebra generated by the first-order sub-signature. As a consequence, there is no need to give a definition of RPO, it will be implicitly given by restricting the computation rules of CPO to the sub-signature.

We assume given:

- a partial ordering on types $>_{\tau}$, function types being strictly bigger than their arguments;

- a quasi-ordering $>_{\mathcal{F}}$ on $\mathcal{F}$, called *precedence*, whose strict part $>_{\mathcal{F}}$ is well-founded, and equivalence is denoted by $\mathcal{=}_{\mathcal{F}}$;

- for every $f \in \mathcal{F}$, a status $stat(f) \in \{\text{lex, mul}\}$ such that symbols equivalent in $\mathcal{=}_{\mathcal{F}}$ have the same status.

**Definition 2 (Computability path relation)** *The computability path relation* $\succcurlyeq^{\mathcal{F}}$ (*for short*) *where*:

- for any given finite set $X$ of variables, $\succcurlyeq^X$ is inductively defined in Figure 1,

- $t \succcurlyeq_{\tau}^X u$ if $t \succcurlyeq^X u$ and $\tau(t) \geq_{\tau} \tau(u)$, also conveniently written in examples $t : \tau(t) \succcurlyeq_{\tau}^X u : \tau(u)$
(F▷) $f(\bar{t}) \succcurlyeq^X v$ if $f \in \mathcal{F}$ and $s \preceq_{\tau}^X v$ for some $s \in \bar{t}$

(F=) $f(\bar{t}) \succcurlyeq^X g(\bar{u})$ if $f \in \mathcal{F}$, $f = \mathcal{F} g$, $(\forall i) f(\bar{t}) \succcurlyeq^X u_i$ and $\bar{t} (\succ_{\tau})_{\text{stat}(f)} \bar{u}$

(F>) $f(\bar{t}) \succcurlyeq^X g(\bar{u})$ if $f \in \mathcal{F}$, $f >_{\mathcal{F}} g$ and $(\forall i) f(\bar{t}) \succcurlyeq^X u_i$

(F@) $f(\bar{t}) \succcurlyeq^X @ (u, v)$ if $f \in \mathcal{F}$, $f(\bar{t}) \succcurlyeq^X u$ and $f(\bar{t}) \succcurlyeq^X v$

(Fλ) $f(\bar{t}) \succcurlyeq^X [y]v$ if $f \in \mathcal{F}$, $f(\bar{t}) \succcurlyeq^X \{z\} v_y^z$, $\tau(y) = \tau(z)$ and $z$ fresh

(FX) $f(\bar{t}) \succcurlyeq^X y$ if $f \in \mathcal{F}$ and $y \in X$

(@▷) @($t, u$) $\succcurlyeq^X v$ if $t \succeq_{\tau}^X v$ or $u \succeq_{\tau}^X \tau v$

(@=) @($t, u$) $\succcurlyeq^X$ @($t'$, $u'$) if $t = t'$ and $u \succcurlyeq^X u'$, or @($t, u$) $\succcurlyeq^X$ $t'$ and @($t, u$) $\succcurlyeq^X$ $u'$ where @($t, u$) $\succcurlyeq^X$ $v$ if $t \succcurlyeq^X v$ or else $u \succeq_{\tau}^X v$ or @($t, u$) $\succcurlyeq^X$ $v$

(@λ) @($t, u$) $\succcurlyeq^X$ $[y]v$ if @($t, u$) $\succcurlyeq^X$ $v_y^z$ and $z$ fresh

(@X) @($t, u$) $\succcurlyeq^X$ $y$ if $y \in X$

(@β) @([x]t, u) $\succcurlyeq^X$ $v$ if $t_x^u \succeq_{\tau}^X v$

(λ▷) $[x]t \succcurlyeq^X v$ if $t_x^z \succeq_{\tau}^X v$, $\tau(x) = \tau(z)$ and $z$ fresh

(λ▷X) $[x]t \succcurlyeq^{X \cup \{z\}} v$ if $t_x^z \succeq_{\tau}^X v$, for some $z \notin (\mathcal{F}\mathcal{V}\mathit{ar}(t) \setminus \mathcal{F}\mathcal{V}\mathit{ar}(v))$ such that $\tau(x) = \tau(z)$

(λ=) $[x]t \succcurlyeq^X [y]v$ if $t_x^z \succcurlyeq^X v_y^z$, $\tau(x) = \tau(y) = \tau(z)$ and $z$ fresh

(λ≠) $[x]t \succcurlyeq^X [y]v$ if $[x]t \succcurlyeq^{X \cup \{z\}} v_y^z$, $\tau(x) \neq \tau(y)$, $\tau(y) = \tau(z)$ and $z$ fresh

(λX) $[x]t \succcurlyeq^X y$ if $y \in X$

(λη) $[x]@ (t, x) \succcurlyeq^X v$ if $t \succeq_{\tau}^X v$ and $x \notin \mathcal{F}\mathcal{V}\mathit{ar}(t)$

<caption>Fig. 1. Core CPO</caption>

The parameter $X$ serves as a meta-level binder to keep track of the variables that were previously bound in the right-hand side but have become free when destructuring a right-hand side abstraction. We shall say that a variable $x$ is fresh with respect to a comparison $u \succcurlyeq^X v$ if $x \notin X \cup \mathcal{F}\mathcal{V}(u, v)$.

Note that the parameter $X$ is carried along computations without change, except in rules ($\mathcal{F}\lambda$) and ($\lambda \neq$) where it increases with a variable which cannot occur in the left-hand side, and in the re-synchronisation rule ($\lambda \vdash X$), where it decreases, hence keeping this property true. Therefore, any comparison $u \succcurlyeq^X v$ generated from an initial comparison $s \succcurlyeq^\emptyset t$ implies $X \cap \mathcal{F}\mathcal{V}ar(u) = \emptyset$. Explicit variable renamings and the associated freshness conditions are used to make the relation invariant by $\alpha$-equivalence and by appropriate renaming of the variables in $X$. Note finally that the condition in rule ($\lambda \vdash X$) is equivalent to $z \in \mathcal{F}\mathcal{V}ar(v)$ or $z \notin (\mathcal{F}\mathcal{V}ar(v) \cup \mathcal{F}\mathcal{V}ar(()))$, hence $z$ fresh.

**Theorem 3 ([BJR15] )** *The computability path ordering $\succcurlyeq^X$ is (i) stable under instantiation, under $\alpha$-conversion and under renaming of the variables in $X$ away from the free variables of the compared terms; and (ii) the computability path ordering $\succcurlyeq^\emptyset$ is monotonic and well-founded.*

*Proof.* The proof given in [BJR15] does not consider rule ($\lambda \vdash X$), which is used here, but was not in previous examples we had to carry out. Monotonicity is an easy property proved by induction on the structure of terms and by inspecting the different cases of the definition. It holds therefore without change since Rule
(λ▷X) cannot be used to reduce a term with ≻$^{∅}$. As for well-foundedness, the proof given in [BJR15] amounts to check strong normalization of all reducts of a term t by ≻$^{∅}$, using a specific computability predicate that needs no modification. By the same token, it holds without change as well. We are left with the renamings and stability. The case of renamings is quite easy, since the new rule does not care about the variables names x and z, but about their types that must be equal. This is similar to the other rules handling abstractions, and the arguments used in [BJR15] for those rules go through as well. As an example, we adapt the proof of a key property used for that purpose:

**Lemma 4** If $t \succcurlyeq^X v$, then $\mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(v) \subseteq \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(t) \cup X$.

*Proof.* By induction on the definition of ≻$^X$, carrying out Case (λ▷X) only. By induction hypothesis, $\mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(v) \subseteq \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(t_x^z) \cup X = (\mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}([x]t) \cup \{z\}) \cup X = \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}([x]t) \cup (X \cup \{z\})$, and we are done.

Stability, on the other hand, is slightly more delicate, it is carried out in Lemma 6.

**Definition 5** We say that a substitution $\sigma$ is away from a set $X$ of variables if $\forall y \in \text{Dom}(\sigma) : \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(\sigma(y)) \cap X = \emptyset$.

**Lemma 6 (Stability)** Assume that $u \succcurlyeq^X v$ and let $\sigma$ be a substitution of domain $\mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(u)$, and away from $X$. Then, $u\sigma \succcurlyeq^X v\sigma$.

*Proof.* We proceed by induction on the definition of ≻$^X$, carrying out Case (λ▷X) only: $[x]t \succcurlyeq^{X \cup \{z\}} v$ if $t_x^z \succcurlyeq^X v$, $z \in \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(v)$ or $z$ fresh and $\tau(x) = \tau(z)$. Let $\sigma$ be a substitution of domain $\mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}([x]t)$ away from $X \cup \{z\}$. Since ≻$^X$ is closed under α-equivalence, we can also assume that $\sigma$ is away from $x$. By induction hypothesis, $t_x^z \sigma \succcurlyeq^{X,z} v\sigma$. Since $\sigma$ is away from $x$, $z$, then $t_x^z \sigma = (t\sigma)_x^z$, hence $(t\sigma)_x^z \succcurlyeq^X v\sigma$. By our assumptions on $v$ and $\sigma$, $z \in \mathcal{F}\mathcal{V}\mathcal{a}\mathcal{r}(v\sigma)$ or $z$ fresh. Therefore, $[x]t\sigma \succcurlyeq^X v\sigma$ by Case (λ▷X). And since $\sigma$ is away from $x$, $([x]t)\sigma = [x](t\sigma)$ and we are done. □

# 5 Using CPO

In the following, we will use CPO to show termination of various rewriting systems built over the following signatures:

1. The set of types is generated from propositional constants $A, B, C, \dots$ and various type constructors $\rightarrow$ (the type constructor of our simply typed lambda calculus), $\Rightarrow, \vee, \wedge, \times, \dots$. Since types don't include variables that can be abstracted over, non-functional types can be considered for CPO as forming an infinite set constants. Types are ordered with the recursive path ordering $>_{\tau}$ generated by the precedence $\Rightarrow>_{\mathcal{F}}\rightarrow$. Remember that RPO is defined by the three rules $(\mathcal{F}\succ)$, $(\mathcal{F}>)$ and $(\mathcal{F}=)$ of CPO. In particular, thanks to $(\mathcal{F}>)$, any type expression is bigger than one of its subexpressions. For example, $A \vee B >_{\tau} A$.
2. The set of terms is generated by a set of term constructors equipped with an arity which dictates the number of their arguments. Following (as already said) the Coq tradition, the lambda calculus abstraction is denoted by square brackets, while $\lambda$ is seen as an operator transforming a term whose type is an arrow into one whose type is a double arrow. The beta reduction rule of the lambda calculus will therefore be $\beta([x]t, u) \rightarrow t_x^u$, where $t_x^u$ represents the term $t$ in which free occurrences of $x$ have been replaced by $u$.

3. The function symbols are declared below with their types. Equivalent presentations in terms of typing rules will be given later, which explain why two different abstractions and applications are needed, the one of the lambda calculus first, and the other one which are function symbols:

<table><tr><td>[x]u : A → B → (A → B)</td><td>%λ-abstraction of Core CPO</td></tr><tr><td>@(u, v) : (A → B) → A → B</td><td>%application of Core CPO</td></tr><tr><td>λ(u) : (A → B) → (A ⇒ B)</td><td>%user abstraction</td></tr><tr><td>u v : (A ⇒ B) → A → B</td><td>%user application</td></tr><tr><td>δ<sup>1</sup> (u, v) : (A ∧ B) → (A → C) → C</td><td></td></tr><tr><td>δ<sup>2</sup> (u, v) : (A ∧ B) → (B → C) → C</td><td></td></tr><tr><td>δ<sub>∀</sub>(u, v, w) : (A ∨ B) → (A → C) → (B → C) → C</td><td></td></tr><tr><td>⟨u, v⟩ : A → B → (A ∧ B)</td><td></td></tr><tr><td>inl(u) : A → A ∨ B</td><td></td></tr><tr><td>inr(u) : B → A ∨ B</td><td></td></tr><tr><td>inlr(u) : A → B → A ∨ B</td><td></td></tr><tr><td>⊕(u, v) : A → A → A</td><td></td></tr></table>

We will assume the following for the signature of function symbols:

- the precedence $\delta_{\vee} >_{\mathcal{F}} \oplus >_{\mathcal{F}} \{\langle, \rangle, \text{inl}, \text{inr}, \text{inlr}\} >_{\mathcal{F}} \lambda$,

- a multiset status for all function symbols,

- the subterm ordering for comparing types.

4. CPO is a well-founded relation, but is not transitive (despite its name). It is however "almost transitive", but may not be in case the second step is the rule $(@\beta)$, that is, a beta-reduction. In that case, we need to exhibit a so-called "middle term" $t$ so as to prove $s \succ u$ by proving $s \succ t$ and $t \succ u$.

# 6 Propositional natural deduction

The typing rules and reduction rules of propositional natural deduction are given Figures 2 and 3.

**Theorem 7** *The rules of Figure 3 terminate.*

*Proof.* We show that left-hand sides are strictly bigger than right-hand sides in CPO. To this end, we choose: for the order on types the recursive path ordering as said, which is well-founded; for the precedence, the empty one; and no status is needed, anyone will do.
The first rule decreases by case ($\mathcal{F} \triangleright$), since $t \succeq_{\tau}^{\varphi} t$.

For the second rule, we have to prove that $\lambda([x]t) u \succ t_x^u$, for which we consider the middle term $@([x]t, u)$ which yields two goals, of which the second $@([x]t, u) \succ t_x^u$ is case ($@\beta$). We are therefore left with the goal ($\succeq$ is enough since we have a strict comparison already):

$\lambda([x]t) u \succeq @([x]t, u)$, which yields two subgoals by case ($\mathcal{F} @$):

1. $\lambda([x]t) u \succ [x]t$, which yields by case ($\mathcal{F} \triangleright$) the subgoal

1.1. $\lambda([x]t) : A \Rightarrow B \succeq_{\tau} [x]t : A \rightarrow B$, for which the type comparison $A \Rightarrow B >_{\tau} A \rightarrow B$ succeeds since $\Rightarrow >_{\mathcal{F}} \Rightarrow$, while the subgoal $\lambda([x]t) \succeq [x]t$ succeeds by ($\mathcal{F} \triangleright$).

2. $\lambda([x]t) u \succ u$, which yields by ($\mathcal{F} \triangleright$)

2.1. $u \succeq_{\tau} u$, which succeeds trivially.

The last four are all similar, using again the middle term $@([x]t, u)$. We carry out the last one:

$\delta_{\vee}(inr(u), [x]v, [y]w) \succ @([y]w, u)$, which yields by ($\mathcal{F} >$):

1. $\delta_{\vee}(inr(u), [x]v, [y]w) \succeq [y]w$, which succeeds by ($\mathcal{F} \triangleright$).

2. $\delta_{\vee}(inr(u), [x]v, [y]w) \succ u$, which yields by ($\mathcal{F} \triangleright$):

2.1. $inr(u) : A \lor B \succeq_{\tau} u : A$, for which the comparison $A \lor B >_{\tau} A$ succeeds as expected, while the subgoal $inr(u) \succeq u$ succeeds by ($\mathcal{F} \triangleright$).

# 7 Adding +

We consider an extension of propositional Natural Deduction with the rule

$$ \frac{\Gamma \vdash A \quad \Gamma \vdash A}{\Gamma \vdash A} \text{ sum} $$

Such a rule can create an interstice between the introduction rule and elimination rule of a connective, introducing new forms of commuting cuts, for example

$$ \frac{\frac{\frac{\pi_1}{\Gamma, A \vdash B} \quad \frac{\pi_2}{\Gamma, A \vdash B}}{\Gamma \vdash A \Rightarrow B} \Rightarrow \mathbf{-i}}{\Gamma \vdash A \Rightarrow B} \Rightarrow \mathbf{i} \quad \text{sum} \quad \frac{\pi_3}{\Gamma \vdash A} \Rightarrow \mathbf{-e} $$

To reduce such a cut, we can commute the sum rule, either with the introduction rules above

$$ \frac{\frac{\pi_1}{\Gamma, A \vdash B} \quad \frac{\pi_2}{\Gamma, A \vdash B}}{\Gamma, A \vdash B} \text{ sum} \quad \frac{\pi_3}{\Gamma \vdash A \Rightarrow B} \Rightarrow \mathbf{-i} \quad \frac{\pi_4}{\Gamma \vdash A \Rightarrow B} \Rightarrow \mathbf{-e} $$
or with the elimination rule below

$$ \frac{\frac{\pi_1}{\Gamma, A \vdash B} \Rightarrow \mathbf{i}}{\Gamma \vdash A \Rightarrow B} \frac{\pi_3}{\Gamma \vdash A} \Rightarrow \mathbf{e}} \frac{\pi_2}{\Gamma, A \vdash B} \Rightarrow \mathbf{i}}{\Gamma \vdash A \Rightarrow B} \frac{\pi_3}{\Gamma \vdash A} \Rightarrow \mathbf{e}} \sum \frac{\pi_3}{\Gamma \vdash A \Rightarrow B} \Rightarrow \mathbf{e}}{\Gamma \vdash B} $$

that both reduce with the usual reduction rules.

Commuting the sum rule with the introduction rules above should be preferred as it yields better properties of the irreducible proofs, in particular a stronger introduction property. But such a commutation is not always possible. In particular, the disjunction has two introduction rules and there seems to be no way to commute the sum rule with the introduction rules in the proof

$$ \frac{\frac{\pi_1}{\Gamma \vdash A} \vee \mathbf{i1}}{\Gamma \vdash A \vee B} \frac{\pi_2}{\Gamma \vdash B} \vee \mathbf{i2}}{\Gamma \vdash A \vee B} \sum $$

Thus, there seems to be no way to reduce the proof

$$ \frac{\frac{\pi_1}{\Gamma \vdash A} \vee \mathbf{i1}}{\Gamma \vdash A \vee B} \frac{\pi_2}{\Gamma \vdash A \vee B} \vee \mathbf{i2}}{\Gamma \vdash A \vee B} \sum \frac{\pi_3}{\Gamma, A \vdash C} \pi_4}{\Gamma, B \vdash C} \vee \mathbf{elim} $$

by commuting the sum rule with the introduction rules.

Thus, we commute the sum rule commutes with the introduction rules when possible, but with the elimination rule of the disjunction.

The typing rules and reduction rules of propositional logic are given Figures 4 and 5.

**Theorem 8** *The rules of Figure 5 terminate.*

*Proof.* Termination proofs using CPO are incremental, we don't need to check again the first six rules since the order on types, precedence and statuses remain the same. Further, we won't detail the type comparisons generated, since they all succeed obviously.

Rule 7 decreases by ($\mathcal{F} \triangleright$). For rule 8, we have the successive comparisons:

$\lambda([x]t) \boldsymbol{+} \lambda([x]u) \succ \lambda([x](t \boldsymbol{+} u))$, which generates a single goal by ($\mathcal{F} >$):

1. $\lambda([x]t) \boldsymbol{+} \lambda([x]u) \succ [x](t \boldsymbol{+} u)$, which yields by ($\mathcal{F} \lambda$) the subgoal

1.1. $\lambda([x]t) \boldsymbol{+} \lambda([x]u) \succ \{z\} t_x^z \boldsymbol{+} u_x^z$, which generates one new goal by ($\mathcal{F}=$), assuming $\boldsymbol{+}$ has a multiset status:

1.1.1.0. $\{\lambda([x]t), \lambda([x]u)\}(\succ_z)_{\tau} \text{mul} \{t_x^z, u_x^z\}$, which reduces to two new similar goals:

1.1.1.1. $\lambda([x]t) : A \Rightarrow B \succeq^z t_x^z : B$. Succeeds by using $@([x]t, z)$ as middle term, with the first comparison $\lambda([x]t) : A \Rightarrow B \succeq^z @([x]t, z)$ which
succeeds by ($\mathcal{F}$>), since the second argument $z$ of the application is smaller than any term by ($\mathcal{F}X$), while the first is smaller by ($\mathcal{F} \triangleright$).

$$1.1.1.2 \lambda([x]u) : A \Rightarrow B \succeq_{\tau}^{z} u_x^z : B. \text{ As above..}$$

We now move to rule 9:

($t, u) \boldsymbol{+} (v, w) \succ (t \boldsymbol{+} v, u \boldsymbol{+} w$), which generates two goals by ($\mathcal{F}$>):

1. ($t, u) \boldsymbol{+} (v, w) \succ t \boldsymbol{+} v$, which generates by ($\mathcal{F}$=):

1.1 ($t, u) : A \wedge B \succ_{\tau} t : A$, which succeeds by ($\mathcal{F} \triangleright$)

1.2 ($t, u) : A \wedge B \succ_{\tau} u : B$, which succeeds similarly by ($\mathcal{F} \triangleright$)

2. ($t, u) \boldsymbol{+} (v, w) \succ u \boldsymbol{+} w$, which succeeds similarly as goal 1.

For rule 10, the last one, we get:

$\delta_{\vee}(t \boldsymbol{+} u, [x]v, [y]w) \succ \delta_{\vee}(t, [x]v, [y]w) \boldsymbol{+} \delta_{\vee}(u, [x]v, [y]w)$:

1. $\delta_{\vee}(t \boldsymbol{+} u, [x]v, [y]w) \succ \delta_{\vee}(t, [x]v, [y]w)$, which yields by case ($\mathcal{F}$=):

1.1 {$t \boldsymbol{+} u, [x]v, [y]w$} ($\succ_{\tau})_{mul}\{t, [x]v, [y]w\}$, which succeeds since, by Case ($\mathcal{F} \triangleright$), $t \boldsymbol{+} u : A \vee B \succ_{\tau} t : A \vee B$, the other two arguments of the multiset being identical.

2 $\delta_{\vee}(t \boldsymbol{+} u, [x]v, [y]w) \succ \delta_{\vee}(u, [x]v, [y]w)$, which succeeds similarly, and we are done. $\square$

# 8 The in-left-right-calculus

We further extend Natural Deduction, to allow the commutation of the sum rule with the introduction rules of the disjunction. To do so, we add a third introduction rule for the disjunction

$$\frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A \vee B} \quad \forall \text{-i3}$$

The typing rules and reduction rules of propositional logic are given Figures 6 and 7.

**Theorem 9** *The rewrite system of Figure 7 terminates.*

*Proof.* We have already proved all rules from (1) to (9) included.

For Rule (11), we need to prove that

$\delta_{\vee}(inlr(t, u), [x]v, [y]w) \succ v_x^t \boldsymbol{+} w_y^u$. Using the middle term $@([x]v, t) \boldsymbol{+} @([y]w, u)$, two goals are generated by ($\mathcal{F}$>):

1. $\delta_{\vee}(inlr(t, u), [x]v, [y]w) \succ @([x]v, t)$, which yields by ($\mathcal{F}$@):

1.1. $\delta_{\vee}(inlr(t, u), [x]v, [y]w) \succ [x]v$, which succeeds by ($\mathcal{F} \triangleright$),

2. $\delta_{\vee}(inlr(t, u), [x]v, [y]w) \succ @([y]w, u)$, which works similarly.

Rule (12) succeeds easily with successively ($\mathcal{F}$>), ($\mathcal{F}$=), and bigsub twice, the generated type comparisons being $A \wedge B \succ_{\tau} A$ and $A \wedge B \succ_{\tau} B$.

Rule (13) succeeds easily with successively ($\mathcal{F}$>), and twice (bigsub twice).

Rule (14) uses the multiset status of $\boldsymbol{+}$:

$inl(t) + inlr(v, w) \succ inlr(t + v, w)$, generates by ($\mathcal{F} \triangleright$):

1. $inl(t) \boldsymbol{+} inlr(v, w) \succ t \boldsymbol{+} v$ which generates by ($\mathcal{F}$=)
This leads to the system described in Figures 8 and 9.

**Theorem 10** *The rewrite system of Figure 9 terminates.*

First, as before, we describe the signature, precedence and statuses needed.

- Signature: there are four sorts: term, type (of which unit is a particular type), and scalar. We use $a, b$ for scalars, $e$ for units, $A, B, C$ for types, and $u, v, w, t$ for terms.

$$ 
\begin{array}{l}
[x]u : A \to B \to (A \to B) \\
@ (u, v) : (A \to B) \to A \to B
\end{array}
$$

$$ 
\begin{array}{l}
a+b : S \to S \to S \\
a \times b : S \to S \to S \\
a \bullet u : S \to A \to A \\
(a) \star : S \to \mathbf{1} \\
\delta_1(e, u) : \mathbf{1} \to A \to A
\end{array}
$$

$$ 
\begin{array}{l}
\star : A \\
u \oplus v : A \to A \to A \\
\lambda([x]u) : A \to B \to (A \to \mathcal{B}) \\
u \vee (A \to \mathcal{B}) \to A \to B \\
inl(u) : A \to (A \oplus B) \\
inr(u) : B \to (A \oplus B) \\
inlr(u) : A \to B \to (A \oplus B) \\
\delta_{\oplus}(u, v, w) : (A \oplus B) \to (A \to C) \to (B \to C) \to C \\
\delta_{\oplus}^{nd}(u, v, w) : (A \oplus B) \to (A \to C) \to (B \to C) \to C
\end{array}
$$

- the precedence: $\delta_1 >_F \bullet >_F \star >_F \times$ and
$\{\delta_\oplus, \delta_\oplus^{nd}\} >_F \oplus >_F \{inl, inr, inlr, \star\} >_F \{+, \times, \lambda\}$,

- a multiset status for all function symbols,

- the recursive path ordering for comparing types, scalars and units being minimal and $\to$ maximal.

*Proof.* Many rules have similar proofs, in which case we prove only one of them.

$\delta_1(a, \star, t) \succ a \bullet t$. By ($\mathcal{F}$).

$\lambda([x]t) u \succ u_x^t$. As for the similar rule number (2) that we already encountered, we use the middle term $@([x]t, u)$, and Rule ($\mathcal{F}$@) to compare $\lambda([x]t) u$ with $@([x]t, u)$.

$\delta_{\oplus}(inl(t), [x]v, [y]w) \succ v_x^t$. Similar.

$\delta_{\oplus}(inr(u), [x]v, [y]w) \succ w_y^u$. Similar.

$\delta_{\oplus}(inlr(t, u), [x]v, [y]w) \succ v_x^t \oplus w_y^u$. Starts with ($\mathcal{F}$), then similar.

$\delta_{\oplus}^{nd}(inl(t), [x]v, [y]w) \succ v_x^t$. Similar.

$\delta_{\oplus}^{nd}(inr(u), [x]v, [y]w) \succ w_y^u$. Similar.

$\delta_{\oplus}^{nd}(inlr(t, u), [x]v, [y]w) \succ v_x^t$. Similar.
$\delta_{\oplus}^{nd}(inlr(t, u), [x]v, [y]w) \succ w_y^u$. Similar.

$a, b, c \succ (a+b), c$. By $(\mathcal{F}>)$ twice, then $(\mathcal{F}\triangleright)$ twice.

$\lambda([x]t) \succ \lambda([x]u) \succ \lambda([x](t \oplus u))$. By $(\mathcal{F}>)$, then $(\mathcal{F}\lambda)$, we get

1. $\lambda([x]t) \succ \lambda([x]u) \succ^z (t \oplus u)_x^z = t_x^z \oplus u_x^z$. By $(\mathcal{F}=)$, we manage to get

$$1.1. \lambda([x]t) \succ^z t_x^z$$

$$1.2. \lambda([x]u) \succ^z u_x^z$$

that can both be proved with the usual middle term trick.

$inl(t) \oplus inl(v) \succ inl(t \oplus v)$. By $(\mathcal{F}>)$, then $(\mathcal{F}=)$, then $(\mathcal{F}\triangleright)$ twice.

$inl(t) \oplus inr(w) \succ inlr(t, w)$. Similar.

$inl(t) \oplus inlr(v, w) \succ inlr(t \oplus v, w)$. Similar.

$inr(u) \oplus inl(v) \succ inlr(v, u)$. Similar.

$inr(u) \oplus inr(w) \succ inr(u \oplus w)$. Similar.

$inr(u) \oplus inlr(v, w) \succ inlr(v, u \oplus w)$. Similar.

$inlr(t, u) \oplus inl(v) \succ inlr(t \oplus v, u)$. Similar.

$inlr(t, u) \oplus inr(w) \succ inlr(t, u \oplus w)$. Similar.

$inlr(t, u) \oplus inlr(v, w) \succ inlr(t \oplus v, u \oplus w)$. Similar.

$a \bullet (b, c) \succ ((a \times b), c)$. By $(\mathcal{F}>)$ twice, then $(\mathcal{F}\triangleright)$ twice.

$a \bullet \lambda([x]t) \succ \lambda([x](a \bullet t))$. By $(\mathcal{F}>)$, we get

1. $a \bullet \lambda([x]t) \succ [x](a \bullet t)$, and by $(\mathcal{F}\lambda)$:

1.1. $a \bullet \lambda([x]t) \succ^z a \bullet t_x^z$. By $(\mathcal{F}=)$, we get:

1.1.1. $\{a, \lambda([x]t)\} \succ_z^t \{a, t_x^z\}$, which reduces to

1.1.1. $\lambda([x]t) \succ_z^t t_x^z$, which suceeds with $@([x]t, z)$ as middle term.

$a \bullet inl(t) \succ inl(a \bullet t)$. By successively $(\mathcal{F}>)$, $(\mathcal{F}=)$ and $(\mathcal{F}\triangleright)$.

$a \bullet inr(t) \succ inr(a \bullet t)$. Similar.

$a \bullet inlr(t, u) \succ inlr(a \bullet t, a \bullet u)$. Similar.

# 10 Discussion

We have not used yet the new rule $(\lambda\triangleright X)$. The reason is that Cynthia Kop showed us we could use the middle term trick instead, which we did. Let us now use the new rule in order to avoid guessing a middle term. We need to prove:

$\lambda([x]t) \succ^z t_x^z$, which yields by $(\mathcal{F}\triangleright)$

$$[x]t \succeq_{\tau}^{z} t_x^z$$

The type of an abstraction being always bigger than that of the abstracted term, the goal becomes

$$[x]t \succeq^{z} t_x^z$$

Assuming now that $z$ occurs in $t_x^z$ (implying that $x$ occurs in $t$), or that $z$ does not occur in $t_x^z$, in which case it does not occur in $t$ either, hence in $[x]t$, we get by $(\lambda\triangleright X)$

$$t_x^z \succeq t_x^z, \text{ which succeeds.}$$

As observed, this new syntax-directed rule improves the transitivity of CPO. It could be used each time here where we used a middle term, making of this little improvement a quite substantial one.
# 11 Conclusion

In many cases, we have used a middle term to overcome the lack of transitivity of CPO. These cases are all similar, their shape is discussed in [BJR15], where a tactic is suggested that would cover our uses of a middle term here. We have also used the new (re-synchronization) rule to carry out the termination proof without using middle terms as discussed in Section 10.

The quantum calculus, whose termination proved here was only conjectured before, is a very interesting example which shows very well indeed both the flexibility and strength of CPO.

The well-foundedness proof of CPO is based on Girard's reducibility candidates, hence its name. It is therefore no wonder that CPO is so efficient to prove termination of sets of rules that describe various forms of cut elimination. CPO is implemented in Wanda [Kop20], and possibly in other termination tools as well. We believe that it should be a must to implement CPO in all termination tools that exist on the market and participate to the termination competition.

CPO accepts a variety of typing disciplines, with the immortant exception of polymorphic types. There is no real reason, though, except lazyness of its authors.

**Acknowledgements:** To Cynthia Kop who suggested the use of a middle term in order to avoid using the re-synchronisation rule.

# References

BJR15. Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. The computability path ordering. *Log. Methods Comput. Sci.*, 11(4), 2015. doi: 10.2168/LMCS-11(4:3)2015.

DCD24. Alejandro Diaz-Caro and Gilles Dowek. A linear lambda calculus. *Mathematical Structures in Computer Science*, 34(10):1103–1133, 2024. doi: 10:1017/S096012952400019.

DCD25. Alejandro Diaz-Caro and Gilles Dowek. A new introduction rule for disjunc-tions. arXiv:2502.19172, 2025. URL: https://archiv.org/abs/2502.19172.

Der82. Nachum Dershowitz. Orderings for term-rewriting systems. *Theor. Comput. Sci.*, 17:279–301, 1982. doi:10.1016/0304-3975(82)90026-3.

JR07. Jean-Pierre Jouannaud and Albert Rubio. Polymorphic higher-order recursive path orderings. *J. ACM*, 54(1):2:1–2:48, 2007. doi:10.1145/1206035.1206037.

Kop20. Cynthia Kop. WANDA - a higher order termination tool (system description). In Zena M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)*, volume 167 of *LIPIcs*, pages 36:1–36:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.36, doi:10.4230/LIPICS.FSCD.2020.36.
<figure><img src="image_2.png" /><figcaption>**Fig. 2.** The typing rules of propositional logic</figcaption></figure>

$$ \delta_{\top}(\star, t) \rightarrow t \qquad (1) $$

$$ \lambda([x]t) u \rightarrow t_x^u \qquad (2) $$

$$ \delta_{\wedge}^{1}(\langle t, u \rangle, [x]v) \rightarrow v_x^t \qquad (3) $$

$$ \delta_{\wedge}^{2}(\langle t, u \rangle, [x]v) \rightarrow v_x^u \qquad (4) $$

$$ \delta_{\vee}(inl(t), [x]v, [y]w) \rightarrow v_x^t \qquad (5) $$

$$ \delta_{\vee}(inr(u), [x]v, [y]w) \rightarrow w_y^u \qquad (6) $$

<figure><img src="image_3.png" /><figcaption>**Fig. 4.** The typing rules of the plus-calculus</figcaption></figure>
$$ \delta_{\top}(\star, t) \rightarrow t \qquad (1) $$

$$ \lambda([x]t) u \rightarrow t_x^u \qquad (2) $$

$$ \delta_{\wedge}^{1}(\langle t, u \rangle, [x]v) \rightarrow v_x^t \qquad (3) $$

$$ \delta_{\wedge}^{2}(\langle t, u \rangle, [x]v) \rightarrow v_x^u \qquad (4) $$

$$ \delta_{\vee}(inl(t), [x]v, [y]w) \rightarrow v_x^t \qquad (5) $$

$$ \delta_{\vee}(inr(u), [x]v, [y]w) \rightarrow w_y^u \qquad (6) $$

$$ \star \star \star \rightarrow \star \qquad (7) $$

$$ \lambda([x]t) \star \lambda([x]u) \rightarrow \lambda([x](t \star u)) \qquad (8) $$

$$ \langle t, u \rangle \star \langle v, w \rangle \rightarrow \langle t \star v, u \star w \rangle \qquad (9) $$

$$ \delta_{\vee}(t \star u, [x]v, [y]w) \rightarrow \delta_{\vee}(t, [x]v, [y]w) \star \delta_{\vee}(u, [x]v, [y]w) \qquad (10) $$

<figure><img src="image_4.png" /><figcaption>Fig. 6. The typing rules of the in-left-right-calculus</figcaption></figure>
$$ \delta_{\top}(\star, t) \rightarrow t \qquad (1) $$

$$ \lambda([x]t) u \rightarrow t_x^u \qquad (2) $$

$$ \delta_{\wedge}^{1}((t, u), [x]v) \rightarrow v_x^t \qquad (3) $$

$$ \delta_{\wedge}^{2}((t, u), [x]v) \rightarrow v_x^u \qquad (4) $$

$$ \delta_{\vee}(inl(t), [x]v, [y]w) \rightarrow v_x^t \qquad (5) $$

$$ \delta_{\vee}(inr(u), [x]v, [y]w) \rightarrow w_y^u \qquad (6) $$

$$ \delta_{\vee}(inlr(t, u), [x]v, [y]w) \rightarrow v_x^t + w_y^u \qquad (11) $$

$$ \star \star \star \rightarrow \star \qquad (7) $$

$$ \lambda([x]t) \star \lambda([x]u) \rightarrow \lambda([x](t \star u)) \qquad (8) $$

$$ \langle t, u \rangle \star \langle v, w \rangle \rightarrow \langle t \star v, u \star w \rangle \qquad (9) $$

$$ inl(t) \star inl(v) \rightarrow inl(t \star v) \qquad (12) $$

$$ inl(t) \star inr(w) \rightarrow inlr(t, w) \qquad (13) $$

$$ inl(t) \star inlr(v, w) \rightarrow inlr(t \star v, w) \qquad (14) $$

$$ inr(u) \star inl(v) \rightarrow inlr(v, u) \qquad (15) $$

$$ inr(u) \star inr(w) \rightarrow inr(u \star w) \qquad (16) $$

$$ inr(u) \star inlr(v, w) \rightarrow inlr(v, u \star w) \qquad (17) $$

$$ inlr(t, u) \star inl(v) \rightarrow inlr(t \star v, u) \qquad (18) $$

$$ inlr(t, u) \star inr(w) \rightarrow inlr(t, u \star w) \qquad (19) $$

$$ inlr(t, u) \star inlr(v, w) \rightarrow inlr(t \star v, u \star w) \qquad (20) $$

<caption>**Fig. 7.** The reduction rules of the in-left-right-calculus</caption>

$$
\begin{array}{ccc}
\begin{array}{c} x : A \vdash x : A \\ \vdash a \star : 1 \end{array} & \begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : A \\ \vdash t \star u : A \end{array} & \begin{array}{c} \text{sum} \\ \Gamma \vdash a \bullet t : A \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : A \\ \vdash t \star u : A \end{array} & \begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : A \\ \vdash t \star u : A \end{array} & \begin{array}{c} \text{sum} \\ \Gamma \vdash a \bullet t : A \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma, x : A \vdash t : B \\ \vdash \lambda([x]t) : A \rightarrow B \end{array} & \begin{array}{c} \Gamma \vdash t : A \rightarrow B \quad \Gamma \vdash u : A \\ \vdash \Delta \vdash \delta_1(t, u) : A \end{array} & \begin{array}{c} \text{sum} \\ \Gamma, \Delta \vdash \delta_1(t, u) : A \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma \vdash t : A \\ \vdash inl(t) : A \oplus B \end{array} & \begin{array}{c} \Gamma \vdash t : A \oplus B \\ \vdash i1 \end{array} & \begin{array}{c} \Gamma \vdash t : B \\ \vdash inr(t) : A \oplus B \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : B \\ \vdash inlr(t, u) : A \oplus B \end{array} & \begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : B \\ \vdash i3 \end{array} & \begin{array}{c} \Gamma \vdash t : A \quad \Gamma \vdash u : B \\ \vdash i3 \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma \vdash t : A \oplus B \quad \Gamma \vdash u : C \\ \vdash \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array} & \begin{array}{c} \Gamma, \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array} & \begin{array}{c} \Gamma, \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array} \\
\text{prod}(a) & & \\
\begin{array}{c} \Gamma \vdash t : A \oplus B \quad \Gamma \vdash u : C \\ \vdash \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array} & \begin{array}{c} \Gamma, \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array} & \begin{array}{c} \Gamma, \Delta \vdash \delta_\oplus(t, [x]u, [y]v) : C \end{array}
\end{array}
$$

<caption>**Fig. 8.** The typing rules of the quantum in-left-right-calculus</caption>
$$
\begin{align*}
\delta_1 (a.^{\star}, t) &\rightarrow a \bullet t \tag{21} \\
\lambda([x]t) u &\rightarrow t_x^u \tag{22} \\
\delta_\oplus (inl(t), [x]v, [y]w) &\rightarrow v_x^t \tag{23} \\
\delta_\oplus (inr(u), [x]v, [y]w) &\rightarrow w_y^u \tag{24} \\
\delta_\oplus (inlr(t, u), [x]v, [y]w) &\rightarrow v_x^t + w_y^u \tag{25} \\
\delta_\oplus^{nd} (inl(t), [x]v, [y]w) &\rightarrow v_x^t \tag{26} \\
\delta_\oplus^{nd} (inr(u), [x]v, [y]w) &\rightarrow w_y^u \tag{27} \\
\delta_\oplus^{nd} (inlr(t, u), [x]v, [y]w) &\rightarrow v_x^t \tag{28} \\
\delta_\oplus^{nd} (inlr(t, u), [x]v, [y]w) &\rightarrow w_y^u \tag{29}
\end{align*}
$$

$$
\begin{align*}
a.^{\star} + b.^{\star} &\rightarrow (a + b).^{\star} \tag{30} \\
\lambda([x]t) + \lambda([x]u) &\rightarrow \lambda([x](t + u)) \tag{31} \\
inl(t) + inl(v) &\rightarrow inl(t + v) \tag{32} \\
inl(t) + inr(w) &\rightarrow inlr(t, w) \tag{33} \\
inl(t) + inlr(v, w) &\rightarrow inlr(t + v, w) \tag{34} \\
inr(u) + inl(v) &\rightarrow inlr(v, u) \tag{35} \\
inr(u) + inr(w) &\rightarrow inr(u + w) \tag{36} \\
inr(u) + inlr(v, w) &\rightarrow inlr(v, u + w) \tag{37} \\
inlr(t, u) + inl(v) &\rightarrow inlr(t + v, u) \tag{38} \\
inlr(t, u) + inr(w) &\rightarrow inlr(t, u + w) \tag{39} \\
inlr(t, u) + inlr(v, w) &\rightarrow inlr(t + v, u + w) \tag{40}
\end{align*}
$$

$$
\begin{align*}
a \bullet b.^{\star} &\rightarrow (a \times b).^{\star} \tag{41} \\
a \bullet \lambda([x]t) &\rightarrow \lambda([x](a \bullet t)) \tag{42} \\
a \bullet inl(t) &\rightarrow inl(a \bullet t) \tag{43} \\
a \bullet inr(t) &\rightarrow inr(a \bullet t) \tag{44} \\
a \bullet inlr(t, u) &\rightarrow inlr(a \bullet t, a \bullet u) \tag{45}
\end{align*}
$$

<caption>Fig. 9. The reduction rules of the quantum in-left-right-calculus</caption>