text:
\section{Introduction}
\label{sec:intro}

We present two results for proving confluence of first-order
left-linear term rewrite systems, which extend and generalise
three classical results: Knuth and Bendix' criterion~\cite{Knut:Bend:70}
and strong and parallel closedness due to Huet~\cite{Huet:80}.
Our idea is to reduce confluence of a term rewrite system $\Rultrs{\aRul}$
to that of a subsystem $\Rultrs{\dRul}$ comprising rewrite rules
needed for \emph{closing} the critical pairs of $\Rultrs{\aRul}$.
In Section~\ref{sec:hot} we introduce \emph{hot-decreasingness},
requiring that critical pairs can be closed using rules
that are either below those in the peak or in a
terminating subsystem $\Rultrs{\dRul}$.
In Section~\ref{sec:cpcs} we introduce the notion of a
\emph{critical-pair-closing system} and present a confluence-preservation
result based on relative termination $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ of
the duplicating part $\Rultrs{\dRul}_{\m{d}}$ of $\Rultrs{\dRul}$.
For the left-linear systems we consider, our first criterion
generalises both Huet's parallel closedness and Knuth and Bendix' criterion,
and the second Huet's strong closedness.
In Section~\ref{sec:implementation}, we assess viability of the new techniques,
reporting on their implementation and empirical results.

Huet's parallel closedness result relies on the notion
of overlap whose geometric intuition is subtle~\cite{Baad:Nipk:98,Nage:Midd:16}, and
reasoning becomes intricate for development closedness as covered by Theorem~\ref{thm:hot}.
We factor the classical theory of overlaps
and critical pairs through the \emph{encompassment} lattice in which overlapping
redex-patterns \emph{is} taking their join and the amount of overlap between
redex-patterns is computed \emph{via} their meet,
thus allowing to reason algebraically about overlaps.
Methodologically, our contribution here is the introduction of
the lattice-theoretic language itself, relevant as it allows one to
reason about occurrences of patterns\footnote{%
Modelled in various ways, via e.g.:
tree homomorphisms (tree automata~\cite{Tata:07}),
term-operations (algebra),
context-variables,
labelling (rippling~\cite{Bund:etal:05}), to name a few.
}
and their amount of (non-)overlap, omnipresent in deduction.
Technically, whereas Huet's critical pair lemma~\cite{Huet:80} is well-suited
for proving confluence of \emph{terminating} TRSs, it is ill-suited to do so
for \emph{orthogonal} TRSs.
Our lattice-theoretic results remedy this, allowing to decompose a reduction $R$ both
\emph{horizontally} (as $\binap{\srelsco}{R_1}{R_2}$) and
\emph{vertically} (as $\substra{x}{R_2}{R_1}$), enabling both
termination and orthogonality reasoning in confluence proofs
(Theorem~\ref{thm:hot}).

In the last decade various classical confluence results for \emph{term}
rewrite systems have been factored through the decreasing diagrams
method~\cite{Oost:94,Oost:08} for proving confluence of \emph{abstract} rewrite systems,
often leading to generalisations along the way:
e.g.\ Felgenhauer's multistep labelling~\cite{Felg:15} generalises
Okui's simultaneous closedness~\cite{Okui:98},
the layer framework~\cite{Felg:Midd:Zank:Oost:15}
generalises Toyama's modularity~\cite{Toya:87},
critical pair systems~\cite{Hiro:Midd:11} generalise both
orthogonality~\cite{Rose:73} and Knuth and Bendix' criterion~\cite{Knut:Bend:70},
and Jouannaud and Liu generalise, among others~\cite{Liu:16},
parallel closedness, but in a way we do not know
how to generalise to development closedness~\cite{Oost:97}.
This paper fits into this line of research.\footnote{%
\ifextendedversion
For space reasons we have omitted the proof by decreasing diagrams of Theorem~\ref{thm:cpcs}
from the main text.  See the appendix for omitted proofs.
\else
For space reasons we have omitted the proof by decreasing diagrams of Theorem~\ref{thm:cpcs}.
\fi
}

We assume the reader is familiar
with term rewriting~\cite{Ders:Joua:90,Baad:Nipk:98,Tere:03} in general
and confluence methods~\cite{Knut:Bend:70,Huet:80,Oost:08} in particular.
Notions not explicitly defined in this paper can all be found in those
works.

\section{Preliminaries on decreasingness and encompassment}
\label{sec:prelims}

We recall the key ingredients of
the decreasing diagrams method for proving confluence,
see~\cite{Ohle:02,Tere:03,Oost:08,Liu:16},
and revisit the classical notion of critical pair,
recasting its traditional account~\cite{Knut:Bend:70,Huet:80,Baad:Nipk:98}
based on redexes (substitution instances of left-hand sides)
into one based on redex-patterns (left-hand sides).

\subsubsection{Decreasingness}
\label{sec:decreasing}

Consider an ARS comprising an $I$-indexed relation
${\to} = \bigcup_{{\ell} \in I} {\to_{\ell}}$ equipped with a
well-founded strict order $\succ$.
We refer to
$\{ {\kappa} \in I \mid {\ell} \succ {\kappa} \}$ by $\orddwna{{\ell}}$, and to
$\orddwna{{\ell}} \cup \orddwna{{\kappa}}$ by $\orddwna{{\ell},{\kappa}}$.
For a subset $J$ of $I$ we define $\to_J$ as $\bigcup_{{\ell} \in J} {\to_{\ell}}$.
\begin{definition} \label{def:decreasing}
  A diagram for a peak $\iarsinva{{\ell}}{{b}}{\iarsa{{\kappa}}{\aobj}{{c}}}$
  is \emph{decreasing} if its closing conversion has shape
  $\relap{\binap{\srelsco}{\ip{\aarsequ}{\orddwna{{\ell}}}
}{\binap{\srelsco}{\ip{\aarsref}{{\kappa}}
}{\binap{\srelsco}{\ip{\aarsequ}{\orddwna{{\ell},{\kappa}}}
}{\binap{\srelsco}{\aiarsinvref{{\ell}}
        }{\ip{\aarsequ}{\orddwna{{\kappa}}}
        }}}}}{{b}}{{c}}$.

  An ARS in this setting is called \emph{decreasing} if every peak
  can be completed into a decreasing diagram.
\end{definition}
One may think of decreasing diagrams as combining the diamond
property~\cite[Theorem~1]{Newm:42} (via the steps in the closing conversion
with labels ${\ell}$, ${\kappa}$) at the basis of confluence of \emph{orthogonal}
systems~\cite{Chur:Ross:36,Rose:73}, with local
confluence diagrams~\cite[Theorem~3]{Newm:42} (via the conversions with
labels $\orddwna{{\ell},{\kappa}}$) at the basis of
confluence of \emph{terminating} systems~\cite{Knut:Bend:70,Mayr:Nipk:98}.
\begin{theorem}[\textnormal{\cite{Oost:94,Oost:08}}]  \label{thm:dd:complete}
An ARS is confluent if it is decreasing.
Conversely, every \emph{countable} ARS that is confluent, is decreasing
for some set of indices $I$.
\end{theorem}
For the converse part it suffices that the set of \emph{labels} $I$ is a doubleton,
a result that can be reformulated without referring to decreasing diagrams, as follows.
\begin{lemma}[\textnormal{\cite{Endr:Klop:Over:18}}]
  \label{lem:countable:confluent:spanning}
  A countable confluent rewrite relation has a spanning forest.
\end{lemma}
Here a spanning forest for ${\to}$ is a relation $\relap{\srelle}{\Blue{\triangleright}}{{\to}}$
that is \emph{spanning} ($\relap{\sreleq}{\reltre{{\barsinv\kern-.485em\bars}}}{\reltre{\aarssym}}$) and a \emph{forest}, i.e.\
deterministic ($\relap{\barsinv}{{b}}{\relap{\Blue{\triangleright}}{\aobj}{{c}}}$ implies $\relap{\sobjeq}{{b}}{{c}}$)
and acyclic.

\subsubsection{Critical peaks revisited}
\label{sec:critical:peaks}

We introduce \emph{clusters} as the structures obtained \emph{after}
the matching of the left-hand side of a rule in a rewrite step,
but \emph{before} its replacement by the right-hand side.
When proving the aforementioned results in Sections~\ref{sec:hot}
and \ref{sec:cpcs}, we use them as a tool to analyse overlaps and critical peaks.
To illustrate our notions we use the following running example.
We refer to \cite{Tere:03,Hiro:Midd:11} for the notions of multistep.
\begin{example} \label{exa:cluster:1}
  In the TRS $\Rultrs{\aRul}$ with $\funap{\arul}{x} \hastype \binap{\srulstr}{f(f(x))}{g(x)}$
  the term ${t} \isdefd f(f(f(f(a))))$  allows the step
  $f(\funap{\arul}{f(a)}) \hastype \relap{\aars}{{t}}{f(g(f(a)))}$ and
  multistep $\funap{\arul}{\funap{\arul}{a}} \hastype \relap{\aarsdev}{{t}}{g(g(a))}$.
\end{example}
Here $f(\funap{\arul}{f(a)})$ and $\funap{\arul}{\funap{\arul}{a}}$ are so-called proofterms,
\emph{terms} representing \emph{proofs} of rewritability in rewriting logic~\cite{Mese:92,Tere:03}.
The source of a proofterm can be computed by the $2$nd-order substitution
$\mathsf{src}$ of the left-hand side of the rule for the rule symbol\footnote{%
$\mathsf{src}$ can be viewed as tree homomorphism~\cite{Tata:07},
or as a term algebra $\funap{\algap{\salglhs}{{\varrho}}}{\vec{{t}}} \isdefd \substra{\vec{{x}}}{\vec{{t}}}{{\ell}}$.}
$\subap{\mathsf{src}}{f(\funap{\arul}{f(a)})} \isdefd
 \relap{\strmeq}{\msubstra{{\varrho}}{\lambda x.f(f(x))}{f(\funap{\arul}{f(a)})}
      }{f(f(f(f(a))))
      }$, and, \emph{mutatis mutandis}, the same for the target via $\mathsf{tgt}$.
Proofclusters, introduced here,
abstract from such proofterms by allowing to represent the matching and substitution phases
of multisteps as well, by means of let-expressions.
\begin{example} \label{exa:cluster:2}
  The multistep in Example~\ref{exa:cluster:1}
  comprises three phases~\cite[Chapter~4]{Oost:94}:
  \begin{enumerate}
  \item
    $\clslet{\amtrmvar,\varmvar\btrmvar\hspace{-0.52ex}}{\hspace{-0.52ex}\lambda x.f(f(x)),\lambda y.f(f(y))}{\mtrmvara{\funap{\bmtrmvar}{a}}}$
    denotes \emph{matching} $f(f(x))$ twice;
  \item
    $\clslet{\amtrmvar,\varmvar\btrmvar\hspace{-0.52ex}}{\hspace{-0.52ex}\lambda x.\funap{\arul}{x},\lambda x.\funap{\arul}{x}}{\mtrmvara{\funap{\bmtrmvar}{a}}}$
    denotes \emph{replacing} by ${\varrho}$ twice;
  \item

    $\clslet{\amtrmvar,\varmvar\btrmvar\hspace{-0.52ex}}{\hspace{-0.52ex}\lambda x.g(x),\lambda x.g(x)}{\mtrmvara{\funap{\bmtrmvar}{a}}}$
    denotes \emph{substituting} $g(x)$ twice.
  \end{enumerate}
\end{example}
To represent these we assume to have
\emph{proofterms} ${t}, {s}, {u}, \ldots$ over a signature comprising
\emph{function} symbols $\asym, {g}, {h}, \ldots$,
\emph{rule} symbols ${\varrho}, {\theta}, {\eta}, \ldots$,
$2$nd-order variables $\amtrmvar, \varmvar\btrmvar, \varmvar\ctrmvar, \ldots$,
all having natural number arities,
and $1$st-order variables ${x}, {y}, {z}, \ldots$
(with arity ${0}$)
We call proofterms without $2$nd-order variables or rule symbols,
\emph{$1$st-order} proofterms respectively \emph{terms},
ranged over by ${M}$, ${N}$, ${L}$, $\ldots$.
\begin{definition}
  A \emph{proofcluster} is a let-expression
  $\clslet{\vec{\amtrmvar}}{\vec{Q}}{{t}}$, where
  \begin{itemize}
  \item
    $\vec{\amtrmvar}$ is a
    vector $\aimtrmvar{{1}},\ldots,\aimtrmvar{{n}}$
    of (pairwise distinct) second-order variables;
  \item
    $\vec{Q}$ is a vector of length ${n}$
    of closed $\lambda$-terms
    $\ip{Q}{{i}} = \lambda \vec{\ip{\atrmvar}{{i}}}.\ip{\btrm}{{i}}$,
    where $\ip{\btrm}{{i}}$ is a proofterm
    and the length of the vector $\vec{\ip{\atrmvar}{{i}}}$ of variables is the arity of $\aimtrmvar{{i}}$; and
  \item
    ${t}$ is a proofterm, the \emph{body}, with its $2$nd-order variables among $\vec{\amtrmvar}$.
  \end{itemize}
  Its \emph{denotation} $\algtrm{\clslet{\vec{\amtrmvar}}{\vec{Q}}{{t}}}$
  is $\msubstra{\vec{\amtrmvar}}{\vec{Q}}{{t}}$.
  It is a \emph{cluster} if $\ip{\btrm}{{1}},\ldots,\ip{\btrm}{{n}},{t}$ are terms.
\end{definition}
We let $\acls$, ${\zeta}$, ${\xi}$, $\ldots$ range over (proof)clusters.
They denote (proof)terms.
\begin{example} \label{exa:cluster:3}
  Using $\acls$, ${\zeta}$, ${\xi}$ for the three
  let-expressions in Example~\ref{exa:cluster:2}, each
  is a proofcluster and $\acls$, ${\xi}$ are clusters.
  Their denotations are the
  term $\algtrm{\acls} \isdefd \relap{\strmeq}{f(f(f(f(a))))}{{t}}$,
  proofterm $\algtrm{{\zeta}} \isdefd \funap{\arul}{\funap{\arul}{a}}$, and
  term $\algtrm{{\xi}} \isdefd g(g(a))$.
\end{example}
We assume the usual variable renaming conventions, both for the $2$nd-order
ones in let-binders and the $1$st-order ones in $\lambda$-abstractions.
We say a proofcluster $\acls$ is \emph{linear} if every (let or $\lambda$) binding
binds exactly once, and~\emph{canonical}~\cite{Meti:83}
if, when a binding variable occurs to the left of another such (of the same type),
then the first bound occurrence of the former occurs before that of the latter
in the pre-order walk of the relevant proofterm.
\begin{example} \label{exa:cluster:4}
  Let ${\zeta}'$ and ${\xi}'$ be the clusters
  $\clslet{\amtrmvar}{\lambda x.f(f(x))}{\mtrmvara{\mtrmvara{a}}}$ and
  $\clslet{\amtrmvar,\varmvar\btrmvar}{\lambda yz.f(f(y)),\lambda x.f(f(x))}{\funap{\bmtrmvar}{\mtrmvara{a,f(a)}}}$.
  Each of $\acls$, ${\zeta}'$, ${\xi}'$ denotes ${t}$ in Example~\ref{exa:cluster:1}.
  The cluster $\acls$ is linear and canonical,
  ${\zeta}'$ is canonical but not linear ($\amtrmvar$ occurs twice in the body), and
  ${\xi}'$ is neither linear ($z$ does not occur in $f(y)$)
  nor canonical ($\varmvar\btrmvar$ occurs outside of $\amtrmvar$ in the body).
\end{example}
We adopt the convention that absent $\lambda$-binders are inserted linearly, canonically;
$\clslet{\amtrmvar}{f(f(x))}{\mtrmvara{\mtrmvara{a}}}$ is ${\zeta}'$.
Clusters witness encompassment ${\trmencref{}{}}$~\cite{Ders:Joua:90}.
\begin{proposition} \label{prop:encompassment}
  $\relap{\makebox[0pt]{\makebox[7.5pt][r]{\raise 0.6pt \hbox{$\cdot$}}}{\trianglerighteq}}{{t}}{{s}}$ iff
  $\exists {u},\amtrmvar$ s.t.\
  $\relap{\strmeq}{\algtrm{\clslet{\amtrmvar}{{s}}{{u}}}}{{t}}$
  and $\amtrmvar$ occurs once in ${u}$.
\end{proposition}
We define the \emph{size} $\funap{\trmsiz{\_}}{{t}}$ of a proofterm ${t}$
in a way that is compatible with encompassment.
Formally, $\funap{\trmsiz{\_}}{{t}}$ is the pair comprising the number
of non-$1$st-order-variable symbols in ${t}$, and the sum over the $1$st-order variables ${x}$,
of the \emph{square} of the number of occurrences of ${x}$ in ${t}$.
Then $\relap{\snatgt}{\funap{\trmsiz{\_}}{{t}}}{\funap{\trmsiz{\_}}{{s}}}$ if $\relap{\strmenc}{{t}}{{s}}$,
where we (ab)use ${>}$ to denote the lexicographic
product of the greater-than relation with itself,
e.g. $\relap{\snatgt}{\funap{\trmsiz{\_}}{g(a,a)} \isdefd \pair{{3}}{{0}}
    }{\relap{\snatgt}{\funap{\trmsiz{\_}}{g(x,x)} \isdefd \pair{{1}}{{4}}
           }{\funap{\trmsiz{\_}}{g(x,y)} \isdefd \pair{{1}}{{2}}
           }}$.
For a proofcluster $\acls$ given by
$\clslet{\vec{{x}}}{\vec{{s}}}{{t}}$
its \emph{pattern}-size $\clspsz{\acls}$ is $\natSum{{i}}{\funap{\trmsiz{\_}}{\ip{\btrm}{{i}}}}$
(adding component-wise, with empty sum $\pair{{0}}{{0}}$)
and its \emph{body}-size $\clsbsz{\acls}$ is $\funap{\trmsiz{\_}}{{t}}$.
Encompassment ${\trmencref{}{}}$ is at the basis of the theory of reducibility~\cite[Section~3.4.2]{Tata:07}:
${t}$ is reducible by a rule $\binap{\srulstr}{{\ell}}{{r}}$ iff $\relap{\makebox[0pt]{\makebox[7.5pt][r]{\raise 0.6pt \hbox{$\cdot$}}}{\trianglerighteq}}{{t}}{{\ell}}$.
For instance,
$\clslet{\amtrmvar}{f(f(x))}{f(\mtrmvara{f(a)})}$ is a witness
to reducibility of ${t}$ in Example~\ref{exa:cluster:1}.
We call it, or simply $f(f(x))$, a pattern in ${t}$.
\begin{definition} \label{def:pattern}
  Let $\acls$ be a canonical linear proofcluster $\clslet{\vec{\amtrmvar}}{\vec{{s}}}{{t}}$
  with term ${t}$.
  We say $\acls$ is a \emph{multipattern} if each $\ip{\btrm}{{i}}$ is
  a non-variable $1$st-order term, and
  $\acls$ is a \emph{multistep} if each $\ip{\btrm}{{i}}$
  has shape $\funap{\arul}{\vec{{x}}}$, i.e.\ a rule symbol applied to
  a sequence of pairwise distinct variables.
  If $\vec{\amtrmvar}$ has length ${1}$ we drop the prefix `multi'.
\end{definition}
We use $\aStp,{\Psi},{\Omega},\ldots$ to range over multisteps, and $\astp,{\psi},{\omega},\ldots$
to range over steps. Taking their denotation yields the usual multistep~\cite{Tere:03,Hiro:Midd:11}
and step ARSs ${\arsdev}$ and~${\to}$ underlying a TRS $\Rultrs{\aRul}$.
These can be alternatively obtained by first applying $\mathsf{src}$ and $\mathsf{tgt}$
(of which only the former is guaranteed to yield a multipattern, by left-linearity)
and then taking denotations:
$\relap{\strmeq}{\algtrm{\subap{\mathsf{src}}{\aStp}}
      }{\subap{\mathsf{src}}{\algtrm{\aStp}}
      }$ and
$\relap{\strmeq}{\algtrm{\subap{\mathsf{tgt}}{\aStp}}
      }{\subap{\mathsf{tgt}}{\algtrm{\aStp}}
      }$.
Pattern- and body-sizes of multipatterns are compositional.
\begin{proposition} \label{prop:multipattern:size}
  For multipatterns $\acls$,$\vec{\acls}$ if
  $\relap{\strmeq}{\acls}{\substra{\vec{{x}}}{\vec{\acls}}{\ip{\acls}{{0}}}}$
  with each variable among $\vec{{x}}$ occurring once in the body of $\ip{\acls}{{0}}$, then
  $\relap{\snateq}{\clspsz{\acls}}{\natSum{{i}}{\ip{\acls}{{i}}}}$, and
  $\relap{\snatge}{\clsbsz{\acls}}{\clsbsz{\ip{\acls}{{i}}}}$ for all ${i}$,
  with strict inequality holding in case the substitution is not a bijective renaming.
  Here multipattern-substitution substitutes in the body and combines let-bindings.
\end{proposition}
Multipatterns are ordered by refinement $\sclsle$.
\begin{definition} \label{def:refinement}
  Let $\acls$ and ${\zeta}$ be multipatterns
  $\clslet{\vec{\amtrmvar}}{\vec{{s}}}{{t}}$ and
  $\clslet{\vec{\varmvar\btrmvar}}{\vec{{u}}}{{w}}$.
  We say $\acls$ \emph{refines} ${\zeta}$

  and write $\relap{\sclsle}{\acls}{{\zeta}}$,
  if there is a $2$nd-order substitution ${\sigma}$ on $\vec{\varmvar\btrmvar}$
  with $\relap{\strmeq}{\subap{\asub}{{w}}}{{t}}$ and
  $\relap{\strmeq}{\algtrm{\clslet{\vec{\amtrmvar}
                        }{\vec{{s}}
                        }{\subap{\asub}{\imtrmvarb{{i}}{\vec{\ip{\btrmvar}{{i}}}}}}
                        }
        }{\ip{\ctrm}{{i}}
        }$
  for all ${i}$,
  with $\vec{\ip{\btrmvar}{{i}}}$ the variables of $\ip{\ctrm}{{i}}$.
\end{definition}
\begin{example} \label{exa:cluster:6}
  We have $\relap{\sclsle}{\acls}{\acls'}$ with $\acls'$ being $\clslet{\varmvar\ctrmvar}{f(f(f(f(z))))}{\funap{\cmtrmvar}{a}}$,
  and $\acls$ as in Example~\ref{exa:cluster:3},
  as witnessed by the $2$nd-order substitution mapping $\varmvar\ctrmvar$ to $\lambda {x}.\mtrmvara{\funap{\bmtrmvar}{{x}}}$.
\end{example}
\begin{lemma} \label{lem:lattice}
  $\sclsle$ is a finite distributive lattice~\cite{Dave:Prie:90} on
  multipatterns denoting a $1$st-order term ${t}$, with least element $\clsbot$ the empty let-expression
  $\clslet{}{}{{t}}$, and greatest element $\clstop$ of shape
  $\clslet{\amtrmvar}{{t}'}{\mtrmvara{\vec{{x}}}}$ with
  $\vec{{x}}$ the vector of variables in ${t}$.
\end{lemma}
\begin{proof}[Idea]
  Although showing that $\sclsle$ is reflexive and transitive is easy,
  showing anti-symmetry or existence of/constructions
  for meets ${\sqcap}$ and joins ${\sqcup}$, directly is not.
  Instead, it \emph{is} easy to see that each multipattern
  $\clslet{\vec{\amtrmvar}}{\vec{{s}}}{{t}}$ is determined by the set
  of the (non-empty, convex,\footnote{%
Here convex means that for each pair of positions $p$,$q$ in
the set, all positions on the shortest path from $p$ to $q$
in the term tree are also in the set, cf.~\cite[Definition~8.6.21]{Tere:03}.
}
   pairwise disjoint) sets of node
  positions of its patterns $\ip{\btrm}{{i}}$ in ${t}$, and vice versa.
  For instance, the multipatterns
  $\acls$ and $\acls'$ in Example~\ref{exa:cluster:6} are determined by
  $\setstr{\setstr{\varepsilon,1},
           \setstr{\possco{1}{1},\possco{1}{\possco{1}{1}}}}$ and
  $\setstr{\setstr{\varepsilon,1,\possco{1}{1},
                   \possco{1}{\possco{1}{1}}
                  }}$.
  Viewing multipatterns as sets in that way
  $\relap{\sclsle}{\acls}{{\zeta}}$ iff

  $\forall\binap{\ssetin}{\aPos}{\acls}$, $\exists\binap{\ssetin}{Q}{{\zeta}}$ with $\relap{\ssetle}{\aPos}{Q}$.
  Saying $\binap{\ssetin}{\aPos,Q}{\binap{\ssetlub}{\acls}{{\zeta}}}$
  have \emph{overlap} if $\relap{\ssetneq}{\binap{\ssetglb}{\aPos}{Q}}{\setemp}$,
  denoted by $\relap{\sclsovl}{\aPos}{Q}$, characterising meets and joins now also is easy:
  $\binap{\sclsglb}{\acls}{{\zeta}} \isdefd
   \setabs{\binap{\ssetglb}{\aPos}{Q}
         }{\text{$\binap{\ssetin}{\aPos}{\acls}$, $\binap{\ssetin}{Q}{{\zeta}}$, and $\relap{\sclsovl}{\aPos}{Q}$}}$, and
  $\binap{\sclslub}{\acls}{{\zeta}} \isdefd
   \setabs{\setLub{}{\aiPos{\sclsovl}}
         }{\binap{\ssetin}{\aPos}{\binap{\ssetlub}{\acls}{{\zeta}}}
         }$, where
  $\aiPos{\sclsovl} \isdefd \setabs{\binap{\ssetin}{Q}{\binap{\ssetlub}{\acls}{{\zeta}}}}{\relap{\sclsovlequ}{\aPos}{Q}}$,
  i.e.\ the sets connected to $\aPos$ by successive overlaps.
  On this set-representation $\sclsle$ can be shown to be a finite distributive lattice
  by set-theoretic reasoning,
  using that the intersection of two overlapping patterns is a pattern again\footnote{%
This fails for, e.g., connected graphs; these may fall apart into non-connected ones.
}.
  For instance, $\clsbot$ \emph{is} the empty set and
  $\clstop$ \emph{is} the singleton containing the set of all non-variable positions in ${t}$.
  \qed
\end{proof}
The (proof of the) lemma allows to freely switch between viewing multisteps and multipatterns as
let-expressions and as sets of sets of positions,
and to reason about (non-)overlap of multipatterns and multisteps in lattice-theoretic terms.
We show any multistep $\aStp$ can be
decomposed \emph{horizontally}
as $\astp$ followed by $\stpres{\aStp}{\astp}$
for any step $\binap{\sstpin}{\astp}{\aStp}$~\cite{Hiro:Midd:11,Oost:97},
and \emph{vertically} as some vector $\vec{\aStp}$
substituted in a prefix $\ip{\aStp}{0}%\mathsf{out}}$ of $\aStp$,
and that peaks can be decomposed correspondingly.
\begin{definition} \label{def:critical}
  For a pair of multipatterns $\acls$,${\zeta}$ denoting the same term
  its \emph{amount} of overlap\footnote{%
For the amount of overlap for \emph{redexes} in parallel reduction $\mathrel{\wash{\mbox{}\,\,\,\prsymbol}\mathord{\longrightarrow}}$,
see e.g.~\cite{Huet:80,Baad:Nipk:98,Nage:Midd:16}.}
   and non-overlap is
  $\binap{\spkovl}{\acls}{{\zeta}} \isdefd \clspsz{\binap{\sclsglb}{\acls}{{\zeta}}}$
  respectively
  $\binap{\spkprt}{\acls}{{\zeta}} \isdefd \clsbsz{\binap{\sclslub}{\acls}{{\zeta}}}$,
  we say $\acls$,${\zeta}$ is \emph{overlapping} if
  $\relap{\sclsneq}{\binap{\sclsglb}{\acls}{{\zeta}}}{\clsbot}$,
  and \emph{critically} overlapping if moreover
  $\relap{\sclseq}{\binap{\sclslub}{\acls}{{\zeta}}}{\clstop}$
  and $\relap{\strmeq}{\algtrm{\acls}}{\algtrm{{\zeta}}}$ is linear.
  This extends to peaks $\iarsdevinva{\aStp}{{s}}{\iarsdeva{{\Psi}}{{t}}{{u}}}$ via
  $\subap{\mathsf{src}}{\aStp}$ and $\subap{\mathsf{src}}{{\Psi}}$.
\end{definition}
Note $\acls$,${\zeta}$ is overlapping iff $\relap{\snatneq}{\binap{\spkovl}{\acls}{{\zeta}}}{\pair{{0}}{{0}}}$.
Critical peaks $\iarsinva{\astp}{{s}}{\iarsa{{\psi}}{{t}}{{u}}}$
are classified by comparing the root-positions $\aipos{\astp}$, $\aipos{{\psi}}$
of their patterns with respect to the prefix order $\ordpfx{\prec}$,
into being \emph{outer--inner} ($\relap{\spospfx}{\aipos{\astp}}{\aipos{{\psi}}}$),
\emph{inner--outer} ($\relap{\spospfx}{\aipos{{\psi}}}{\aipos{\astp}}$), or
\emph{overlay} ($\binap{\sposeq}{\aipos{{\psi}}}{\aipos{\astp}}$),
and induce the usual~\cite{Knut:Bend:70,Huet:80,Ders:Joua:90,Baad:Nipk:98,Ohle:02,Tere:03}
notion of critical \emph{pair} $\pair{{s}}{{u}}$.\footnote{%
We exclude neither overlays of a rule with itself
nor pairs obtained by symmetry.}
\begin{definition} \label{def:inner}
  A pair $\pair{\acls'}{{\zeta}'}$ of overlapping patterns such that $\acls'$, ${\zeta}'$ are
  in the multipatterns $\acls$, ${\zeta}$ with $\relap{\sclseq}{\clstop}{\binap{\sclslub}{\acls}{{\zeta}}}$,
  is called \emph{inner}, if it is minimal among all such pairs,
  comparing them in the
  lexicographic product of $\ordpfx{\prec}$ with itself,
  via the root-positions of their patterns, ordering these themselves first by $\ordpfx{\preceq}$.
  This extends to pairs of steps in peaks of multisteps via $\mathsf{src}$.
\end{definition}
\begin{proposition} \label{prop:inner:overlay}
  If $\pair{\astp}{{\psi}}$ is an inner pair for a critical peak
  $\binap{\srelsco}{\zp{\aarsdevinv}{\aStp}}{\ip{\aarsdev}{{\Psi}}}$,
  and $\binap{\sstpin}{\astp}{\aStp}$, $\binap{\sstpin}{{\psi}}{{\Psi}}$ contract
  redexes at the same position,
  then $\relap{\sclseq}{\astp}{\aStp}$ and $\relap{\sclseq}{{\psi}}{{\Psi}}$.
\end{proposition}
For patterns and peaks of ordinary steps, their join
being top, entails they are overlapping, and
the patterns in a join are joins of their constituent patterns.
\begin{proposition} \label{prop:critical:peak}
  Linear patterns $\acls$,${\zeta}$ are critically overlapping iff
  $\relap{\sclseq}{\binap{\sclslub}{\acls}{{\zeta}}}{\clstop}$.
\end{proposition}
\begin{lemma} \label{lem:join:join}
  If
  ${\xi} \isdefd \binap{\sclslub}{\acls}{{\zeta}}$
  and $\relap{\sclsle}{\acls,{\zeta}}{{\xi}}$ are witnessed by the $2$nd-order substitutions ${\sigma}$, ${\tau}$,
  for multipatterns $\acls$ and ${\zeta}$ given by
  $\clslet{\vec{\amtrmvar}}{\vec{{t}}}{{M}}$ and
  $\clslet{\vec{\varmvar\btrmvar}}{\vec{{s}}}{{N}}$,
  then for all let-bindings $\varmvar\ctrmvar\,=\,{u}$ of ${\xi}$,
  $\relap{\strmeq}{\ip{\clstop}{{u}}
        }{\binap{\sclslub}{(\clslet{\vec{\amtrmvar}}{\vec{{t}}}{\subap{\asub}{\funap{\cmtrmvar}{\vec{{z}}}}})
                }{(\clslet{\vec{\varmvar\btrmvar}}{\vec{{s}}}{\subap{\bsub}{\funap{\cmtrmvar}{\vec{{z}}}}})
                }
        }$.
\end{lemma}
\begin{lemma}[Vertical] \label{lem:vertical}
  A  peak
  $\iarsdevinva{\aStp
              }{{s}
    }{\iarsdeva{{\Psi}
              }{{t}
              }{{u}
              }}$
  of overlapping multisteps either is critical or
  it can be vertically decomposed as:
  \[ \iarsdevinva{\substra{\vec{{x}}}{\vec{\aStp}}{\ip{\aStp}{0}%\mathsf{out}}}
                }{\substra{\vec{{x}}}{\vec{{s}}}{\ip{\btrm}{0}%\mathsf{out}}}
      }{\iarsdeva{\substra{\vec{{x}}}{\vec{{\Psi}}}{\ip{\bStp}{0}%\mathsf{out}}}
                }{\substra{\vec{{x}}}{\vec{{t}}}{\ip{\atrm}{0}%\mathsf{out}}}
                }{\substra{\vec{{x}}}{\vec{{u}}}{\ip{\ctrm}{0}%\mathsf{out}}}
                }} \]
  for peaks
  $\iarsdevinva{\ip{\aStp}{{i}}
              }{\ip{\btrm}{{i}}
    }{\iarsdeva{\ip{\bStp}{{i}}
              }{\ip{\atrm}{{i}}
              }{\ip{\ctrm}{{i}}
              }}$
  with
  $\relap{\snatge}{\binap{\spkovl}{\aStp}{{\Psi}}
        }{\binap{\spkovl}{\ip{\aStp}{{i}}}{\ip{\bStp}{{i}}}
        }$ and
  $\relap{\snatgt}{\binap{\spkprt}{\aStp}{{\Psi}}
        }{\binap{\spkprt}{\ip{\aStp}{{i}}}{\ip{\bStp}{{i}}}
        }$, for all ${i}$.
\end{lemma}
Let $\aStp$, ${\Psi}$ in
$\iarsdevinva{\aStp}{{s}}{\iarsdeva{{\Psi}}{{t}}{{u}}}$
be given by
$\clslet{\vec{\amtrmvar}\!}{\!\vec{\funap{\arul}{\vec{{x}}}}}{{M}}$ and
$\clslet{\vec{\varmvar\btrmvar}\!}{\!\vec{\funap{\brul}{\vec{{y}}}}}{{N}}$,
for rules
$\irula{{i}}{\vec{\ip{\atrmvar}{{i}}}} \hastype \binap{\srulstr}{\ip{\alhs}{{i}}}{\ip{\arhs}{{i}}}$ and
$\irulb{{j}}{\vec{\ip{\btrmvar}{{j}}}} \hastype \binap{\srulstr}{\ip{\blhs}{{j}}}{\ip{\brhs}{{j}}}$.
Lemma~\ref{lem:lattice} entails that if $\aStp$, ${\Psi}$ are non-overlapping
their patterns are (pairwise) disjoint,
so that the join $\binap{\sclslub}{\subap{\mathsf{src}}{\aStp}}{\subap{\mathsf{src}}{{\Psi}}}$
is given by taking the (disjoint) union of the let-bindings:
$\clslet{\vec{\amtrmvar}\vec{\varmvar\btrmvar}
         }{\vec{{\ell}}\vec{{g}}
         }{{L}
         }$ for some ${L}$ such that
$\relap{\strmeq}{\msubstra{\vec{\varmvar\btrmvar}}{\vec{{g}}}{{L}}}{{M}}$ and
$\relap{\strmeq}{\msubstra{\vec{\amtrmvar}}{\vec{{\ell}}}{{L}}}{{N}}$.
We define the \emph{join}\footnote{%
This does not create ambiguity with joins of multipatterns since if
$\relap{\sclsneq}{\aStp}{{\Psi}}$, then $\relap{\sclsneq}{\algtrm{\aStp}}{\algtrm{{\Psi}}}$
unless the let-bindings of both are empty, so both are bottom.
}
$\binap{\sclslub}{\aStp}{{\Psi}}$ and \emph{residual} $\stpres{\aStp}{{\Psi}}$ by
$\clslet{\vec{\amtrmvar}\vec{\varmvar\btrmvar}
       }{\vec{\funap{\arul}{\vec{{x}}}}\vec{\funap{\brul}{\vec{{y}}}}
       }{{L}
       }$ respectively
$\clslet{\vec{\amtrmvar}
       }{\vec{\funap{\arul}{\vec{{x}}}}
       }{\msubstra{\vec{\varmvar\btrmvar}}{\vec{{d}}}{{L}}
       }$, where, as substituting the right-hand sides $\vec{{d}}$
may lose being linear and canonical, we implicitly canonise and
linearise the latter by reordering and replicating
let-bindings.
Then
$\relap{\binap{\srelsco}{\ip{\aarsdev}{\binap{\sclslub}{\aStp}{{\Psi}}}
              }{\zp{\aarsdevinv}{\stpres{\aStp}{{\Psi}}}
              }
      }{{t}
      }{{u}
      }$, giving rise to the classical
residual theory~\cite{Chur:Ross:36,Huet:Levy:91a,Boud:85,Bare:85},
see~\cite[Section~8.7]{Tere:03}.
We let $\binap{\sstpin}{\astp}{\aStp}$ abbreviate
$\exists {\Psi}.\relap{\sclseq}{\aStp}{\binap{\sclslub}{\astp}{{\Psi}}}$.
\begin{example} \label{exa:cluster:5}
  The steps $\astp$ and ${\psi}$ given by
  $\clslet{\amtrmvar}{\lambda x.\funap{\arul}{x}}{\mtrmvara{f(f(a))}}$ respectively
  $\clslet{\amtrmvar}{\lambda x.\funap{\arul}{x}}{f(f(\funap{\bmtrmvar}{a}))}$,
  are non-overlapping, $\binap{\sstpin}{\astp,{\psi}}{{\zeta}}$,
  $\relap{\sclseq}{\binap{\sclslub}{\astp}{{\psi}}}{{\zeta}}$,
  and $\iarsdeva{\stpres{\astp}{{\psi}}}{f(f(g(a)))}{g(g(a))}$,
  for ${\zeta}$ and ${\varrho}$ as in Example~\ref{exa:cluster:3}.
\end{example}
\begin{lemma}[Horizontal] \label{lem:horizontal}
  A peak
  $\relap{\binap{\srelsco}{\zp{\aarsdevinv}{\aStp}}{\ip{\aarsdev}{{\Psi}}}
        }{{t}
        }{{s}
        }$
  of multisteps either
  \begin{enumerate}
  \item \label{ite:horizontal:non-overlap}
    is non-overlapping and then
    $\relap{\binap{\srelsco}{\ip{\aarsdev}{\stpres{{\Psi}}{\aStp}}}{\zp{\aarsdevinv}{\stpres{\aStp}{{\Psi}}}}
        }{{t}
        }{{s}
        }$, with the rule symbols occurring in
    $\stpres{{\Psi}}{\aStp}$ contained in ${\Psi}$
    (and those in $\stpres{\aStp}{{\Psi}}$ contained in $\aStp$); or
  \item \label{ite:horizontal:overlap}
    it can be horizontally decomposed:
    $\relap{\binap{\srelsco}{\binap{\srelsco}{\zp{\aarsdevinv}{\stpres{\aStp}{\astp}}}{\zp{\aarsinv}{\astp}}
                  }{\binap{\srelsco}{\ip{\aars}{{\psi}}}{\ip{\aarsdev}{\stpres{{\Psi}}{{\psi}}}}
                  }
          }{{t}
          }{{s}
          }$
    for some peak $\binap{\srelsco}{\zp{\aarsinv}{\astp}}{\ip{\aars}{{\psi}}}$
    of overlapping steps $\binap{\sstpin}{\astp}{\aStp}$ and $\binap{\sstpin}{{\psi}}{{\Psi}}$.
  \end{enumerate}
\end{lemma}
The above allows to refactor the proof of the critical pair
lemma~\cite[Lemma~3.1]{Huet:80} for left-linear TRSs,
as an induction on the amount of \emph{non-overlap} between
the steps in the peak, such that the critical peaks form the \emph{base} case:
\begin{lemma} \label{lem:critical:pair}
  A left-linear TRS is locally confluent if all critical pairs are joinable.
\end{lemma}
\begin{proof}
  We show every peak $\binap{\srelsco}{\aiarsinvref{\astp}}{\ip{\aarsref}{{\psi}}}$
  of empty or single steps is joinable,
  by induction on the amount of non-overlap
  ($\binap{\spkprt}{\astp}{{\psi}}$) ordered by $\strmgt$.
  We distinguish cases on whether $\astp$, ${\psi}$ are overlapping
  ($\relap{\snatneq}{\binap{\spkovl}{\astp}{{\psi}}}{\pair{{0}}{{0}}}$) or not.
  If $\astp$, ${\psi}$ do not have overlap, in particular when either $\astp$ or ${\psi}$
  is empty, then we conclude by Lemma~\ref{lem:horizontal}(\ref{ite:horizontal:non-overlap}).
  If $\astp$, ${\psi}$ do have overlap, then by Lemma~\ref{lem:vertical} the peak either
  \begin{itemize}
  \item
    is critical and we conclude by assumption; or
  \item
    can be (vertically) \emph{decomposed} into smaller such peaks
    $\binap{\srelsco}{\aiarsinvref{\ip{\astp}{{i}}}
           }{\ip{\aarsref}{\ip{\bstp}{{i}}}
           }$.
    Since these are $\strmgt$-smaller, the induction hypothesis yields
    them joinable, from which we conclude by reductions and joins being
    closed under \emph{composition}. \qed
  \end{itemize}
\end{proof}
\begin{remark}
  Apart from enabling our proof of Theorem~\ref{thm:hot} below,
  we think this refactoring is methodologically interesting,
  as it extends to (parallel and) simultaneous critical pairs,
  then yielding, we claim, simple statements and proofs
  of confluence results~\cite{Okui:98,Felg:15} based on these
  and their higher-order generalisations.
\end{remark}

\section{Confluence by hot-decreasingness}
\label{sec:hot}

Linear TRSs have a critical-pair criterion for so-called
rule-labelling~\cite{Oost:08,Hiro:Midd:11,Zank:Felg:Midd:15}:
If all critical peaks are decreasing with respect some rule-labelling,
then the TRS is decreasing, hence confluent.
We introduce the hot-labelling extending that result to left-linear
TRSs. To deal with non-right-linear rules we make use of a
rule-labelling for multisteps that is invariant under duplication,
cf.~\cite{Felg:15,Zank:Felg:Midd:15}.
\begin{remark}
  Na{\"\i}ve extensions fail.
  Non-left-linear TRSs need not
  be confluent even without critical pairs~\cite[Exercise~2.7.20]{Tere:03}.
  That non-right-linear TRSs need not be confluent even if all critical peaks
  are decreasing for rule-labelling, is witnessed by~\cite[Example~8]{Hiro:Midd:11}.
\end{remark}
\begin{definition}
  For a TRS $\Rultrs{\aRul}$, terminating subsystem $\Rultrs{\dRul} \subseteq \Rultrs{\aRul}$,
  and labelling of $\binap{\ssetdif}{\Rultrs{\aRul}}{\Rultrs{\dRul}}$-rules
  into a well-founded order ${\succ}$,
  \emph{hot}-labelling $\hot{\aLab}$ maps a multistep
  $\aStp \hastype \iarsdeva{\Rultrs{\aRul}}{{t}}{{s}}$
  \begin{itemize}
  \item
    to the \emph{term} ${t}$ if $\aStp$ contains $\Rultrs{\dRul}$-rules only; and
  \item
    to the \emph{set} of ${\succ}$-maximal $\binap{\ssetdif}{\Rultrs{\aRul}}{\Rultrs{\dRul}}$-rules in $\aStp$ otherwise.
  \end{itemize}
  The \emph{hot}-order $\hot{\aord}$ relates terms by $\ip{\aarstra}{\Rultrs{\dRul}}$,
  sets by $\ip{\aord}{\mul}$, and all sets to all terms.
\end{definition}
Note $\hot{\aord}$ is a well-founded order as series composition~\cite{Bech:Groo:Reto:97}
of $\ip{\aarstra}{\Rultrs{\dRul}}$ and $\ip{\aord}{\mul}$, which are well-founded orders by the
assumptions on $\Rultrs{\dRul}$ and ${\succ}$.
Taking the \emph{set} of maximal rules in a multistep
makes hot-labelling invariant under duplication.
As with the notation $\orddwna{{\ell}}$, we denote
$\{ {\kappa} \mid \relap{\aordhot}{{\ell}}{{\kappa}} \}$ by $\ordhotdwna{{\ell}}$, and
$\{ {\kappa} \mid \relap{\aordrefhot}{{\ell}}{{\kappa}} \}$ by $\ordhotrefdwna{{\ell}}$.
\begin{definition} \label{def:hot:decreasing:trs}
  A TRS $\Rultrs{\aRul}$ is \emph{hot-decreasing} if its critical peaks
  are decreasing for the hot-labelling, for some $\Rultrs{\dRul}$
  and ${\succ}$, such that each outer--inner critical peak $\binap{\srelsco}{\zp{\aarsinv}{{\ell}}}{{\to}}$ for label ${\ell}$,
  is decreasing by a conversion of shape (oi):
  $\binap{\srelsco}{\ip{\aarsequ}{\ordhotdwna{{\ell}}}}{\zp{\aarsdevinv}{\ordhotrefdwna{{\ell}}}}$.
\end{definition}
\begin{theorem} \label{thm:hot}
  A left-linear TRS is confluent, if it is hot-decreasing.
\end{theorem}
Before proving Theorem~\ref{thm:hot}, we give (non-)examples and special cases.
\begin{example} \label{exa:nats:hot}
  Consider the left-linear TRS $\Rultrs{\aRul}$:
  \[\begin{array}{lrcl@{\,\,\,\,}lrcl@{\,\,\,\,}lrcl}
  {\varrho}_1\hastype & \m{nats}                  & {\to} & \m{0} : \m{inc}(\m{nats}) &
  {\varrho}_3\hastype & \m{inc}(x : y)            & {\to} & \m{s}(x) : \m{inc}(y)     &
  {\varrho}_5\hastype & \m{hd}(x : y)             & {\to} & x \\
  {\varrho}_2\hastype & \m{d}(x)                  & {\to} & x : (x : \m{d}(x))        &
  {\varrho}_4\hastype & \m{inc}(\m{tl}(\m{nats})) & {\to} & \m{tl}(\m{inc}(\m{nats})) &
  {\varrho}_6\hastype & \m{tl}(x : y)             & {\to} & y
  \end{array}\]
  By taking $\Rultrs{\dRul} \isdefd {\setemp}$, labelling rules by themselves, and
  ordering $\relap{\aord}{\ip{\arul}{4}}{\ip{\arul}{1},\ip{\arul}{3},\ip{\arul}{6}}$
  the only critical peak
  $\binap{\srelsco}{\zp{\aarsinv}{\setstr{\ip{\arul}{4}}}}{\ip{\aars}{\setstr{\ip{\arul}{1}}}}$
  can be completed into the decreasing diagram:
  \begin{center}
  \begin{tikzpicture}
  \node (t) at (0,0.9) {$\m{tl}(\m{inc}(\m{nats}))$};
  \node (o) at (4,0.9) {$\m{inc}(\m{tl}(\m{nats}))$};
  \node (s) at (8,0.9) {$\m{inc}(\m{tl}(\m{0} : \m{inc}(\m{nats})))$};
  \node (u) at (0,0)   {$\m{tl}(\m{inc}(\m{0} : \m{inc}(\m{nats})))$};
  \node (v) at (4.3,0) {$\m{tl}(\m{s}(\m{0}) : \m{inc}(\m{inc}(\m{nats}))$};
  \node (w) at (8,0)   {$\m{inc}(\m{inc}(\m{nats}))$};
  \draw[->]
    (o) edge node[anchor=north] {$\scriptstyle\{{\varrho}_4\}$} (t)
    (o) edge node[anchor=north] {$\scriptstyle\{{\varrho}_1\}$} (s)
    (t) edge node[anchor=east]  {$\scriptstyle\{{\varrho}_1\}$} (u)
    (u) edge node[anchor=north] {$\scriptstyle\{{\varrho}_3\}$} (v)
    (v) edge node[anchor=north] {$\scriptstyle\{{\varrho}_6\}$} (w)
    (s) edge node[anchor=west]  {$\scriptstyle\{{\varrho}_6\}$} (w)
  ;
  \end{tikzpicture}\vspace{-0.7em}
  \end{center}
  Since the peak is outer--inner, the closing conversion must be of (oi)-shape
  $\binap{\srelsco}{\ip{\aarsequ}{\ordhotdwna{\setstr{\ip{\arul}{4}}}}}{\zp{\aarsdevinv}{\ordhotrefdwna{\setstr{\ip{\arul}{4}}}}}$.
  It is, so
  the system is confluent by Theorem~\ref{thm:hot}.
\end{example}
\begin{example} \label{exa:half:levy:hot}
  Consider the left-linear confluent TRS $\Rultrs{\aRul}$:
  \[\begin{array}{lrcl@{\quad\quad}lrcl@{\quad\quad}lrcl}
    {\varrho}_1 \hastype & f(a,a) & {\to} & b      &
    {\varrho}_3 \hastype & f(c,x) & {\to} & f(x,x) &
    {\varrho}_5 \hastype & f(c,c) & {\to} & f(a,c) \\
    {\varrho}_2 \hastype & a      & {\to} & c      &
    {\varrho}_4 \hastype & f(x,c) & {\to} & f(x,x)
  \end{array}\]
  Since $b$ is an $\Rultrs{\aRul}$-normal form,
  the only way to join the outer--inner critical peak
  $\iarsinva{\ip{\arul}{1}}{b}{\iarsa{\ip{\arul}{2}}{f(a,a)}{f(c,a)}}$
  is by a conversion starting with a step
  $\iarsinva{\ip{\arul}{1}}{b}{f(a,a)}$.
  As its label must be identical to the same step in the peak, not smaller,
  whether we choose $\ip{\arul}{1}$ to be in $\Rultrs{\dRul}$ or not,
  the peak is not hot-decreasing, so Theorem~\ref{thm:hot} does not apply.

  That hot-decreasingness in Theorem~\ref{thm:hot} cannot be weakened
  to (ordinary) decreasingness, can be seen by considering $\Rultrs{\aRul}'$ obtained
  by omitting ${\varrho}_5$ from $\Rultrs{\aRul}$.  Although $\Rultrs{\aRul}'$ is not
  confluent~\cite[Example 8]{Hiro:Midd:11},
  by taking $\Rultrs{\dRul} = \varnothing$ and $\relap{\aord}{\ip{\arul}{1}}{\ip{\arul}{3},\ip{\arul}{4}}$,
  we can show that all critical peaks of $\Rultrs{\aRul}'$ are decreasing for the
  hot-labelling.
\end{example}
A special case of Theorem~\ref{thm:hot}, is that a left-linear terminating
TRS is confluent~\cite{Knut:Bend:70}, if each critical pair is joinable,
as can be seen by setting $\Rultrs{\dRul} \isdefd \Rultrs{\aRul}$.
\begin{corollary} \label{cor:dev:closed}
  A left-linear development closed TRS is confluent~\cite[Cor.~24]{Oost:97}.
\end{corollary}
\begin{proof}
  A TRS is development closed if for every critical pair $\pair{{t}}{{s}}$
  such that ${t}$ is obtained by an outer step, $\relap{\aarsdevinv}{{t}}{{s}}$ holds.
  Taking $\Rultrs{\dRul} \isdefd {\setemp}$ and labelling all rules the same, say by $0$,
  yields that each outer--inner or overlay critical peak is labelled as
  $\relap{\binap{\srelsco}{\zp{\aarsinv}{\setstr{0}}}{\ip{\aars}{\setstr{0}}}}{{t}}{{s}}$, and can
  be completed as $\iarsdevinva{\setstr{0}}{{t}}{{s}}$,
  yielding a hot-decreasing diagram of (oi)-shape.
  We conclude by Theorem~\ref{thm:hot}. \qed
\end{proof}
The proof of Theorem~\ref{thm:hot} uses the following structural properties
of decreasing diagrams specific to the hot-labelling. The labelling was designed so they hold.
\begin{lemma}  \label{lem:hot:structural}
  \begin{enumerate}
  \item \label{ite:hot:decreasing}
    If the peak $\iarsdevinva{{\ell}}{{s}}{\iarsdeva{{\kappa}}{{t}}{{u}}}$
    is hot-decreasing, then it can be completed into a hot-decreasing
    diagram of shape
    $\iarsequa{\ordhotdwna{{\ell}}
            }{{s}
  }{\iarsdeva{{\kappa}
            }{{s}'
  }{\iarsequa{\ordhotdwna{{\ell}{\kappa}}
            }{{s}''
}{\iarsdevinva{{\ell}
            }{{u}''
  }{\iarsequa{\ordhotdwna{{\kappa}}}
            }{{u}'
            }{{u}
            }}}}$
    such that the $1$st-order variables in all terms in the diagram
    are contained in those of ${t}$.
  \item \label{ite:hot:commute}
    If the multisteps $\aStp$, ${\Psi}$ in the peak
    $\iarsdevinva{\aStp}{{s}}{\iarsdeva{{\Psi}}{{t}}{{u}}}$
    are non-overlapping, then the valley
    $\relap{\binap{\srelsco}{\ip{\aarsdev}{\stpres{{\Psi}}{\aStp}}
        }{\zp{\aarsdevinv}{\stpres{\aStp}{{\Psi}}}
         }
        }{{s}
        }{{u}
        }$ completes it into a hot-decreasing diagram.
  \item \label{ite:hot:vertical}
  If the peak
  $\iarsdevinva
              }{{s}
    }{\iarsdeva
              }{{t}
              }{{u}}}$ and vector of peaks
  $\iarsdevinva
              }{\vec{{s}}
    }{\iarsdeva
              }{\vec{{t}}
              }{\vec{{u}}
              }}$
  have hot-decreasing diagrams, so does the composition
  $\iarsdevinva
              }{\substra{\vec{{x}}}{\vec{{s}}}{{s}}
    }{\iarsdeva
              }{\substra{\vec{{x}}}{\vec{{t}}}{{t}}
              }{\substra{\vec{{x}}}{\vec{{u}}}{{u}}
              }}$.
   \end{enumerate}
\end{lemma}
The proof of Theorem~\ref{thm:hot}
refines our refactored proof (see Lemma~\ref{lem:critical:pair})
of Huet's critical pair lemma,
by wrapping the induction on the amount of non-overlap ($\spkprt$)
between multisteps,
into an outer induction on their amount of overlap ($\spkovl$).
\begin{proof}[of Theorem~\ref{thm:hot}]
  We show that every peak
  $\iarsdevinva{\aStp}{{s}}{\iarsdeva{{\Psi}}{{t}}{{u}}}$
  of multisteps $\aStp$ and ${\Psi}$
  can be closed into a hot-decreasing diagram,
  by induction on the pair
  $\pair{\binap{\spkovl}{\aStp}{{\Psi}}}{\binap{\spkprt}{\aStp}{{\Psi}}}$
  ordered by the lexicographic product of ${>}$ with itself.
  We distinguish cases on whether or not $\aStp$ and ${\Psi}$ have overlap.

  If $\aStp$ and ${\Psi}$ do not have overlap,
  Lemma~\ref{lem:horizontal}(\ref{ite:horizontal:non-overlap})
  yields
  $\relap{\binap{\srelsco}{\ip{\aarsdev}{\stpres{{\Psi}}{\aStp}}
        }{\zp{\aarsdevinv}{\stpres{\aStp}{{\Psi}}}
         }
        }{{s}
        }{{u}
        }$.
  This valley completes the peak into a hot-decreasing diagram
  by Lemma~\ref{lem:hot:structural}(\ref{ite:hot:commute}).

  If $\aStp$ and ${\Psi}$ do have overlap, then we further distinguish cases on whether
  or not the overlap is critical.

  If the overlap is not critical, then by Lemma~\ref{lem:vertical}
  the peak can be vertically decomposed into a number of peaks between
  multisteps $\ip{\aStp}{{i}}$, $\ip{\bStp}{{i}}$ that have an
  amount of overlap that is not greater,
  $\relap{\snatge}{\binap{\spkovl}{\aStp}{{\Psi}}
        }{\binap{\spkovl}{\ip{\aStp}{{i}}}{\ip{\bStp}{{i}}}
        }$, and a strictly smaller amount of non-overlap
  $\relap{\snatgt}{\binap{\spkprt}{\aStp}{{\Psi}}
        }{\binap{\spkprt}{\ip{\aStp}{{i}}}{\ip{\bStp}{{i}}}
        }$.
  Hence the I.H.\ applies and yields that each such peak can be completed into a hot-decreasing
  diagram. We conclude by vertically recomposing them
  yielding a hot-decreasing diagram by Lemma~\ref{lem:hot:structural}(\ref{ite:hot:vertical}).

  If the overlap is critical, then by Lemma~\ref{lem:horizontal} the peak can be
  horizontally decomposed as
     $\iarsdevinva{\stpres{\aStp}{\astp}
               }{{s}
     }{\iarsinva{\astp
               }{{s}'
        }{\iarsa{{\psi}
               }{{t}
     }{\iarsdeva{\stpres{{\Psi}}{{\psi}}
               }{{u}'
               }{{u}
               }}}}$
  for some peak $\iarsinva{\astp}{{s}'}{\iarsa{{\psi}}{{t}}{{u}'}}$
  of overlapping steps $\binap{\sstpin}{\astp}{\aStp}$ and $\binap{\sstpin}{{\psi}}{{\Psi}}$,
  i.e.\ such that $\relap{\sclseq}{\aStp}{\binap{\sclslub}{\astp}{\aStp'}}$
  $\relap{\sclseq}{{\Psi}}{\binap{\sclslub}{{\psi}}{{\Psi}'}}$ for some $\aStp'$, ${\Psi}'$.
  We choose $\pair{\astp}{{\psi}}$ to be \emph{inner} among such overlapping pairs
  (see Definition~\ref{def:inner}),
  assuming w.l.o.g.\ that $\relap{\spospfxref}{\aipos{\astp}}{\aipos{{\psi}}}$
  for the root-positions $\aipos{\astp}$,$\aipos{{\psi}}$ of their patterns.
  We distinguish cases on whether or not $\aipos{\astp}$ is a strict prefix of $\aipos{{\psi}}$.

  If $\binap{\sposeq}{\aipos{\astp}}{\aipos{{\psi}}}$,
  then $\relap{\sclseq}{\astp}{\aStp}$ and $\relap{\sclseq}{{\psi}}{{\Psi}}$
  by Proposition~\ref{prop:inner:overlay},
  so the peak \emph{is} overlay, from which we conclude
  since such peaks are hot-decreasing by assumption.

  Suppose $\relap{\spospfx}{\aipos{\astp}}{\aipos{{\psi}}}$.
  We will construct a hot-decreasing diagram $D$ for the peak
  $\iarsdevinva{\aStp}{{s}}{\iarsdeva{{\Psi}}{{t}}{{u}}}$
  out of several smaller such diagrams
  as illustrated in Figure~\ref{fig:outer:inner},
  using the multipattern
  $\acls \isdefd \binap{\sclslub}{\subap{\mathsf{src}}{\aStp}}{\subap{\mathsf{src}}{{\psi}}}$
  as a basic building block;
  it has as patterns those of $\aStp'$ and the join of the patterns of $\astp$, ${\psi}$.
  To make $\acls$ explicit, unfold
  $\aStp$ and ${\Psi}$ to let-expressions
  $\clslet{\vec{\amtrmvar}}{\vec{\funap{\arul}{\vec{{x}}}}}{{M}}$ respectively
  $\clslet{\vec{\varmvar\btrmvar}}{\vec{\funap{\brul}{\vec{{y}}}}}{{N}}$,
  for rules of shapes
  $\irula{{i}}{\vec{\ip{\atrmvar}{{i}}}} \hastype \binap{\srulstr}{\ip{\alhs}{{i}}}{\ip{\arhs}{{i}}}$ and
  $\irulb{{j}}{\vec{\ip{\btrmvar}{{j}}}} \hastype \binap{\srulstr}{\ip{\blhs}{{j}}}{\ip{\brhs}{{j}}}$.
  We let $\vec{\amtrmvar} = \vec{\amtrmvar}'\amtrmvar$
  and $\vec{\varmvar\btrmvar} = \vec{\varmvar\btrmvar}'\varmvar\btrmvar$ be
  such that $\amtrmvar$ and $\varmvar\btrmvar$ are the $2$nd-order variables
  corresponding to $\binap{\sstpin}{\astp}{\aStp}$ and $\binap{\sstpin}{{\psi}}{{\Psi}}$
  for rules
  $\funap{\arul}{\vec{{x}}} \hastype \binap{\srulstr}{{\ell}}{{r}}$ and
  $\funap{\brul}{\vec{{y}}} \hastype \binap{\srulstr}{{g}}{{d}}$.
  By the choice of $\pair{\astp}{{\psi}}$ as inner,
  $\subap{\mathsf{src}}{\astp}$ is the \emph{unique} pattern in $\subap{\mathsf{src}}{\aStp}$ overlapping
  $\subap{\mathsf{src}}{{\psi}}$.
  As a consequence we can write $\acls$ as
  $\clslet{\vec{\amtrmvar}'\varmvar\ctrmvar
         }{\vec{{\ell}}'\hat{{t}}
         }{{L}
         }$, for some pattern $\hat{{t}}$, the
  join of the patterns of $\astp$,${\psi}$, such that
  ${\sigma}$ maps $\varmvar\ctrmvar$ to a term of shape $\mtrmvara{\vec{\ip{\blhs}{{\psi}}}}$
  as $\astp$ is the outer step,
  and ${\tau}$ maps it to a term of shape $\ctxa{\funap{\bmtrmvar}{\vec{\ip{\alhs}{\astp}}}}$,\footnote{%
$\actx$ is a prefix of the left-hand side ${\ell}$ of ${\varrho}$.
For instance, for a peak from $f(g(a))$ between
${\varrho} \hastype \binap{\srulstr}{f(g(a))}{\ldots}$ and
${\theta} \hastype \binap{\srulstr}{g(x)}{\ldots}$,
$\varmvar\ctrmvar$ is mapped by ${\sigma}$ to $\mtrmvara{}$ and
by ${\tau}$ to $f(\funap{\bmtrmvar}{a})$.}
  where ${\sigma}$, ${\tau}$ witness $\relap{\sclsle}{\subap{\mathsf{src}}{\aStp},\subap{\mathsf{src}}{{\psi}}}{\acls}$.
  That the other $2$nd-order variables are $\vec{\amtrmvar}'$
  follows by ${\sigma}$ being the identity on them (their patterns do not overlap ${\psi}$),
  and that these are bound to the patterns $\vec{{\ell}}'$ by
  ${\tau}$ mapping them to $1$st-order terms (only $\varmvar\ctrmvar$ can be mapped to a non-$1$st-order term).
   \begin{figure}[t]
     \def$\aStp${$\aStp$}
     \def$\astp${$\astp$}
     \def$\stpres{\aStp}{\astp}${$\stpres{\aStp}{\astp}$}
     \def$\bStp${${\Psi}$}
     \def$\bstp${${\psi}$}
     \def{}
     \def$\rlft{\hat{\bStp}}${$\rlft{\hat{{\Psi}}}$}
     \def{}
     \def{}
     \def$\clft{\aStp'}{\hat{\aStp}}${$\clft{\aStp'}{\hat{\aStp}}$}
     \def$\stpres{\bStp}{\bstp}${$\stpres{{\Psi}}{{\psi}}$}
     \def$\hat{\bStp'}${$\hat{{\Psi}'}$}
     \def$\hat{\aStp'}${$\hat{\aStp'}$}
     \def\nfig{$$}
     \def$\ast${$\ast$}
     \def{}
     \def$D'${$D'$}
     \def$D_{\text{IH}}${$D_{\text{IH}}$}
      \begin{center}
      \scalebox{0.45}{\input{hotconversion.pdf_t}}
      \end{center}
       \caption{Outer--inner critical peak construction}
          \label{fig:outer:inner}
      \end{figure}

  We start with constructing a hot-decreasing diagram $\hot{D}$
  for the \emph{critical} peak
  $\iarsinva{\hat{\astp}}{\hat{{s}}}{\iarsa{\hat{{\psi}}}{\hat{{t}}}{\hat{{u}}}}$
  encompassed by the peak between $\astp$ and ${\psi}$, as follows.
  We set $\hat{\astp}$ and $\hat{{\psi}}$ to
  $\clslet{\amtrmvar}{\funap{\arul}{\vec{{x}}}}{\subap{\asub}{\funap{\cmtrmvar}{\vec{{z}}}}}$ respectively
  $\clslet{\varmvar\btrmvar}{\funap{\brul}{\vec{{y}}}}{\subap{\bsub}{\funap{\cmtrmvar}{\vec{{z}}}}}$.
  This yields a peak as desired, which
  is outer--inner as $\relap{\spospfx}{\aipos{\hat{\astp}}}{\aipos{\hat{{\psi}}}}$
   by $\relap{\spospfx}{\aipos{\astp}}{\aipos{{\psi}}}$,
  and critical by Lemma~\ref{lem:join:join},
  hence by the hot-decreasingness assumption,
  it can be completed into a hot-decreasing diagram $\hat{D}$ by a conversion of (oi)-shape:
     $\iarsequa{\ordhotdwna{\funap{\aLabhot}{\hat{\astp}}}
              }{\hat{{s}}
 }{\iarsdevinva{\ordhotrefdwna{\funap{\aLabhot}{\hat{\astp}}}
              }{\hat{{w}}
              }{\hat{{u}}
              }}$.
  Below we  refer to its conversion and multistep as $\hat{{\Psi}}$ and $\hat{\aStp}$.
Based on $\hat{D}$ we construct a hot-decreasing
    diagram $D'$ (Figure~\ref{fig:outer:inner}, left) for the peak
    $\iarsdevinva{\aStp
                }{{s}
         }{\iarsa{{\psi}
               }{{t}
               }{{u}'
               }}$
    by constructing a conversion
    $\rlft{\hat{{\Psi}}} \hastype
     \relap{\aarsequ}{{s}
            }{{w}''
            }$ and
    a multistep
    $\clft{\aStp'}{\hat{\aStp}} \hastype
     \relap{\aarsdev}{{u}'}{{w}''}$,
    with their composition (reversing the latter) of (oi)-shape.

    The conversion $\rlft{\hat{{\Psi}}} \hastype
     \relap{\aarsequ}{{s}
            }{{w}''
            }$
    is constructed by
      lifting the closing conversion $\hat{{\Psi}}$ of the diagram $\hat{D}$ back into  $\acls$.
    Formally, for any multistep
    $\hat{{\Omega}}$
    given by
    $\clslet{\vec{\hat{\varmvar\ctrmvar}}
           }{\vec{\funap{\crul}{\vec{{w}}}}
           }{\hat{{L}}
           }$ for rules $\irulc{{k}}{\vec{\ip{\dtrmvar}{{k}}}}$,
   occurring anywhere in $\hat{{\Psi}}$ ,
   we define its \emph{lifting} $\rlft{\hat{{\Omega}}}$ to be
   $\clslet{\vec{\hat{\varmvar\ctrmvar}}
           }{\vec{\funap{\crul}{\vec{{w}}}}
           }{\substra{\vec{\amtrmvar}',\varmvar\ctrmvar}{\vec{{r}}',\hat{{L}}}{{L}}
           }$.
    That is, we update $\acls$
    by substituting\footnote{%
For this to be a valid $2$nd-order substitution, the $1$st-order variables of $\hat{{\Omega}}$ ($\hat{{L}}$)
must be contained in those of $\hat{{t}}$, which we may assume by
Lemma~\ref{lem:hot:structural}(\ref{ite:hot:decreasing}).}
   both $\hat{{\Omega}}$ (for $\varmvar\ctrmvar$, instead of binding that to $\hat{{t}}$)
   and the \emph{right}-hand sides $\vec{{r}}'$ in its body.
   Because right-hand sides $\vec{{r}}$ need not be linear,
   the resulting proofclusters may have to be linearised (by replicating let-bindings) first to obtain multisteps.
   This extends to terms ${p}$ by $\rlft{{p}} \isdefd \algtrm{\rlft{(\clslet{}{}{{p}})}}$.
   That this yields multisteps and terms that connect into a conversion
        $\iarsequa{\rlft{\hat{{\Psi}}}
              }{\relap{\strmeq}{{s}}{\rlft{\hat{{s}}}}
              }{\relap{\strmeq}{\rlft{\hat{{w}}}}{{w}''}
              }$
   as desired follows by \emph{computation}.
   E.g.,
      $\relap{\sclseq}{{s}
     }{\relap{\sclseq}{\substra{\vec{\amtrmvar}',\amtrmvar}{\vec{{r}}',{r}}{{M}}
     }{\relap{\sclseq}{\substra{\vec{\amtrmvar}',\varmvar\ctrmvar}{\vec{{r}}',\hat{{s}}}{{L}}
            }{\rlft{\hat{{s}}}
            }}}$
    using that ${\sigma}$ witnesses $\relap{\sclsle}{\subap{\mathsf{src}}{\aStp}}{\acls}$ so that
    $\relap{\sclseq}{{M}}{\subap{\asub}{{L}}}$
    and
    $\relap{\strmeq}{\hat{{s}}
          }{\algtrm{\clslet{\amtrmvar}{{r}}{\subap{\asub}{\funap{\cmtrmvar}{\vec{{z}}}}}}
          }$.
    That the labels in $\rlft{\hat{{\Psi}}}$ are strictly below $\funap{\aLabhot}{\aStp}$
    follows for \emph{set}-labels from that lifting clearly does not introduce rule symbols
    and from that labels of rule symbols in $\hat{{\Psi}}$ are, by assumption, strictly below the
    label of the rule ${\varrho}$ of $\astp$. In case $\aStp$ is \emph{term}-labelled, by ${t}$, it follows
    from closure of $\ip{\aars}{\Rultrs{\dRul}}$-reduction under lifting (which also contracts $\aStp'$).

  The multistep $\clft{\aStp'}{\hat{\aStp}} \hastype \relap{\aarsdev}{{u}'}{{w}''}$
  is the \emph{combination} of the multisteps $\aStp'$ (the redex-patterns in $\aStp$ other than $\astp$)
  and $\hat{\aStp}$, lifting the latter into $\acls$.
  For $\hat{\aStp} \hastype \relap{\aarsdev}{\hat{{u}}}{\hat{{w}}}$ given by
  $\clslet{\vec{\hat{\amtrmvar}}}{\vec{\funap{\hat{{\varrho}}}{\hat{{x}}}}}{\hat{{M}}}$,
  it is defined as
  $\clslet{\vec{\amtrmvar}'\vec{\hat{\amtrmvar}}
         }{\vec{\funap{\arul}{\vec{{x}}}'}\vec{\funap{\hat{{\varrho}}}{\vec{\hat{{x}}}}}
         }{\substra{\varmvar\ctrmvar}{\hat{{M}}}{{L}}
         }$.
  Per construction it
  only contracts rules in $\aStp'$, $\hat{\aStp}$,
  so has a label in $\ordhotrefdwna{\funap{\aLabhot}{\aStp}}$
  by $\relap{\sclseq}{\aStp}{\binap{\sclslub}{\astp}{\aStp'}}$ and the
  label of $\hat{\aStp}$ is in $\ordhotrefdwna{\funap{\aLabhot}{\hat{\astp}}}$ by the (oi)-assumption.
  That $\clft{\aStp'}{\hat{\aStp}} \hastype \relap{\aarsdev}{{u}'}{{w}''}$
  follows again by \emph{computation}, e.g.\
   $\relap{\strmeq}{\algtrm{\clslet{\vec{\amtrmvar}'\vec{\hat{\amtrmvar}}
                         }{\vec{{r}}'\vec{\hat{{r}}}
                         }{\substra{\varmvar\ctrmvar}{\hat{{M}}}{{L}}
                         }}
  }{\relap{\strmeq}{\substra{\vec{\amtrmvar}',\varmvar\ctrmvar
                  }{\vec{{r}}',\substra{\vec{\hat{\amtrmvar}}}{\vec{\hat{{r}}}}{\hat{{M}}}
                  }{{L}
                  }
  }{\relap{\strmeq}{\substra{\vec{\amtrmvar}',\varmvar\ctrmvar}{\vec{{r}}',\hat{{w}}}{{L}}
  }{\relap{\strmeq}{\rlft{\hat{{w}}}
         }{{w}''
         }}}}$.

  Finally, applying the I.H.\ to the peak
  $\iarsdevinva{\clft{\aStp'}{\hat{\aStp}}
              }{{w}''
    }{\iarsdeva{\stpres{{\Psi}}{{\psi}}
              }{{u}'
              }{{u}
              }}$ yields some hot-decreasing diagram $D_{\text{IH}}$ (Figure~\ref{fig:outer:inner}, right).
  Prefixing $\rlft{\hat{{\Psi}}}$ to its closing conversion between ${w}''$ and ${u}$,
  then closes the original peak
    $\iarsdevinva{\aStp
               }{{s}
     }{\iarsdeva{{\Psi}
               }{{t}
               }{{u}
               }}$ into a hot-decreasing diagram $D$,
  because
  labels of steps in $\rlft{\hat{{\Psi}}}$ are in $\ordhotdwna{\funap{\aLabhot}{\aStp}}$,
    $\relap{\aordrefhot}{\funap{\aLabhot}{\aStp}
               }{\funap{\aLabhot}{\clft{\aStp'}{\hat{\aStp}}}
               }$ as seen above, and
     $\relap{\aordrefhot}{\funap{\aLabhot}{{\Psi}}
                }{\funap{\aLabhot}{\stpres{{\Psi}}{{\psi}}}
                }$.
  The I.H.\ applies since
  $\binap{\spkovl}{\aStp}{{\Psi}} > \binap{\spkovl}{(\clft{\aStp'}{\hat{\aStp}})}{(\stpres{{\Psi}}{{\psi}})}$:
  To see this, we define
  ${L}' \isdefd \substra{\vec{\varmvar\ctrmvar}'}{\vec{{\ell}'}}{{L}}$ and
  $F' \isdefd \clslet{\vec{\hat{\amtrmvar}}
           }{\vec{\hat{{\ell}}}
           }{\substra{\varmvar\ctrmvar}{\hat{{M}}}{{L}'}
           }$ and collect needed ingredients (the joins are disjoint):\\
  $\begin{array}{l@{\quad=\quad}lclcl}
    D & \subap{\mathsf{src}}{\aStp} & \isdefd &
     \binap{\sclslub}{(\clslet{\vec{\amtrmvar'}}{\vec{{\ell}}'}{\substra{\varmvar\ctrmvar}{\hat{{t}}}{{L}}}
          )}{\src{\astp}} & = & \binap{\sclslub}{\src{\aStp'}}{\src{\astp}}\\
    E & \subap{\mathsf{src}}{{\Psi}} & \isdefd &
    \binap{\sclslub}{(\clslet{\vec{\varmvar\btrmvar}'}{\vec{{g}}'}{\substra{\varmvar\btrmvar}{{g}}{{N}}})
          }{\src{{\psi}}
          }
     &
     = & \binap{\sclslub}{\src{{\Psi}'}}{\src{{\psi}}} \\
     D' & \subap{\mathsf{src}}{(\clft{\aStp'}{\hat{\aStp}})} & \isdefd &
     \binap{\sclslub}{(\clslet{\vec{\amtrmvar}'
           }{\vec{{\ell}}'
           }{\substra{\varmvar\ctrmvar}{\hat{{u}}}{{L}}
           })}{F'} \\
     E' & \subap{\mathsf{src}}{(\stpres{{\Psi}}{{\psi}})} & \isdefd &
     \clslet{\vec{\varmvar\btrmvar}'}{\vec{{g}}'}{\substra{\varmvar\btrmvar}{{d}}{{N}}}
   \end{array}$\\
   Using these one may reason with sets of patterns (not let-expressions
   as $\relap{\strmneq}{{t}}{{s}'}$; the sets are positions in both ${t}$,${s}'$)
   as follows, relying on distributivity:
   \begin{equation} \label{eqn:decrease}
     \relap{\sclsgt}{(\binap{\sclsglb}{D}{E})
    }{\relap{\sclseq}{(\binap{\sclsglb}{\ip{\bctx}{-}}{E})
    }{\relap{\sclseq}{(\binap{\sclsglb}{\ip{\bctx}{-}}{E'})
    }{\relap{\sclsge}{(\binap{\sclsglb}{\ip{\bctx}{+}'}{E'})
           }{(\binap{\sclsglb}{D'}{E'})
           }}}}
    \end{equation}
    where $F$ is the singleton
    $\setstr{\setabs{\binap{\ssetin}{p}{\subap{\mathsf{src}}{\astp}}}{\aipos{{\psi}} \npreceq p}}$
   having all positions in $\astp$ not below ${\psi}$'s root,
    $\ip{\bctx}{-} \isdefd
     \binap{\sclslub}{\src{\aStp'}
           }{F
           }$, and
    $\ip{\bctx}{+}' \isdefd \binap{\sclslub}{(\binap{\ssetdif}{D'}{F'})}{F}$. \qed
\end{proof}

\section{Confluence by critical-pair closing systems}
\label{sec:cpcs}

We introduce a confluence criterion based on identifying for
a term rewrite system $\Rultrs{\aRul}$ a subsystem $\Rultrs{\dRul}$ such that
every $\Rultrs{\aRul}$-\emph{critical peak} can be \emph{closed} by means of
$\Rultrs{\dRul}$-conversions,
rendering the rules used in the peak redundant.
\begin{definition} \label{def:cpcs}
A TRS $\Rultrs{\dRul}$ is \emph{critical-pair closing} for a TRS
$\Rultrs{\aRul}$, if $\Rultrs{\dRul}$ is a subsystem of $\Rultrs{\aRul}$
(namely $\Rultrs{\dRul} \subseteq \Rultrs{\aRul}$)
and  $\iarsequa{\Rultrs{\dRul}}{s}{t}$ holds for all critical
pairs $\pair{s}{t}$ of $\Rultrs{\aRul}$.
\end{definition}
We phrase the main result of this section as a preservation-of-confluence result.
We write $\to_{\Rultrs{\bRul}/\Rultrs{\aRul}}$ for
$\twoheadrightarrow_\Rultrs{\aRul} \cdot \to_\Rultrs{\bRul} \cdot \twoheadrightarrow_\Rultrs{\aRul}$, and if it is terminating,
$\Rultrs{\bRul}/\Rultrs{\aRul}$ is said to be \emph{(relatively) terminating}.
By $\Rultrs{\dRul}_{\m{d}}$ we denote the set of all duplicating rules in $\Rultrs{\dRul}$.
\begin{theorem} \label{thm:cpcs}
  If $\Rultrs{\dRul}$ is a critical-pair-closing system for a left-linear TRS $\Rultrs{\aRul}$
  such that $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ is terminating,
  then $\Rultrs{\aRul}$ is confluent if $\Rultrs{\dRul}$ is confluent.
\end{theorem}
Any left-linear TRS is critical-pair-closing for itself.
However, the power of the method relies on choosing \emph{small} $\Rultrs{\dRul}$.
Before proving Theorem~\ref{thm:cpcs}, we illustrate it by some (non-)examples
and give a special case.
\begin{example} \label{exa:nats} \label{ex:nats:2}
  Consider again the TRS $\Rultrs{\aRul}$ in Example~\ref{exa:nats:hot}.
  As we observed, the only critical pair originating from $\ip{\arul}{4}$ and
  $\ip{\arul}{1}$ is closed by
  $\binap{\srelsco}{\ip{\aars}{\ip{\arul}{1}}
 }{\binap{\srelsco}{\ip{\aars}{\ip{\arul}{3}}
 }{\binap{\srelsco}{\ip{\aars}{\ip{\arul}{6}}
         }{\zp{\aarsinv}{\ip{\arul}{6}}
         }}}$.
  So the subsystem $\Rultrs{\dRul} \isdefd \{ {\varrho}_1, {\varrho}_3, {\varrho}_6 \}$
  is a critical-pair-closing system for $\Rultrs{\aRul}$.
  As all $\Rultrs{\dRul}$-rules are linear,  $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ is vacuously terminating.
  Thus, by Theorem~\ref{thm:cpcs} it is sufficient to show confluence of $\Rultrs{\dRul}$.
  Because $\Rultrs{\dRul}$ has no critical pairs, the empty TRS
  $\setemp$ is a critical-pair-closing TRS for $\Rultrs{\dRul}$.
  As $\setemp/\Rultrs{\dRul}$ is terminating, confluence of $\Rultrs{\dRul}$ follows from
  that of $\setemp$, which is trivial.
\end{example}
Observe how confluence was shown by successive applications of the theorem.
\begin{remark}
  In our experiments (see Section~\ref{sec:implementation}),
  $\frac{3}{4}$ of the TRSs proven confluent by means
  of Theorem~\ref{thm:cpcs} used more than $1$ iteration,
  with the maximum number of iterations being $6$.
  For countable ARSs (see Corollary~\ref{cor:cpcs:ars} below) $1$ iteration suffices,
  which can be seen by setting $\Rultrs{\dRul}$ to the spanning
  forest obtained by Lemma~\ref{lem:countable:confluent:spanning}.
  This provides the intuition underlying rule specialisation
   in Example~\ref{exa:half:levy:1} below.
\end{remark}
\begin{example} \label{exa:half:levy}
  Although confluent, the TRS $\Rultrs{\aRul}$ in Example~\ref{exa:half:levy:hot}
  does not have any confluent critical-pair-closing subsystem
  $\Rultrs{\dRul}$ such that $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ is terminating,
  not even $\Rultrs{\aRul}$ itself:
  Because of $b$ being in normal form in the critical pair induced by
  $\iarsinva{{\varrho}_1}{b}{\iarsa{{\varrho}_2}{f(a,a)}{f(a,c)}}$,
  any such subsystem must contain ${\varrho}_4$,
  as one easily verifies, but ${\varrho}_4$ is both duplicating and non-terminating (looping).

  Note that the termination condition of $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ cannot be
  omitted from Theorem~\ref{thm:cpcs}.  Although the TRS $\Rultrs{\aRul}'$ in
  Example~\ref{exa:half:levy:hot} is not confluent, it admits the confluent
  critical-pair-closing system $\{ {\varrho}_1, {\varrho}_3, {\varrho}_4 \}$.
\end{example}
\begin{remark}
  The example is taken from~\cite{Hiro:Midd:11} where it was used
  to show that decreasingness of \emph{critical} peaks
  need not imply that of \emph{all} peaks, for rule labelling.
  That example, in turn was adapted from L\'evy's TRS in~\cite{Huet:80}
  showing that strong confluence need not imply confluence for left-linear TRSs.
\end{remark}
\begin{example}
  For \emph{self-joinable} rules, i.e.\ rules that are self-overlapping and
  whose critical pairs need further applications of the rule itself to join,
  Theorem~\ref{thm:cpcs} is not helpful since
  the critical-pair-closing system $\Rultrs{\dRul}$ then contains the rule itself.
  Examples of self-joinable rules are associativity
  $\binap{\srulstr}{(x \cdot y)\cdot z}{x\cdot(y \cdot z)}$ and self-distributivity
  $\binap{\srulstr}{(x \cdot y)\cdot z}{(x\cdot z)\cdot(y \cdot z)}$,
  with confluence of the latter being known to be hard (currently no tool
  can handle it automatically).\footnote{See problem 127 of
\url{http://cops.uibk.ac.at/results/?y=2019-full-run&c=TRS}.}
\end{example}
The special case we consider is that of TRSs that \emph{are} ARSs,
i.e.\ where all function symbols are nullary.
The identification is justified by that any ARS
in the standard sense~\cite{Ohle:02,Tere:03} can be presented as
$\ip{\aars}{\Rultrs{\aRul}}$ for the TRS $\Rultrs{\aRul}$ having a nullary symbol for each
object, and a rule for each step of the ARS.
Since ARSs have no duplicating rules, Theorem~\ref{thm:cpcs} specialises to
the following result.
\begin{corollary} \label{cor:cpcs:ars}
  If $\Rultrs{\dRul}$ is critical-pair-closing for ARS $\Rultrs{\aRul}$,
  $\Rultrs{\aRul}$ is confluent if $\Rultrs{\dRul}$ is.
\end{corollary}
\begin{example} \label{exa:cpcs:ars}
  Consider the TRS $\Rultrs{\aRul}$ given by
  $\relap{\aars}{{c}}{\relap{\aars}{\aobj'}{\relap{\aars}{\aobj}{{b}}}}$ and
  $\relap{\aars}{\aobj}{\relap{\aars}{\aobj'}{{c}}}$.
  It is an ARS having the critical-pair-closing system $\Rultrs{\dRul}$ given by the first part
  $\relap{\aars}{{c}}{\relap{\aars}{\aobj'}{\relap{\aars}{\aobj}{{b}}}}$.
  Since $\Rultrs{\dRul}$ is orthogonal it is confluent by Corollary~\ref{cor:cpcs:ars},
  so $\Rultrs{\aRul}$ is confluent by the same corollary.
  In general, a confluent ARS may have many non-confluent
  critical-pair-closing systems. Requiring local confluence is no impediment to that:
  The subsystem $\Rultrs{\dRul}'$ of $\Rultrs{\aRul}$ obtained by removing $\relap{\aars}{{c}}{\aobj'}$
  allows to join all $\Rultrs{\aRul}$-critical peaks, but is not confluent;
  it simply is Kleene's example~\cite[Figure~1.2]{Tere:03} showing that
  local confluence need not imply confluence.
\end{example}
For $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ to be vacuously terminating it is sufficient that all
rules are linear.%
\begin{example} \label{ex:running}
  Consider the linear TRS $\Rultrs{\aRul}$ consisting of
  $\rho_1\colon f(x) \to f(f(x))$,
  $\rho_2\colon f(x) \to g(x)$, and
  $\rho_3\colon g(x) \to f(x)$.
  The subsystem $\Rultrs{\dRul} = \{ \rho_1, \rho_3 \}$ is critical-pair-closing
  and has no critical pairs, so $\Rultrs{\aRul}$ is confluent.
\end{example}
From the above it is apparent that, whereas
usual redundancy-criteria are based on \emph{rules}
being redundant, the theorem gives a sufficient criterion
for \emph{peaks} of steps being redundant.
This allows one to leverage the power of extant confluence methods.
Here we give a generalisation of Huet's strong closeness
theorem~\cite{Huet:80} as a corollary of Theorem~\ref{thm:cpcs}.
\begin{definition} \label{def:strongly:closed}
  A TRS $\Rultrs{\aRul}$ is \emph{strongly closed}~\cite{Huet:80} if
  $s \twoheadrightarrow_\Rultrs{\aRul}^{} \cdot \fromBT{\Rultrs{\aRul}}{=} t$ and
  $s \to_\Rultrs{\aRul}^= \cdot \tfromBT{\Rultrs{\aRul}}{} t$

  hold
  for all critical pairs
  $\pair{s}{t}$.
\end{definition}
\begin{corollary} \label{cor:gsc}
A left-linear TRS $\Rultrs{\aRul}$ is confluent if there exists a
critical-pair-closing system $\Rultrs{\dRul}$ for $\Rultrs{\aRul}$ such that $\Rultrs{\dRul}$ is
linear and strongly closed.
\end{corollary}
\begin{example} \label{exa:strongly:closed}
  Consider the linear TRS $\Rultrs{\aRul}$:
  \[\begin{array}{lrcl@{\quad}lrcl}
    {\varrho}_1\hastype & h(f(x,y))    & {\to} & f(h(r(x)),y) &
    {\varrho}_2\hastype & f(x,k(y,z))  & {\to} & g(p(y),q(z,x)) \\
    {\varrho}_3\hastype & h(q(x,y))    & {\to} & q(x,h(r(y))) &
    {\varrho}_4\hastype & q(x,h(r(y))) & {\to} & h(q(x,y)) \\
    {\varrho}_5\hastype & h(g(x,y))    & {\to} & g(x,h(y)) \\
    {\varrho}_6\hastype & a(x,y,z)     & {\to} & h(f(x,k(y,z))) &
    {\varrho}_7\hastype & a(x,y,z)     & {\to} & g(p(y),q(z,h(r(x))))
  \end{array}\]
  $\Rultrs{\dRul} = \{ {\varrho}_1,\ldots,{\varrho}_5 \}$ is critical-pair-closing for $\Rultrs{\aRul}$,
  since the $\Rultrs{\aRul}$-critical peak between ${\varrho}_6$ and ${\varrho}_7$ can be $\Rultrs{\dRul}$-closed:
  $\iarsa{{\varrho}_1
        }{h(f(x,k(y,z)))
 }{\iarsa{{\varrho}_2
        }{f(h(r(x)),k(y,z))
        }{g(p(y),q(z,h(r(x))))
        }}$.
  Because $\Rultrs{\dRul}$ is strongly closed and also linear,
  confluence of $\Rultrs{\aRul}$ follows by Corollary~\ref{cor:gsc}.
\end{example}
\begin{remark}
  Neither of the TRSs in Examples~\ref{ex:running} and~\ref{exa:strongly:closed}
  is strongly closed. The former not, because
  $f(f(x)) \twoheadrightarrow_\Rultrs{\aRul} \cdot \fromBT{\Rultrs{\aRul}}{=} g(x)$ does not hold,
  and the latter not because
  $g(p(y),q(z,h(r(x)))) \twoheadrightarrow_\Rultrs{\aRul} \cdot \fromBT{\Rultrs{\aRul}}{=} h(f(x,k(y,z)))$ does not hold.
\end{remark}
Having illustrated the usefulness of Theorem~\ref{thm:cpcs}, we now present
its proof.
In TRSs there are \emph{two} types of peaks: overlapping
and non-overlapping ones.
As Example~\ref{exa:half:levy} shows, confluence criteria only addressing
the former need not generalise from ARSs to TRSs.
Note that one of the peaks showing non-confluence of $\Rultrs{\aRul}'$,
the one between ${\varrho}_2$ and ${\varrho}_3$ (${\varrho}_4$), is non-overlapping.
Therefore, restricting to a subsystem without ${\varrho}_2$
can only provide a partial analysis of confluence of $\Rultrs{\aRul}'$;
the (non-overlapping) interaction between $\Rultrs{\dRul}$ and $\binap{\ssetdif}{\Rultrs{\aRul}}{\Rultrs{\dRul}}$
is not accounted for, and indeed that is fatal here.
The intuition for our proof is that the problem is that
the number of such interactions is unbounded due to the presence
of the duplicating and non-terminating rule ${\varrho}_3$ (and ${\varrho}_4$) in $\Rultrs{\dRul}$,
and that requiring termination of $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ bounds that number
and suffices to regain confluence.
This is verified by showing that $\twoheadrightarrow_\Rultrs{\dRul} \cdot \mathrel{\wash{\,\,\,\circ}\mathord{\longrightarrow}}_\Rultrs{\aRul}$ has
the diamond property.
\begin{lemma}
\label{lem:abstract_criterion}
Let ${\to_\AA} = \bigcup_{a \in I} {\to_a}$ be a relation equipped with a
well-founded order $\succ$ on a label set $I$, and let $\to_\mathcal{B}$ be a
confluent relation with ${\to_\mathcal{B}} \subseteq {\twoheadrightarrow_\AA}$.  The relation
${\to_\AA}$ is confluent if
\begin{enumerate}
\item
\(\binap{\srelsco}{\zp{\aarsinv}{a}}{\ip{\aars}{b}}
  \subseteq
  (\binap{\srelsco}{\ip{\aars}{\AA}}{\zp{\aarsinv}{\AA}}) \cup
  \bigcup_{\{ a,b \} \succ_{\mathsf{mul}} \{ a',b' \}}
  (\binap{\srelsco}{\zp{\aarsinv}{a'}}{\binap{\srelsco}{\ip{\aarsequ}{\mathcal{B}}}{\ip{\aars}{b'}}})
\)
for all
$a, b \in I$; and
\item
\(
{\binap{\srelsco}{\zp{\aarsinv}{a}}{\ip{\aars}{\mathcal{B}}}}
\subseteq
 \binap{\srelsco}{(\ip{\aarstre}{\mathcal{B}}}{\zp{\aarsinv}{a})} \cup
 \bigcup_{a \succ a'} (\binap{\srelsco}{\ip{\aarstre}{\mathcal{B}}}{\binap{\srelsco}{\zp{\aarsinv}{a'}}{\ip{\aarsequ}{\mathcal{B}}}})
\)
for all
$a \in I$.
\end{enumerate}
Here $\succ_{\mathsf{mul}}$ stands for the multiset extension of $\succ$.
\end{lemma}
\begin{proof}[Sketch]
Let ${\rightarrowtail} \isdefd \binap{\srelsco}{\ip{\aarstre}{\mathcal{B}}}{\ip{\aars}{\AA}}$.
We claim that
\(
  \binap{\srelsco}{\zp{\aarsinv}{a}
}{\binap{\srelsco}{\aiarsnco{m}{\mathcal{B}}
}{\binap{\srelsco}{\ezp{\aarsinv}{n}{\mathcal{B}}
        }{\ip{\aars}{b}
        }}}
  \subseteq
  \binap{\srelsco}{{\rightarrowtail}
        }{{\leftarrowtail}
        }
\)
holds for all labels $a, b$ and numbers $m, n \geqslant 0$.
The claim is shown by well-founded induction on $(\{a,b\}, m + n)$ with
respect to the lexicographic product of $\succ_{\mathsf{mul}}$ and the greater-than
order ${>}$ on $\mathbb{N}$.
Thus, the diamond property of
${\rightarrowtail}$ follows from the claim and confluence of $\mathcal{B}$.  As
${\to_\AA} \subseteq {\rightarrowtail} \subseteq {\twoheadrightarrow_\AA}$, we conclude
confluence of $\AA$ by e.g.~\cite[Proposition~1.1.11]{Tere:03}.
\end{proof}
\begin{proof}[of Theorem~\ref{thm:cpcs} by Lemma~\ref{lem:abstract_criterion} ]
  Let $I$ comprise pairs of a term and a natural number,
  and define $\iarsa{\pair{\hat{\atrm}}{{n}}}{{t}}{{s}}$ if
  $\iarstrea{\Rultrs{\aRul}}{\hat{\atrm}}{\iarsdeva{\Rultrs{\aRul}}{{t}}{{s}}}$
  with ${n}$ the maximal length of a development of the multistep,\footnote{%
By the Finite Developments Theorem lengths of such developments are finite~\cite{Tere:03}.}
  and $\ip{\aars}{\mathcal{B}} \isdefd \ip{\aars}{\Rultrs{\dRul}}$,
  in Lemma~\ref{lem:abstract_criterion}.
  As well-founded order $\succ$ on indices we
  take the lexicographic product of $\Rultrs{\dRul}_{\m{d}}/\Rultrs{\aRul}$ and
  greater-than ${>}$.
  Henceforth the proof and its case analysis of peaks
  follows the above decreasing-diagrams-based proof.
  Because of this, we only present the interesting case, leaving the others to the reader:
  \begin{itemize}
  \item
    Suppose $\iarsinva{\pair{\hat{\atrm}}{{n}}}{{s}}{\iarsa{\Rultrs{\dRul}}{{t}}{{u}}}$
    where the steps do not have overlap. Then
    by Lemma~\ref{lem:horizontal}(\ref{ite:horizontal:non-overlap}),
    $\relap{\binap{\srelsco}{\ip{\aarsdev}{\Rultrs{\dRul}}}{\zp{\aarsdevinv}{\Rultrs{\aRul}}}}{{s}}{{u}}$,
    so $\relap{\binap{\srelsco}{\ip{\aarstre}{\Rultrs{\dRul}}}{\zp{\aarsdevinv}{\Rultrs{\aRul}}}}{{s}}{{u}}$.
    Distinguish cases on the type of
    the $\Rultrs{\dRul}$-rule employed in $\iarsa{\Rultrs{\dRul}}{{t}}{{u}}$.

    If the rule is duplicating, then
    $\relap{\binap{\srelsco}{\ip{\aarstre}{\Rultrs{\dRul}}}{\zp{\aarsinv}{\pair{{u}}{{m}}}}}{{s}}{{u}}$
    for ${m}$ the maximal length of a development of the
    $\ip{\aarsdev}{\Rultrs{\aRul}}$-step from ${u}$, and condition~2 is satisfied as
    $\iarsa{\Rultrs{\dRul}_{\m{d}}}{{t}}{{u}}$ implies
    $\pair{\hat{\atrm}}{{n}} \succeq \pair{{u}}{{m}}$.

    If the rule is non-duplicating, then
    $\relap{\binap{\srelsco}{\ip{\aarstre}{\Rultrs{\dRul}}}{\zp{\aarsinv}{\pair{\hat{\atrm}}{{n}}}}}{{s}}{{u}}$
    as $\iarstrea{\Rultrs{\aRul}}{\hat{\atrm}}{\iarsa{\Rultrs{\aRul}}{{t}}{{u}}}$ by assumption and
    the length of the maximal development of the residual multistep
    does not increase
    when projecting over a linear rule.
    Again, condition~2 is satisfied. \qed
  \end{itemize}
\end{proof}

\section{Implementation and experiments}
\label{sec:implementation}

The presented confluence techniques have been implemented in the confluence
tool \SAIGAWA version~1.12~\cite{Hiro:Klei:12}.
We used the tool to test the criteria on $432$ left-linear TRSs in
COPS~\cite{Hiro:Nage:Midd:18}
Nos.~1--1036, where we ruled out duplicated problems.  Out of $432$
systems, $224$ are known to be confluent and $173$ are non-confluent.

We briefly explain how we automated the presented techniques.  As
illustrated in Example~\ref{ex:nats:2},
Theorem~\ref{thm:cpcs} can be used as
a stand-alone criterion.
The condition $s \to_\Rultrs{\aRul}^* \cdot \fromBT{\Rultrs{\aRul}}{=} t$ of strong
closedness is tested by
$s \to_\Rultrs{\aRul}^{\leqslant 5} \cdot \fromBT{\Rultrs{\aRul}}{=} t$.
For a critical peak $s \leftarrow \cdot \to t$ of $\Rultrs{\dRul}$,
hot-decreasingness is tested by
$s \twoheadrightarrow_\Rultrs{\dRul} \cdot \tfromB{\Rultrs{\dRul}} t$.
For any other critical peak $s \fromB{{\ell}} \cdot \to t$,
we test
the disjunction of
\(
s \to_{\ordhotdwna{{\ell}}}^{\leqslant 5} \cdot
\mathrel{\zp{\aarsdevinv}{\ordhotrefdwna{{\ell}}}} t
\)
and
\(
s \twoheadrightarrow_\Rultrs{\dRul} \cdot \mathrel{\zp{\aarsdevinv}{\ordhotrefdwna{{\ell}}}} t
\)
if it is outer--inner one, and if it is overlay, the disjunction of
\(
s \to_{\ordhotdwna{{\ell}}}^{\leqslant 5} \cdot
\mathrel{\zp{\aarsdevinv}{\ordhotrefdwna{{\ell}}}} t
\)
and $s \twoheadrightarrow_\Rultrs{\dRul} \cdot \tfromB{\Rultrs{\dRul}} t$ is used.  Order constraints for
hot-labeling are solved by SMT solver Yices~\cite{Dute:14}.
For proving (relative) termination we employ the termination tool NaTT
version~1.8~\cite{Yama:Kusa:Saka:14}.
Finally, suitable subsystems $\Rultrs{\dRul}$ used in our criteria are searched by
enumeration.

Table~\ref{tab:experiments} gives a summary of the
results.\footnote{Detailed data are available from:
\url{http://www.jaist.ac.jp/project/saigawa/19cade/}}
The tests were run on a PC equipped with Intel Core
i7-8500Y CPU (1.5 GHz) and 16 GB memory using a timeout of $60$ seconds.
For the sake of comparison we also tested
Knuth and Bendix' theorem (\textsf{kb}),
the strong closedness theorem (\textsf{sc}), and
development closedness theorem (\textsf{dc}).
As theoretically expected,
they are subsumed by their generalizations.
\begin{table}[tb]
\caption{Experimental results}
\label{tab:experiments}
\centering
\begin{tabular}{l@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\toprule
& Thm.~\ref{thm:hot}
& Thm.~\ref{thm:cpcs}
& Cor.~\ref{cor:gsc}
& \textsf{kb}
& \textsf{dc}
& \textsf{sc}
\\[0.5ex]
\# proved (\# timeouts)
& 101 (46)
& 81 (24)
& 94 (15)
& 45 (18)
& 34 (1)
& 62 (1)
\\
\bottomrule
\end{tabular}
\end{table}

\section{Conclusion and future work}
\label{sec:conclusion}

We presented two methods for proving confluence of TRSs,
dubbed critical-pair-closing systems and hot-decreasingness.
We gave a lattice-theoretic characterisation of overlap.
Since many results in term rewriting, and beyond, are
based on reasoning about overlap, which is notoriously hard~\cite{Nage:Midd:16},
we expect that formalising our characterisation
could simplify or even enable formalising them.
We expect that both methods
generalise to commutation, extend to
HRSs~\cite{Mayr:Nipk:98}, and can be
strengthened by considering rule \emph{specialisations}.
\begin{example} \label{exa:half:levy:1}
  Analysing the TRS $\Rultrs{\aRul}$ of Example~\ref{exa:half:levy}
  one observes that for closing the critical pairs
  only (non-duplicating) \emph{instances} of the duplicating rules
  ${\varrho}_3$ and ${\varrho}_4$ are used. Adjoining these specialisations
  allows the method to proceed:
  Adjoining
  ${\varrho}_{3}(a) \hastype \binap{\srulstr}{f(c,a)}{f(a,a)}$ and
  ${\varrho}_{4}(a) \hastype \binap{\srulstr}{f(a,c)}{f(a,a)}$ to $\Rultrs{\aRul}$
  yields a (reduction-equivalent) TRS
  having critical-pair-closing system
  $\{ {\varrho}_1, {\varrho}_{3}(a), {\varrho}_{4}(a), {\varrho}_5 \}$.
  Since this is a linear system without critical pairs,
  it is confluent, so $\Rultrs{\aRul}$ is as well.
\end{example}

\bibliographystyle{splncs04}

redpajama_set_name: RedPajamaArXiv


The German American Trade Affiliation is a nonprofit group that offers seminars and advice on web site selection, funding, customs affairs, and finding brokers and distributors for companies seeking to do business with the U.S. Exam candidates will obtain an utility for licensure at the test centers upon passage of the examination. Create an Online Account with TREC, Submit Online Software for Inactive Salesperson, and Send them your Course Completion Certificates.
Two varieties PearsonVue offers you when you move the 2 sections of the State Exam. As a way to qualify for the Salesperson State Exam, you have to full: Actual Property Rules, Actual Property Observe, and one elective course of your selection.
Examine Information to Passing the State Real Estate Exam. Colleges are required by legislation to take care of course completion data for three years. Every scholar has the power to attend / repeat the course as wanted till the scholar has the Nevada Actual Estate license.
Since it's such an emotional purchase, buyers may go back to the same house(s) multiple occasions, which might be a bit irritating. Larson Academic Providers provides the best quality actual property education available. EAccessny is a safe, password-protected occupational licensing management system obtainable online 24/7.
Workplaces of real estate agents and brokers have been named the fastest-rising trade based mostly on a study by Sageworks , a monetary information company. Plus, you get a further three programs to satisfy your Gross sales Agent Apprentice Education (SAE) requirement. Most pre-licensing programs present students with pattern tests, and lots of real estate commissions publish sample questions online.
State particular: All of our programs are approved by each state's real estate fee guaranteeing you're absolutely versed within the related legal guidelines and rules governing your state. Applicants with an lively license in a non-reciprocal state must adjust to Minnesota dealer license necessities.


text:
HomeSouthern Methodist University
credit: Jeffrey Beall/license
www.smu.edu
6425 Boaz St, Dallas, TX 75275-0221
Southern Methodist University is a large private university located in Dallas, TX ranked 95th in the United States. It has a total of 6,947 full-time undergraduate students and is not very competitive, accepting 47.29% of applicants. Southern Methodist University offers 217 different majors and is best known for its Office Management and Supervision, Fitness Administration, and Real Estate programs (nationally ranked 2nd, 9th, and 9th respectively). With an annual tuition of $50,200 per year, Southern Methodist University is exceptionally expensive. 70.9% of students graduate starting the next phase of their lives, working. After finishing their studies, alumni go on to earn close to $60,700 per year, which is 46% greater than the national median.
2022 Best Colleges for Office Management and Supervision in America
2022 Best Accredited Online Colleges for Office Management and Supervision in America
2022 Best Accredited Online Colleges for Finance in America
https://www.smu.edu/Admission/Apply
9% Finance, General5% Economics, General5% Accounting81% Others
9% Finance, General
5% Economics, General
5% Accounting
Economics, General
Office Management and Supervision
Sport and Fitness Administration/Management

redpajama_set_name: RedPajamaCommonCrawl


text:
Study Group:
All About Campaigns
Bill Carrick
Spring 2023 Fellow, Center for the Political Future
Bill Carrick is a strategic and media consultant for candidates and ballot initiatives in California and nationally.
Bill is the founder of the firm, Carrick Consulting, Inc., which specializes in the creation, production, and placement of advertising for candidates, ballot initiatives, and organizations.
Clients have included: Senator Dianne Feinstein's campaigns for Senate and Governor, LA Mayor Eric Garcetti and former LA Mayors James Hahn and Dick Riordan, President Bill Clinton, Democratic Leader Dick Gephardt, House Democratic Whip Jim Clyburn, the Democratic Congressional Campaign Committee, and The Democratic Senatorial Campaign Committee.. In California, Carrick has handled over a dozen successful campaigns for Democratic Candidates running for Statewide Constitutional Offices. Most recently, Carrick worked for Los Angeles Sheriff-Elect Robert Luna.
Bill Carrick has developed communications and advertising strategies for several ballot initiatives, including defeating tort reform initiatives, school vouchers, San Fernando Valley and Hollywood secessions from Los Angeles, Governor Schwarzenegger's redistricting scheme, and he successfully managed the passage of a New LA City Charter. In addition, he created the advertising campaign and strategy for New Mexico Governor Bill Richardson's successful education initiatives.
In 2016, Carrick was the strategic and media consultant for the passage of Los Angeles County's Measure M, the largest local infrastructure measure in the nation, winning over 70% of the vote. In the 2017 LA City Elections, he supervised and created the television and on-line advertising for the No on Measure S campaign. He was also lead strategist and media consultant for Mayor Eric Garcetti's 2017 re-election and served in that capacity for Senator Dianne Feinstein's 2018 re-election.
Bill grew up in South Carolina where he began his career in politics and advertising. He went on to work in Washington, DC as Senator Ted Kennedy's political director and later as campaign manager for the 1988 Gephardt for President Campaign before moving to California.
Study Group: All About Campaigns
"All About Campaigns" does a deep dive into all aspects of local, state, and federal campaigns. Examine strategy and tactics, messaging, organizing, fieldwork, coalition building, media and advertising, issues, and policy. Students will create and develop rival campaign plans.
Mondays, 3 - 5 p.m. PT, SOS B15
End Date: April 10, 2023
Apply for the study group with Bill Carrick


But first, a little bit of me.
My son has left for a month long trip to Indonesia, and as per his usual, he waited til the last minute to get stuff done. He did start early but faltered near the end. It came to packing and travel snacks; this is where we are polar opposites.
I am a planner and I like to be well ready, waaaaaay before hand. Like, packed suitcases 2 weeks before with lists, photocopies of important documents, snacks & food stuffs prepped for a quick throw it all together and bake it up the night before, and all meds/necessities Ziploc-ed and good to go. I even buy the book(s) I am going to read 2 weeks before and torture myself by keeping them in plain view, while not allowing myself to even have a sneak peak read. It makes the travel day extra fun to look forward to, along with the actual trip of course.
We had planned on pre-prep a week before, he said all was fine. Yeah right.
"Mom, do you have any yummy snacks for travelling? Like those muffin thingy's you were talking about?"
My son, 23 and still flying by the seat of his pants. He also trains a lot and lkes healthier and gf options.
Good thing I had just made myself a batch of muffins and had frozen cookie dough on hand-just in case. Turns out neither items made it to flight, apparently both were too tasty to resist. He even exchanged one of the muffins for a free java jolt from one of his friends who works at a coffee shop. She texted him a while later exclaiming they're "soooo good" tastiness.
We were having fun being silly, taking selfies or togethers? Meh. You get the point.
We caught up on life moments, cracked jokes, talked street food and safety stuff for travel. We were both excited for his first, long, far away, travel adventure. I prayed so hard for his safety and continue to do so, he landed safely and has begun to have fun. I need a vacation. Maybe baking travel muffins will kick-start my next get away. Sooner than later, I hope. Pb, we need to get this wagon train a movin'.
Well, this Paleo muffin recipe is one I make the day before I get on a plane. There are no refined sugars, no soy, no dairy, and it is vegetarian. I like that it has loads of fiber, good fats, protein, and tastes outrageously good. I kid you not, whenever I go to Poppa Bear, these come on flight with me. Pb likes to munch on the remaining one's and looks forward to eating these nom nom's of delight. He always asks if I am bringing them with when I come see him.
They are not a light and fluffy, cake muffin, like you are used to. These are more compact, smaller, more dense, and nutritionally sound-also filling. They are a perfect travel food and have helped me when stuck places where allergy-free items are not available.
This recipe comes from my mother, she found a recipe somewhere, didn't like it, and gave it a great makeover.
Typical pastry Chef, I get it from her honestly.
I further tweaked the recipe, I reduced the eggs and upped the flax. These are not nut-free, they contain almonds, you can try with different nuts if you like.
Here goes, and as always there are pics to guide you down below.
-Mix together until well combined, add in frozen fruit, stir until just incorporated.
-Bake for 20 minutes, turn tray halfway and bake for another 15-20 minutes.
-Only remove from oven when golden brown, allow to cool in tray.
-Remove from tray and enjoy!
-Store in an airtight container in fridge for up to 5 days, can freeze up to 2-3 weeks.
Mixing flax eggs to sit as I prep the dry and then wet ingredients.
These get a light golden brown on them, they are perfect when they look like the above pic on the left. It is as I stated before, a more dense, not high baking, empty calories, sugar laden fluff.
They are healthy but remember that these are high in good fats, and too much of anything is not a good thing.
Eat max 1 or 2 per day, you will be fine.
Any questions or comments can be left down below, I like hearing from you, and feel free to test these on your next trip and tell us all about it!


text:
Q: Access Type Mismatch Having two tables:
MyTable1:
  id       AutoNumber
  typecode Text

MyTable2
  id      AutoNumber
  pid     Number
  freq    Number

using System.Data.OleDb;
namespace AccessSelect
{
    class Program
    {
        static void Main(string[] args)
        {
            var sql = @"select 'x' from mytable1 where typecode=@typeCode and EXISTS (
                        select 'x' from mytable2 where (freq=0 OR freq=@freq) and mytable1.id=mytable2.pid)";

            using (OleDbConnection conn = new OleDbConnection(@"Provider=Microsoft.Jet.OLEDB.4.0;Data Source=gpi.mdb;Jet OLEDB:Database Password=???"))
            {
                conn.Open();
                OleDbCommand cmd = new OleDbCommand(sql, conn);

                cmd.Parameters.Add(new OleDbParameter("@typeCode", "KK3000"));
                cmd.Parameters.Add(new OleDbParameter("@freq", 50));

                var o = cmd.ExecuteScalar();
            }
        }
    }
}

I keep getting the exception 'Data type mismatch in criteria expression.'
If I change the SQL to contain the values:
select 'x' from mytable1 where typecode='KK3000' and EXISTS (
 select 'x' from mytable2 where (freq=0 OR freq=50) and  mytable1.id=mytable2.pid)

I don't get the error....
Any idea to what is wrong?

A: From MSDN:

The OLE DB .NET Provider does not support named parameters for passing
  parameters to an SQL statement or a stored procedure called by an
  OleDbCommand when CommandType is set to Text. In this case, the
  question mark (?) placeholder must be used. For example:

So change your query to:
select 'x' from mytable1 where typecode = ?
     and EXISTS (select 'x' from mytable2 where (freq=0 OR freq = ?) and mytable1.id=mytable2.pid)

And you have to add parameters in the same order as they occur in query.

A: Changed it to:
static void Main(string[] args)
{
    var sql = @"select 'x' from mytable1 where typecode=@typeCode and EXISTS (
                select 'x' from mytable2 where (freq=0 OR freq=@freq) and mytable1.id=mytable2.pid)";

    using (OleDbConnection conn = new OleDbConnection(@"Provider=Microsoft.Jet.OLEDB.4.0;Data Source=gpi.mdb;Jet OLEDB:Database Password=???"))
    {
        conn.Open();
        OleDbCommand cmd = new OleDbCommand(sql, conn);

        cmd.Parameters.Add(new OleDbParameter("@freq", 50));
        cmd.Parameters.Add(new OleDbParameter("@typeCode", "KK3000"));

        var o = cmd.ExecuteScalar();
    }
}

and now it seems to work... a bit strange though...

redpajama_set_name: RedPajamaStackExchange


text:
Paddy Power's Oscar Pistorius ad to be pulled after record 5,200 complaints
Watchdog says ad offering 'money off if he walks' in murder trial is likely to cause widespread offence, as 122,000 sign petition
Part of Paddy Power's ad featuring a mock-up of Oscar Pistorius as an Academy Award
Wed 5 Mar 2014 11.25 EST
The advertising watchdog has ordered Paddy Power to pull its controversial ad featuring Oscar Pistorius, after a wave of protest has seen it become the most complained-about campaign ever.
The advert shows a photograph of Pistorius superimposed on a statue of an Oscar award. Next to it, the ad states "It's Oscar Time. Money back if he walks. We will refund all losing bets on the Oscar Pistorius trial if he is found not guilty."
The Advertising Standards Authority has so far received 5,200 complaints about the press ads, which offer refunds for losing bets if the South African Paralympian is found not guilty of the murder of his girlfriend Reeva Steenkamp.
The wave of complaints has in part been fuelled by an online petition on Change.org which has attracted more than 122,000 signatures.
The ASA said the strength of the public outcry has forced it to take the "unusual step" of telling Paddy Power to pull the ad immediately.
The watchdog will usually allow a campaign to continue to run until it has finished its investigation into whether there has been a breach of the UK advertising code.
In the case of the Pistorius ad the ASA is investigating whether the ad is offensive for trivialising issues surrounding a murder trial, the death of a woman and disability.
The watchdog said that it is also looking at whether the ad "brings the good reputation of advertising generally into dispute".
"We consider the ad may be seriously prejudicial to the general public on the ground of the likely further serious and/or widespread offence it may cause," the ASA said in a statement published on Wednesday. "We are also concerned that the good reputation of the advertising industry may be further damaged by continued publication of this ad."
The ASA said that the ad should "remain out of all circulation in UK media" until it finishes its investigation, which is being fast tracked.
It is not investigating complaints about the ad appearing on Paddy Power's website, as the company is based in Ireland and is out of the remit of the UK watchdog.
The number of complaints dwarfs the previous record holder, an ad for KFC that featured people in a call centre singing with their mouths full, which drew 1,671 complaints.
A spokesman for Paddy Power said that the ad was only meant to run as a one-off on Sunday following the Oscars, was not part of a longer media campaign, and only ran in the Sun on Sunday in the UK.
"Jean Hatchet [who started the petition on Change.org] has run an incredibly fast-paced and powerful campaign on the site," said John Coventry of Change.org. "The past 48 hours have seen a powerful outpouring of support for her story which has pushed the ASA to act."
Oscar Pistorius trial accidentally sees images of Reeva Steenkamp's body
Michel Roux Jr criticises 'frustrating' BBC as he leaves MasterChef
Peppa Pig: wallowing in bad language?
Oscar Pistorius trial – live coverage – Thursday 13 March 2014
Oscar Pistorius murder trial: court is shown photos of blood stains at house
John Humphrys: pro-Europe BBC shied away from immigration debate
Oscar Pistorius trial: bat-wielding moment could be crucial to case
BBC ready to contemplate alternative to the compulsory licence fee
Oscar Pistorius clashed with police officer who took his gun, court told
David Cameron mocked for paying for Facebook friends


text:
Damascus Countryside: Arbin Locals Speak Out Against Fatah Al-Sham Violations
Monday October 10th, 2016 by ARA News (Kurdish website)
Eastern Ghouta residents warn key Islamist group against continued violations as possibility of unrest heightens
Citizens and revolutionary groups from Arbin in Eastern Ghouta, Damascus countryside, issued a statement late last week expressing their discontent with the violations of Jabhat Fatah al-Sham rebel group, formerly known as Nusra Front.
The statement, which was signed by a number of local relief and security bodies, said that "after their long silence and patience about the violations of Nusra Front, the people and organizations of Arbin demand a stop to the interference in civilian's issues and in their revolutionary and public institutions."
The signatories called for the release of all prisoners in Fatah al-Sham's prisons, namely Hajj Khaled Abou Wahbi, the chairman of the neighborhoods committees in Arbin. They also stressed that the key rebel group would be held responsible for any social movement that might erupt as a result of the violations.
The statement added: "Mesbah Yassin, a Jabhat Fatah al-Sham commander, has become illegitimate after the latest violations including inciting arrests, spreading rumors and lies about the committees and institutions of Arbin city and using his soldiers to carry out his objectives."
Aladdin Kurdi, a media activist from the Damascus countryside, told ARA news that "a state of discontent and anger spread among the civilians and organizations in the city. The local committees sent many appeals to the leadership of Jabhat Fatah Al-Sham but there was no response. A social movement might start in the city if [the group] does not put an end to its members' violations."


The recent tragedy in Orlando has darkened the colorful month of June, which is gay pride month. Typically during gay pride we can acknowledge and celebrate our identities and all of the accomplishments and successes the LGBTQ community has achieved. This year there are many other feelings present: sadness, loss, grief, and anger, to name a few. So how can we celebrate in light of such a horrific event, when so many are in pain?
In these moments we are left with having to experience multiple, often conflicting feelings and parts. It might be tempting to avoid these feelings, to isolate, or to engage in compulsive behaviors as an escape. However, if we allow ourselves to experience these feelings, we begin to strengthen those "feeling muscles" and learn how to better manage our emotions. It then becomes a little easier to manage those difficult emotions and allow ourselves to focus on the positive aspects of celebrating our pride.
Gay pride is a time when we can all acknowledge and appreciate what we are proud of in ourselves. This is a time when we can stop focusing entirely on our deficits and focus on our successes, accomplishments, and strengths. In this gay pride month, both pain and joy are felt. Neither is more important than the other. What is important is to manage and share our feelings in a way in which we can embrace the celebration of pride while honoring the tragedy of Orlando and the work that remains.
Experience Wellness Group provides LGBTQ-friendly individual, group, couples and family therapy. We also offer grief counseling and supportive psychotherapy. Our new weekly group focuses on learning tools to manage difficult emotions. Please call 917-362-9770 or email us at adrienne.glasser@gmail.com for more information or to set up an appointment.
Leon Silvers, LMHC is a primary and group therapist at Experience Wellness Group. At Experience Wellness he treats adults, families, couples and teens through mindful psychotherapies.
Thank you for writing this eloquent short piece. I enjoyed it. You articulated the complexity of the tragic events of Orlando coupled with the acknowledgement and appreciation of progress made in according LGBTQ community a central, as opposed to a marginal, place in our communities well.


text:
Q: Wordpress get post content and upgrade a page I am stuck to upgrade my function.php in order to:
check if there is draft post
if there is get the content, title and category
if there is a page with title = post_category upgrade the content of the page
with the post_content(and post_title)
else create a page with title = post_category and content = post_content and post_title
The code
add_action( 'wp_insert_post', 'privatepostcheck' );

function privatepostcheck(){

    $args = array(
              'post_type' => 'post',
              'post_status' => 'draft'
              );
    // get the draft post
    $posts_array = get_posts( $args );
    foreach($posts_array as $post){
        // foreach draft post get title, content and category
        $posttext = get_the_content($post);
        $postcate = get_the_category($post);
        $postitle = get_the_title($post);

        //check if there is page with name = post category
        //get the page
        $page = get_page_by_title( $postcate );
        //get content
        $content_page = apply_filters('the_content', $page ->post_content);
        $content_post = apply_filters('the_content', $post->post_content);
        $page = array(
                'post_content' => "asidasoidjasoidjsaoi<br>".$content_page,
            );
        wp_update_post( $page );
}