# Sort-Based Confluence Criteria for Non-Left-Linear
## Higher-Order Rewriting

Thiago Felicissimo, Jean-Pierre Jouannaud

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

To cite this version:

Thiago Felicissimo, Jean-Pierre Jouannaud. Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. 2025. hal-04973508v2

HAL Id: hal-04973508

https://hal.science/hal-04973508v2

Preprint submitted on 28 May 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Sort-Based Confluence Criteria for
Non-Left-Linear Higher-Order Rewriting

Thiago Felicissimo¹[0009-0000-1074-9275] and
Jean-Pierre Jouannaud²[0000-0003-4790-9927]

¹ INRIA, France

thiago.felicissimo@inria.fr

² Université Paris-Saclay, INRIA, Deducteam, Laboratoire de Méthodes Formelles

jeanpierre.jouannaud@gmail.com

**Abstract.** Powerful confluence criteria for higher-order rewriting exist for left-linear systems, even in the presence of critical pairs and non-termination. On the other hand, confluence criteria that allow for mixing non-termination and non-left-linearity are either extremely limited or hardly usable in practice. In this paper, we study confluence criteria which explore sort information to make proving higher-order confluence possible, even in the presence of non-termination and non-left-linearity. We give many interesting examples of systems covered by our results, including a (confluent) variant of Klop's counterexample, and a calculus issuing from a dependent type theory with cumulative universes.

**Keywords:** Higher-Order Rewriting · Left Non-Linear Rules · Confluence.

# 1 Introduction

When proving confluence of higher-order rewrite systems, one generally has to be in one of the following two cases. If the rewrite system being considered is terminating, then by the critical pair criterion it suffices to check that critical pairs are joinable [24]. In most situations this requirement is too restrictive, but if the system is left-linear then many criteria that avoid termination exist, such as orthogonality [20] and development-closedness [26]. If however neither left-linearity nor termination hold, then few criteria allow showing confluence. In such cases, proving confluence can indeed become a subtle problem: as shown by Klop [19], even adding the simple rule $f(\mathcal{X}, \mathcal{X}) \rightarrow a$ to the untyped $\lambda$-calculus destroys its confluence.

In this paper, we propose criteria that leverage sort information to prove confluence of higher-order systems that are neither left-linear nor terminating. To do this, we define the *confined sorts* of a system $\mathcal{R}$ as those that can appear in instantiations of non-linearavariables. Then, assuming that the subsystem $\mathcal{R}_c \subseteq \mathcal{R}$ operating in the confined sorts is confluent, we show how confluence of $\mathcal{R}$ can be established by closing the critical pairs of $\mathcal{R}_{nc} := \mathcal{R} \setminus \mathcal{R}_c$ using *decreasing diagrams* [27]. More precisely, we provide a criterion that assumes termination
<figure><img src="image_3.png" /><figcaption>Fig. 1. Higher-order deduction modulo with natural numbers</figcaption></figure>

of $R_c$ (Theorem 1) and another which does not (Theorem 2), but requires one to consider the more advanced notion of *cyclic critical pairs* [23]. Finally, we also give a combination criterion (Theorem 3), which allows to prove confluence of a non-left-linear system by splitting it into two, such that the *weakly confined* sorts of one does not interfere with the ones of the other.

Our results prove confluence of many interesting examples not covered by any published criterion (but some of them are covered by our previous non-published work [5,8]). These include for instance a confluent variant of Klop's counterexample, given at Figure 1. Very minor changes to it can break its confluence (see Remark 3), showing that establishing this property is a non-trivial matter.

The full proofs of our results are given in the appendix, so as to make the paper more accessible to non-specialists.

## 2 Preliminaries

We work within a formalism of sorted second-order rewriting. This can be seen as Hamana's Second-order Computational Systems [13], simply-typed Combinatory Reduction Systems (CRSs) [20], or Pattern Rewrite Systems (PRSs) [24] with only function symbols of order at most two and variables of order at most one. In particular, this allows us to use criteria developed for any of these formalisms.

*Variables, metavariables and function symbols* Given a set $A$, let $A^*$ be the set of lists of elements in $A$, written $\boldsymbol{a} = a_1, \dots, a_k$, and let $\varepsilon$ be the empty list.

Let $S$ be a set of *sorts*, written $s$, as in multi-sorted first-order logic/rewriting (sorts can also be understood as syntactic classes). We assume we are given:

- An infinite set of variables $x, y, z, \dots \in \mathcal{V}$, each equipped with a sort.

- An infinite set of *metavariables* $X, T, U, \dots \in \mathcal{M}$, each equipped with a (*simple*) *arity*, that is, an element of $S^* \times S$ written as $\{s\}$. Metavariables are referred to by characters in upper-case *typewriter font*, but we may use the letter $e$ for being a variable or meta-variable, indifferently.

- A *signature* $\Sigma$ of *function symbols* $f, g, h \in \mathcal{F}$, each equipped with a *binding* *arity* [11], that is, an element of $(S^* \times S)^* \times S$ written as $(\{s_1\} s'_1, \dots, \{s_k\} s'_k)s$. Function symbols are referred to either by the letters $f, g, h$ or by names in blue serif font, as in the example of Figure 1.

An *arity* $\{s_1, \dots, s_k\}$ indicates that the *metavariable* takes $k$ arguments, each of sort $s_i$, and produces a term of sort $s$. A *binding* *arity* $(\{s_1\} s'_1, \dots, \{s_k\} s'_k)s$
indicates that the symbol takes k arguments, each of sort $s'_i$ and binding variables of sorts $s_i$, and produces a term of sort $s$. We write the assignment of a variable (resp. metastariable or symbol) to its sort (resp. arity or binding arity) as $x : s$ (resp. $\mathcal{X} : \{s\}s$ or $f : (\{s_1\}s'_1, \dots, \{s_k\}s'_k)s$), and often abbreviate $\{\varepsilon\}s$ and $(\varepsilon)s$ as $s$. We assume infinitely many variables and metastariables for each sort and arity. We however consider $\Sigma$ to be variable and chosen by the user, and so we do **not** assume that we have a function symbol for each possible binding arity.

**Terms** The set $\mathcal{T}_s$ of terms of sort $s$ is defined by the following rules. Terms are defined simultaneously with **abstractions**: given a list of variables $\boldsymbol{x} : s$ and a term $t \in \mathcal{T}_{s'}$ we have the abstraction $\boldsymbol{x}.t \in \mathcal{T}_{\{s\}s'}$ of arity $\{s\}s'$. As usual, terms and abstractions are considered modulo $\alpha$-equality. In the following, any definition made for terms is tacitly extended to abstractions $\boldsymbol{x}.t$ by treating the variables $\boldsymbol{x}$ as bound. We can abstract abstractions by taking $\boldsymbol{y}.(\boldsymbol{x}.t) := \boldsymbol{x}\boldsymbol{y}.t$, and an abstraction $\boldsymbol{x}.t$ with $\boldsymbol{x}$ empty is often implicitly coerced to the term $t$.

$$ \frac{x : s}{x \in \mathcal{T}_s} \qquad \frac{\begin{array}{l} \mathcal{X} : \{s_1, \dots, s_k\} s \\ t_i \in \mathcal{T}_{s_i} \quad (i = 1, \dots, k) \end{array}}{\mathcal{X}\{t_1, \dots, t_k\} \in \mathcal{T}_s} \qquad \frac{\begin{array}{l} f : (\{s_1\} s'_1, \dots, \{s_k\} s'_k) s \\ \boldsymbol{x}_i.t_i \in \mathcal{T}_{\{s_i\} s'_i} \quad (i = 1, \dots, k) \end{array}}{f(\boldsymbol{x}_1.t_1, \dots, \boldsymbol{x}_k.t_k) \in \mathcal{T}_s} $$

We write $fv(t)$ for the set of free variables of $t$, $mv(t)$ for its set of metastariables, $mv^l(t)$ for its set of linear metastariables (occurring only once), and $mv^{nl}(t)$ for its non-linear metastariables, defined as $mv^{nl}(t) := mv(t) \setminus mv^l(t)$. A term $t$ is said to be *ground* if $fv(t) = \emptyset$, *meta-free* if $mv(t) = \emptyset$, and *linear* if $mv^{nl}(t) = \emptyset$.

**Substitutions** A substitution $\sigma$ is a set of pairs either of the form $x \mapsto t$ with $x : s$ and $t \in \mathcal{T}_s$, or $\mathcal{X} \mapsto \boldsymbol{x}.t$ with $\mathcal{X} : \{s\}s'$ and $\boldsymbol{x}.t \in \mathcal{T}_{\{s\}s'}$, such that each variable or metastariable appears to the left of $\mapsto$ at most once. The application of a substitution $\sigma$ to a term $t$ or an abstraction $\boldsymbol{x}.t$ is written $t[\sigma]$ or $(\boldsymbol{x}.t)[\sigma]$. The main cases of their definitions are $x[\sigma] := t$ if $x \mapsto t \in \sigma$, $\mathcal{X}\{\boldsymbol{t}\}[\sigma] := u[\boldsymbol{x} \mapsto \boldsymbol{t}[\sigma]]$ if $\mathcal{X} \mapsto \boldsymbol{x}.u \in \sigma$ and $(\boldsymbol{x}.t)[\sigma] := \boldsymbol{x}.t[\sigma]$. As usual, we must rename bound variables to avoid capturing. We define the application of $\sigma$ to another substitution $\tau$, written $\tau[\sigma]$, by applying $\sigma$ point-wise to all entries of $\tau$. We define $\text{dom}(\sigma)$ by: $x \in \text{dom}(\sigma)$ iff $x \mapsto t \in \sigma$ for some $t$, and $\mathcal{X} \in \text{dom}(\sigma)$ iff $\mathcal{X} \mapsto \boldsymbol{x}.t \in \sigma$ for some $\boldsymbol{x}.t$.

**Positions** We define positions $p, q, \dots$ as words over natural numbers, and write $\varepsilon$ for the empty word and $p \cdot q$ for word concatenation. We write $\leq$ for the prefix order and $\leq_{lex}$ for the lexicographic extension of the order on natural numbers. We say that $p, q$ are *parallel* when they are incomparable with respect to $\leq$.

Given a term $t$ or abstraction $\boldsymbol{x}.t$, we write $\mathcal{Pos}(t)$ and $\mathcal{Pos}(\boldsymbol{x}.t)$ for their sets of positions. Given a position $p$ of $t$ or $\boldsymbol{x}.t$, the operations $t|_p$ and $(\boldsymbol{x}.t)|_p$ take the (abstracted) subterm at $p$, whose body is often denoted by $t^p$. These are defined simultaneously by $t|_\varepsilon := t$ and $\mathcal{X}\{\dots, t_i, \dots\}|_{ip} := t_i|_p$ and $f(\dots, \boldsymbol{x}_i.t_i, \dots)|_{ip} := (\boldsymbol{x}_i.t_i)|_p$ and $(\boldsymbol{x}.t)|_p := \boldsymbol{x}.t|_p$. A position $p$ is *functional* if $t|_p = \boldsymbol{x}.t^p$ with $t^p$ headed by a function symbol, and *nested* if, for some $q < p$, we have $t|_q = \boldsymbol{x}.t^q$ with $t^q$ headed by a metastariable (otherwise said, the path from $\varepsilon$ to $p$ in $t$
passes through a *metavariable* at some point). A *metavariable* $\chi$ of $t$ is said to be
*strongly linear* if it is linear and occurs at a non-nested position, and we write
$mv^{sl}(t)$ for the set of such *met variables*, and $mv^{nsl}(t) := mv(t) \setminus mv^{sl}(t)$. Finally,
given $p \in \mathcal{Pos}(t)$ and an abstraction $x.u$ of same arity as $t|_p = x.t^p$, we write
$t\{[x.u]\}_{p}$ for the result of replacing $t^p$ by $u$ in $t$.

Patterns A pattern is an abstraction $x.t$ (written just $t$ if $x = \varepsilon$) such that $fv(t) \subseteq x$ and, for all $p$, if $t|_p = y.X\{u\}$ then $u = y$.<fnref n="3" /> Two patterns $x.t$, $x.u$ are disjoint if $mv(t) \cap mv(u) = \emptyset$. A pattern unification problem is an equation $x.t \stackrel{?}{=} x.u$ where the left- and right-hand sides are disjoint patterns of same arity. A substitution $\sigma$ with $dom(\sigma) = mv(t) \cup mv(u)$ for which $(x.t)[\sigma] = (x.u)[\sigma]$ is called a unifier of $x.t \stackrel{?}{=} x.u$. A unifier $\theta$ is more general than a unifier $\sigma$ if there exists $\tau$ such that $\theta[\tau] = \sigma$. A major property of pattern unification is that it is decidable and, in the positive case, enjoys most-general unifiers (mgus).

Abstract Rewriting Given a binary relation $\to$ over some set $\mathcal{A}$, we write $\stackrel{=}{\to}$ for its reflexive closure, $\longleftarrow$ for its reflexive-transitive closure and $\leftrightarrow$ for its reflexive-symmetric-transitive closure (also called its associated conversion). Given two such relations $\xrightarrow{1}, \xrightarrow{2}$, we write $\xrightarrow{1} \cdot \xrightarrow{2}$ for $\{(a, c) \mid \exists b.a \xrightarrow{1} b \text{ and } b \xrightarrow{2} c\}$. If the relation $\mathbb{R}$ under consideration is not denoted by an arrow, we also employ the notation $\mathbb{R}^*$ for its reflexive-transitive closure.

A binary relation $\to$ is said to be confluent when $\leftarrow\leftarrow \cdot \to\to \subseteq \to\leftarrow \cdot \leftarrow\leftarrow$ and terminating when there is no infinite sequence $a \to a' \to a'' \to \dots$.

An important result about abstract rewriting that will be useful in this paper is van Oostrom’s decreasing diagrams criterion [27]. Suppose some well-founded set of labels $\mathcal{L}$ and a family of binary relations $\mathfrak{F} = \{\xrightarrow{\alpha}\}_{\alpha \in \mathcal{L}}$, all of them over $\mathcal{A}$. We say that family $\mathfrak{F}$ is decreasing if every divergence $\leftarrow\underset{\alpha}{\cdot} \to\underset{\beta}{\cdot}$ is included in a decreasing diagram (DD in short), that is:

$$ \leftarrow\underset{\beta}{\cdot} \to\underset{\alpha}{\cdot} \subseteq \leftarrow\leftarrow\underset{\alpha}{\cdot} \to\underset{\beta}{\cdot} =\underset{\alpha}{\cdot} \to\leftarrow\leftarrow\underset{\beta}{\cdot} $$

where $\underset{<\alpha}{\to}$ denotes $\cup_{\gamma<\alpha} \xrightarrow{\gamma}$ and $\underset{<\alpha}{\to} \cup \underset{<\beta}{\to}$ denotes $\underset{<\alpha}{\to} \cup \underset{<\beta}{\to}$. Van Oostrom’s criterion asserts that, if $\mathfrak{F}$ is decreasing, then the relation $\cup_{\alpha} \underset{\alpha}{\to}$ is confluent [27,17].

Term Rewriting A rewrite rule is a pair $\ell \to r$ whose left-hand side $\ell$ is a pattern not equal to a *metavariable*, and whose right-hand side $r$ is a ground term of same sort as $\ell$, such that $mv(r) \subseteq mv(\ell)$. A *rewrite system* $\mathcal{R}$ is a set of rewrite rules, and we sometimes name its elements using natural numbers $k$, writing $k : \ell \to r$.

Given a term $t$, a rewrite system $\mathcal{R}$ and a position $p \in \mathcal{Pos}(t)$, we say that $t$ rewrites to $u$ with $\mathcal{R}$ at $p$, written $t \xrightarrow{p} u$ (possibly omitting $\mathcal{R}$ and/or $p$), if for some $\sigma$ with $dom(\sigma) = mv(\ell)$, we have $t|_p = x.(\ell[\sigma])$ and $u = t\{[x.(r[\sigma])]\}_{p}$. We

<footnote n="3">³ In most works one only asks $u$ to be a subset of $y$ [22]. To simplify technicalities, here we chose to consider fully extended patterns, for which $u = y$.</footnote>
write $\sigma \to \sigma'$ if $\text{dom}(\sigma) = \text{dom}(\sigma')$ and for some $e \in \text{dom}(\sigma)$ we have $\sigma(e) \to \sigma'(e)$ and that the restrictions of $\sigma, \sigma'$ to $\text{dom}(\sigma) \setminus \{e\}$ are equal. The definitions of confluence and termination are lifted from abstract rewriting to rewrite systems $\mathcal{R}$ by considering the restriction of $\mathcal{R}$ to meta-free terms (eg., $\mathcal{R}$ is confluent if the restriction of $\mathcal{R}$ to meta-free terms is confluent).

## 3 Sort confinement

In this section, we define the concept of sort confinement, a simple powerful idea with roots in [3,5] and which will serve as the basis for our criteria.

**Sort pre-order** We define the sort pre-order $\leq$ in $\mathcal{S}$ by $s \leq s'$ when there is some meta-free $t \in \mathcal{T}_{s'}$ and $p \in \mathcal{P}os(t)$ such that $t|_p = x.t^p$ with $t^p \in \mathcal{T}_s$.

Note that this definition is only interesting because we ask $t$ to be meta-free, otherwise we could just take the term $X\{x\}$ with $x: s$ and $X: \{s\} s'$. For the same reason, this definition would not make sense in higher-order frameworks such as Pattern Rewrite Systems (PRSs) [24], in which one does not make a distinction between variables and VARIABLES. Note also that $\leq$ is a property of the user-specified signature $\Sigma$ alone: it exists independently of any given rewrite system. Finally, it is easy to see that $\leq$ is indeed reflexive and transitive, but not anti-symmetric, and moreover that it is decidable for finite $\Sigma$.

**Confined sorts** Given a rewrite system $\mathcal{R}$, we define its confined sorts to be

$$ \mathcal{S}_c(\mathcal{R}) := \{s \in \mathcal{S} \mid \exists \ell \to r \in \mathcal{R}, X \in \text{mv}^{nl}(\ell) \cup \text{mv}^{nsl}(r), \text{st. } X: \{\dots\} s' \text{ with } s \leq s'\} $$

and we define its confined part $\mathcal{R}_c$ to be the rules in $\mathcal{R}$ with sort in $\mathcal{S}_c(\mathcal{R})$, and its non-confined part to be $\mathcal{R}_{nc} := \mathcal{R} \setminus \mathcal{R}_c$. A meta-free term $t$ is then said to be *confined* if it is of a confined sort. In other words, $\mathcal{S}_c(\mathcal{R})$ isolates the sorts that can appear inside (1) meta-free instances of non-linear VARIABLES or (2) meta-free instances of non-strongly linear VARIABLES or $r$, and $\mathcal{R}_c$ contains exactly the rules from $\mathcal{R}$ that can act on confined terms. This notion of confinement can be weakened by dropping (2), yielding the weakly confined sorts:

$$ \mathcal{S}_{wc}(\mathcal{R}) := \{s \in \mathcal{S} \mid \exists \ell \to r \in \mathcal{R}, X \in \text{mv}^{nl}(\ell), \text{st. } X: \{\dots\} s' \text{ with } s \leq s'\} $$

**Example 1.** Consider the rewrite system $\mathcal{R}$ containing the rules $\Upparrow(\mathcal{N}, \mathcal{N}, X) \to X$ and $@(\lambda(x.T\{x\}), U) \to T\{U\}$, where $@: (\text{tm}, \text{tm})\text{tm}, \lambda: (\{\text{tm}\}\text{tm})\text{tm}$ and $\Upparrow: (\text{nat}, \text{nat}, \text{tm})\text{tm}$. The sort pre-order $\leq$ is given by $\{(\text{nat}, \text{nat}), (\text{nat}, \text{tm}), (\text{tm}, \text{tm})\}$, therefore we obtain $\mathcal{S}_c(\mathcal{R}) = \{\text{nat}, \text{tm}\}$, $\mathcal{R}_c = \mathcal{R}$ and $\mathcal{S}_{wc}(\mathcal{R}) = \{\text{nat}\}$.

In the next sections, we introduce criteria for proving confluence of a system whose confined part $\mathcal{R}_c$ is confluent (Theorems 1 and 2), or to combine two systems such that one does not interfere with the weakly confined sorts of another (Theorem 3). These can then be combined as building blocks for proving confluence of larger systems (as illustrated in Example 11).
## 4 A criterion for when $\mathcal{R}_c$ is terminating

We start with our first and more basic criterion, which requires the confined system $\mathcal{R}_c$ to be terminating. This allows us to start gently, by recalling some preliminary notions such as lifting, overlaps and critical pairs, before moving to more advanced variants of these concepts in Section 5.

Lifting Because a subterm at position $p$ depends on the sequence of variables bound on the path from the root to $p$, one needs to introduce the concept of lifting [24]. Given a fixed list of sorts $s$, let $(-)^*$ be a function that picks for each metavariable $\mathcal{X} : \{s_\mathcal{X}\} s_\mathcal{X}$ a unique metavariable $\mathcal{X}^* : \{s, s_\mathcal{X}\} s_\mathcal{X}$ — formally, we assume one such function for each choice of $s$. Given $\mathbf{x} : s$ and a finite set of variables $M'$, we define the *lifting substitution* $\text{lift}_{\mathbf{x}}$ (omitting $M'$ from the notation) to be the one containing $\mathcal{X} \mapsto \mathbf{y} \cdot \mathcal{X}^*\{\mathbf{x}, \mathbf{y}\}$ for each $\mathcal{X} : \{s_\mathcal{X}\} s_\mathcal{X}$ in $M'$. In the case where $s = \varepsilon$ we assume $(-)^*$ to be the identity, so that $t[\text{lift}_\varepsilon] = t$ for all $t$. Given a substitution $\sigma$ defined over $M'$, we then write $\mathbf{x} \cdot \sigma$ for the abstraction of $\mathbf{x}$ in $\sigma$, which is defined as the substitution containing $\mathcal{X}^* \mapsto \mathbf{x} \cdot \mathbf{y} \cdot t$ for each $\mathcal{X} \mapsto \mathbf{y} \cdot t \in \sigma$. Importantly, we have $\text{lift}_{\mathbf{x}}[\mathbf{x} \cdot \sigma] = \sigma$.

Overlaps and critical pairs Given disjoint patterns $t_1$ and $\mathbf{y} \cdot t_2$, we say that $t_1$ overlaps $\mathbf{y} \cdot t_2$ at $p$ when $p$ is a functional position of $t_2$ and, writing $(\mathbf{y} \cdot t_2)|_p = \mathbf{x} \cdot t_2^p$, the unification problem $\mathbf{x} \cdot t_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x} \cdot t_2^p$ admits a meta-free unifier. Note that, if $\mathbf{x} = \varepsilon$, the problem becomes just $t_1 \stackrel{?}{=} t_2^p$, as lifting with $\varepsilon$ is the identity.

Let $\ell_1 \to r_1$, $\ell_2 \to r_2$ be two rules renamed apart and $p$ a position such that $\ell_1$ overlaps $\ell_2$ at $p$ and, if $p = \varepsilon$, then the rules are not equal up to renaming. In this case, the rules yield the *critical pair* $\langle \ell_2, \{\mathbf{x} \cdot r_1[\text{lift}_{\mathbf{x}}]\}|_p[\theta], r_2[\theta] \rangle$, with $\theta$ the mgu of the problem $\mathbf{x} \cdot \ell_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x} \cdot \ell_2^p$ where $\ell_2|_p = \mathbf{x} \cdot \ell_2^p$.

**Example 2.** Consider the rules $g(\mathcal{Y}, \mathcal{Y}) \to \mathcal{Y}$ and $f(x.g(\mathcal{X}\{x\}, x)) \to \mathcal{X}\{a\}$. The firstlhs overlaps the second at position 1. Indeed, we have $f(x.g(\mathcal{X}\{x\}, x))|_1 = x.g(\mathcal{X}\{x\}, x)$ and $g(\mathcal{Y}, \mathcal{Y})[\text{lift}_{\mathcal{X}}] = g(\mathcal{Y}^*\{x\}, \mathcal{Y}^*\{x\})$, yielding the unification problem $x.g(\mathcal{Y}^*\{x\}, \mathcal{Y}^*\{x\}) \stackrel{?}{=} x.g(\mathcal{X}\{x\}, x)$, which admits the meta-free unifier $\theta = \{\mathcal{X} \mapsto \mathcal{X} \cdot x, \mathcal{Y}^* \mapsto x \cdot \mathcal{X}\}$. This is actually an mgu, so we obtain the critical pair $\langle f(x \cdot \mathcal{X}), a \rangle$.

Rule labeling An important ingredient of our criteria will be the use of *rule labeling* [27,29], a technique for proving confluence of term rewrite systems using decreasing diagrams. However, because in our case we will only need to label non-confined rules, we give an adaptation of the usual definition to our setting.

A labeled rewrite system is a system $\mathcal{R}$ equipped with a well-founded set $\mathcal{L}$ of labels and an assignment of a label for each rule in $\mathcal{R}_{nc}$. If a rule $\ell \to r \in \mathcal{R}_{nc}$ is labelled by $\alpha$, we denote this by writing $\ell \to_{\alpha} r$. Given some $\alpha \in \mathcal{L}$, we define $\mathcal{R}_{\alpha} := \{\ell \to r \mid \ell \to_{\alpha} r \in \mathcal{R}_{nc}\}$, $\mathcal{R}_{<\alpha} := \mathcal{R}_c \cup (\bigcup_{\gamma<\alpha} \mathcal{R}_{\gamma})$ and $\mathcal{R}_{<\alpha, \beta} := \mathcal{R}_{<\alpha} \cup \mathcal{R}_{<\beta}$. Note that the confined rules are always included in $\mathcal{R}_{<\alpha}$, so one can think of them as being labelled by a new bottom element $c$ adjoined to $\mathcal{L}$.
The criterion We are now ready to give our first criterion. In order to simplify notations, we often drop the $\mathcal{R}$ of $\mathcal{R}_{nc}$, $\mathcal{R}_c$, $\mathcal{R}_\alpha$, etc, under an arrow, keeping its subscript, allowing us to write, e.g., $\xrightarrow{c}$ for $\xrightarrow{\mathcal{R}_c}$ or $\xleftarrow{<\alpha}$ for $\xrightarrow{\mathcal{R}_{<\alpha}}$. Moreover, recall that a position $q \in \mathcal{P}os(t)$ is non-nested if the path from $\varepsilon$ to $q$ in $t$ does not pass through a variable — a condition needed in the higher-order setting for the stability of $\xrightarrow{\rightarrow}$ under substitution [9, Proposition 4].

**Theorem 1.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(a) $\mathcal{R}_c$ is confluent and terminating.

(b) For all $\ell \to r \in \mathcal{R}_{nc}$ and $\ell_c \to r_c \in \mathcal{R}_c$, $\ell_c$ does not overlap $\ell$.

(c) If $\langle u_1, u_2 \rangle$ is a critical pair of $\ell_1 \to_{\alpha_1} r_1$, $\ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$u_1 \mathrel{\begin{tikzpicture}[baseline=(current bounding box.center)] \node (U) at (0,0) {$u'_1$}; \node (D) at (0,1) {$u''_1$}; \draw[->] (U) -- (D); \node at (0.5,0.5) {$\xrightarrow{q_1}$}; \node at (0.5,1.5) {$\xrightarrow{q_2}$}; \end{tikzpicture}} \mathrel{\begin{tikzpicture}[baseline=(current bounding box.center)] \node (U) at (0,0) {$u'_1$}; \node (D) at (0,1) {$u''_1$}; \draw[->] (U) -- (D); \node at (0.5,0.5) {$\xrightarrow{q_1}$}; \node at (0.5,1.5) {$\xrightarrow{q_2}$}; \end{tikzpicture}} = u_2 \mathrel{\begin{tikzpicture}[baseline=(current bounding box.center)] \node (U) at (0,0) {$u''_2$}; \node (D) at (0,1) {$u'_2$}; \draw[->] (U) -- (D); \node at (0.5,0.5) {$\xleftarrow{<\alpha_1, \alpha_2}$}; \node at (0.5,1.5) {$\xleftarrow{<\alpha_2}$}; \end{tikzpicture}}$$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.

In (c), recall that $u'_i \xrightarrow{q_i} u''_i$ means either $u'_i = u''_i$ or $u'_i \xrightarrow{q_i} u''_i$, so in the first case we can take $q_i$ to be any position in $u'_i$, and by taking $q_i = \varepsilon$ the non-nesting constraint is trivially verified. Moreover, as can be guessed by its shape, the closing diagram is a DD for some suitable labeling, to be given in Section 7.

**Remark 1.** Note that condition (c) behaves the same for symmetric root critical pairs, in the sense that, if $\ell_1$ and $\ell_2$ each overlap the other one at $\varepsilon$, then the two generated critical pairs $\langle r_1[\theta], r_2[\theta] \rangle$ and $\langle r_2[\theta], r_1[\theta] \rangle$ (where $\theta$ is the mgu of $\ell_1 \stackrel{?}{=} \ell_2$) either both satisfy or do not satisfy (c). Therefore, in such a situation, it suffices to verify the condition for one of the critical pairs.

Let us now see an example of how the criterion can be applied.

**Example 3.** Consider the following example. The symbol Eq checks equality of two lists for a given prefix length. The elements $x.t$ of such lists denote functions $f: \mathbb{N} \to \mathbb{N}$ defined only in terms of zero, successor and addition. The five rules for $+$ ensure that, if $x.t$ and $x.u$ are ground and meta-free, of arity $\{\text{nat}\}\text{nat}$ and represent the same function, then they are convertible, morally justifying why the check provided by Eq is complete. We can then add symbols for generating infinite lists of functions and compare their prefixes. As an example, we add $\Lambda_1$ and $\Lambda_2$ which generate the sequences $f, f^2, f^4, f^8, \dots$ and $f, 2f, 4f, 8f, \dots$.

<table><tr><td>0 : nat</td><td>S : (nat)nat</td><td>+(0, M) → M</td><td>+(S(N), M) → S(+ (N, M))</td></tr><tr><td>+</td><td>(nat, nat)nat</td><td>+(N, 0) → N</td><td>+(N, S(M)) → S(+ (N, M))</td></tr><tr><td>Λ<sub>1</sub>, Λ<sub>2</sub> : ({nat}nat)tm</td><td></td><td>+(N, +(M, P)) → +( (N, M), P)</td><td>Eq(0, X, Y) → T</td></tr><tr><td>cons : ({nat}nat, tm)tm</td><td></td><td>Eq(S(P), cons(x.N{x}, X), cons(x.N{x}, Y)) → Eq(P, X, Y)</td><td></td></tr><tr><td>Eq : (nat, tm, tm)tm</td><td></td><td>Λ<sub>1</sub>(x.N{x}) → cons(x.N{x}, Λ<sub>1</sub>(x.N{N{x}}))</td><td></td></tr><tr><td>T : tm</td><td></td><td>Λ<sub>2</sub>(x.N{x}) → cons(x.N{x}, Λ<sub>2</sub>(x.+(N{x}, N{x})))</td><td></td></tr></table>
Let us now prove confluence using Theorem 1. The only confined sort is nat, so $\mathcal{R}_c$ contains the five rules defining $+$. Using first-order techniques, it is easy to see that $\mathcal{R}_c$ is terminating and confluent, showing (a). Condition (b) is also easily verified and (c) is trivial, given that there are no critical pairs in $\mathcal{R}_{nc}$.

The following example, although covered by first-order techniques [3], illustrates how the choice of the labeling can intervene when applying Theorem 1.

*Example 4.* Considering the following non-terminating system, containing a symmetric equality check for natural numbers.

$$ \begin{array}{lclcl} 0 & : & \mathit{tm} & \quad & \mathit{Eq} \ ; (\mathit{tm}, \mathit{tm})\mathit{prop} & \quad & 1 : \mathit{Eq}(0, \mathit{S}(N)) \to \bot & \quad & 3 : \mathit{Eq}(\mathit{S}(N), 0) \to \bot \\ \mathit{S} \ ; (\mathit{tm})\mathit{tm} & & & \top, \bot & : & \mathit{prop} & \quad & 2 : \mathit{Eq}(\mathit{N}, \mathit{M}) \to \mathit{Eq}(\mathit{M}, \mathit{N}) & \quad & 4 : \mathit{Eq}(\mathit{N}, \mathit{N}) \to \top \end{array} $$

Let us prove its confluence using Theorem 1. The only confined sort is tm and therefore $\mathcal{R}_c$ is empty, so it suffices to check condition (c). We have the following critical pairs (ignoring symmetric counterparts):

- $\langle \mathit{Eq}(0, \mathit{S}(X)), \bot \rangle$ with rules 2 and 3, closes as $\mathit{Eq}(0, \mathit{S}(X)) \xrightarrow{\epsilon} \bot$ with rule 1.

- $\langle \mathit{Eq}(\mathit{S}(X), 0), \bot \rangle$ with rules 2 and 1, closes as $\mathit{Eq}(\mathit{S}(X), 0) \xrightarrow{\epsilon} \bot$ with rule 3.

- $\langle \mathit{Eq}(X, X), \top \rangle$ with rules 2 and 4, closes as $\mathit{Eq}(X, X) \xrightarrow{\epsilon} \top$ with rule 4.

Therefore, we can conclude confluence by labeling rules 1 and 3 the same.

# 5 A criterion for when $\mathcal{R}_c$ is potentially non-terminating

The termination requirement for $\mathcal{R}_c$ in Theorem 1 is unfortunately violated in many examples of interest, such as the one of Figure 1. In this section, we show how this restriction can be dropped at the cost of considering more complex notions of unification, overlaps and critical pairs.

**Linearization** Let us assume for every metavariable $X$ and position $p$, a fresh metavariable $X_p$ uniquely determined by $X$ and $p$. Given a term $t$, we write $\hat{t}$ for the linear term obtained by replacing each occurrence of a non-linear metavariable $X$ at position $p$ by $X_p$. Given $X \in \mathit{mv}(\hat{t})$, define $\tilde{X} \in \mathit{mv}(t)$ by $\tilde{X} := X$ when $X \in \mathit{mv}(t)$, otherwise $X$ is of the form $Y_p$ for some $Y \in \mathit{mv}(t)$ and $p$, so define $\tilde{X} := Y$. Given a substitution $\sigma$ with $\mathit{dom}(\sigma) = \mathit{mv}(\hat{t})$, we say that $\sigma$ is equalized if for every $X, Y \in \mathit{mv}(\hat{t})$ with $\tilde{X} = \tilde{Y}$ we have $\sigma(X) = \sigma(Y)$. When $\sigma$ is equalized, we can define the substitution $\tilde{\sigma} := \{\tilde{X} \mapsto x.u \mid X \mapsto x.u \in \sigma\}$ which satisfies $\hat{t}[\sigma] = t[\tilde{\sigma}]$. Moreover, given $\sigma$ with $\mathit{dom}(\sigma) = \mathit{mv}(\hat{t})$, we write $\sigma^#$ for the substitution of domain $\mathit{mv}(t)$ obtained by sending the linear $X$ to $\sigma(X)$ and the non-linear $X$ to $\sigma(X_p)$ with $p$ being the minimal (for $\leq_{lex}$) position for $X$ in $t$ — hence, we have $\sigma^# = \tilde{\sigma}$ when $\sigma$ is equalized. Intuitively, the $\#$ operator truncates its input substitution so as to obtain a substitution of domain $\mathit{mv}(t)$. Finally, if $\sigma$ is defined over $\mathit{mv}(\hat{t}_1) \cup \mathit{mv}(\hat{t}_2)$ with $\mathit{mv}(t_1) \cap \mathit{mv}(t_2) = \emptyset$, we write $\tilde{\sigma}$ and $\sigma^#$ for $\tilde{\sigma}_1 \cup \tilde{\sigma}_2$ and $\sigma_1^# \cup \sigma_2^#$, where $\sigma_i$ is the restriction of $\sigma$ to $\mathit{mv}(\hat{t}_i)$.
**Example 5.** The linearization of $t = \text{Eq}(\mathcal{X}, \mathcal{X})$ yields the linear pattern $\hat{t} = \text{Eq}(\mathcal{X}_1, \mathcal{X}_2)$. The substitution $\sigma = \{\mathcal{X}_i \mapsto 0\}$ is equalized for $\hat{t}$, and thus $\tilde{\sigma}$ is well-defined and satisfies $\hat{t}[\sigma] = t[\tilde{\sigma}]$ and $\tilde{\sigma} = \sigma^{\#}$. On the order hand, $\tau = \{\mathcal{X}_1 \mapsto 0, \mathcal{X}_2 \mapsto S(0)\}$ is not equalized, hence $\tau^{\#} = \{\mathcal{X} \mapsto 0\}$ but $\tilde{\tau}$ is not well-defined.

**Cyclic unification** Given disjoint patterns $\mathcal{x}.t_1, \mathcal{x}.t_2$ and a rewrite system $\mathcal{R}$, we consider the $\mathcal{R}$-cyclic unification problem $\mathcal{x}.t_1 \stackrel{?}{=} \mathcal{x}.t_2$, whose $\mathcal{R}$-cyclic unifiers are defined as the (syntactic) unifiers $\sigma$ of the linearized problem $\mathcal{x}.\hat{t}_1 \stackrel{?}{=} \mathcal{x}.\hat{t}_2$ that satisfy the condition: for all $\mathcal{X}, \mathcal{Y} \in \text{mv}(\hat{t}_1) \cup \text{mv}(\hat{t}_2)$, if $\tilde{\mathcal{X}} = \tilde{\mathcal{Y}}$ then $\sigma(\mathcal{X}) \leftarrow\stackrel{\mathcal{R}}{\Rightarrow} \sigma(\mathcal{Y})$. The following example motivates the terminology of “cyclic”: this notion of unification allows for solutions which are morally infinite, but represented in a finite way by the rewrite system $\mathcal{R}$.

**Example 6.** Consider the $\mathcal{R}$-cyclic unification problem $\text{Eq}(\mathcal{X}, \mathcal{X}) \stackrel{?}{=} \text{Eq}(\mathcal{Y}, S(\mathcal{Y}))$. Its linearization is $\text{Eq}(\mathcal{X}_1, \mathcal{X}_2) \stackrel{?}{=} \text{Eq}(\mathcal{Y}_1, S(\mathcal{Y}_2))$, which admits the syntactic unifier (actually, mgu) $\theta = \{\mathcal{X}_1 \mapsto \mathcal{Z}_1, \mathcal{X}_2 \mapsto S(\mathcal{Z}_2), \mathcal{Y}_1 \mapsto \mathcal{Z}_1, \mathcal{Y}_2 \mapsto \mathcal{Z}_2\}$. Assuming a term $\infty$ such that $\infty \stackrel{\mathcal{R}}{\Rightarrow} S(\infty)$, we obtain a cyclic unifier with $\sigma := \theta[\mathcal{Z}_i \mapsto \infty]$. Indeed, we then have $\sigma(\mathcal{X}_1) \leftarrow\stackrel{\mathcal{R}}{\Rightarrow} \sigma(\mathcal{X}_2)$ and $\sigma(\mathcal{Y}_1) = \sigma(\mathcal{Y}_2)$.

As suggested by the above example, the set of cyclic unifiers of $\mathcal{x}.t_1 \stackrel{?}{=} \mathcal{x}.t_2$ can be characterized by the mgu of the associated linearized problem $\mathcal{x}.\hat{t}_1 \stackrel{?}{=} \mathcal{x}.\hat{t}_2$. For this, suppose that $\mathcal{x}.\hat{t}_1 \stackrel{?}{=} \mathcal{x}.\hat{t}_2$ admits an mgu $\theta$ and consider the set $C_f$ obtained by simplifying the set of equations $C_0 := \{\theta(\mathcal{X}) \stackrel{?}{=} \theta(\mathcal{Y}) \mid \mathcal{X}, \mathcal{Y} \in \text{dom}(\theta) \text{ with } \tilde{\mathcal{X}} = \tilde{\mathcal{Y}}\}$ until no more possible with the following decomposition rule:

$$ \{\mathcal{x}.f(\mathcal{x}_1.t_1, \dots, \mathcal{x}_k.t_k) \approx \mathcal{x}.f(\mathcal{x}_1.t'_1, \dots, \mathcal{x}_k.t'_k)\} \cup \mathcal{C} \\ \rightsquigarrow \{\mathcal{x}\mathcal{x}_i.t_i \approx \mathcal{x}\mathcal{x}_i.t'_i\}_{i=1,\dots,k} \cup \mathcal{C} $$

We define the associated congruence of $\theta$, denoted $\simeq_{\theta}$ (or just $\simeq$ when $\theta$ is obvious), to be the smallest equivalence relation stable under context containing $t_1[\mathcal{x} \mapsto \mathcal{u}] \simeq t_2[\mathcal{x} \mapsto \mathcal{u}]$ for each $\mathcal{x}.t_1 \approx \mathcal{x}.t_2 \in C_f$ and $\mathcal{u}$ of the appropriate arity. The pair $(\theta, \simeq)$ is then called a description of cyclic unifiers (dcu) for the cyclic unification problem $t_1 \stackrel{?}{=} t_2$. Because mgus are unique up to renaming and $\simeq$ is uniquely determined for each $\theta$, it follows that dcus are unique up to renaming.

**Example 7.** Take the cyclic unification problem $\text{Eq}_3(S(\mathcal{X}), \mathcal{X}, S(\mathcal{Z})) \stackrel{?}{=} \text{Eq}_3(\mathcal{Y}, \mathcal{Y}, \mathcal{Y})$. Its linearization is $\text{Eq}_3(S(\mathcal{X}_{1.1}), \mathcal{X}_2, S(\mathcal{Z})) \stackrel{?}{=} \text{Eq}_3(\mathcal{Y}_1, \mathcal{Y}_2, \mathcal{Y}_3)$, which admits the mgu $\theta = \{\mathcal{X}_{1.1} \mapsto \mathcal{W}_1, \mathcal{X}_2 \mapsto \mathcal{W}_2, \mathcal{Z} \mapsto \mathcal{W}_3, \mathcal{Y}_1 \mapsto S(\mathcal{W}_1), \mathcal{Y}_2 \mapsto \mathcal{W}_2, \mathcal{Y}_3 \mapsto S(\mathcal{W}_3)\}$. The calculation of $C_0$ yields $\{\mathcal{W}_1 \approx \mathcal{W}_2, S(\mathcal{W}_1) \approx \mathcal{W}_2, S(\mathcal{W}_1) \approx S(\mathcal{W}_3), \mathcal{W}_2 \approx S(\mathcal{W}_3)\}$, and by simplifying $S(\mathcal{W}_1) \approx S(\mathcal{W}_3)$ into $\mathcal{W}_1 \approx \mathcal{W}_3$ we obtain $\simeq$ as the congruence generated by $C_f = \{\mathcal{W}_1 \approx \mathcal{W}_2, S(\mathcal{W}_1) \approx \mathcal{W}_2, \mathcal{W}_1 \approx \mathcal{W}_3, \mathcal{W}_2 \approx S(\mathcal{W}_3)\}$. So we have the dcu $(\theta, \simeq)$.

Let us say that $\tau \mathcal{R}$-realizes $\simeq$ if $u_1 \simeq u_2$ implies $u_1[\tau] \leftarrow\stackrel{\mathcal{R}}{\Rightarrow} u_2[\tau]$. The following characterization result justifies the name of “description of solutions”.
**Proposition 1 (Characterization of cyclic unifiers).** Suppose that $\mathcal{R}$ is confluent and that $\mathbf{x}.t_1$, $\mathbf{x}.t_2$ are disjoint patterns such that, for all $\ell \to r \in \mathcal{R}$, $\ell$ does not overlap $\mathbf{x}.\hat{t}_i$. If $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$ admits an $\mathcal{R}$-cyclic unifier, then it admits a dcu $(\theta, \simeq)$. Moreover, a meta-free $\sigma$ with $\text{dom}(\sigma) = \text{mv}(\hat{t}_1, \hat{t}_2)$ is an $\mathcal{R}$-cyclic unifier of $t_1 \stackrel{?}{=} t_2$ iff there is a meta-free $\tau$ that $\mathcal{R}$-realizes $\simeq$ and satisfies $\sigma = \theta[\tau]$.

**Cyclic overlap** The definition of cyclic overlaps is then obtained by directly adapting the standard one. Given patterns $t_1$ and $\mathbf{y}.t_2$ with disjoint sets of metavariables, we say that $t_1 \mathcal{R}$-cyclicly overlaps $\mathbf{y}.t_2$ at $p$ if $p$ is a functional position of $t_2$ and, writing $(\mathbf{y}.t_2)|_p = \mathbf{x}.t_2^p$, the cyclic unification problem $\mathbf{x}.t_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.t_2^p$ admits some meta-free $\mathcal{R}$-cyclic unifier.

**Remark 2.** As a consequence of Proposition 1, if $\mathbf{x}.t_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.t_2^p$ admits a dcu $(\theta, \simeq)$ such that no meta-free $\tau$ realizes $\simeq$, then $t_1$ does not cyclicly overlap $\mathbf{y}.t_2$ at $p$, a reasoning which is often useful to rule out the existence of a cyclic overlap.

Let $\ell_1 \to r_1$, $\ell_2 \to r_2$ be two rules renamed apart and $p$ a position such that $\ell_1 \mathcal{R}$-cyclicly overlaps $\ell_2$ at $p$ and, if $p = \varepsilon$, then the rules are not equal up to renaming. We then have the $\mathcal{R}$-cyclic critical pair $\langle \ell_2[\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]]|_p[\theta^{\#}], r_2[\theta^{\#}], \simeq \rangle$ with $(\theta, \simeq)$ a dcu for $\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.\ell_2^p$ where $\ell_2|_p = \mathbf{x}.\ell_2^p$ (note that a dcu must exist, by Proposition 1). As can be seen, the truncation operator $\#^p$ is used to get a substitution $\theta^{\#}^p$ defined over $\text{mv}(\ell_1[\text{lift}_{\mathbf{x}}]) \cup \text{mv}(\ell_2^p)$ from $\theta$. One might think that we are losing information doing this, however this is compensated by the fact that we also store $\simeq$, which will be used for joining critical pairs.

**Example 8.** Looking at Example 9 and taking $\mathcal{R}$ to contain only rule 4, it is easy to see that thelhs of rule 1 $\mathcal{R}$-cyclicly overlaps the rhs of rule 2 at $\varepsilon$. Their left-hand sides admit the dcu $(\theta, \simeq)$ given in Example 7, which yields $\theta^{\#} = \{\mathbf{X} \mapsto \mathbf{W}_1, \mathbf{Z} \mapsto \mathbf{W}_3, \mathbf{Y} \mapsto \mathbf{S}(\mathbf{W}_1)\}$. Therefore, this overlap yields the cyclic critical pair $\langle \text{Eq}_3(\mathbf{S}(\mathbf{W}_1), \mathbf{W}_1, \mathbf{W}_3), \top, \simeq \rangle$.

**The criterion** We are now finally ready to state our result. In its statement, we write $\leftarrow\leftarrow_{\simeq;\mathcal{R}}$ for the reflexive-symmetric-transitive closure of $\mathcal{R} \to \simeq$.

**Theorem 2.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(a) $\mathcal{R}_c$ is confluent.

(b) For all $\ell \to r \in \mathcal{R}_{nc}$ and $\ell_c \to r_c \in \mathcal{R}_c$, $\ell_c$ does not overlap $\ell_c$.

(c) If $\langle u_1, u_2, \simeq \rangle$ is an $\mathcal{R}_c$-cyclic critical pair of $\ell_1 \to_{\alpha_1} r_1$, $\ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$u_1 \leftarrow\leftarrow_{\simeq;\langle\alpha_1\rangle} u'_1 \xrightarrow{\alpha_2} u''_1 \leftarrow\leftarrow_{\simeq;\langle\alpha_1,\alpha_2\rangle} u''_2 \xrightarrow{\alpha_1} u'_2 \leftarrow\leftarrow_{\simeq;\langle\alpha_2\rangle} u_2$$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.
This criterion looks very similar to Theorem 1, with the crucial difference that we do not require termination of $\mathcal{R}_c$ anymore. In order to compensate this, we now need to consider $\mathcal{R}_c$-cyclic critical pairs in (c) and, as explained previously, we can employ the congruence $\simeq$ for closing them. Moreover, we have also strengthened the second assumption, by requiring that left-hand sides in $\mathcal{R}_c$ do not overlap the linearized left-hand sides in $\mathcal{R}_{nc}$ — see Remark 4 for why this stronger assumption is needed. Finally, note that Remark 1 still holds for this second criterion. Let us now see how the criterion can be applied.

*Example 9.* Consider the following toy example equipped with any labeling, and let us show its confluence using Theorem 2.

<table><tr><td>0, ∞ : tm</td><td>1 : Eq<sub>3</sub>(S(X), X, S(Z)) → Eq<sub>3</sub>(S(X), X, Z)</td></tr><tr><td>S : (tm)tm</td><td>2 : Eq<sub>3</sub>(Y, Y, Y) → ⊤</td></tr><tr><td>Eq<sub>3</sub> : (tm, tm, tm)prop</td><td>3 : Eq<sub>3</sub>(S(V), 0, V) → ⊥</td></tr><tr><td>⊤, ⊥ : prop</td><td>4 : ∞ → S(∞)</td></tr></table>

The only confined sort is tm, hence $\mathcal{R}_c = \{\infty \to S(\infty)\}$, which is confluent by orthogonality, showing (a). Condition (b) is easily verified. For (c) we need to check cyclic critical pairs between 1 and 2, 1 and 3, and 2 and 3. For 1 and 2, we have $\langle \mathrm{Eq}_3(\mathrm{S}(\mathrm{W}_1), \mathrm{W}_1, \mathrm{W}_3), \top, \simeq \rangle$, given in Example 8, and its symmetric counterpart — which, as explained in Remark 1, we do not need to consider. It can be closed with the diagram $\mathrm{Eq}_3(\mathrm{S}(\mathrm{W}_1), \mathrm{W}_1, \mathrm{W}_3) \simeq \mathrm{Eq}_3(\mathrm{W}_1, \mathrm{W}_1, \mathrm{W}_1) \xrightarrow{\epsilon} \top$ and $\epsilon$ is trivially non-nested. Regarding cyclic critical pairs between 1 and 3 and between 2 and 3, their cyclic unification problems each admit a dcu $(\theta, \simeq)$ whose congruence $\simeq$ identifies 0 and $S(t)$ for some $t$. Yet, no meta-free $\tau$ realizes $\simeq$ given that, by confluence of $\mathcal{R}_c$, $0[\tau] \longleftrightarrow_c S(t)[\tau]$ is impossible. So, by Remark 2, they do not cyclicly overlap.

This example already shows the strength of our criterion even for the first-order fragment. Indeed, none of the major first-order confluence checkers (CSI [25], ACP [4], etc) are able to prove its confluence — for this experiment, we used the above system without sorts as, by persistency of first-order confluence [2], it is confluent without sorts iff it is confluent with sorts. More generally, we are not aware of any criterion that is able to show its confluence, apart from ours. For our next example, let us see a confluent variant of Klop’s counterexample.

*Example 10.* Consider the system of Figure 1 equipped with any labeling, and let us show its confluence using Theorem 2. Once again, the only confined sort is tm, hence $\mathcal{R}_c$ contains only the $\beta$-rule, which is confluent by orthogonality, showing (a). Condition (b) is again easily verified. For (c), we only have a cyclic critical pair $\langle \mathrm{Eq}(\mathrm{W}_1, \mathrm{W}_2), \top, \simeq \rangle$ (and its symmetric counterpart), with $\simeq$ satisfying $\mathrm{W}_1 \simeq \mathrm{W}_2$, which can be closed with the diagram $\mathrm{Eq}(\mathrm{W}_1, \mathrm{W}_2) \simeq \mathrm{Eq}(\mathrm{W}_1, \mathrm{W}_1) \xrightarrow{\epsilon} \top$.

*Remark 3.* Consider the system obtained by adding $\mathrm{Eq}(S(M), M) \to \bot$ to Figure 1. This extension breaks confluence, as now we can reproduce Huet’s counterexample [16], by defining $\infty$ with the fixpoint combinator of the untyped $\lambda$-calculus:

$$ \top \leftarrow \mathrm{Eq}(\infty, \infty) \longrightarrow \mathrm{Eq}(S(\infty), \infty) \longrightarrow \bot $$
Note that the plain critical pairs of $\mathcal{R}_{nc}$ still satisfy condition (c) of Theorem 1, so this also shows why considering plain critical pairs instead of cyclic ones in condition (c) of Theorem 2 would not be enough.

Confluence can however be restored by removing the $\beta$-rule: indeed, without $\beta$, Eq(N, N) does not cyclicly overlap Eq(S(M), M), given that the congruence $\simeq$ of their dcu satisfies $W_1 \simeq S(W_1)$, which is not realizable anymore.

Finally, changing in Figure 1 the sorts of Eq, $\top$, $\bot$ to tm also breaks confluence, as we can then reproduce Klop's counterexample.

**Remark 4.** Unlike with Theorem 1, for Theorem 2 it is not sufficient to consider in (b) only overlaps with non-linearized rhs of $\mathcal{R}_{nc}$. Indeed, consider the rules $\infty \to S(\infty)$, $\max(X, X) \to X$ and Eq($\max(S(X), X), X) \to \bot$, where $\infty : \text{tm}$, $\max : (\text{tm}, \text{tm})\text{tm}$, Eq : $(\text{tm}, \text{tm})\text{prop}$ and $\bot : \text{prop}$. The confined part $\mathcal{R}_c$ contains the rules for $\infty$ and $\max$, and can be shown confluent by [18, Theorem 2] (actually, $\mathcal{R}_c$ is a variant of [18, Example 9]), proving (a). Condition (c) is trivially satisfied, as there are no cyclic overlaps in $\mathcal{R}_{nc}$. Finally, neither $\infty$ nor $\max(X, X)$ overlaps Eq($\max(S(X), X), X)$. Yet, confluence fails, given that

$$ \bot \leftarrow \text{Eq}(\max(S(\infty), \infty), \infty) \to \text{Eq}(\max(S(\infty), S(\infty)), \infty) \to \text{Eq}(S(\infty), \infty) $$

and Eq($S(\infty), \infty$) does not reduce to $\bot$. Of course, if we remove the rule $\infty \to S(\infty)$ then $\mathcal{R}_c$ becomes terminating, so we obtain confluence using Theorem 1.

# 6 A combination criterion

We have seen how Theorems 1 and 2 can be applied to show the confluence of systems for which no other published criterion was available before. Nevertheless, it is often useful to split the system under consideration in two so as to allow the application of two different criteria, each one fitting the fragment under choice. To this end, we provide the following combination criterion. Here, given a set of sorts $S' \subseteq S$, we write $\mathcal{R}|_{S'}$ for the set of rules of $\mathcal{R}$ whose sort is in $S'$.

**Theorem 3.** Let $\mathcal{R}_1, \mathcal{R}_2$ be (non-necessarily disjoint) rewrite systems such that:

(1) $\mathcal{R}_1$ and $\mathcal{R}_2$ are both confluent.

(2) $\mathcal{R}_2|_{S_{wc}(\mathcal{R}_1)} = \mathcal{R}_1|_{S_{wc}(\mathcal{R}_2)} = \emptyset$.

(3) There are no critical pairs between rules of $\mathcal{R}_1$ and $\mathcal{R}_2$.

Then $\mathcal{R}_1 \cup \mathcal{R}_2$ is confluent.

So, to split a system $\mathcal{R}$ into $\mathcal{R}_1 \cup \mathcal{R}_2$, we must ensure that (3) no critical pairs exist between them, and (2) that one cannot operate on the weakly confined sorts of the other. If these conditions are satisfied, then it suffices to show confluence of each system separately. Let us now see how this can be applied.

**Example 11.** Consider an extension of Example 10 with the following rules (from [24]), adding connectives and rules for computing the negation normal form.
$$ \neg : (\mathbf{prop})\mathbf{prop} \qquad \neg(\neg(X)) \rightarrow X $$

$$ \vee, \wedge : (\mathbf{prop}, \mathbf{prop})\mathbf{prop} \qquad \neg(\wedge(X, Y)) \rightarrow \vee(\neg(X), \neg(Y)) \qquad \neg(\forall(x.X\{x\}) \rightarrow \exists(x.\neg(X\{x\})) $$

$$ \exists, \forall : (\{\mathbf{tm}\})\mathbf{prop})\mathbf{prop} \qquad \neg(\vee(X, Y)) \rightarrow \wedge(\neg(X), \neg(Y)) \qquad \neg(\exists(x.X\{x\}) \rightarrow \forall(x.\neg(X\{x\})) $$

If we now try to apply Theorem 2 we realize that no labeling satisfying condition (c) can be found. Instead, we can apply Theorem 3 to split the rewrite system into $R_1 \cup R_2$, where $R_1$ is the set of rules of Example 10 and $R_2$ the set of rules given above. Indeed, it is easy to see that there are no critical pairs between $R_1$ and $R_2$, and moreover we have $S_{wc}(R_1) = \{\mathbf{tm}\}$ and $S_{wc}(R_2) = \emptyset$ and thus $R_2|_{S_{wc}(R_1)} = R_1|_{S_{wc}(R_2)} = \emptyset$. To conclude, it thus suffices to show that $R_1$ and $R_2$ are both confluent. In Example 10 we have already shown $R_1$ to be confluent when considering a smaller signature, and it is easy to see that the added connectives do not change the sort pre-order, hence the argument given in Example 10 is still valid. For the confluence of $R_2$, we can exploit its termination to conclude confluence by closing the critical pairs — see [24, Example 4.9].

**Example 12.** The following system (taken from [8]) contains a fragment of the rewrite rules for defining dependent type theory with cumulative Tarski-style universes. Here, we write $\hat{\uparrow}_t^u(v)$ for $\hat{\uparrow}(t, u, v)$ and $\Pi_t(u, x.v)$ for $\Pi(t, u, x.v)$.

$$ 0 : \mathbf{nat} \qquad \max : (\mathbf{nat}, \mathbf{nat})\mathbf{nat} \qquad \max(0, Y) \rightarrow Y \qquad \hat{\uparrow}_X^X(T) \rightarrow T $$

$$ S : (\mathbf{nat})\mathbf{nat} \qquad \hat{\uparrow} : (\mathbf{nat}, \mathbf{nat}, \mathbf{tm})\mathbf{tm} \qquad \max(X, 0) \rightarrow X \qquad \hat{\uparrow}_Y^Y(\hat{\uparrow}_X^X(T)) \rightarrow \hat{\uparrow}_X^Z(T) $$

$$ \Pi : (\mathbf{nat}, \mathbf{tm}, \{\mathbf{tm}\})\mathbf{tm}\mathbf{tm} \qquad \max(S(X), S(Y)) \rightarrow S(\max(X, Y)) $$

$$ @ : (\mathbf{tm}, \mathbf{tm})\mathbf{tm} \qquad \hat{\uparrow}_X^Y(\Pi_X(A, x.B\{x\})) \rightarrow \Pi_Y(\hat{\uparrow}_X^Y(A), x.\hat{\uparrow}_X^Y(B\{x\})) $$

$$ \lambda : (\{\mathbf{tm}\})\mathbf{tm}\mathbf{tm} \qquad @ (\lambda(x.T\{x\}), U) \rightarrow T\{U} $$

Let us show confluence with Theorem 3. For this, take $R_2$ containing only the $\beta$-rule and $R_1$ containing the other rules. Confluence of $R_2$ follows by orthogonality, and confluence of $R_1$ follows because all critical pairs close and the system is terminating. We also have $R_1|_{S_{wc}(R_2)} = R_1|_{\emptyset} = \emptyset$ and $R_2|_{S_{wc}(R_1)} = R_2|_{\{\mathbf{nat}\}} = \emptyset$, and we can directly verify that there are no critical pairs between $R_1$ and $R_2$. Therefore, we can conclude confluence of $R_1 \cup R_2$.

**Remark 5.** In the above example, note that the metavariable $U$ of sort $\mathbf{tm}$ occurs nested in the right-hand side of the $\beta$-rule. Therefore, the sort $\mathbf{tm}$, which is not weakly confined, is confined. This shows the benefit of considering weakly confined sorts in Theorem 3, otherwise condition (2) would not be satisfied.

**Example 13.** Consider the following extension of System F with an operator allowing to cast a term of type $A$ to any other type $A'$, along with a rewrite rule for eliminating identity casts. As shown by Girard in his PhD thesis [12], this system is non-normalizing even when considering only well-typed System F terms. Nevertheless, we can prove it to be confluent on all terms using Theorem 3.

$$ @ : (\mathbf{tm}, \mathbf{tm})\mathbf{tm} \qquad \lambda : (\{\mathbf{tm}\})\mathbf{tm}\mathbf{tm} \qquad @ (\lambda(x.T\{x\}), U) \rightarrow T\{U} $$

$$ \mathbf{inst} : (\mathbf{tm}, \mathbf{ty})\mathbf{tm} \qquad \mathcal{A} : (\{\mathbf{ty}\})\mathbf{tm}\mathbf{tm} \qquad \mathbf{inst}(\mathcal{A}(x.T\{x\}), A) \rightarrow T\{A} $$

$$ \rightarrow : (\mathbf{ty}, \mathbf{ty})\mathbf{ty} \qquad \forall : (\{\mathbf{ty}\})\mathbf{ty}\mathbf{ty} \qquad \mathbf{cast} : (\mathbf{ty}, \mathbf{ty}, \mathbf{tm})\mathbf{tm} \qquad \mathbf{cast}(A, A, T) \rightarrow T $$
Let us take $\mathcal{R}_1$ containing the two $\beta$-rules, and $\mathcal{R}_2$ containing the rule for cast. The system $\mathcal{R}_1$ is confluent by orthogonality, and $\mathcal{R}_2$ is confluent by the critical pair criterion, since it is terminating and has no critical pairs. We also have $\mathcal{R}_1|_{S_{wc}(\mathcal{R}_2)} = \mathcal{R}_1|_{\{ty\}} = \emptyset$ and $\mathcal{R}_2|_{S_{wc}(\mathcal{R}_1)} = \mathcal{R}_2|_{\emptyset} = \emptyset$, and there are no critical pairs between $\mathcal{R}_1$ and $\mathcal{R}_2$. We thus conclude confluence of $\mathcal{R}_1 \cup \mathcal{R}_2$.

**Proof idea** We now discuss informally how we prove **Theorem 3** — the full proof can be found in the appendix. Recall that Hindley-Rosen's lemma states that the union of two relations $\xrightarrow{1}, \xrightarrow{2}$ is confluent whenever each $\xrightarrow{i}$ is confluent and the two commute (that is, when $\xleftarrow{1} \cdot \xrightarrow{2} \subseteq \xleftarrow{2} \cdot \xrightarrow{1}$). Because of condition (1), to show confluence of $\mathcal{R}_1 \cup \mathcal{R}_2$ it therefore suffices to prove that $\xrightarrow{\mathcal{R}_1}$ and $\xrightarrow{\mathcal{R}_2}$ commute on meta-free terms (recall that we only show confluence for meta-free terms). This can be established by adapting the well-known technique of showing that orthogonal rewriting $\Rightarrow$ (also called simultaneous or multi-step rewriting) satisfies the diamond property, a technique notably found in proofs of confluence by orthogonality [6]. Indeed, because $\xrightarrow{\mathcal{R}_i} \subseteq \xrightarrow{\mathcal{R}_i} \subseteq \xrightarrow{\mathcal{R}_i}$, we have that $\xrightarrow{\mathcal{R}_i} \text{ and } \xrightarrow{\mathcal{R}_i}^* \text{ are equal, so to show that } \mathcal{R}_1 \text{ and } \mathcal{R}_2 \text{ commute we can instead show } \xleftarrow{\mathcal{R}_1} \cdot \xrightarrow{\mathcal{R}_1} \subseteq \xrightarrow{\mathcal{R}_2} \cdot \xleftarrow{\mathcal{R}_2} \text{ on meta-free terms, a result analogous to the diamond property but when mixing different rewrite systems.}$

The proof of the above result then relies on the following key property: if $t \stackrel{\cdot}{\Rightarrow} t'$ then the $\mathcal{R}_2$ redexes in $t$ are never destroyed (and vice versa for $t \stackrel{\cdot}{\Rightarrow} t'$). To ensure this in the left-linear case, it is sufficient to ask for absence of critical pairs (condition (3)). However, in the non-left-linear case, a redex can also be destroyed by changing the value of non-linear occurrences of the same metamariable: for instance, if $f(\mathbf{x}, \mathbf{x}) \to \mathbf{x} \in \mathcal{R}_1$ and $a \to b \in \mathcal{R}_2$, then the reduction $f(a, a) \stackrel{\cdot}{\Rightarrow} f(a, b)$ destroys the redex $f(\mathbf{x}, \mathbf{x})[\mathbf{x} \mapsto a]$. This problem is ruled out by condition (2), which ensures that a rule from $\mathcal{R}_1$ cannot operate inside meta-free instances of non-left-linear metamariables of $\mathcal{R}_2$, and vice versa. Therefore, conditions (2) and (3) combined allow us to show $\xleftarrow{\mathcal{R}_1} \cdot \xRightarrow{\mathcal{R}_2} \subseteq \xRightarrow{\mathcal{R}_2} \cdot \xleftarrow{\mathcal{R}_1}$ on meta-free terms, and thus conclude the proof of **Theorem 3**.

# 7 Proof idea for Theorems 1 and 2

We now explain the idea of the proofs for **Theorems 1 and 2** — the full proofs appear in the appendix. It turns out that their proofs can be factored out by instead proving a unifying theorem (**Theorem 4**) which is then shown to imply **Theorems 1 and 2**. To state it, we first recall the notion of *R*-critical pairs.

Given a rewrite system $\mathcal{R}$ and two patterns $\mathbf{x}.t$ and $\mathbf{x}.u$ of same arity, an *R*-unification problem is a pair $\mathbf{x}.t \stackrel{?}{=} \mathbf{x}.u$, and an *R*-unifier for it is a substitution $\sigma$ with $\text{dom}(\sigma) = \text{mv}(t_1) \cup \text{mv}(t_2)$ and $(\mathbf{x}.t)[\sigma] \xleftarrow{\mathcal{R}} (\mathbf{x}.u)[\sigma]$. Given patterns $t_1$ and $\mathbf{y}.t_2$ with disjoint sets of metamariables, we then say that $t_1 \mathcal{R}$-overlaps $\mathbf{y}.t_2$.
at $p$ if $p$ is a functional position of $t_2$ and, writing $(\mathbf{y}.t_2)|_p = \mathbf{x}.t_2^p$, the unification problem $\mathbf{x}.t_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.t_2^p$ admits some meta-free $\mathcal{R}$-unifier. Finally, given two rules $\ell_1 \to r_1$, $\ell_2 \to r_2$ renamed apart and a position $p$ such that $\ell_1 \in \mathcal{R}$-overlaps $\ell_2$ at $p$, we have the $\mathcal{R}$-critical pair $\langle \ell_2, \{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}|_p[\sigma], r_2[\sigma] \rangle$ for each meta-free $\mathcal{R}$-unifier $\sigma$ of the associated $\mathcal{R}$-unification problem. Note that, compared with the previous notions of overlap, we do not discard the case $p = \varepsilon$ when the rules are the same. Moreover, we do not use mgus or dcus to capture critical pairs in a finite way: for each overlap, we have potentially infinitely many critical pairs, one for every meta-free unifier $\sigma$. We can now state the unifying theorem:

**Theorem 4.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(i) $\mathcal{R}_c$ is confluent.

(ii) If $t \stackrel{c}{\rightleftharpoons} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and $t, \sigma$ both meta-free with $\text{dom}(\sigma) = \text{mv}(\ell)$, then $t \stackrel{c}{\rightleftharpoons} \ell[\sigma']$ for some $\sigma'$ with $\sigma \stackrel{c}{\rightleftharpoons} \sigma'$.

(iii) If $\langle u_1, u_2 \rangle$ is an $\mathcal{R}_c$-critical pair of $\ell_1 \to \alpha_1, r_1, \ell_2 \to \alpha_2, r_2 \in \mathcal{R}_{nc}$, then

$$u_1 \stackrel{<\alpha_1}{\rightleftharpoons} u'_1 \stackrel{q_1}{\underset{\alpha_2}{\rightleftharpoons}} u''_1 \stackrel{<\alpha_1, \alpha_2}{\rightleftharpoons} u''_2 \stackrel{q_2}{\underset{\alpha_1}{\rightleftharpoons}} u'_2 \stackrel{<\alpha_2}{\rightleftharpoons} u_2$$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.

Even though the above theorem is stronger than Theorems 1 and 2, it is much harder to use in practice, since condition (ii) quantifies over infinitely many $\sigma$ and $t$. Similarly, in (iii) we have to verify an infinite number of $\mathcal{R}_c$-critical pairs, given that, as explained, we do not use most general unifiers (which may not exist) in the definition of $\mathcal{R}_c$-critical pairs. This is why we chose to present the above result as an auxiliary tool, rather than a main result of this paper.

*Proof idea* To prove Theorem 4, we introduce a relation $\triangleright_{\alpha}$ which allows to rewrite with $\mathcal{R}_c$ before matching a rule in $\mathcal{R}_{\alpha}$: we have $t \stackrel{p}{\underset{\alpha}{\rightleftharpoons}} u$ when $t|_p = \mathbf{x}.t^p$ and $t_p \stackrel{c}{\rightleftharpoons} \ell[\sigma]$ and $u = t\{\mathbf{x}.(r[\sigma])\}|_p$ for some $\ell \to r \in \mathcal{R}_{\alpha}$. Let us write $\rightsquigarrow_{<\alpha}$ for the reflexive-symmetric-transitive closure of $(\cup_{\beta<\alpha} \triangleright_{\beta}) \cup \stackrel{c}{\rightleftharpoons}$. We can then show both that $\stackrel{c}{\rightleftharpoons} \cdot \triangleright_{\alpha} \subseteq \triangleright_{\alpha} \cdot \stackrel{c}{\rightleftharpoons}$ and $\stackrel{c}{\rightleftharpoons} \cdot \triangleright_{\alpha_1} \subseteq \stackrel{c}{\rightleftharpoons} \cdot \triangleright_{\alpha_2} = \stackrel{c}{\rightleftharpoons} \cdot \triangleright_{<\alpha_1, \alpha_2}$ on meta-free terms, and moreover we have $\stackrel{c}{\rightleftharpoons} \cdot \stackrel{c}{\rightleftharpoons} \subseteq \stackrel{c}{\rightleftharpoons} \cdot \stackrel{c}{\rightleftharpoons}$ on meta-free terms by assumption (i). This proves that $(\cup_{\alpha} \triangleright_{\alpha}) \cup \stackrel{c}{\rightleftharpoons}$ is decreasing on meta-free terms and thus confluent, by labeling $\triangleright_{\alpha}$ with $\alpha$ and $\stackrel{c}{\rightleftharpoons}$ with a new bottom element $\perp$ adjoined to $\mathcal{L}$. Because $(\cup_{\alpha} \triangleright_{\alpha}) \cup \stackrel{c}{\rightleftharpoons}$ and $\stackrel{c}{\rightleftharpoons}$ generate the same transitive closure, we conclude confluence of $\mathcal{R}$.

The proofs of both Theorems 1 and 2 then go by showing that, under the assumptions of these theorems, we can prove condition (ii) and moreover reduce $\mathcal{R}$-critical pairs to either plain critical pairs or $\mathcal{R}$-cyclic critical pairs, which can then be closed in an appropriate way by assumption, proving (iii). Therefore, confluence follows by Theorem 4.
# 8 Towards automating our criteria

Applying critical-pair criteria like Theorems 1 to 3 for checking confluence usually involves a large number of mechanical calculations, whose automation is therefore often helpful. While we leave the automation of our criteria for future work, in this section we take a first step in this direction by sketching how they could be used to decompose a finite rewrite system $\mathcal{R}$ into a set of subsystems $\mathbf{R}$ such that $\mathcal{R}$ is confluent whenever $\mathcal{R}'$ is confluent for all $\mathcal{R}' \in \mathbf{R}$. This strategy could then be used as the basis for a future implementation, by relying on existing tools to verify confluence of the obtained subsystems.

We now define a procedure DECOMP(-) which, given a finite rewrite system $\mathcal{R}$, returns $\mathbf{R}$ satisfying the property claimed above. We first start by using Theorem 3 to split $\mathcal{R}$ into as many fragments $\mathcal{R}^1, \dots, \mathcal{R}^n$ with disjoint signatures as possible, in such a way that they pairwise satisfy condition (2) — note that condition (3) is automatically ensured by the assumption that the signatures are disjoint. In the next step, we calculate the confined part $\mathcal{R}_c^i$ of $\mathcal{R}^i$ and, if $\mathcal{R}_c^i$ equals $\mathcal{R}^i$, we add $\mathcal{R}^i$ to $\mathbf{R}$, otherwise we attempt to apply Theorem 1 or Theorem 2. To know which result to apply, we try to prove termination of $\mathcal{R}_c^i$ by applying existing techniques — such as the ones implemented by the automated termination prover Wanda [21]. If termination can be proved, we try to verify conditions (b) and (c) of Theorem 1, otherwise we try to verify conditions (b') and (c') of Theorem 2. If the conditions are satisfied, we check confluence of $\mathcal{R}_c^i$ by recursively calling DECOMP($\mathcal{R}_c^i$) and adding the calculated subsystems to $\mathbf{R}$, otherwise we simply add $\mathcal{R}^i$ to $\mathbf{R}$. It is a direct consequence of Theorems 1 to 3 that $\mathcal{R}$ is confluent if $\mathcal{R}'$ is confluent for all $\mathcal{R}' \in \text{DECOMP}(\mathcal{R})$.

Finally, let us comment on how the conditions of Theorems 1 to 3 can be verified. Conditions (b) of Theorem 1, (b') of Theorem 2, and (2) of Theorem 3 are obviously decidable, the hard work is verifying conditions (c) of Theorem 1 and (c') of Theorem 2. For these verifications, one could adapt the strategy employed in various previous work, which encode the problem using arithmetic constraints [14,1]. In the specific case of Theorem 2, a further complication is the use of the congruence $\simeq$ for closing cyclic critical pairs. To address this, in the cases where the equations in $C_f$ are all first-order, one could try to use (ground) completion to calculate a rewrite system for $\simeq$, treating the metavariables as new function symbols. The same strategy may sometimes also work for higher-order equations.

# 9 Related and future work

The core strategy of our work, of using sort information to rule out reductions inside non-linear metavariables of rules, already appears in some forms in the literature. We were directly inspired by the unpublished work of Assaf et al. [5], which introduces a confined syntactic class where instances of non-linear metavariables live. This was generalized in unpublished work by Felicissimo [8], by instead considering a framework of sorted rewriting. As we do in Section 3,
he instead uses the sort pre-order to define confinement *a posteriori* in terms of the sorts of non-linear variables. Unbeknownst to him, this idea had already appeared independently in the first-order setting: Aoto *et al.* [3] use the same sort-based strategy to forbid reductions inside non-linear variables, and moreover also employ decreasing diagrams for closing critical pairs. Their work however differs significantly from ours by (1) being restricted to the first-order setting, and (2) imposing the confined fragment to be terminating — a restriction we drop in Theorem 2. They moreover leverage persistency of first-order confluence to treat unsorted systems, a strategy we cannot employ given that confluence is not persistent in higher-order rewriting.

A different work stemming from Assaf *et al.* and closely related to ours is the one by Férey and Jouannaud [10], which provides a criterion establishing higher-order non-left-linear confluence in a set of *layered* terms. Unfortunately, the abstract characterization of this set impairs the applicability of their result.

The work by Klein and Hirokawa [18] is also very much related to ours. Their criterion resembles in particular our Theorem 4: both statements use the notion of *R*-critical pairs and the proofs both employ a rewrite relation applying a directed form of matching modulo. Their result however departs from ours by (1) being restricted to the first-order setting, and (2) requiring a relative termination condition. On the other hand, thanks to this termination hypothesis, they allow for closing critical pairs very liberally, without the need for decreasing diagrams.

The notion of cyclic unification and cyclic critical pairs originates in the work by Liu *et al.* [23], though our definitions are actually considerably different. Their criterion also allows proving confluence of non-left-linear non-terminating systems by closing cyclic critical pairs with decreasing diagrams, but is restricted to the first-order setting. Moreover, their result constrains the use of the congruence $\simeq$ to the bottom of the closing diagram, hence they cannot handle cases like Example 9 which require the application of $\simeq$ before a rewrite step.

Finally, our Theorem 3 is closely related to van Oostrom and van Raamsdonk's weakly orthogonal combination criterion [28]. Their result, which imposes left-linearity, would be a particular case of ours, had they not relaxed (3) to allow for trivial critical pairs, which we believe could also be handled in our case.

For future work, Theorems 1 and 2 could be adapted to instead use weak confinement, by employing a form of orthogonal rewriting in their proofs. Indeed, the only reason sorts of non-linear and nested variables of right-hand sides are considered confined is to prevent the duplication of non-confined redexes, which ceases to be a problem if one can reduce non-overlapping redexes in a single step. This adaptation should be doable, at the cost of having to consider *nested critical pairs* (also known as *multi-multi* [15]), as in Dowek *et al.* [7].

*Acknowledgements* The authors thank Loïc Pujet for suggesting Example 13 and the anonymous reviewers for their helpful comments and remarks.
References

1. Takahito Aoto. Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling. In Christopher Lynch, editor, *Proceedings of the 21st International Conference on Rewriting Techniques and Applications*, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7–16, Dagstuhl, Germany, 2010. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

2. Takahito Aoto and Yoshihito Toyama. Persistency of confluence. *JUCS - Journal of Universal Computer Science*, 3(11):1134–1147, 1997.

3. Takahito Aoto, Yoshihito Toyama, and Kazumasa Uchida. Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams. In Gilles Dowek, editor, *Rewriting and Typed Lambda Calculi*, pages 46–60, Cham, 2014. Springer International Publishing.

4. Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama. Proving confluence of term rewriting systems automatically. In Ralf Treinen, editor, *Rewriting Techniques and Applications*, pages 93–102, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.

5. Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Untyped Confluence in Dependent Type Theories. In *Proceedings Higher-Order Rewriting Workshop*, Proc. Higher-Order rewriting Workshop, Porto, Portugal, June 2016. Easy-Chair.

6. Marc Bezem, Jan Willem Klop, and Roel de Vrijer. *Term rewriting systems*. 2003.

7. Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, and Jiaxiang Liu. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. *Mathematical Structures in Computer Science*, 32(7):898–933, 2022.

8. Thiago Felicissimo. A Confluence Criterion for Non Left-Linearity in a $\beta\eta$-Free Reformulation of HRSs. In *11th International Workshop on Higher-Order Rewriting (HOR 2023)*, 2023.

9. Thiago Felicissimo and Jean-Pierre Jouannaud. Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. Technical report available at https://hal.science/hal-04973508, 2025.

10. Gaspard Férey and Jean-Pierre Jouannaud. Confluence in non-left-linear untyped higher-order rewrite theories. In Niccolò Veltri, Nick Benton, and Silvia Ghilezan, editors, *PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, September 6-8, 2021*, pages 8:1–8:14. ACM, 2021.

11. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In *14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999*, pages 193–202. IEEE Computer Society, 1999.

12. Jean-Yves Girard. *Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur*. PhD thesis, 1972.

13. Makoto Hamana. Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding. *Mathematical Structures in Computer Science*, 32(4):542–573, 2022.

14. Nao Hirokawa and Aart Middeldorp. Decreasing diagrams and relative termination. In *Journal of Automated Reasoning*, volume 47, pages 481–501, 2011.

15. Nao Hirokawa, Julian Nagele, VV Oostrom, Michio Oyamaguchi, et al. Critical peaks redefined-$\phi \sqcup \psi = \top$. In *6th International Workshop on Confluence*, 2017.

16. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. *Journal of the ACM (JACM)*, 1980.
17. Jean-Pierre Jouannaud and Vincent van Oostrom. Diagrammatic confluence and completion. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, *Automata, Languages and Programming, 36th International Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II*, volume 5556 of Lecture Notes in Computer Science, pages 212–222. Springer, 2009.

18. Dominik Klein and Nao Hirokawa. Confluence of Non-Left-Linear TRSs via Relative Termination. In Nikolaj Bjørner and Andrei Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning*, pages 258–273, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.

19. Jan Willem Klop. *Combinatory reduction systems*. PhD thesis, Univ. Utrecht, 1980.

20. Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk. Combinatory reduction systems: introduction and survey. *Theoretical computer science*, 121(1-2):279–308, 1993.

21. Cynthia Kop. WANDA - a Higher Order Termination Tool. In Zena M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1–36:19, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

22. Tomer Libal and Dale Miller. Functions-as-constructors higher-order unification: extended pattern unification. *Ann. Math. Artif. Intell.*, 90(5):455–479, 2022.

23. Jiaxiang Liu, Jean-Pierre Jouannaud, and Mizuhito Ogawa. Confluence of Layered Rewrite Systems. In Stephan Kreutzer, editor, *24th EACSL Annual Conference on Computer Science Logic (CSL 2015)*, volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pages 423–440, Dagstuhl, Germany, 2015. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

24. Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. *Theoretical computer science*, 192(1):3–29, 1998.

25. Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New evidence – a progress report. In Leonardo de Moura, editor, *Automated Deduction – CADE 26*, pages 385–397, Cham, 2017. Springer International Publishing.

26. Vincent van Oostrom. Developing developments. *Theoretical Computer Science*, 175(1):159–181, 1997.

27. Vincent van Oostrom. Confluence by decreasing diagrams: converted. In Andrei Voronkov, editor, *Rewriting Techniques and Applications*, pages 306–320, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

28. Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: The higher-order case. In Anil Nerode and Yu. V. Matiyasevich, editors, *Logical Foundations of Computer Science*, pages 379–392, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.

29. Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Labelings for decreasing diagrams. *J. Autom. Reason.*, 54(2):101–133, 2015.

## A Basic preliminary results

We start in this section by giving proofs of some basic preliminary results, which will be useful for us for the proofs to come.

The following first two properties are well-known and will be often used without announcement.
**Proposition 2 (Basic rewriting properties).**

**Stability** If $t \underset{\mathbb{R}}{\longrightarrow} t'$ and $\sigma \stackrel{p}{\longrightarrow} \sigma'$ then $t[\sigma] \stackrel{q}{\longrightarrow} t'[\sigma']$.

**Orthogonality** If $t \stackrel{p}{\longleftarrow}_{\mathbb{R}_1} \cdot \stackrel{q}{\longrightarrow}_{\mathbb{R}_2} u$ with $p, q$ parallel then $t \stackrel{q}{\longrightarrow}_{\mathbb{R}_2} \cdot \stackrel{p}{\longleftarrow}_{\mathbb{R}_1} u$.

The following property, which holds without restrictions in the first-order setting, requires an additional hypothesis for higher-order systems. For instance, 1 is a position of $X\{a\}$ but not a position of $X\{a\}[X \mapsto x.x] = a$.

**Proposition 3.** Assume that $p$ is a non-nested position of $t$. Then, for all $\sigma$, $p$ is a non-nested position of $t[\sigma]$ and we have $t|_p[\sigma] = t[\sigma]|_p$, and moreover $t\{x.u\}|_p[\sigma] = t[\sigma]\{(x.u)[\sigma]\}|_p$ for all $x.u$ of same arity as $t|_p$.

*Proof.* By induction on $t$.

A corollary of the above is the following result, which also requires the non-nesting hypothesis in the higher-order setting. Indeed, we have for instance $X\{a\} \xrightarrow{1/\mathbb{R}} X\{b\}$ with $a \to b \in \mathbb{R}$, but $X\{a\}[X \mapsto x.f(x,x)] = f(a,a)$ does not reduce in one step to $X\{b\}[X \mapsto x.f(x,x)] = f(b,b)^4$.

**Proposition 4.** If $p$ is non nested in $t$ and $t \xrightarrow{p/\mathbb{R}} t'$, then, for all $\sigma$, we have $t[\sigma] \xrightarrow{p/\mathbb{R}} t'[\sigma]$.

*Proof.* Follows easily by using Proposition 3.

For the following result, recall that $p$ is a functional (resp., variable or metavariable) position of $t$ if $t|_p = x.t_p$ with $t_p$ headed by a function symbol (resp., variable or metavariable).

**Proposition 5.** Let $t$ be a pattern, $\sigma$ a substitution with $\text{dom}(\sigma) = \text{mv}(t)$, and $p$ a position of $t[\sigma]$. Then, exactly one of the following statements hold:

(a) $p$ is a non-nested functional position of $t$.

(b) $p$ is a non-nested variable position of $t$.

(c) For some metavariable position $q$ of $t$, we have $q \le p$.

*Example 14.* Consider $t = f(x.x, y.X\{y\})$ and $\sigma = \{X \mapsto z.g(z, z)\}$. We have $t[\sigma] = f(x.x, y.g(y, y))$ and thus $\text{Pos}(t[\sigma]) = \{\varepsilon, 1, 2, 2 \cdot 1, 2 \cdot 2\}$. Position $\varepsilon$ is in case (a) of the above result, position 1 is in case (b), and the last three are in case (c). Note that position $2 \cdot 1$ is also a variable position of $t$, however it is nested.

**Proposition 6.** If $x.t$ is a pattern and $\sigma_1, \sigma_2$ two substitutions with $\text{dom}(\sigma_i) = \text{mv}(t)$ and $(x.t)[\sigma_1] = (x.t)[\sigma_2]$ then $\sigma_1 = \sigma_2$.

<footnote n="4">⁴ This is the reason why we require the positions $q_1, q_2$ of the closing diagrams in Theorems 1, 2 and 4 to be non-nested.</footnote>
*Proof.* By induction on $t$.

**Lemma 1.** If $t, u$ are meta-free terms with $t \mathrel{\mathop{\rightleftharpoons}}_{\mathbb{R}} u$, then we have $t \mathrel{\mathop{\rightleftharpoons}}_{\mathbb{R}} u$ with a conversion going only trough meta-free terms. As a consequence, if $\mathbb{R}$ is confluent, then $t \mathrel{\mathop{\rightleftharpoons}}_{\mathbb{R}} \cdot \mathrel{\mathop{\rightleftharpoons}}_{\mathbb{R}} u$.

*Proof.* We can apply everywhere a substitution sending each metabariable $\mathcal{X}$ of arity $\{s\} s'$ to some fresh variable $x$ of sort $s'$, and this does not change the endpoints $t$ and $u$. The second point then follows directly by applying confluence.

Let us define $\hat{mv}(\hat{t}) := mv(\hat{t}) \setminus mv(t)$ — that is, the set of metabariables of $\hat{t}$ of the form $\chi_p$. Given a term $t$ and a substitution $\theta$ defined over $mv(\hat{t})$, we define the hereditarily non-linear metabariables of $\theta$ to be

$$mv^{hnl}(\theta) := \bigcup_{x \in \hat{mv}(\hat{t})} mv(\theta(x))$$

In other words, $mv^{hnl}(\theta)$ contains the metabariables that appear in $\theta(\chi_p)$ for some $\chi_p \in \hat{mv}(\hat{t})$. The following lemma justifies why they are called as such: they are the only ones that matter for equalizing $\theta$.

**Lemma 2.** Given a term $t$, let $\theta$ be a substitution with $dom(\theta) = mv(\hat{t})$, and $\tau$ any substitution. If $\theta[\tau]$ is equalized for $\hat{t}$ and we have $mv^{hnl}(\theta) \subseteq dom(\tau')$ for some $\tau' \subseteq \tau$, then $\theta[\tau']$ is also equalized and, assuming $mv(\tau')$ and $dom(\tau \setminus \tau')$ are disjoint, we have $\theta[\tau] = \theta[\tau'])[\tau \setminus \tau']$.

*Proof.* To see that $\theta[\tau']$ is equalized, note that, if $\tilde{\chi} = \tilde{\gamma}$ but $\chi \neq \gamma$, then we necessarily have $\chi, \gamma \in \hat{mv}(\hat{t})$ and thus $\theta(\chi)[\tau] = \theta(\chi)[\tau']$ and $\theta(\gamma)[\tau] = \theta(\gamma)[\tau']$. Therefore, from $\theta(\chi)[\tau] = \theta(\gamma)[\tau]$ we directly obtain that $\theta(\chi)[\tau'] = \theta(\gamma)[\tau']$. It is then easy to see that $\theta[\tau] = \theta[\tau'])[\tau \setminus \tau']$.

Recall that the definition of the operation $(\hat{-})$ and the substitutions lift$_x$ rely on choice functions for picking metabariables. In the case of $(\hat{-})$, given $\chi$ and a position $p$ we must pick a new metabariable $\chi_p$ of same arity as $\chi$. In the case of lift$_x$, given $\chi$ of arity $\{s_\chi\} s_\chi$ and a list of sorts $s$ we must pick a new metabariable $\chi^*$ of arity $\{s, s_\chi\} s_\chi$. We now suppose that these functions are defined in a coherent way, such that $(\chi_p)^* = (\chi^*)_p$.<fnref n="5" />

**Proposition 7.** For all patterns $t$ and $x$, we have $\hat{t}[\text{lift}_x] = t[\text{lift}_x]$.

*Proof.* Direct, once we have $(\chi_p)^* = (\chi^*)_p$.

<footnote n="5">⁵ This can be for instance achieved by implementing metabariables as pairs $(n, \{s_\chi\} s_\chi)$ with $n$ a natural number and $\{s_\chi\} s_\chi$ their arity, and defining $(n, \{s_\chi\} s_\chi)^* := (n, \{s, s_\chi\} s_\chi)$ and defining $\chi_p$ parametrically on the arity component. Alternatively, this discussion can be completely dropped by employing instead a nameless representation of metabariables, in which case $\chi$ and $\chi^*$ would be represented by the same de Bruijn index.</footnote>
## A.1 Basic properties of overlaps

**Lemma 3.** Given disjoint patterns $t_1$ and $x.t_2$, suppose any of the following:

- For some $p$, $t_1$ overlaps $(x.t_2)|_p$.

- For some fresh $y$, $t_1$ overlaps $yx.t_2[\text{lift}_y]$.

- For some renaming $\mu$ with $\text{dom}(\mu) = \text{mv}(t_2)$, $t_1$ overlaps $x.t_2[\mu]$.

Then $t_1$ overlaps $x.t_2$.

**Remark 6.** Note that it is **not** true that, if $t_1$ overlaps $t_2$, then $t_1$ overlaps $x.t_2$. Indeed, consider the counterexample $t_1 = g(X, X)$, $t_2 = g(x, Y)$ and $x = x$. The problem $g(X, X) \stackrel{?}{=} g(x, Y)$ admits the meta-free unifier $\sigma = \{X \mapsto x, Y \mapsto x\}$ however, the problem $x.g(X^*\{x\}, X^*\{x\}) \stackrel{?}{=} x.g(x, Y)$, where $g(X^*\{x\}, X^*\{x\}) = g(X, X)[\text{lift}_x]$, admits no unifier, due to the nature of capture-avoiding substitution.

**Lemma 4.** Let $x.t$ be a linear pattern overlaped by no rhs in $\mathcal{R}$, and suppose that $(x.t)[\sigma] \xrightarrow{p} x.u$ for some $\sigma$ with $\text{dom}(\sigma) = \text{mv}(t)$. Then $x.u = (x.t)[\sigma']$ for some $\sigma'$ with $\sigma \stackrel{\mathcal{R}}{\longrightarrow} \sigma'$. Moreover, if $t$ is headed by a function symbol, then $p \neq \varepsilon$.

*Proof.* By induction of $x.t$. If $x.t = x.x\{x\}$ then $\sigma$ contains a single entry $X \mapsto x.v$ and we have $(x.t)[\sigma] = x.v \xrightarrow{p} x.u$. Therefore, by taking $\sigma' = X \mapsto x.u$ the conditions are satisfied. The case $x.t = x.x$ is impossible. Finally, if $x.t = x.f(x_1.t_1, \dots, x_k.t_k)$ then by the absence of overlaps we cannot have $p = \varepsilon$. Therefore, we must have $p = i \cdot q$ for some $i$, and thus $x.u = x.f(x_1.u_1, \dots, x_k.u_k)$. Writing $\sigma_i$ for the restriction of $\sigma$ to $\text{mv}(t_i)$, we have $(xx_i.t_i)[\sigma_i] \xrightarrow{q} xx_i.u_i$ and by (IH), $xx_i.u_i = (xx_i.t_i)[\sigma'_i]$ for some $\sigma'_i$ with $\sigma_i \stackrel{\mathcal{R}}{\longrightarrow} \sigma'_i$. Defining $\sigma' := \sigma'_i \cup (\sigma \setminus \sigma_i)$ satisfies the conditions.

## A.2 Computing syntactic unifiers from $\mathcal{R}$-unifiers

**Proposition 8.** Assume $\mathcal{R}$ is confluent and terminating, and $x.t_1$ and $x.t_2$ are patterns overlapped by no rhs in $\mathcal{R}$. If $x.t_1 \stackrel{?}{=} x.t_2$ admits a meta-free $\mathcal{R}$-unifier $\sigma_1 \cup \sigma_2$, then it admits a meta-free syntactic unifier $\sigma'_1 \cup \sigma'_2$ with $\sigma_i \stackrel{\mathcal{R}}{\longrightarrow} \sigma'_i$.

*Proof.* Consider the $\mathcal{R}$-normal forms $\sigma'_1, \sigma'_2$ of $\sigma_1, \sigma_2$. Because $\sigma_1, \sigma_2$ are meta-free, it follows that the same holds for $\sigma'_1, \sigma'_2$. Using Lemma 1, we can apply confluence to $(x.t_1)[\sigma'_1] \Longleftarrow_{\mathcal{R}} (x.t_1)[\sigma_1] \Longleftarrow_{\mathcal{R}} (x.t_2)[\sigma_2] \Longleftarrow_{\mathcal{R}} (x.t_2)[\sigma'_2]$ to deduce $(x.t_1)[\sigma'_1] \stackrel{\mathcal{R}}{\longrightarrow} \cdot \stackrel{\mathcal{R}}{\Longleftarrow} (x.t_2)[\sigma'_2]$. However, the two terms are in normal form: indeed, the substitution is already in normal form, and a step above it would contradict the absence of overlaps. Therefore, we conclude $(x.t_1)[\sigma'_1] = (x.t_2)[\sigma'_2]$.

The termination requirement above can be exchanged with linearity:
**Proposition 9.** Assume $\mathcal{R}$ is confluent, and $\mathbf{x}.t_1$ and $\mathbf{x}.t_2$ are linear patterns overlaped by no rhs in $\mathcal{R}$. If $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$ admits a meta-free $\mathcal{R}$-unifier $\sigma_1 \cup \sigma_2$, then it admits a meta-free syntactic unifier $\sigma'_1 \cup \sigma'_2$ with $\sigma_i \underset{\mathcal{R}}{\longrightarrow} \sigma'_i$.

*Proof.* The terms $(\mathbf{x}.t_1)[\sigma_1]$ and $(\mathbf{x}.t_2)[\sigma_2]$ are meta-free, therefore we can use Lemma 1 to apply confluence to $(\mathbf{x}.t_1)[\sigma_1] \mathrel{\substack{\rightleftarrows \\ \overrightarrow{\mathcal{R}}}} (\mathbf{x}.t_2)[\sigma_2]$ and deduce $(\mathbf{x}.t_1)[\sigma_1] \mathrel{\substack{\rightleftarrows \\ \overrightarrow{\mathcal{R}}}} \cdot \mathrel{\substack{\rightleftarrows \\ \overrightarrow{\mathcal{R}}}} (\mathbf{x}.t_2)[\sigma_2]$. Now the result follows by simply iterating Lemma 4.

As a corollary, we can also compute $\mathcal{R}$-cyclic unifiers from $\mathcal{R}$-unifiers:

**Corollary 1.** Assume $\mathcal{R}$ is confluent, $\mathbf{x}.t_1$ and $\mathbf{x}.t_2$ are patterns such that no rhs in $\mathcal{R}$ overlaps $\mathbf{x}.\hat{t}_1$ or $\mathbf{x}.\hat{t}_2$, and $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$ admits a meta-free $\mathcal{R}$-unifier $\tau_1 \cup \tau_2$. Let $\sigma_i$ be the unique equalized substitution satisfying $\tilde{\sigma}_i = \tau_i$. Then, $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$ admits a meta-free $\mathcal{R}$-cyclic unifier $\sigma'_1 \cup \sigma'_2$ such that $\sigma_i \underset{\mathcal{R}}{\longrightarrow} \sigma'_i$.

*Proof.* Because $\tau_1 \cup \tau_2$ is a meta-free $\mathcal{R}$-unifier of $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$, by taking $\sigma_1, \sigma_2$ as defined in the statement, it follows that $\sigma_1 \cup \sigma_2$ is a meta-free $\mathcal{R}$-unifier of $\mathbf{x}.\hat{t}_1 \stackrel{?}{=} \mathbf{x}.\hat{t}_2$. By Proposition 9 we thus obtain a meta-free syntactic unifier $\sigma'_1 \cup \sigma'_2$ of $\mathbf{x}.\hat{t}_1 \stackrel{?}{=} \mathbf{x}.\hat{t}_2$ satisfying $\sigma_i \underset{\mathcal{R}}{\longrightarrow} \sigma'_i$. Finally, because $\sigma_i$ is equalized, for all $\mathbf{X}, \mathbf{Y} \in \text{mv}(\hat{t}_i)$ with $\tilde{\mathbf{X}} = \tilde{\mathbf{Y}}$ we have $\sigma'_i(\mathbf{X}) \mathrel{\substack{\rightleftarrows \\ \overrightarrow{\mathcal{R}}}} \sigma_i(\mathbf{X}) = \sigma_i(\mathbf{Y}) \mathrel{\substack{\rightleftarrows \\ \overrightarrow{\mathcal{R}}}} \sigma_i(\mathbf{Y})$, showing that $\sigma'_1 \cup \sigma'_2$ is an $\mathcal{R}$-cyclic unifier of $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$.

### A.3 Basic results on pattern unification

Let us say that $\theta$ is a pattern substitution when $\theta(\mathbf{X})$ is a pattern for all $\mathbf{X} \in \text{dom}(\theta)$. The following result is well-known and trivial.

**Proposition 10.** If $\theta$ is an mgu for $\mathbf{x}.t_1 \stackrel{?}{=} \mathbf{x}.t_2$ then $\theta$ is a pattern substitution.

*Proof.* By direct induction on the pattern unification algorithm, and the fact that mgus are unique up to renamings.

The following result is probably well-known, but these authors were not able to find a proof of it in the literature.

**Proposition 11.** Let $\mathbf{x}.t_1, \mathbf{x}.t_2$ be disjoint linear patterns with mgu $\theta = \theta_1 \cup \theta_2$. There exists a renaming $\mu$ such that, if $\mathbf{X}$ occurs in $t_i$ at $p_X$, then for some $i_X \in \{1, 2\}$ we have $\theta(\mathbf{X}) = \mathbf{x}.t_{i_X}|_{p_X}[\mu]$.

In the following proof, let us say that $\theta, \theta'$ are extensionally equal, denoted $\theta \doteq \theta'$, when $t[\theta] = t[\theta']$ for all $t$.

*Proof.* For the proof, we recall the non-failing rules of (fully extended and linear) pattern unification, consisting of rewriting pairs $C;S$ where $C$ is a pattern unification problem and $S$ a set if solved forms, that is, equations of the shape
$x \cdot X\{x\} \stackrel{?}{=} x \cdot t$ st no two equations share the samelhs. Given a solved form $S$, we write $\theta_S$ for the substitution containing $X \mapsto x \cdot t$ for each $x \cdot X\{x\} \stackrel{?}{=} x \cdot t \in S$. The mgu of a problem $t_1 \stackrel{?}{=} t_2$ is then obtained by reducing $\{t_1 \stackrel{?}{=} t_2\}; \emptyset$ to $\emptyset; S$ and returning an mgu $\theta$ with $\theta \stackrel{?}{=} \theta_S$.<fnref n="6" />

$$C \cup \{x.x \stackrel{?}{=} x.x\}; S \rightsquigarrow C; S$$

$$C \cup \{x.f(x_1.t_1, \dots, x_k.t_k) \stackrel{?}{=} x.f(x_1.t'_1, \dots, x_k.t'_k)\}; S \rightsquigarrow C \cup \{xx_i.t_i \stackrel{?}{=} xx_i.t'_i\}_{i=1, \dots, k}; S$$

$$C \cup \{x.X\{x\} \stackrel{?}{=} x.t\}; S \rightsquigarrow C; S \cup \{x.X\{x\} \stackrel{?}{=} x.t\}_{(p,1)}$$

$$C \cup \{x.t \stackrel{?}{=} x.X\{x\}\}; S \rightsquigarrow C; S \cup \{x.X\{x\} \stackrel{?}{=} x.t\}_{(p,2)}$$

In order to show (2), we have made a small cosmetic change to the usual rules of pattern unification, by annotating equations with a position to remember their relationship with the initial patterns of the problem. This then allows us to show that, if we have a run $\{x.t_1 \stackrel{?}{=} x.t_2\}; \emptyset \rightsquigarrow C; S$, then:

$$- y.u_1 \stackrel{?}{=} y.u_2 \in C \text{ implies } x.t_i|_p = y.u_i.$$

$$- y.X\{y\} \stackrel{?}{=} y.u \in S \text{ implies that } p \text{ is the position of } X \text{ in } t_i, \text{ and that } x.t_{i_x}|_p = y.u \text{ for } i_x \text{ the opposite of } i.$$

Now, consider a run $\{x.t_1 \stackrel{?}{=} x.t_2\}; \emptyset \rightsquigarrow^* \emptyset; S$, returning at the end an mgu $\theta$ extensionally equal to $\theta_S$. We claim that, for all $X$ occurring in $x.t_i$ at $p$, we have $y.X\{y\}[\theta_S] = x.t_{i_x}|_p$ for some $i_x$. First, by the properties already stated, if $X \in \text{dom}(\theta_S) \cap \text{mv}(t_i)$, we have $\theta_S(X) = x.t_{i_x}|_p$ for some $i_x$, and where $p$ is the position of $X$ in $t_i$. On the other hand, if $X$ occurs in $x.t_i$ at $p$ but $X \notin \text{dom}(\theta_S)$, we have $(y.X\{y\})[\theta_S] = x.t_i|_p$ trivially, given that $x.t_i|_p = y.X\{y\} = (y.X\{y\})[\theta_S]$. Because mgus are unique modulo renaming, we conclude the result.

### A.4 Characterization of cyclic unifiers

For the following proofs, recall that $C$ denotes a set of equations between patterns, and that $\rightsquigarrow$ is the rule

$$\{x.f(x_1.t_1, \dots, x_k.t_k) \approx x.f(x_1.t'_1, \dots, x_k.t'_k)\} \cup C \rightsquigarrow \{xx_i.t_i \approx xx_i.t'_i\}_{i=1, \dots, k} \cup C$$

Given a pattern $t$, let $\mathcal{D}_t(C)$ be the predicate "for all $x.u_1 \approx x.u_2 \in C$, $x.u_i$ is linear and $t$ does not overlap $x.u_i$ (for $i=1, 2$)".

**Lemma 5.** Given a pattern $t$, if $C \rightsquigarrow C'$ and $\mathcal{D}_t(C)$ then $\mathcal{D}_t(C')$.

<footnote n="6">⁶ Note that we cannot directly return $\theta_S$ because we require mgus to be defined over all metavariables of the problem. Therefore, the returned mgu $\theta$ is obtained by adding trivial entries $X \mapsto y.X\{y\}$ for all $X \in \text{mv}(t_1, t_2) \setminus \text{dom}(\theta_S)$.</footnote>
*Proof.* Follows directly from Lemma 3.

Given a substitution $\tau$, and assuming an underlying rewrite system $\mathcal{R}$, let $\mathfrak{P}_\tau(C)$ be the predicate “for all $x.t \approx x.u \in C$, we have $(x.t)[\tau] \overset{\mathcal{R}}{\rightleftharpoons} (x.u)[\tau]$”.

**Lemma 6.** Suppose that $\mathcal{R}$ is confluent and $\mathcal{D}_\ell(C)$ for all $\ell \to r \in \mathcal{R}$, and let $\tau$ be a meta-free substitution with $\text{dom}(\tau) = \text{mv}(C)$. If $C \rightsquigarrow C'$ then $\mathfrak{P}_\tau(C)$ iff $\mathfrak{P}_\tau(C')$.

*Proof.* The right-to-left direction is trivial, let us now see the other one. If $(x.t_1)[\tau] \overset{\mathcal{R}}{\rightleftharpoons} (x.t_2)[\tau]$ for some $x.t_1 \approx x.t_2 \in C$ with each $t_i$ of the form $f(x_1.u_i^1, \dots, x_k.u_i^k)$, then by using Lemma 1 we can apply confluence and obtain $(x.t_1)[\tau] \underset{\mathcal{R}}{\longrightarrow} \cdot \underset{\mathcal{R}}{\longleftarrow} (x.t_2)[\tau]$. Now, by iterating Lemma 4 we obtain that none of these steps take place at the head, therefore we can conclude $(xx_j.u_j^1)[\tau] \underset{\mathcal{R}}{\rightleftharpoons} (xx_j.u_j^2)[\tau]$ for $j = 1, \dots, k$.

**Proposition 1 (Characterization of cyclic unifiers).** Suppose that $\mathcal{R}$ is confluent and that $x.t_1, x.t_2$ are disjoint patterns such that, for all $\ell \to r \in \mathcal{R}$, $\ell$ does not overlap $x.\hat{t}_i$. If $x.t_1 \stackrel{?}{=} x.t_2$ admits an $\mathcal{R}$-cyclic unifier, then it admits a dcu $(\theta, \simeq)$. Moreover, a meta-free $\sigma$ with $\text{dom}(\sigma) = \text{mv}(\hat{t}_1, \hat{t}_2)$ is an $\mathcal{R}$-cyclic unifier of $t_1 \stackrel{?}{=} t_2$ iff there is a meta-free $\tau$ that $\mathcal{R}$-realizes $\simeq$ and satisfies $\sigma = \theta[\tau]$.

*Proof.* For the first statement, note that if $x.t_1 \stackrel{?}{=} x.t_2$ admits a cyclic unifier, then this is also a unifier of $x.\hat{t}_1 \stackrel{?}{=} x.\hat{t}_2$, which therefore admits an mgu $\theta$. Therefore, by calculating the $\simeq$ associated to $\theta$, we obtain a dcu $(\theta, \simeq)$ for $x.t_1 \stackrel{?}{=} x.t_2$.

For the second statement, let us establish some preliminary facts. In the following discussion, let $C_0$ and $C_f$ be the sets of equations used for the definition of $(\theta, \simeq)$. First note that, because equations in $C_0$ are of the form $\theta(\chi) \approx \theta(\Upsilon)$ with $\chi, \Upsilon \in \text{dom}(\theta)$ and with $\theta$ a syntactic mgu of $x.\hat{t}_1 \stackrel{?}{=} x.\hat{t}_2$, by Proposition 11 the left- and right-hand side of constraints in $C_0$ are all of the shape $x.\hat{t}_{j_q}[\mu]$ for some $j$ and $q$ and renaming $\mu$. Therefore, by Lemma 3 and the absence of overlaps, we obtain $\mathcal{D}_\ell(C_0)$ for all $\ell \to r \in \mathcal{R}$. By iterating Lemmas 5 and 6 on $C_0 \rightsquigarrow C_f$ we then obtain $\mathfrak{P}_\tau(C_0)$ iff $\mathfrak{P}_\tau(C_f)$. Finally, note that we have $\mathfrak{P}_\tau(C_f)$ iff $\tau$ realizes $\simeq$. With these facts, we are now ready to show the result.

For the left-to-right direction, first note that because $\sigma$ is a syntactic unifier for $x.\hat{t}_1 \stackrel{?}{=} x.\hat{t}_2$, of which $\theta$ is a (syntactic) mgu, then we must have $\sigma = \theta[\tau]$ for some meta-free $\tau$ with $\text{dom}(\tau) = \text{mv}(\theta)$. Moreover, by assumption we also have $\theta(\chi)[\tau] = \sigma(\chi) \overset{\mathcal{R}}{\rightleftharpoons} \sigma(\Upsilon) = \theta(\Upsilon)[\tau]$ for all $\chi, \Upsilon \in \text{mv}(\hat{t}_1) \cup \text{mv}(\hat{t}_2)$ with $\tilde{\chi} = \tilde{\Upsilon}$, so we have $\mathfrak{P}_\tau(C_0)$. By the above discussion, we get $\mathfrak{P}_\tau(C_f)$ and thus that $\tau$ realizes $\simeq$.

For the right-to-left direction, it is already clear that $(x.\hat{t}_1)[\sigma] = (x.\hat{t}_2)[\sigma]$ because $\sigma = \theta[\tau]$ and $\theta$ is a syntactic mgu of $x.\hat{t}_1 \stackrel{?}{=} x.\hat{t}_2$. Moreover, because $\tau$ realizes $\simeq$, we have $\mathfrak{P}_\tau(C_f)$. By the above discussion, this implies $\mathfrak{P}_\tau(C_0)$, which in turn implies that $\sigma(\chi) = \theta(\chi)[\tau] \overset{\mathcal{R}}{\rightleftharpoons} \theta(\Upsilon)[\tau] = \sigma(\Upsilon)$ for all $\chi, \Upsilon \in \text{mv}(\hat{t}_1) \cup \text{mv}(\hat{t}_2)$ with $\tilde{\chi} = \tilde{\Upsilon}$. Therefore, $\sigma$ is indeed a cyclic unifier.
## B Proof of Theorem 3

We define orthogonal rewriting — also known as multi-step rewriting, or simultaneous rewriting — with $\mathcal{R}$, denoted $\underset{\mathcal{R}}{\stackrel{n}{\rightleftharpoons}}$, by the inference rules in Figure 2.

As can be seen, we annotate the arrow with the number of contracted redexes, which will be used as an induction measure in the proofs.

<figure><img src="image_4.png" /><figcaption>Fig. 2. Orthogonal rewriting with $\mathcal{R}$</figcaption></figure>

Orthogonal rewriting satisfies the following well-known basic properties. The omitted proofs are similar to the ones one can find in [6, Chapter 11].

**Proposition 12 (Basic properties of $\Rightarrow$).** For all $\mathcal{R}$, we have:

1. $t \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} t$ for all $t$.

2. $t_1 \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} t_2$ and $\sigma_1 \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} \sigma_2$ imply $t_1[\sigma_1] \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} t_2[\sigma_2]$, for all $t_1, t_2, \sigma_1, \sigma_2$.

3. $\underset{\mathcal{R}}{\longrightarrow} \subset \underset{\mathcal{R}}{\longrightarrow} \subseteq \underset{\mathcal{R}}{\longrightarrow}$, and therefore, for all $t, t'$, we have $t \underset{\mathcal{R}}{\longrightarrow} t'$ iff $t \underset{\mathcal{R}}{\stackrel{0}{\Rightarrow}} t'$.

The following lemma is the cornerstone of the proof of Theorem 3.

**Lemma 7.** Given some $\mathcal{R}$, let $x.t$ be a pattern such that:

- If $x \in \text{mv}^{nl}(t)$ is of arity $\{\dots\}s$, then no rule in $\mathcal{R}$ has a sort $s'$ with $s' \preceq s$.

- For all $\ell \to r \in \mathcal{R}$, $\ell$ does not overlap $x.t$.

Then, for all meta-free $\sigma$ with $\text{dom}(\sigma) = \text{mv}(t)$, $(x.t)[\sigma] \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} x.t'$ implies $x.t' = (x.t)[\sigma']$ for some $\sigma'$ with $\sigma \underset{\mathcal{R}}{\stackrel{n}{\Rightarrow}} \sigma'$.
**Proof.** By induction on $x.t$. The only interesting case is $x.t = x.f(x_1.t_1, \dots, x_k.t_k)$, in which case by absence of overlaps the derivation of $f(x_1.t_1, \dots, x_k.t_k)[\sigma] \stackrel{n}{\rightleftharpoons} t'$ cannot end with ORTHO, and hence it ends with SYMB. Therefore, we have $x.t' = x.f(x_1.t'_1, \dots, x_k.t'_k)$ and $xx_i.t_i[\sigma_i] \stackrel{n_i}{\rightleftharpoons} xx_i.t'_i$ with $n = \sum_i n_i$ and $\sigma_i$ being the restriction of $\sigma$ to $mv(t_i)$. By IH, for all $i$ we have $xx_i.t'_i = (xx_i.t_i)[\sigma'_i]$ for some $\sigma'_i$ with $dom(\sigma'_i) = mv(t_i)$ and $\sigma_i \stackrel{n_i}{\rightleftharpoons} \sigma'_i$. Now note that $\sigma' := \bigcup_i \sigma'_i$ is well-defined: indeed, if $\chi \in dom(\sigma'_i) \cap dom(\sigma'_j)$ for $i \neq j$ then $\chi$ is a non-linear variable of $t$. Because $\sigma_i(\chi)$ and $\sigma_j(\chi)$ are meta-free, by sort constraints no rule of $\mathcal{R}$ can be used in the derivations of $\sigma_i(\chi) \stackrel{\sigma'_i}{\rightleftharpoons} \sigma'_j(\chi)$ and $\sigma_j(\chi) \stackrel{\sigma'_j}{\rightleftharpoons} \sigma'_i(\chi)$, so we obtain $\sigma'_i(\chi) = \sigma_i(\chi) = \sigma(\chi) = \sigma_j(\chi) = \sigma'_j(\chi)$. We can thus conclude $\sigma \stackrel{n}{\rightleftharpoons} \sigma'$ and $x.t' = x.f(x_1.t_1[\sigma'_1], \dots, x_k.t_k[\sigma'_k]) = (x.t)[\sigma']$ as required.

In the following statement, let us define $i^*$ by $1^* = 2$ and $2^* = 1$.

**Corollary 2.** Under the assumptions of Theorem 3, for all $i = 1, 2$ and $\ell \to r \in \mathcal{R}_i$ and meta-free $\sigma$ with $dom(\sigma) = mv(\ell)$, if $\ell[\sigma] \stackrel{n}{\rightleftharpoons} u$ by a derivation that does not finish by ORTHO, then $u = \ell[\sigma']$ with $\sigma \stackrel{n}{\rightleftharpoons} \sigma'$.

**Proof.** We have $\ell = f(x_1.t_1, \dots, x_k.t_k)$, so the argument is essentially the same as the one in Lemma 7, with the exception that calls to the IH are replaced by uses of Lemma 7.

**Proposition 13.** Under the assumptions of Theorem 3, if $t_1 \stackrel{t_0}{\rightleftharpoons} t_2$ with $t_0$ meta-free, then $t_1 \stackrel{\mathcal{R}_2}{\rightleftharpoons} t_2$.

**Proof.** We show that, if $t_1 \stackrel{n_1}{\rightleftharpoons} t_0 \stackrel{n_2}{\rightleftharpoons} t_2$ with $t_0$ meta-free, then $t_1 \stackrel{\mathcal{R}_2}{\rightleftharpoons} t_2$, by two nested inductions: an outer one on $n_1 + n_2$ and an inner one on the derivations of $t_0 \stackrel{n_1}{\rightleftharpoons} t_1$ and $t_0 \stackrel{n_2}{\rightleftharpoons} t_2$. If none of the derivations end with ORTHO, the result follows directly by the inner IH. Otherwise, we have the following cases:

- Case ORTHO/ORTHO. Note that both sides must apply the same rewrite rule, otherwise we would have a critical pair, contradicting assumption (3). So, for some $\ell \to r \in \mathcal{R}_1 \cap \mathcal{R}_2$ we have $t_0 = \ell[\sigma_0]$ and, for $i = 1, 2$, we have $t_i = r[\sigma_i]$ and $\sigma_0 \stackrel{m_1}{\rightleftharpoons} \sigma_i$ with $m_i < n_i$. By the outer IH applied to $\sigma_1 \stackrel{m_1}{\rightleftharpoons} \sigma_0 \stackrel{m_2}{\rightleftharpoons} \sigma_2$ we get $\sigma_1 \stackrel{\mathcal{R}_2}{\rightleftharpoons} \sigma_3 \stackrel{\mathcal{R}_1}{\rightleftharpoons} \sigma_2$ for some $\sigma_3$. Using Proposition 12, we conclude

$$t_1 = r[\sigma_1] \stackrel{\mathcal{R}_2}{\rightleftharpoons} r[\sigma_3] \stackrel{\mathcal{R}_1}{\rightleftharpoons} r[\sigma_2] = t_2$$

- Case SYMB/ORTHO. We have $t_1 \stackrel{n_1}{\rightleftharpoons} t_0 = \ell[\sigma_0] \stackrel{n_2}{\rightleftharpoons} r[\sigma_2] = t_2$ for some $\sigma_0 \stackrel{m_2}{\rightleftharpoons} \sigma_2$ with $m_2 < n_2$ and $\ell \to r \in \mathcal{R}_2$. By Corollary 2 we deduce that $t_1 = \ell[\sigma_1]$ with $\sigma_0 \stackrel{n_1}{\rightleftharpoons} \sigma_1$. Because $n_1 + n_2 > n_1 + m_2$, we can apply the
outer IH to $\sigma_1 \underset{\mathcal{R}_1}{\overset{n_1}{\rightleftharpoons}} \sigma_0 \overset{m_1}{\rightleftharpoons} \sigma_2$ to obtain $\sigma_1 \underset{\mathcal{R}_2}{\rightleftharpoons} \sigma_3 \underset{\mathcal{R}_1}{\rightleftharpoons} \sigma_2$ for some $\sigma_3$. Using Proposition 12, we conclude

$$t_1 = \ell[\sigma_1] \underset{\mathcal{R}_2}{\Longrightarrow} r[\sigma_3] \underset{\mathcal{R}_1}{\Longleftarrow} r[\sigma_2] = t_2$$

– Case ORTHO/SYMB. Symmetric to the above.

The proof of Theorem 3 is now direct.

**Theorem 3.** Let $\mathcal{R}_1, \mathcal{R}_2$ be (non-necessarily disjoint) rewrite systems such that:

(1) $\mathcal{R}_1$ and $\mathcal{R}_2$ are both confluent.

(2) $\mathcal{R}_2|_{S_{wc}(\mathcal{R}_1)} = \mathcal{R}_1|_{S_{wc}(\mathcal{R}_2)} = \emptyset$.

(3) There are no critical pairs between rules of $\mathcal{R}_1$ and $\mathcal{R}_2$.

Then $\mathcal{R}_1 \cup \mathcal{R}_2$ is confluent.

*Proof.* By Hindley-Rosen's lemma, it suffices to show that each $\xrightarrow{\mathcal{R}_i}$ is confluent on meta-free terms (which we have by hypothesis), and that $\xrightarrow{\mathcal{R}_1}$ and $\xrightarrow{\mathcal{R}_2}$ commute on meta-free terms, that is, that $t_1 \underset{\mathcal{R}_1}{\rightleftharpoons} t_0 \xrightarrow{\mathcal{R}_2} t_2$ with $t_0$ meta-free implies that $t_1 \xrightarrow{\mathcal{R}_2} t_2 \cdot \xleftarrow{\mathcal{R}_1} t_2$. By Proposition 12, $\xrightarrow{\mathcal{R}_i}$ and $\xrightarrow{\mathcal{R}_i}$ generate the same reflexive-transitive closure, so it suffices to show that $\xrightarrow{\mathcal{R}_1}$ and $\xrightarrow{\mathcal{R}_2}$ commute on meta-free terms, which is an easy consequence of Proposition 13.

# C Proofs of Theorems 1, 2 and 4

## C.1 Proof of Theorem 4

Given a label $\alpha \in \mathcal{L}$, we write $t \underset{\alpha}{\overset{p}{\rightleftharpoons}} u$ when $p \in \mathcal{Pos}(t)$ and, for some $\ell \to \alpha$ $r \in \mathcal{R}_{nc}$ and $\sigma$ with $\mathrm{dom}(\sigma) = \mathrm{mv}(\ell)$, we have $t|_p = x.t^p$ and $t_p \xrightarrow{c} \ell[\sigma]$ and $u = t\{x.(r[\sigma])\}_p$.

**Proposition 14 (Basic properties of $\triangleright$).**

1. $\underset{\alpha}{\overset{p}{\triangleright}} \subseteq \underset{c}{\overset{\geq p}{\triangleright}} \cdot \underset{\alpha}{\overset{p}{\triangleright}}$.

2. $\underset{\alpha}{\overset{p}{\triangleright}} \subseteq \underset{\alpha}{\overset{p}{\triangleright}}$.

3. If $t \underset{\alpha}{\overset{p}{\triangleright}} t'$ and $p$ is not nested then $t[\sigma] \underset{\alpha}{\overset{p}{\triangleright}} t'[\sigma]$ with $p$ not nested.

**Lemma 8.** Under the assumptions of Theorem 4, if $t_1 \underset{c}{\overset{p}{\rightleftharpoons}} t_0 \underset{\alpha}{\overset{p}{\rightleftharpoons}} t_2$ with $t_0$ meta-free, then $t_1 \underset{\alpha}{\overset{p}{\rightleftharpoons}} \cdot \underset{c}{\overset{p}{\rightleftharpoons}} t_2$.

*Proof.* By induction on $p$. The case with $p \neq \varepsilon$ follows directly from the IH because, by sort constraints, no $\mathcal{R}_c$ can take place at the head. For $p = \varepsilon$ we have $t \underset{c}{\rightleftharpoons} \cdot \xrightarrow{c} \ell[\sigma]$ and $t_1 = r[\sigma]$ for some $\ell \to \alpha$ $r \in \mathcal{R}_{nc}$. By (ii) we then have $t \xrightarrow{c} \ell[\sigma']$ with $\sigma \xrightarrow{c} \sigma'$. Therefore, we conclude $t_2 \underset{\alpha}{\overset{\varepsilon}{\rightleftharpoons}} r[\sigma'] \underset{c}{\rightleftharpoons} r[\sigma] = t_1$.
**Lemma 9.** If $\mathcal{X} \in \text{mv}^{sl}(t)$ and $u \underset{\alpha}{\overset{\beta}{\to}} u'$ then $t[\mathcal{X} \mapsto \mathbf{x}.u] \underset{\alpha}{\overset{\beta}{\to}} t[\mathcal{X} \mapsto \mathbf{x}.u']$.

*Proof.* By induction on $t$.

**Lemma 10.** Under the assumptions of Theorem 4, if $t_1 \underset{\alpha_1}{\overset{p_1}{\leftarrow}} t_0 \underset{\alpha_2}{\overset{p_2}{\to}} t_2$ with $t_0$ meta-free, then $t_1 \underset{\alpha_1}{\overset{q_1}{\rightleftarrows}} t'_1 \underset{\alpha_2}{\overset{q_2}{\to}} t''_1 \underset{\alpha_1, \alpha_2}{\overset{q_2}{\rightleftarrows}} t'_2 \underset{\alpha_2}{\overset{q_1}{\to}} t''_2$ for some $t'_1, t''_1, t'_2, t''_2$ and $q_1, q_2$ not nested.

*Proof.* We show the result by induction on $p_1$ and $p_2$. If the positions are both different from $\varepsilon$ and parallel, we have $t_1 \underset{\alpha_2}{\overset{p_2}{\to}} \cdot \underset{\alpha_1}{\overset{p_1}{\leftarrow}} t_2$, and because $t_1, t_2$ are meta-free it is trivial that $p_1, p_2$ are not nested. If the positions are both different from $\varepsilon$ but not parallel, the result follows directly from the IH. Now, suppose wlog that $p_2 = \varepsilon$ (the case $p_1 = \varepsilon$ being symmetric), in which case we have $t_0 \underset{c}{\to} \ell_2[\sigma_2]$ and $t_2 = r_2[\sigma_2]$ for some $\ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$. By Lemma 8 we have $t_1 \underset{c}{\to} t'_1 \underset{\alpha_1}{\overset{p_1}{\leftarrow}} \ell_2[\sigma_2]$. By Proposition 5, we have the following cases to consider. In the following, we write just $p$ for $p_1$.

- Case $p$ is a non-nested variable position of $\ell_2$. Impossible, as this would contradict $\ell_2[\sigma_2] \underset{\alpha_1}{\overset{p_1}{\to}} t'_1$.

- Case $q \le p$, for $q$ the position of a variable $\mathcal{X}$ in $\ell_2$. The instantiation of $\mathcal{X}$ by $\sigma_2$ has a subterm that reduces to an $\mathcal{R}_{nc}$ redex, hence it follows that $\mathcal{X}$ is of non-confined sort, and so that $\mathcal{X}$ must be a linear variable of $\ell_2$. Therefore, we have $t'_1 = \ell_2[\sigma'_2]$ with $\sigma_2 \underset{\alpha_1}{\overset{p_1}{\to}} \sigma'_2$ for some $\sigma'_2$. Let us decompose $\sigma_2, \sigma'_2$ as $\sigma_2 = \tau \cup \{\mathcal{X} \mapsto \mathbf{x}.u\}$ and $\sigma'_2 = \tau \cup \{\mathcal{X} \mapsto \mathbf{x}.u'\}$ with $u \underset{\alpha_1}{\to} u'$. Because $\mathcal{X}$ is of non-confined sort, we have either $\mathcal{X} \notin \text{mv}(r_2)$, in which case $r_2[\sigma_2] = r_2[\sigma'_2]$, or $\mathcal{X} \in \text{mv}^{sl}(r_2)$ and so $\mathcal{X} \in \text{mv}^{sl}(r_2[\tau])$, which by Lemma 9 gives $r_2[\sigma_2] = r_2[\tau][\mathcal{X} \mapsto \mathbf{x}.u] \underset{\alpha_1}{\to} r_2[\tau][\mathcal{X} \mapsto \mathbf{x}.u'] = r_2[\sigma'_2]$. In all cases, we conclude $t_1 \underset{\alpha_2}{\overset{\varepsilon}{\to}} r_2[\sigma'_2] = \underset{\alpha_1}{\overset{\varepsilon}{\leftarrow}} r_2[\sigma_2]$ and, because $t_1, t_2$ are meta-free, it is trivial that the two rewrite positions are not nested.

- Case $p$ is a non-nested functional position of $\ell_2$. We have $\ell_2[\sigma_2]|_p \underset{c}{\to} \mathbf{x}.(\ell_1[\sigma_1])$ for some $\ell_1 \to_{\alpha_1} r_1 \in \mathcal{R}_{nc}$ and $\sigma_1$ with $\text{dom}(\sigma_1) = \text{mv}(\ell_1)$, and moreover $t'_1 = \ell_2[\sigma_2]\{\mathbf{x}.(r_1[\sigma_1])\}_p$. Writing $\ell_2|_p = \mathbf{x}.\ell_2^p$, because $p$ is non-nested, by Proposition 3 we have $\ell_2[\sigma_2]|_p = \ell_2|_p[\sigma_2] = (\mathbf{x}.\ell_2^p)[\sigma_2]$. Now let $\sigma_2^p$ be the restriction of $\sigma_2$ to variables in $\text{mv}(\ell_2^p)$. Then, $\tau := (\mathbf{x}.\sigma_1) \cup \sigma_2^p$ is an $\mathcal{R}_c$-unifier for $\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.\ell_2^p$, as shown by

$$ (\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}]) [\tau] = (\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}]) [\mathbf{x}.\sigma_1] = \mathbf{x}.\ell_1[\sigma_1] \underset{c}{\rightleftarrows} (\mathbf{x}.\ell_2^p)[\sigma_2] = (\mathbf{x}.\ell_2^p)[\tau] $$

Therefore, we have an $\mathcal{R}_c$-critical pair $\langle (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\tau], r_2[\tau] \rangle$. By (iii), we have

$$ (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\tau] \underset{\alpha_1}{\rightleftarrows} u'_1 \underset{\alpha_2}{\overset{q_1}{\to}} u''_1 \underset{\alpha_1, \alpha_2}{\rightleftarrows} u''_2 \underset{\alpha_1}{\overset{q_2}{\to}} u'_2 \underset{\alpha_2}{\rightleftarrows} r_2[\tau] $$
for some $u'_1, u''_1, u'_2, u''_2$ and $q_1, q_2$ non-nested. Now, define $\sigma'_2 := \sigma_2 \setminus \sigma_2^p$ and,
using Proposition 4, we obtain

$$ (\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\tau][\sigma'_2] \underset{<\alpha_1}{\rightleftarrows} u'_1[\sigma'_2] \xrightarrow{q_1} = u''_1[\sigma'_2] \underset{<\alpha_1,\alpha_2}{\rightleftarrows} u''_2[\sigma'_2] = \xleftarrow{q_2} u'_2[\sigma'_2] \underset{<\alpha_2}{\rightleftarrows} r_2[\tau][\sigma'_2] $$

Note that we have $\tau \cup \sigma'_2 = (\mathbf{x}.\sigma_1) \cup \sigma_2$. Therefore, we have $r_2[\tau][\sigma'_2] = r_2[\sigma_2] = t_2$ and, because $p$ is non-nested in $\ell_2$, by Proposition 3 we also have

$$ (\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\tau][\sigma'_2] = \ell_2[\sigma_2]\{[\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}][\mathbf{x}.\sigma_1]]\}_p = \ell_2[\sigma_2]\{[\mathbf{x}.r_1[\sigma_1]]\}_p = t'_1 $$

By composing the above diagram with $t_1 \xrightarrow{q'} t'_1$ and the above equations,
and using the fact that $\xrightarrow{q'}$ is included in $\xrightarrow{q'}$ for all $q', \alpha'$, we conclude

$$ t_1 \xrightarrow{q'} t'_1 \underset{<\alpha_1}{\rightleftarrows} u'_1[\sigma'_2] \xrightarrow{q_1} = u''_1[\sigma'_2] \underset{<\alpha_1,\alpha_2}{\rightleftarrows} u''_2[\sigma'_2] = \xleftarrow{q_2} u'_2[\sigma'_2] \underset{<\alpha_2}{\rightleftarrows} r_2[\tau] = t_2 $$

with $q_1, q_2$ not nested.

**Theorem 4.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(i) $\mathcal{R}_c$ is confluent.

(ii) If $t \underset{c}{\rightleftarrows} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and $t, \sigma$ both meta-free with $\mathrm{dom}(\sigma) = \mathrm{mv}(\ell)$, then $t \xrightarrow{q'} \ell[\sigma']$ for some $\sigma'$ with $\sigma \xrightarrow{q'} \sigma'$.

(iii) If $\langle u_1, u_2 \rangle$ is an $\mathcal{R}_c$-critical pair of $\ell_1 \to_{\alpha_1} r_1, \ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$ u_1 \underset{<\alpha_1}{\rightleftarrows} u'_1 \xrightarrow{q_1} = u''_1 \underset{<\alpha_1,\alpha_2}{\rightleftarrows} u''_2 = \xleftarrow{q_2} u'_2 \underset{<\alpha_2}{\rightleftarrows} u_2 $$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.

*Proof.* We have $\xrightarrow{\mathcal{R}} \subseteq ((\bigcup_{\alpha} \triangleright_{\alpha}) \cup \xleftarrow{c}) \subseteq \xleftarrow{\mathcal{R}}$ and thus $\xleftarrow{\mathcal{R}}$ is equal to the reflexive-transitive closure of $(\bigcup_{\alpha} \triangleright_{\alpha}) \cup \xleftarrow{c}$. Therefore, it suffices to show that the relation $(\bigcup_{\alpha} \triangleright_{\alpha}) \cup \xleftarrow{c}$ is confluent. This can be done by applying the decreasing diagram theorem to the restriction of $(\bigcup_{\alpha} \triangleright_{\alpha}) \cup \xleftarrow{c}$ to meta-free terms. For this, we label $\triangleright_{\alpha}$ steps by $\alpha$ and $\xleftarrow{c}$ steps by $\perp$, extending the order on $\mathcal{L}$ to $\mathcal{L} \cup \{\perp\}$ by adding $\perp < \alpha$ for all $\alpha \in \mathcal{L}$.

We then have the following implications, in which $t_0, t_1, t_2$ are all ground: (1) if $t_1 \underset{c}{\rightleftarrows} t_0 \xrightarrow{q_1} t_2$ then $t_1 \xrightarrow{q_1} \xleftarrow{c} t_2$, by confluence of $\mathcal{R}_c$; (2) if $t_1 \underset{c}{\rightleftarrows} t_0 \xrightarrow{p_1} t_2$ then $t_1 \xrightarrow{p_1} \xleftarrow{c} t_2$, by Lemma 8; (3) if $t_1 \xleftarrow{p_1} t_0 \xrightarrow{p_2} t_2$, then $t_1 \underset{<\alpha_1}{\rightleftarrows} t'_1 \xrightarrow{q_1} = t''_1 \underset{<\alpha_1,\alpha_2}{\rightleftarrows} t''_2 = \xleftarrow{q_2} t'_2 \underset{<\alpha_2}{\rightleftarrows} t_2$ for some $t'_1, t''_1, t'_2, t''_2$ and $q_1, q_2$ not nested.

To conclude, we need to verify that only meta-free terms are used in the closing diagrams. In the case of (1) and (2) this is obvious, because only reducts
of $t_1, t_2$, which are meta-free, can appear. In the case of (3), by Lemma 1, it is enough to show that the terms $t'_1, t''_1, t'_2, t''_2$ are meta-free. Because $t''_1, t''_2$ are reducts of $t'_1, t'_2$, it suffices to show that $t'_1, t'_2$ are meta-free. Now, we argue that we can suppose wlog that $t'_1, t'_2$ are meta-free. Indeed, if $\mathcal{X}$ of arity $\{s\}$ $s'$ appears in $t'_i$, let us pick any variable $y$ of sort $s'$. Then, using Proposition 4, we can apply the substitution $\mathcal{X} \mapsto x.y$ everywhere without changing the endpoints or the shape of the diagram.

## C.2 Proof of Theorem 1

**Lemma 11 (Condition (ii)).** Under the assumptions of Theorem 1, if $t \stackrel{c}{\rightleftharpoons} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and meta-free $t, \sigma$ with $\text{dom}(\sigma) = \text{mv}(\ell)$, then $t \stackrel{c}{\rightleftharpoons} \ell[\sigma']$ for some $\sigma' \text{ with } \sigma \stackrel{c}{\rightleftharpoons} \sigma'$.

*Proof.* Suppose that we have $t \stackrel{c}{\rightleftharpoons} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and with $t, \sigma$ meta-free, and let $\sigma'$ be the $\mathcal{R}_c$ normal form of $\sigma$. Using Lemma 1 we can apply confluence to $t \stackrel{c}{\rightleftharpoons} \ell[\sigma] \stackrel{c}{\rightleftharpoons} \ell[\sigma']$ and get $t \stackrel{c}{\rightleftharpoons} t' \stackrel{c}{\rightleftharpoons} \ell[\sigma']$. However, note that $\ell[\sigma']$ is also in $\mathcal{R}_c$ normal form. Indeed, the substitution is already in normal form, and a step above it would contradict (b). Therefore, we have $t \stackrel{c}{\rightleftharpoons} t' = \ell[\sigma']$ and $\sigma \stackrel{c}{\rightleftharpoons} \sigma'$ as required.

**Lemma 12 (Condition (iii)).** Under the assumptions of Theorem 1, if $\langle u_1, u_2 \rangle$ is an $\mathcal{R}_c$-critical pair of $\ell_1 \to \alpha_1, r_1, \ell_2 \to \alpha_2, r_2 \in \mathcal{R}_{nc}$, then

$$u_1 \stackrel{<\alpha_1}{\rightleftharpoons} u'_1 \xrightarrow{\alpha_2} u''_1 \stackrel{<\alpha_1, \alpha_2}{\rightleftharpoons} u''_2 = \xrightarrow{\alpha_1} u'_2 \stackrel{<\alpha_2}{\rightleftharpoons} u_2$$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

*Proof.* Suppose that $\ell_1 \to \alpha_1, r_1, \ell_2 \to \alpha_2, r_2 \in \mathcal{R}_{nc}$ have an $\mathcal{R}_c$-critical pair $\langle u_1, u_2 \rangle$. By the definition of $\mathcal{R}_c$-critical pairs, $\langle u_1, u_2 \rangle$ is of the form $\langle (\ell_2 \{x.r_1[\text{lift}_x]\} \}_{p})[\sigma], r_2[\sigma] \rangle$ with $\sigma$ a meta-free $\mathcal{R}_c$-unifier of $x.\ell_1[\text{lift}_x] \stackrel{?}{=} x.\ell_2^p$ where $\ell_2|_p = x.\ell_2^p$. As usual we assume $\ell_1$ and $\ell_2$ have been renamed so as to be disjoint. Let us show that this $\mathcal{R}_c$-critical pair can be closed with a diagram of the shape given above.

We know that, for all $\ell_c \to r_c \in \mathcal{R}_c$, $\ell_c$ does not overlap $\ell_1, \ell_2$, hence by Lemma 3 we obtain the same for $x.\ell_1[\text{lift}_x]$ and $\ell_2|_p$. By applying Proposition 8 we therefore conclude that $x.\ell_1[\text{lift}_x] \stackrel{?}{=} x.\ell_2^p$ have a meta-free syntactic unifier $\sigma'$ with $\sigma \stackrel{c}{\rightleftharpoons} \sigma'$. Now, let us distinguish two cases.

- Suppose that $p = \varepsilon$ and that $\ell_1[\mu] = \ell_2$ and $r_1[\mu] = r_2$ for some renaming $\mu$ with $\text{dom}(\mu) = \text{mv}(\ell_1)$. Then, the critical pair is just $\langle r_1[\sigma], r_2[\sigma] \rangle$. Let $\sigma = \sigma_1 \cup \sigma_2$ and $\sigma' = \sigma'_1 \cup \sigma'_2$ be the splitting of $\sigma$ and $\sigma'$ according to the metareferences occurring in $\ell_1$ and $\ell_2$. Because $\sigma'$ unifies $\ell_1 \stackrel{?}{=} \ell_2$, we have $\ell_1[\sigma'_1] = \ell_2[\sigma'_2] = \ell_1[\mu[\sigma'_2]]$ and so $\sigma'_1 = \mu[\sigma'_2]$ by Proposition 6. Therefore, we conclude

$$r_1[\sigma] \stackrel{c}{\rightleftharpoons} r_1[\sigma'_1] = r_1[\mu][\sigma'_2] = r_2[\sigma'_2] \stackrel{c}{\rightleftharpoons} r_2[\sigma_2] = r_2[\sigma]$$
a diagram which is indeed of the required shape.

- Otherwise, either $p \neq \varepsilon$ or the rules are not the same, so they have a critical pair $\langle (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\theta], r_2[\theta]\rangle$, where $\theta$ is an mgu of $\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.\ell_2^p$. By (c), we have

$$ (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\theta] \underset{<\alpha_1}{\rightleftarrows} u'_1 \xrightarrow[\alpha_2]{q_1} = u''_1 \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2 = \xleftarrow[\alpha_1]{q_2} u'_2 \underset{<\alpha_2}{\rightleftarrows} r_2[\theta] $$

for some $u'_1, u''_1, u'_2, u''_2$ and $q_1, q_2$ non-nested. Now, because $\sigma'$ is a meta-free unifier of $\mathbf{x}.\ell_1[\text{lift}_{\mathbf{x}}] \stackrel{?}{=} \mathbf{x}.\ell_2^p$, we have $\sigma' = \theta[\mu]$ for some meta-free $\mu$. By applying $\mu$ to the diagram above and using Proposition 4, we obtain

$$ (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\theta][\mu] \underset{<\alpha_1}{\rightleftarrows} u'_1[\mu] \xrightarrow[\alpha_2]{q_1} = u''_1[\mu] \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2[\mu] = \xleftarrow[\alpha_1]{q_2} u'_2[\mu] \underset{<\alpha_2}{\rightleftarrows} r_2[\theta][\mu] $$

with $q_1, q_2$ non-nested. Finally, because we have $\sigma \dashrightarrow \sigma' = \theta[\mu]$, we obtain $(\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\sigma] \xrightarrow[c]{c} (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\theta][\mu]$ and $r_2[\sigma] \xrightarrow[c]{c} r_2[\theta][\mu]$. By composing the above diagram with these two reductions, we conclude

$$ (\ell_2\{\mathbf{x}.r_1[\text{lift}_{\mathbf{x}}]\}_p)[\sigma] \underset{<\alpha_1}{\rightleftarrows} u'_1[\mu] \xrightarrow[\alpha_2]{q_1} = u''_1[\mu] \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2[\mu] = \xleftarrow[\alpha_1]{q_2} u'_2[\mu] \underset{<\alpha_2}{\rightleftarrows} r_2[\sigma] $$

with $q_1, q_2$ non-nested.

**Theorem 1.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(a) $\mathcal{R}_c$ is confluent and terminating.

(b) For all $\ell \to r \in \mathcal{R}_{nc}$ and $\ell_c \to r_c \in \mathcal{R}_c$, $\ell_c$ does not overlap $\ell$.

(c) If $\langle u_1, u_2 \rangle$ is a critical pair of $\ell_1 \to_{\alpha_1} r_1, \ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$ u_1 \underset{<\alpha_1}{\rightleftarrows} u'_1 \xrightarrow[\alpha_2]{q_1} = u''_1 \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2 = \xleftarrow[\alpha_1]{q_2} u'_2 \underset{<\alpha_2}{\rightleftarrows} u_2 $$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.

*Proof.* Follows directly by applying Theorem 4, whose conditions are satisfied by Lemmas 11 and 12.

### C.3 Proof of Theorem 2

**Lemma 13 (Condition (ii)).** Under the assumptions of Theorem 2, if $t \underset{c}{\rightleftarrows} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and meta-free $t, \sigma$ with $\text{dom}(\sigma) = \text{mv}(\ell)$, then $t \xrightarrow{c} \ell[\sigma']$ for some $\sigma'$ with $\sigma \xrightarrow{c} \sigma'$.

*Proof.* Suppose that we have $t \underset{c}{\rightleftarrows} \ell[\sigma]$ for some $\ell \to r \in \mathcal{R}_{nc}$ and some meta-free $t, \sigma$ with $\text{dom}(\sigma) = \text{mv}(\ell)$. Now let $\tau$ be the unique substitution equalized for $\hat{\ell}$ satisfying $\hat{\tau} = \sigma$. Therefore, $t \underset{c}{\rightleftarrows} \hat{\ell}[\tau]$. Using Lemma 1, we can apply
confluence to get $t \underset{c}{\longrightarrow} t' \underset{c}{\longleftarrow} \hat{\ell}[\tau]$. Because of condition (b), by iterating Lemma 4 we obtain $t' = \hat{\ell}[\tau']$ with $\tau \underset{c}{\longrightarrow} \tau'$. Because $\tau$ is equalized and $\tau \underset{c}{\longrightarrow} \tau'$, by confluence we can equalize once again the non-linear positions in $\tau'$, and thus $\tau' \underset{c}{\longrightarrow} \tau''$ with $\tau''$ equalized. We conclude $t \underset{c}{\longrightarrow} \hat{\ell}[\tau''] = \hat{\ell}[\tau'']$ and from $\tau \underset{c}{\longrightarrow} \tau''$ we get $\sigma = \tilde{\tau} \underset{c}{\longrightarrow} \tilde{\tau}''$.

**Lemma 14 (Condition (iii)).** Under the assumptions of Theorem 2, if $\langle u_1, u_2 \rangle$ is an $\mathcal{R}_c$-critical pair of $\ell_1 \to_{\alpha_1} r_1, \ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$u_1 \underset{<\alpha_1}{\rightleftarrows} u'_1 \xrightarrow[\alpha_2]{q_1} u''_1 \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2 \xrightarrow[\alpha_1]{q_2} u'_2 \underset{<\alpha_2}{\rightleftarrows} u_2$$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

*Proof.* Suppose that $\ell_1 \to_{\alpha_1} r_1, \ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$ have an $\mathcal{R}_c$-critical pair $\langle u_1, u_2 \rangle$. By the definition of $\mathcal{R}_c$-critical pairs, $\langle u_1, u_2 \rangle$ is of the form $\langle (\ell_2[\mathbf{x}.r_1[\text{lift}_x]])_p[\tau], r_2[\tau] \rangle$ with $\tau$ a meta-free $\mathcal{R}_c$-unifier of $\mathbf{x}.\ell_1[\text{lift}_x] \stackrel{?}{=} \mathbf{x}.\ell_2^p$ where $\ell_2|_p = \mathbf{x}.\ell_2^p$. As usual we assume $\ell_1$ and $\ell_2$ have been renamed so as to be disjoint. Let us now show that this $\mathcal{R}_c$-critical pair can be closed with a diagram of the shape given above.

By Lemma 3 and (b), no $\text{lhs in } \mathcal{R}_c$ overlaps $\mathbf{x}.\hat{\ell}_1[\text{lift}_x]$ or $\mathbf{x}.\hat{\ell}_2^p$. By Proposition 7, the same holds for $\mathbf{x}.\hat{\ell}_1[\text{lift}_x]$, therefore we can apply Corollary 1 and deduce that $\mathbf{x}.\ell_1[\text{lift}_x] \stackrel{?}{=} \mathbf{x}.\ell_2^p$ admits a meta-free $\mathcal{R}_c$-cyclic unifier $\sigma'$ with $\sigma \underset{c}{\longrightarrow} \sigma'$, where $\sigma'$ is the unique substitution satisfying $\tilde{\sigma} = \tau$. Now, let us distinguish two cases.

- Suppose that $p = \varepsilon$ and that $\ell_1[\mu] = \ell_2$ and $r_1[\mu] = r_2$ for some renaming $\mu$ with $\text{dom}(\mu) = \text{mv}(\ell_1)$. Then, the critical pair is just $\langle r_1[\tau], r_2[\tau] \rangle$. Moreover, note that it is easy to define a renaming $\mu'$ with $\text{dom}(\mu') = \text{mv}(\ell_1)$ that satisfies $\widehat{\ell_1[\mu]} = \hat{\ell}_1[\mu']$ and $(\mu'[\tau'])^# = \mu[\tau'^#]$ for all $\tau'$ with $\text{dom}(\tau') = \text{mv}(\hat{\ell}_2)$. Now, let $\sigma = \sigma_1 \cup \sigma_2$ and $\sigma' = \sigma'_1 \cup \sigma'_2$ be the splitting of $\sigma$ and $\sigma'$ according to the metavariables appearing in $\hat{\ell}_1$ and $\hat{\ell}_2$. Because $\sigma'$ unifies $\hat{\ell}_1 \stackrel{?}{=} \hat{\ell}_2$, we have $\hat{\ell}_1[\sigma'_1] = \hat{\ell}_2[\sigma'_2] = \widehat{\ell_1[\mu]}[\sigma'_2] = \hat{\ell}_1[\mu'[\sigma'_2]]$ and so $\sigma'_1 = \mu'[\sigma'_2]$ by Proposition 6. Finally, note that $\tau = \tilde{\sigma} = \sigma'^#$, so we conclude

$$r_1[\tau] = r_1[\sigma'_1] \underset{c}{\longrightarrow} r_1[\sigma'_1^#] = r_1[(\mu'[\sigma'_2])^#] = r_1[\mu][\sigma'_2^#] = r_2[\sigma'_2^#] \underset{c}{\longleftarrow} r_2[\sigma'_2] = r_2[\tau]$$

a diagram which is indeed of the required shape.

- Otherwise, either $p \neq \varepsilon$ or the rules are not the same, so they have an $\mathcal{R}_c$-cyclic critical pair $\langle (\ell_2[\mathbf{x}.r_1[\text{lift}_x]])_p[\theta^#], r_2[\theta^#], \simeq \rangle$, where $(\theta, \simeq)$ is a dcu of $\mathbf{x}.\ell_1[\text{lift}_x] \stackrel{?}{=} \mathbf{x}.\ell_2^p$. By (c), we have

$$(\ell_2[\mathbf{x}.r_1[\text{lift}_x]])_p[\theta^#] \underset{\simeq; < \alpha_1}{\rightleftarrows} u'_1 \xrightarrow[\alpha_2]{q_1} u''_1 \underset{\simeq; < \alpha_1, \alpha_2}{\rightleftarrows} u''_2 \xrightarrow[\alpha_1]{q_2} u'_2 \underset{\simeq; < \alpha_2}{\rightleftarrows} r_2[\theta^#]$$

for some $u'_1, u''_1, u'_2, u''_2$ and $q_1, q_2$ non-nested. Now, because $\sigma'$ is a meta-free $\mathcal{R}_c$-cyclic unifier of $\mathbf{x}.\ell_1[\text{lift}_x] \stackrel{?}{=} \mathbf{x}.\ell_2^p$, by Proposition 1 we have $\sigma' = \theta[\mu]$
for some meta-free $\mu$ satisfying $\simeq$. By applying $\mu$ to the diagram above, and using Proposition 4 and the fact that $\mu$ realizes $\simeq$, we get

$$ (\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\theta^{\#}][\mu] \underset{<\alpha_1}{\rightleftarrows} u'_1[\mu] \xrightarrow[\alpha_2]{q_1} u''_1[\mu] \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2[\mu] = \xleftarrow[\alpha_1]{q_2} u'_2[\mu] \underset{<\alpha_2}{\rightleftarrows} r_2[\theta^{\#}][\mu] $$

with $q_1, q_2$ non-nested. Now, we already know that $\sigma \underset{c}{\longrightarrow} \sigma' = \theta[\mu]$ with $\sigma$ equalized, hence $\tau = \tilde{\sigma} = \sigma^{\#} \underset{c}{\longrightarrow} (\theta[\mu])^{\#} = \theta^{\#}[\mu]$. So we have $(\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\tau] \underset{c}{\longrightarrow} (\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\theta^{\#}][\mu]$ and $r_2[\tau] \underset{c}{\longrightarrow} r_2[\theta^{\#}][\mu]$. By composing these reductions with the previous diagram, we conclude

$$ (\ell_2\{\mathbf{x}.r_1[\mathrm{lift}_{\mathbf{x}}]\}_p)[\tau] \underset{<\alpha_1}{\rightleftarrows} u'_1[\mu] \xrightarrow[\alpha_2]{q_1} u''_1[\mu] \underset{<\alpha_1, \alpha_2}{\rightleftarrows} u''_2[\mu] = \xleftarrow[\alpha_1]{q_2} u'_2[\mu] \underset{<\alpha_2}{\rightleftarrows} r_2[\tau] $$

with $q_1, q_2$ non-nested.

**Theorem 2.** Given some labeled rewrite system $\mathcal{R}$, suppose that:

(a) $\mathcal{R}_c$ is confluent.

(b) For all $\ell \to r \in \mathcal{R}_{nc}$ and $\ell_c \to r_c \in \mathcal{R}_c$, $\ell_c$ does not overlap $\ell$.

(c) If $\langle u_1, u_2, \simeq \rangle$ is an $\mathcal{R}_c$-cyclic critical pair of $\ell_1 \to_{\alpha_1} r_1, \ell_2 \to_{\alpha_2} r_2 \in \mathcal{R}_{nc}$, then

$$ u_1 \underset{\simeq; < \alpha_1}{\rightleftarrows} u'_1 \xrightarrow[\alpha_2]{q_1} u''_1 \underset{\simeq; < \alpha_1, \alpha_2}{\rightleftarrows} u''_2 = \xleftarrow[\alpha_1]{q_1} u'_2 \underset{\simeq; < \alpha_2}{\rightleftarrows} u_2 $$

for some $u'_1, u''_1, u'_2, u''_2$ with $q_i$ non-nested in $u'_i$.

Then $\mathcal{R}$ is confluent.

*Proof.* Follows directly by applying Theorem 4, whose conditions are satisfied by Lemmas 13 and 14.