%%
%%
\documentclass{llncs}
%\documentclass[a4paper,11pt,twocolumn]{article}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

% \usepackage[scrtime]{prelim2e}
\usepackage{latexsym}
\usepackage{amssymb}
% \usepackage{exptrees}
\usepackage{url}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2

%\newtheorem{theorem}{Theorem}[subsection]
%\newtheorem{theorem}{Theorem}[section]

%\newcounter{theorem}[section]
% \def\thedefinition{\thesection.\arabic{theorem}}

% \newenvironment{theorem}{
%  \refstepcounter{theorem}
%   \trivlist
%    \item[\hskip\labelsep{\bf Theorem \thedefinition}.]}%
%    {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}

% \newcommand{\qed}{}

% \newenvironment{proof}{
 % \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

\newtheorem{condition}{Condition}
% \newtheorem{definition}{Definition}[section]

% \newcounter{definition}[section]
% \def\thedefinition{\thesection.\arabic{definition}}

% \newenvironment{definition}{
%  \refstepcounter{definition}
%   \trivlist
%    \item[\hskip\labelsep{\bf Definition \thedefinition}.]}%
%     {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}

% \newtheorem{lemma}{Lemma}[section]

% \newcounter{lemma}[section]
% \def\thedefinition{\thesection.\arabic{lemma}}

% \newenvironment{lemma}{
%  \refstepcounter{lemma}
%   \trivlist
%    \item[\hskip\labelsep{\bf Lemma \thedefinition}.]}%
%     {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}

% \newtheorem{corollary}{Corollary}[section]
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble


\newcommand{\SN}{\textit{SN}}
\newcommand{\ISN}{\textit{ISN}}
\newcommand{\lpo}{\textit{lpo}}
\newcommand{\lex}{\textit{lex}}
\newcommand{\fwf}{\textit{fwf}}
\newcommand{\ctxt}{\textit{ctxt}}
\newcommand{\cons}{\textit{cons}}
\newcommand{\nil}{\textit{nil}}

\newcommand\cfile{}

\newcommand\comment[1]{} 
% \newcommand\cc[1]{} % for label names 
\newcommand\cc[1]{#1} % for label names 
% \renewcommand\footnote[1]{} % for footnotes
% \pagestyle{myheadings}

% \newcommand{\mystrut}[1]{
% \bpf \A ; "$\vphantom{X}$" \U ['] ; "$\vphantom{X}$" "#1" \epf \ %
% }

\newcommand{\idrule}[2]{
 \mbox{#1 \ $\mbox{#2}$}}

\newcommand{\ds}{\displaystyle\strut}

\newcommand{\urule}[3]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}}{\ds \mbox{#3}}$}}


\newcommand{\brule}[4]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}\ \ \ \ \mbox{#3}}
                   {\ds \mbox{#4}}$}}


\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\cut{(\emph{cut})}
\newcommand\dt{\texttt{dt}}
\newcommand\dtn{\texttt{dtn}}

\newcommand{\pordered}[3]{#1 <_{{#2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{{#2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}
\newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{plain}

\begin{document}

%% Here begins the main text

\title{A General Theorem on Termination of Rewriting}

\author{
 Jeremy E.\ Dawson \ \ and \ \ Rajeev Gor\'e
}

\institute{
Logic and Computation Program, NICTA
\thanks{National ICT Australia is funded by the Australian Government's
Department of Communications, Information Technology and the Arts and
the Australian Research Council through Backing Australia's Ability
and the ICT Centre of Excellence program}
and
\\ Automated Reasoning Group
\\ Australian National University,
   Canberra, ACT 0200, Australia
% following amended since publication, was email addresses
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} \ \ 
  \url{http://users.rsise.anu.edu.au/~rpg/}
}

\date{\today}

%% Title
\maketitle

\begin{abstract}
  We re-express our theorem on the strong-normalisation of display
  calculi as a theorem about the well-foundedness of a certain
  ordering on first-order terms, thereby allowing us to prove the
  termination of systems of rewrite rules. We first show how to use
  our theorem to prove the well-foundedness of the lexicographic
  ordering, the multiset ordering and the recursive path ordering.
  Next, we give examples of systems of rewrite rules which cannot be
  handled by these methods but which can be handled by ours.
  Finally, we show that our method can also prove the termination of
  the Knuth-Bendix ordering and of dependency pairs. \\
  {\bf Keywords}: rewriting, termination, well-founded ordering,
  recursive path ordering

\end{abstract}

\section{Introduction}
\label{s-id}

% A rewrite system consists of a set of equations to be
% used repeatedly to change a term to an equivalent, more tractable
% form.  They can be used in computation or automated reasoning.  While
% it is possible to do this using a particular strategy (choice of
% subterm to be rewritten and rule to be used), it is desirable that,
% regardless of the strategy used, the rewriting procedure terminates,
% and finishes with the same term (which would be \emph{normal}, or not
% further rewriteable).

% This paper addresses the issue of termination.
% It arises out of earlier work on cut-elimination.
% In \cite{dawson-gore-formalised-cut-admissibility} we 
% described an implementation in the Isabelle theorem prover of
% the proof of cut-elimination for the Display Calculus for relation algebra.
% There we proved the \emph{existence} of a sequence of 
% ``reductions'' (each of which replaces a use of the ``cut'' rule 
% by another more tractable use, or removes it entirely).
% In \cite{dawson-gore-machine-checked-strong-normalisation} we set out to
% implement in Isabelle a published proof of the strong normalisation
% (or well-foundedness) of the
% cut-elimination procedure (ie, that wherever in the proof tree a 
% reduction was performed, the procedure would terminate).
% In attempting this, we came across a defect in that proof, so we
% devised and machine-checked a new proof.
% (We have subsequently generalised the Isabelle proofs to cover 
% display calculi generally, not just that for relation algebra).

% The cut-elimination procedure can be seen as repeated application of a
% choice of rewrite rules, and the strong normalization proof as a proof
% of termination of this rewrite system.
% We adapted the proof to the more general context of a term rewriting system,
% and have generalized the proof.

% This paper describes that proof in the context of a general rewrite system.
% We show how our theorem can be used to prove the termination of a number 
% of examples of rewrite systems.
% Notably, we obtain as an easy corollary the fact that the multiset order
% derived from a well-founded order is itself well-founded.
% We also derive the well-foundedness of the lexicographic path order
% (the same proof works also for the multiset path order).
% Yet, as we show, although these orders are simplification orders,
% our theorem is not confined to simplification orders.

% \section{New Introduction}

The traditional method for proving the termination of a rewriting
systems uses well-founded orderings \cite{dersh-har}. The traditional method
for proving strong-normalisation of $\lambda$-calculi is to use
structural induction on lambda terms and their types, backed by
auxiliary well-founded inductions. Recently, structural induction on
derivations have been used to prove cut-elimination
\cite{pfenning-structural-lics94} and to prove strong-normalisation of
the generalised sequent framework of display calculi
\cite{dawson-gore-machine-checked-strong-normalisation}.

We re-express our theorem on the strong-normalisation of display
calculi as a theorem about the well-foundedness of a certain ordering
on first-order terms, thereby allowing us to prove the termination of
systems of rewrite rules. We then show how to use our theorem to prove
the well-foundedness of the lexicographic ordering, the multiset
ordering and the recursive path ordering. Next, we give examples of
systems of rewrite rules which cannot be handled by these methods but
which can be handled by ours.  Finally, we show that our method
can also prove the termination of the Knuth-Bendix ordering and of
dependency pairs.

The results in this paper have been
machine-checked using the logical framework Isabelle,
see \url{http://web.rsise.anu.edu.au/~jeremy/isabelle/snabs/}

\paragraph{Related Work:}

Important methods for proving termination of rewrite systems often use
simplification orderings.
These include the recursive path orderings (\cite{dersh-har}, \cite {kl})
and the Knuth-Bendix ordering.
In \S\ref{s-rpo} and \S\ref{sec:knuth-bend-order} we 
use our theorem to prove the well-foundedness of these orderings.

These orderings have been generalised by Ferreira \& Zantema \cite{fz},
Dershowitz \& Hoot \cite{nat-term} and 
Borralleras, Ferreira \& Rubio \cite{bfr}.
% Generalisations of these orderings by Ferreira \& Zantema \cite{fz}
% provides a necessary and sufficient condition for a term rewrite system to
% be terminating.
Their theorems, like ours, are not limited to simplification orderings,
but they prove the well-foundedness of larger relations
which satisfy the subterm property, 
so if they were closed under context (rewrite relations),
they would also be simplification orderings.
Jean Goubault-Larrecq \cite{jgl} has proved results which are more
general in that they replace the notion of subterm with an arbitrary
well-founded relation.  He also generalises methods for dealing with the
$\lambda$-calculus, where the notion of substitution creates difficulties for 
techniques such as ours.

Arts \& Giesl \cite{dps00} describe a method of proving
termination using ``dependency pairs''.  They give key theorems
and extensive development of resulting techniques.  Their method does
not require a simplification ordering or the subterm property. In
\S\ref{s-dps} we use our theorem to prove one of their key theorems.

\subsection{Notation and Terminology} \label{s-not-term}

Assume that we have fixed some syntax for defining ``terms'' like $r$,
$s$ and $t$. We deliberately leave this notion vague for now.

For an irreflexive binary relation $\rho$ on terms, we will write
$(r, t) \in \rho$, $(r, t) \in\ <_\rho$,
$r <_\rho t$ or $t >_\rho r$ interchangeably.
Relations will be assumed irreflexive unless the contrary is stated,
but are not assumed transitive even when written $<_\rho$.
We say $r$ is \emph{strongly normalising}, or is $\in \SN$, 
(with respect to $\rho$)
if there is no infinite descending sequence
$r = r_0 >_\rho r_1 >_\rho r_2 >_\rho \ldots$ of terms,
and $\rho$ is \emph{well-founded} (or \emph{Noetherian})
if every $r \in \SN$.
We write $\leq_\rho$, $<_\rho^+$ and $<_\rho^*$ for the
reflexive closure, the transitive closure 
and the reflexive transitive closure, respectively, of $<_\rho$.
We write $\sigma \circ \rho$ for the relational composition of 
relations $\sigma$ and $\rho$,
in the sense that $(r, s) \in \sigma \circ \rho$ if there exists $t$ such that 
$(r, t) \in \rho$ and $(t, s) \in \sigma$.

Often (see our examples)
such a relation is described by giving a finite set of ``rewrite rules''
$l_i \to r_i$, where $l_i$ and $r_i$ are terms containing 
(meta-)variables for which terms may be substituted.
% But our main theorem does not assume this.

When a relation is defined by a set of rewrite rules, 
it is also usually taken that it is \emph{closed under context},
ie, that where $C[\_]$ is a context (a term with a ``hole''),
and $l$ rewrites to $r$, then $C[l]$ rewrites to $C[r]$.
Often such a relation is called a \emph{reduction}, such as
the ``$\beta$-reduction'' of the lambda calculus.

The setting of our main theorem is that we are given a binary relation
$\rho$ which may or may not consist of the substitution instances of a
finite set of rewrite rules, and which is not necessarily closed under
context. Then we define $\ctxt\ \rho$ to be the closure under context
of $\rho$ and prove that $\ctxt\ \rho$ is well-founded. When $\rho$
consists of the substitution instances of a finite set of rewrite
rules the well-foundedness of $\ctxt\ \rho$ proves that the associated
rewrite system \emph{terminates}.

To formalise  ``closure under context'',
we must specify a language of terms.
This is a first-order language, with 
a fixed set of function symbols, or
term constructors, of fixed or variable (finite) arity,
whose arguments and results are terms.
This language may or may not contain term variables.
The meta-language used to express rewrite rules and to
discuss rewrites \emph{does} contain term variables.

Given a term like $t = f(a,b,g(c,d))$, its \emph{immediate} subterms
are $a, b$ and $g(c,d)$, its \emph{proper} subterms are these and $c$
and $d$, and its subterms are these and also $t$ itself.  We write
$\overline{s}$ for a sequence of terms $s_1, \ldots, s_m$,
such that these
% $s_1,\ldots, s_m$ 
are the {immediate} subterms of $f(\overline{s})$.
We define the ``closure of $\rho$ under context'', $\ctxt\ \rho$:
for example, if $(c', c) \in \rho$, then $(f(a,g(c')),
f(a,g(c))) \in \ctxt\ \rho$.

\begin{definition}[{closure under context}] 
  Given an irreflexive relation $\rho$ and terms $t_0$ and $t_1$, the
  pair $(t_1, t_0) \in \ctxt\ \rho$ (say ``$t_0$ reduces to
  $t_1$'') if either
%  \begin{enumerate}
% \item 
\emph{(a)} $(t_1, t_0) \in \rho$, or
% \item 
\emph{(b)} $t_0$ and $t_1$ are identical except that exactly one
       immediate subterm of $t_0$ reduces to the
       corresponding immediate subterm of $t_1$.
%  \end{enumerate}
\end{definition}

We also define, inductively, the set \SN\ of strongly normalising
terms.
This definition is equivalent, at least in classical logic, to that given in 
\S\ref{s-not-term}.

\begin{definition}[strongly normalising]
\label{defn:SN}
The set \SN\ of strongly normalising terms is the smallest set of
terms such that if every term $t_1$ to which $t_0$ reduces is in \SN\ 
then $t_0 \in \SN$.  It follows that if $t_0$ cannot be reduced then
$t_0 \in \SN$.

\end{definition}

It is to be understood that concepts such as ``strongly
normalising'', ``reduction'', etc, relate to $\ctxt\ \rho$, which is,
itself, closed under context.  It follows therefore that if $t \in
\SN$ then all subterms of $t$ are in \SN.

\section{A Proof of Termination}
\label{s-sn}
%\cc{sn.tex}\cc{s-sn}

We now re-express our theorem about strong-normalisation for display
calculi from \cite{dawson-gore-machine-checked-strong-normalisation}
to make it applicable to term rewriting.

\subsection{Various Well-Founded Orderings}

To prove that $\ctxt\ \rho$ is well-founded, we use a
binary relation $<_{dt}$ on terms, and show that it
is well-founded.
The relation $<_{dt}$ depends on a relation $<_{cut}$,
which we have the freedom to define.
The relation $<_{cut}$ must be well-founded,
and invariably it is a superset of $\rho$.
It will normally, but not necessarily, depend on the parts of the
terms at or near its head (ie the roots of the corresponding 
abstract syntax trees).

\begin{definition}[ $<_{sn1}$, $<_{sn2}$, $<_{dt}$]\label{defn:porders} 
Given $\rho$ and $<_{cut}$ we define three further binary relations on terms, 
$<_{sn1}$, $<_{sn2}$ and $<_{dt}$:
  
\begin{enumerate}
\item\label{defn:porders-sn1} ${t_1} <_{sn1} {t_0}$ 
  if $t_0$ and $t_1$ are the same except that one of the immediate 
  subterms of  $t_0$ is in \SN\ and reduces to the 
  corresponding immediate subterm of $t_1$.
  
\item\label{defn:porders-sn2} ${t_1} <_{sn2} {t_0}$ 
  if $t_0$ and $t_1$ are the same except that a proper
  subterm of  $t_0$ is in \SN\ and reduces to the 
  corresponding proper subterm of $t_1$.
  
\item\label{defn:porders-dt} 
  $\dtord{t_1}{t_0}$ iff either
   $\cutord{t_1}{t_0}$ or $\snoneord{t_1}{t_0}$.

\end{enumerate}
\end{definition}

Note that ${t_1} <_{sn1} {t_0}$ implies ${t_1} <_{sn2} {t_0}$, and our
main theorem uses only $<_{sn1}$.  However $<_{sn2}$ is sometimes
easier to work with because it is closed under context. We also define
an auxiliary function \fwf\ for ``from well-founded'' which maps a
binary relation $\rho$ to a binary relation $\fwf\ \rho$ as below:
\begin{definition}
Given a relation $\rho$, the pair $(r, t) \in \fwf\ \rho$ if and only if
$(r, t) \in \rho$ and $t$ is strongly normalising (for $\rho$).
\end{definition}

Clearly $\fwf\ \rho$ is well-founded, regardless of whether $\rho$ is.
We then prove 

\begin{theorem} \label{thm:well-founded-1}
  The relations $<_{sn1}$ and $<_{sn2}$ are each well-founded
  \cite{dawson-gore-machine-checked-strong-normalisation}.
\end{theorem}

Despite the notation, these relations need not be transitive.
Intuitively, $t_1 <_{dt} t_0$
means that $t_1$ is closer to being ``normalised'' (in
some sense) than is $t_0$.

Recall that we require $<_{cut}$ to be well-founded.
We also need $<_{dt}$ to be well-founded.
Given that $<_{cut}$ and $<_{sn1}$ are well-founded,
to prove that $<_{dt}$ is well-founded,
we need one of a number of sufficient conditions on the interaction between
$<_{cut}$ and $<_{sn1}$.

\begin{lemma} \label{wf-rs}
Assume that $\tau$ and $\sigma$ are well-founded relations.
Then each of the following conditions is sufficient for 
$\tau \cup \sigma$ to be well-founded:
\begin{enumerate}
\item \label{tco} $\tau \circ \sigma \ \subseteq\ \sigma^* \circ \tau$,
\item \label{otc} $\tau \circ \sigma \ \subseteq\ \sigma \circ \tau^*$,
\item \label{runs} $\tau \circ \sigma \ \subseteq\ \tau \cup \sigma$,
\item \label{dvk} $\tau \circ \sigma \ \subseteq\ (\sigma 
  \circ (\tau \cup \sigma)^*) \cup \tau$.
\end{enumerate}
\end{lemma}

Of these, the last is from Doornbos \& von Karger \cite{dvk},
and is implied by each of the others,
which are in earlier results discussed and cited in \cite{dvk}. 

Clearly $<_{sn1} \subseteq <_{sn2}$,
so to prove that $<_{dt}$ is well-founded
it is enough to prove that $<_{cut} \cup <_{sn2}$ is well-founded.
Sometimes it is easier to prove 
one of the above conditions for $<_{sn2}$ than for $<_{sn1}$.  

\subsection{Strong Normalisation Induced from Immediate Subterms}

We next define the set \ISN, for ``inductively strongly
normalising'', as the set of terms that are in \SN\ if
their immediate subterms are in \SN.
Clearly, $\SN \subseteq \ISN$.

\begin{definition}[\ISN] \label{ISN} 
A term $t \in \ISN$ iff:
%\begin{quote}
if all the immediate subterms of $t$ are in \SN\ then $t \in \SN$.
%\end{quote}
\end{definition}

The next lemma follows from this definition.
We use only the $\Longleftarrow$ part.

\begin{lemma}\label{hereds-sn}
  A term $t \in \SN$ iff every subterm of $t$ is in \ISN.
\end{lemma}

\begin{proof}
$\Longrightarrow$: Assume $t \in \SN$ and
let $u$ be a subterm of $t$, where $t = C[u]$.
Consider any infinite sequence 
$u = u_0, u_1, \ldots$ of reductions starting with $u$.
Since the reduction relation is closed under context,
$t = C[u_0], C[u_1], \ldots$ is also an infinite sequence of reductions,
contradicting $t \in \SN$.
Therefore $u \in \SN$ and so $u \in \ISN$.

$\Longleftarrow$: By induction on the structure of term $t$ ---
assume that the result holds for each immediate subterm $t'$ of $t$.
Assume that every subterm of $t$, including $t$ itself, is in \ISN.
Therefore each immediate subterm $t'$ of $t$ has the
property that every subterm of $t'$ is in \ISN, and so, by the
inductive hypothesis, $t' \in \SN$.  As each $t' \in \SN$, and $t \in
\ISN$, so $t \in \SN$.  \qed \end{proof}

\subsection{Properties we require of $\rho$}

Finally, given a rewrite system, our result requires that the 
relation $\rho$ satisfy certain properties.
The most general version of these is 

\begin{condition}\label{rpc}
For all $(r, l) \in \rho$,
if all proper subterms of $l$ are in \SN\ then,
for all subterms $r'$ of $r$, either 
\begin{enumerate}
  \item \label{rpc-sn} $r' \in \SN$ or
  \item \label{rpc-dt} $r' <_{dt}^+ l$.
\end{enumerate}
\end{condition}

In practice we use a simpler condition which implies
Condition~\ref{rpc}, such as
\begin{condition}\label{rpc1}
For all $(r, l) \in \rho$,
for all subterms $r'$ of $r$, either 
\begin{enumerate}
  \item \label{rpc-srp} $r'$ is a proper subterm of $l$ 
  or is a subterm of a reduction of a proper subterm of $l$
  \item \label{rpc-cut} $r' <_{cut} l$
  \item \label{rps} 
  $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm.
\end{enumerate}
\end{condition}

For if we assume that all proper subterms of $l$ are in \SN\ as
required in the precondition of Condition~\ref{rpc}, then
Condition~\ref{rpc1}\ref{rpc-srp} implies that $r' \in \SN$, and
\ref{rpc1}\ref{rps} implies that $r' <_{sn1} l$, which implies that 
$r' <_{dt}^+ l$.

Note that sometimes, as in Example~\ref{s-diff}, 
we \emph{enlarge} the relation $\rho$ to satisfy 
Conditions 1 and 2.

\subsection{Strong-Normalisation}

\begin{lemma} \label{dth}
Suppose $\rho$ satisfies Condition~\ref{rpc}, and let $t_0$ be any term.
If all terms ${t' <_{dt}^+ t_0}$ are in \ISN, then $t_0 \in \ISN$.
\end{lemma}

\begin{proof}
Given $t_0$, assume that $\rho$ satisfies Condition~\ref{rpc} and that

(a): all terms $t'$ such that ${t'} <_{dt}^+ {t_0}$ are in \ISN.

\noindent We need to show $t_0 \in \ISN$, so we assume that 

(b): all immediate subterms of $t_0$ are in \SN,

\noindent and we show that $t_0 \in \SN$.

To show that $t_0 \in \SN$, we show that every term $t_1$ that can
be obtained from $t_0$ by a single reduction is in \SN.
We consider the two possible cases:
whether the reduction occurs in a proper subterm of $t_0$, 
or is a reduction of $t_0$ as a whole.

Firstly, consider a reduction in a proper subterm of $t_0$:
that is, $(t_1, t_0) \in \ctxt\ \rho \setminus \rho$.
Then the reduction is in an immediate (strongly normalising) subterm of $t_0$.
So $\snoneord{t_1}{t_0}$ and hence $\dtord{t_1}{t_0}$ by
Definition~\ref{defn:porders}\ref{defn:porders-dt}. 
Therefore $t_1 \in \ISN$ by assumption (a). %~\ref{ass1}.
Now each immediate subterm of $t_1$ is equal to, or is a reduction of,
an immediate subterm of $t_0$,
which itself is in \SN\ by assumption (b). %~\ref{ass2}.
All immediate subterms of $t_1$ are therefore in \SN.
Therefore, as $t_1 \in \ISN$, $t_1 \in \SN$.

Secondly, consider a reduction of the whole term $t_0$: that is, 
$({t_1}, {t_0}) \in \rho$.
Thus we get the new term $t_1$ whose subterms are either in \SN\ 
because of Condition~\ref{rpc}\ref{rpc-sn}
or are subterms which
are $<_{dt}^+$-smaller than $t_0$, by 
Condition~\ref{rpc}\ref{rpc-dt}.
That is, every subterm $t_1^s$ of $t_1$ (including
$t_1$ itself) satisfies one of the following:
$$
\mbox{(c):}\  t_1^s \in \SN 
\qquad \qquad
\mbox{(d):}\  {t_1^s} <_{dt}^+ {t_0}
$$

Then $t_1^s \in \ISN$, in case {(c)} because $\SN \subseteq \ISN$,
and in case {(d)} by assumption (a). %~\ref{ass1}.
% Now a subterm $t_1^s$ satisfying (d) is in \ISN, as is a term in \SN.
% Thus every $t_1^s$ is in \ISN.
Since $t_1^s$ is an arbitrary subterm of $t_1$, 
Lemma~\ref{hereds-sn} implies that $t_1 \in \SN$.

In either case $t_1 \in \SN$.
Since $t_1$ was obtained via an arbitrary reduction from $t_0$,
it follows that $t_0 \in \SN$.
Thus we have $t_0 \in \ISN$.  \qed \end{proof}

\begin{theorem} \label{thm:all-sn}
If $\rho$ satisfies Condition~\ref{rpc} and $<_{dt}$ is well-founded,
then every term is strongly normalising.
\end{theorem}

\begin{proof}
As $<_{dt}$ and hence $<_{dt}^+$ are well-founded, 
it follows from Lemma~\ref{dth} by well-founded induction that
every term is in \ISN;
now use Lemma~\ref{hereds-sn}.
\qed \end{proof}

We now have a way of proving termination of a suitable rewrite system.
Given the relation $\rho$, normally the rewrite rules and their substitutional
instances, we define a well-founded relation $<_{cut}$ such that,
when $<_{sn1}$ and $<_{dt}$ are defined as in Definition~\ref{defn:porders},
the resulting $<_{dt}$ is well-founded and Condition~\ref{rpc} is satisfied.
This is enough to show the well-foundedness of $\ctxt\ \rho$.
In the following section we show some examples using this procedure.

\section{Examples using the theorem} \label{s-ex}

As explained above, the crux is to find an
appropriate definition of $<_{cut}$.

\subsection{Multiset order}
Given an irreflexive relation $\rho$ on a set $E$, we can define
the \emph{multiset order} derived from $\rho$ on multisets of elements of $E$. 
We use $A, B$ and $C$ for finite multisets of elements of $E$,
by which we mean both that they contain only finitely many distinct elements 
and that they contain only finitely many copies of each such element.  
We use $A \sqcup B$ to stand for the multiset union.
We consider the irreflexive relation $<_{m1}$ 
defined on finite multisets:

\begin{description}
\item[$\leq_{m1}$:] $\forall C, \forall b \in E$.
  if, for all $c \in C$, $c <_\rho b$,
  then $C \sqcup A <_{m1} \{b\} \sqcup A$ 
% \item[$\leq_{m2}$:] $\forall C,B$ .
  % if, for all $c \in C$, there exists $b \in B$ such that 
  % $c \leq_\rho b$, then $C \leq_{m2} B$.
\end{description}
If $\rho$ is a strict order (an irreflexive, transitive relation),
then $<_{m1}^+$ is equal to the multiset order derived from $\rho$.

% Clearly, $<_{m1}^+ = <_{m2}^+$ if $<_\rho^+$ is irreflexive, and
% $<_{m2}$ is transitive if $<_\rho$ is transitive.  In the literature,
% we have seen the multiset ordering derived from $\rho$ defined as
% either $<_{m2}$, or as $<_{m1}^+$, which are equivalent when $<_\rho$
% is transitive.  Since we aim to prove that the multiset ordering for
% finite multisets is well-founded, or equivalently, that its transitive
% closure is well-founded, either definition will do.

We represent a multiset as a tree, with two sorts of node, ``inner''
nodes ($I$) and ``leaf'' nodes ($L$).  Viewing such a tree as a term,
the function symbols are $I$ and, for each $e \in E$,
$L(e)$, where $I$ has arbitrary arity and each $L(e)$ is nullary. 
% The arguments of the $I$ symbol are
% trees, and the argument of a leaf node is a member of the set $E$.
The ``leaf multiset''
of a tree is the multiset of its leaf nodes,
but with each $L(e)$ changed to $e$.
Note that different trees can have the same leaf multiset.

We define a rewrite relation on such trees (terms) as follows.
For every (finite) multiset 
$C = [c_1, c_2, \ldots, c_k]$ 
and every element 
$b \in E$ 
such that
for all $c_i \in C$, $c_i <_\rho b$ (as in the definition of $<_{m1}$)
we have a rule
$$L(b) \longrightarrow I(L(c_1), L(c_2), \ldots, L(c_k))$$

\begin{theorem}
Given a well-founded order $\rho$, the derived multiset order 
(on finite multisets) is well-founded.
\end{theorem}

\begin{proof}
Clearly, whenever $A <_{m1} B$, any tree whose leaf multiset is $B$
can be reduced to a tree whose leaf multiset is $A$
using the rewrite relation defined above.
Since for a given finite multiset $B$ there always is a tree 
whose corresponding multiset is $B$, 
when we show that rewriting terminates 
we have shown that the multiset order is well-founded.

We prove that this rewrite system terminates.
We define $<_{cut}$ by the rules
$$
L(x) >_{cut} I(y)
\qquad\qquad
L(x) >_{cut} L(y) \mbox{ iff } x >_\rho y
$$

It is clear that $<_{cut}$ is well-founded when $\rho$ is.
To show that $<_{cut} \cup <_{sn1}$ is well-founded, we use 
Lemma~\ref{wf-rs}, by showing that in fact
$<_{sn1} \circ <_{cut} = \emptyset$.
For suppose $t >_{sn1} u >_{cut} v$.
Then $u$ must be of the form $L(x)$, and a proper subterm of $t$ 
must reduce to a proper subterm of $u$ -- but $u$ has no proper subterms.

To show that Condition~\ref{rpc1} is satisfied,
when $L(b) \longrightarrow I(L(c_1), \ldots, L(c_k))$,
we have $L(b) >_{cut} I(L(c_1), \ldots, L(c_k))$ 
by the first rule for $<_{cut}$, and,
for every subterm $L(c_i)$ of the reduced subterm, 
$L(b) >_{cut} L(c_i)$ by the second rule.
\end{proof}

\comment{
\subsection{Lexicographic order}\footnote{Note to reviewers: This
  example is rather trivial and is an obvious candidate
  for saving space but we thought it best to leave it in for now.}
Given a binary relation $\rho$ on a set $E$, it is easy to show that
the lexicographic order $\lex\ \rho$ is well-founded.  (Note that for
this we define $(u, t) \in \lex\ \rho$ only when $u$ and $t$ are the
same length --- or we could also allow $u$ to be shorter than $t$, and
the following treatment would still hold).  However we prove it as
another illustration of the use of Theorem~\ref{thm:all-sn}.  We
represent a list as in Prolog, Lisp or ML, with a binary \cons\ and
nullary \nil\ but write it as $(t_1, \ldots, t_n)$.

Then $\lex\ \rho$ is the closure under context of the single rule
$$
\mbox{if } t_1 >_\rho s_1 \mbox{ then }
(t_1, \ldots, t_n) \longrightarrow (s_1, \ldots, s_n)
$$

We then define $<_{cut}$ by 
\begin{eqnarray*}
\mbox{if } t_1 >_\rho u_1 \mbox{ then }
(t_1, \ldots, t_n) >_{cut} (u_1, \ldots, u_n)
\\
\mbox{if } m < n \mbox{ then }
(t_1, \ldots, t_n) >_{cut} (u_1, \ldots, u_m)
\end{eqnarray*}

It is clear that $<_{cut}$ is well-founded when $\rho$ is.
To show that $<_{cut} \cup <_{sn1}$ is well-founded, we use 
Lemma~\ref{wf-rs}\ref{tco}, by showing that in fact
$<_{cut} \circ <_{sn1} \ \subseteq\ <_{cut}$.
For suppose $(t_1, \ldots, t_n) >_{cut} (u_1, \ldots, u_m) >_{sn1} 
(v_1, \ldots, v_k)$.
Then $k \leq m$ and $v_1 = u_1$, so 
$(t_1, \ldots, t_n) >_{cut} (v_1, \ldots, v_k)$.

It is easy to see that Condition~\ref{rpc1} is satisfied,
and so $\lex\ \rho$ is well-founded.
}

\subsection{A non simplification ordering}
Example 5 of \cite{33ex}, with the single rule
\quad $f(f(x)) \longrightarrow f(g(f(x)))$ \quad
is one for which a simplification ordering cannot be used,
because a simplification ordering would
take $g(f(x))$ to $f(x)$ and so $f(g(f(x)))$ to $f(f(x))$, giving a cycle.

But Theorem~\ref{thm:all-sn} is not limited to simplification orderings.
We define $<_{cut}$ according to the number of consecutive $f$ symbols
starting from the head of a term.
Alternatively, we could use the total number of pairs of adjacent $f$ 
symbols, as suggested in \cite{33ex}.
Thus $f(f(x)) >_{cut} f(g(y))$,
$f(f(x)) >_{cut} g(y)$, and $f(f(x)) >_{cut} f(x)$.
Finally, any subterm of $x$ is a proper subterm of $f(f(x))$.
Thus Condition~\ref{rpc1} is satisfied.
Clearly also, rewriting a subterm cannot increase the number
of consecutive $f$ symbols, so 
% $<_{sn1} \ \subseteq\ \leq_{cut}$,
% following wrong - would need to consider a quasi-order 
% whence (as $<_{cut}$ is transitive), 
$<_{sn1} \circ <_{cut} \ \subseteq\ <_{cut}$ 
(and likewise $<_{cut} \circ <_{sn1} \ \subseteq\ <_{cut}$).
Thus $<_{dt} \;=\; <_{cut} \cup <_{sn1}$ is well-founded by Lemma~\ref{wf-rs}.
Therefore the system terminates, by Theorem~\ref{thm:all-sn}.

\subsection{A recursive path ordering example} \label{s-diff}
We now consider a typical example whose termination is shown by the recursive
path ordering (see, for example, \cite{nat-term} or \cite{dersh-har}).
% \begin{eqnarray*}
% D(x + y) & \longrightarrow & Dx + Dy \\
% D(x \times y) & \longrightarrow & x \times Dy + Dx \times y \\
% (x \times (y + z)) & \longrightarrow & x \times y + x \times z \\
% (x \times y) \times z & \longrightarrow & x \times (y \times z) \\
% (x + y) + z & \longrightarrow & x + (y + z) \\
% \end{eqnarray*}

$$
\begin{array}{rcl@{\qquad\qquad}rcl}
D(x + y) & \longrightarrow & Dx + Dy &
(x \times y) \times z & \longrightarrow & x \times (y \times z) \\
D(x \times y) & \longrightarrow & x \times Dy + Dx \times y &
(x + y) + z & \longrightarrow & x + (y + z) \\
x \times (y + z) & \longrightarrow & x \times y + x \times z & & &
\end{array}
$$
The recursive path ordering is a simplification ordering.
To prove termination we must actually add
the following simplification rules as rewrite rules:
$$
x + y \longrightarrow x \qquad
x + y \longrightarrow y \qquad
x \times y \longrightarrow x \qquad
x \times y \longrightarrow y
$$
Clearly, if additional rules $R'$ are added to a rewrite system $R$, and the 
resulting system $R \cup R'$ terminates, then the original system $R$
terminates.

We define $<_{cut}$ as below by first defining
the relation $<_h$, which
depends on the head symbol,
and then defining the relations $<_\times$ and $<_+$
which are for the rewrite rules capturing associativity:
\begin{itemize}
\item $D(x) >_h y \times z \qquad D(x) >_h y + z \qquad x \times y >_h z + w$ 
\item if $x'$ is an immediate subterm of $x$, then 
$x + y >_+ x' + z$ and
$x \times y >_\times x' \times z$
\item $<_{cut} = (<_h \cup <_\times \cup <_+)$.
\end{itemize}

We now prove that this rewrite system terminates.
Clearly $<_{cut}$ is well-founded, since the immediate subterm relation is
well-founded.

To show that $<_{cut} \cup <_{sn1}$ is well-founded, 
we in fact show that $<_{cut} \cup <_{sn2}$ is well-founded,
using Lemma~\ref{wf-rs}\ref{tco}.
First we show that $<_{cut} \circ <_{sn2} \ \subseteq\ 
  <_{sn2}^* \circ <_{cut}$.
For suppose $t >_{cut} u >_{sn2} v$.
If $t >_h u$ then clearly $t >_h v$.
Suppose $t >_\times u$, say $t = x \times y$, $u = x' \times z$ and
$x'$ is an immediate subterm of $x$.
There are two cases for $u >_{sn2} v$,
namely that a strongly normalising subterm of either $x'$ or $z$
reduces to a corresponding subterm of $v$.
Firstly, if $z \longrightarrow w$, then we also have
$v = x' \times w$ and $t >_{cut} v$.
Secondly, if $x' \longrightarrow w'$,
then $v = w' \times z$.
As $x'$ is a subterm of $x$, let $w$ be the term obtained from $x$ by rewriting
its subterm $x'$ to $w'$.
Then $t = x \times y >_{sn2} w \times y$: but
note that this step of the argument would not hold for $>_{sn1}$.
Then $w'$ is an immediate subterm of $w$, so we have
$w \times y >_{cut} w' \times z = v$.
That is, $(v, t) \in\ <_{sn2} \circ <_{cut}$.

So, in each case, $(v, t) \in\ <_{sn2}^* \circ <_{cut}$,
and so $<_{cut} \cup <_{sn2}$ is well-founded,
by Lemma~\ref{wf-rs}\ref{tco}.

Finally, we need to consider all pairs $(r', l)$,
where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$. 
In many cases $l >_h r'$: for example $D(x + y) >_h Dx + Dy$.
In other cases, $r'$ is a proper subterm of $l$: for example whenever
a (meta-)variable appears on the right-hand side of a rule,
and $r'$ is the term the variable stands for, or any subterm of it.
In the case of the associative rewrite rule 
$l = (x \times y) \times z \longrightarrow r = x \times (y \times z) $,
we have that $l >_\times r$, by definition; 
the rule for the associativity of $+$ is similar.

Finally, we have cases for $(r', l)$ such as
$(D(x), D(x + y))$ or $(y \times z, (x \times y) \times z)$.
Here, since a proper subterm $l'$ of $l$ is assumed to be strongly normalising,
and $x + y \longrightarrow x$ (likewise $x \times y \longrightarrow y$)
we have 
$D(x + y) >_{sn1} D(x)$ and $(x \times y) \times z >_{sn1} y \times z$.

Thus in all cases either $r'$ is a proper subterm of $l$ or (assuming
proper subterms of $l$ are in \SN) $l >_{dt}
r'$, so the system terminates by Theorem~\ref{thm:all-sn}.

\subsection{Ackermann's function}
Ackermann's function on the natural numbers
can be defined by the following rewrite rules \cite[Example 29]{33ex}
\begin{eqnarray*}
A(0, y) & \longrightarrow & S(y) \\
A (S(x), 0) & \longrightarrow & A(x, S(0)) \\
A (S(x), S(y)) & \longrightarrow & A(x, A (S(x), y)) 
\end{eqnarray*}

It can be shown to terminate using the lexicographic path ordering.
This is reflected in the relation $>_{cut}$ we use,
which is defined by the following cases:

\begin{eqnarray}
\label{Acut1} A(x, y) & >_{cut} & S(z) \\
\label{Acut2} A (S(x), y) & >_{cut} & A(x, z) \\
\label{Acut3} A (x, S(y)) & >_{cut} & A(x, y) 
\end{eqnarray}

We now prove that this rewrite system terminates.
It is clear that $>_{cut}$ is well-founded using the 
lexicographic ordering on arguments.
It is also clear that for each $(r', l)$, 
where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$, 
either $l >_{cut} r'$ or $r'$ is a proper subterm of $l$.

It remains to show that $<_{cut} \cup <_{sn1}$ is well-founded.
Again we show that $<_{cut} \cup <_{sn2}$ is well-founded,
using Lemma~\ref{wf-rs}\ref{tco}.
We show that $<_{cut} \circ <_{sn2} \ \subseteq\ 
  <_{sn2}^* \circ <_{cut}$.
For suppose $t >_{cut} u >_{sn2} v$.
If $t >_{cut} u$ by rule (\ref{Acut1}),
ie $t = A(x, y)$ and $u = S(z)$, then $v = S(z')$ and so
$t >_{cut} v$.
If $t >_{cut} u$ by rule (\ref{Acut2}), 
then $t = A (S(x), y)$ and $u = A(x, z)$.
There are two cases for $u >_{sn2} v$:
$v = A(x, z')$ where $z \longrightarrow z'$, in which case $t >_{cut} v$, or 
$v = A(x', y)$ where $x \longrightarrow x'$ % WRONG and $x \in \SN$,
by reducing a strongly normalising subterm of $x$,
in which case $t = A (S(x), y) >_{sn2} A (S(x'), y) >_{cut} A(x', z) = v$.
The case for rule (\ref{Acut3}) is similar.

So in all cases
$(v, t) \in\ <_{sn2}^* \circ <_{cut}$,
and so $<_{cut} \cup <_{sn2}$ is well-founded,
by Lemma~\ref{wf-rs}\ref{tco}.
Therefore the system terminates by Theorem~\ref{thm:all-sn}.

\subsection{Insertion sort}
\newcommand{\sort}{\textit{sort}}
\newcommand{\ins}{\textit{insert}}
\newcommand{\choo}{\textit{choose}}
This example \cite[Example 32]{33ex}
is more difficult than the previous two, though the approach is similar.
The rules are
\begin{eqnarray*}
\sort(\nil) & \longrightarrow & \nil \\
\sort(\cons (x, y)) & \longrightarrow & \ins (x, \sort (y)) \\
\ins (x, \nil) & \longrightarrow & \cons (x, \nil) \\
\ins (x, \cons (v, w)) & \longrightarrow & \choo (x, \cons (v, w), x, v) \\
\choo (x, \cons (v, w), y, 0) & \longrightarrow & \cons (x, \cons (v, w)) \\
\choo (x, \cons (v, w), 0, s(z)) & \longrightarrow &
  \cons (v, \ins (x, w)) \\
\choo (x, \cons (v, w), s(y), s(z)) & \longrightarrow &
  \choo (x, \cons (v, w), y, z) 
\end{eqnarray*}

To define $>_{cut}$, we start by defining an order $>_h$,
contained in $>_{cut}$, which depends on the head symbol,
using this (transitive) order on symbols:
$\sort > \{\ins, \choo\} > \cons$.
We notice that the rules (considered as definitions)
define \ins\ and \choo\ in terms of each other,
so we continue by defining 
$$
\begin{array}{c}
\ins (x, w) >_{cut} \choo (y, w, a, b) >_{cut} \ins (x, w') \\
\choo (y, w, a, b) >_{cut} \choo (y', w, a', b') 
\end{array}
$$
where $>_{cut}$ is transitive and $w',a'$ are immediate subterms of $w,a$.
It is easy to see that $>_{cut}$ is well-founded.
As in \S\ref{s-diff}, we add a simplification rule 
$$\cons (x, y) \longrightarrow y$$
%  where $l = \sort(\cons (x, y)) >_{sn1} \sort (y) = r'$.

Then, for every $(r', l)$ where $l \rightarrow r$ is a rewrite rule
and $r'$ is a subterm of $r$,
either $l >_{cut} r'$, $l >_{sn1} r'$ or $r'$ is a proper subterm of $l$.

Again we show that 
$<_{cut} \circ <_{sn2} \ \subseteq\ <_{sn2}^* \circ <_{cut}$,
using the same technique as in the previous two examples.
Therefore the system terminates by Theorem~\ref{thm:all-sn}.

The ordering $<_{cut}$ is similar to that used in \cite[Example 32]{33ex}, 
and \cite{nat-term}.
% and indeed our main theorem has apparent
% similarities to the recursive path orderings and the general path ordering of
% Dershowitz \cite{nat-term}.
% However, as we showed above, our theorem is not limited to simplification
% orderings, whereas the general path ordering and recursive path orderings
% are simplification orderings.

\subsection{The factorial example}
Example 21 of \cite{33ex} is almost the usual definition of the factorial
function, but modified so that we can not use a simplification ordering.
The rules are
% \begin{eqnarray*}
% P(S(x)) & \longrightarrow & x \\
% F(0) & \longrightarrow & 0 \\
% F(S(x)) & \longrightarrow & S(x) \times F(P(S(x))) \\
% 0 \times y & \longrightarrow & 0 \\
% S(x) \times y & \longrightarrow & x \times y + y \\
% x + 0 & \longrightarrow & x \\
% x + S(y) & \longrightarrow & S(x + y) 
% \end{eqnarray*}

$$
\begin{array}{rcl@{\qquad\qquad}rcl}
P(S(x)) & \longrightarrow & x &
F(0) & \longrightarrow & 0 \\
F(S(x)) & \longrightarrow & S(x) \times F(P(S(x))) &
0 \times y  & \longrightarrow &  0 \\
S(x) \times y & \longrightarrow & x \times y + y &
x + 0 & \longrightarrow & x \\
x + S(y) & \longrightarrow & S(x + y) & & & 
\end{array}
$$

As usual we define a (transitive) ordering $<_h$ 
of terms based on the following ordering of head symbol:
$ F > \times > + > S$.
But we need to define $<_{cut}$ to be the union of $<_h$ and the following
additional cases 
$$F(S(x)) >_{cut} F(P(S(x))) \qquad F(S(x)) >_{cut} F(P(x))$$
We can not use a simplification ordering because
if we allowed $P(x) \longrightarrow x$ the system would not terminate,
but would ``cycle'' between terms containing $F(S(x))$ and 
terms containing $F(P(S(x)))$. 
We do, however, need to add the rule $S(x) \longrightarrow x$.
The proofs of termination given in \cite[Examples 21, 25]{33ex} 
are based on interpreting arguments to the function symbols as natural numbers.

Now for each $(r', l)$ where 
$l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$, 
it is reasonably easy to see that
we have one of the following cases:
\begin{itemize}
\item $r'$ is a proper subterm of $l$
\item $r' <_h l$
\item $r'$ is $l$, but with $S$ removed from a subterm
  (to give $r' <_{sn1} l$)
\item $r'$ is $F(P(S(x)))$ and $l$ is $F(S(x))$
  (so $r' <_{cut} l$).
\end{itemize}

It is easy to see that $<_{cut}$ is well-founded.
To show that $<_{cut} \cup <_{sn2}$ is well-founded
we need to use a more general case of Lemma~\ref{wf-rs} than hitherto.
In fact we show 
$<_{cut} \circ <_{sn2} \ \subseteq\ (<_{sn2}^* \circ <_{cut}) \cup <_{sn2}^+$,
which implies \ref{dvk} of Lemma~\ref{wf-rs}.

Suppose $t >_{cut} u >_{sn2} v$.
If $t >_h u$ then clearly $t >_h v$.
Suppose $t = F(S(x))$ and $u = F(P(S(x)))$ or $u = F(P(x))$.
If $u >_{sn2} v$ by way of reducing the $x$ in $u$ to $x'$
(reducing a strongly normalising subterm of $x$),
then % we have $x \in \SN$ and so 
$t = F(S(x)) >_{sn2} F(S(x')) >_{cut} v$.
Otherwise we need to consider specific cases:
\begin{itemize}
\item $u = F(P(S(x)))$, $S(x) \longrightarrow x$ where $S(x) \in \SN$,
  $v = F(P(x))$:
  then $t >_{cut} v$
\item $u = F(P(S(x)))$, $P(S(x)) \longrightarrow x$ where $P(S(x)) \in \SN$,
  $v = F(x)$: here, as $S(x) \longrightarrow x$ and $S(x) \in \SN$,
  we have $t >_{sn2} v$
\item $u = F(P(x))$, where $x = S(y)$, 
  $P(S(y)) \longrightarrow y$ and $P(S(y)) \in \SN$, $v = F(y)$:
  here, as $S(y) \longrightarrow y$ and $S(y) \in \SN$,
  we have $t = F(S(S(y)) >_{sn2} F(S(y)) >_{sn2} F(y) = v$.
\end{itemize}

Thus $<_{cut} \cup <_{sn2}$ is well-founded and the system terminates
by Theorem~\ref{thm:all-sn}.

\comment{
\subsection{Semantic Path Ordering Example}

Example 31 of \cite{33ex} uses some rules from
\S\ref{s-diff}, but with an extra rule which prevents the recursive path
ordering from being used.
It can be shown to terminate using the ``semantic path ordering'' of
Kamin \& Levy \cite{kl,fz}. 
The rules are 
\begin{eqnarray*}
(x \times y) \times z & \longrightarrow & x \times (y \times z) \\
(x + y) \times z & \longrightarrow & x \times z + y \times z \\
z \times (x + f(y)) & \longrightarrow & g(z,y) \times (x + a) 
\end{eqnarray*}

We add the same simplification rewrite rules as in \S\ref{s-diff},
but we must also add the following  rule to guarantee Condition~2(a):
$ f(y) \longrightarrow a $.

We then define $<_{cut}$ as the union of the orders $<_h$ (which
depends on the head symbol), and $<_\times$ and $<_g$.
The ordering of symbols for $<_h$ has $\times > \{+, g, a\}$
For $<_\times$ and $<_g$, we have 
\begin{eqnarray}
\label{31x} x \times u + y & >_\times & x \times z \\
\label{31g1} z \times (x + f(y)) & >_{g} & g(z', y') \times (x + a) \\
\label{31g2} z \times (x + f(y)) & >_{g} & g(z', y') \times x \\
\label{31g3} z \times (x + f(y)) & >_{g} & g(z', y') \times a 
\end{eqnarray}

We now prove that this rewrite system terminates.
To show that $<_{cut}$ is well-founded we note that
$<_\times$ is well-founded as the $x$ appearing in rule (\ref{31x})
for $<_\times$is a proper subterm of $x \times u$, and 
the proper subterm relation is
well-founded.
Clearly $<_g$ is well-founded, 
and we notice that $<_g \circ <_\times = \emptyset$ since 
$g(z', y')$ cannot match $x \times u$.  
It follows easily that $<_{cut}$ is well-founded. 

To show that $<_{cut} \cup <_{sn1}$ is well-founded,
we use Lemma~\ref{wf-rs}\ref{tco}, showing
that $<_{cut} \circ <_{sn2} \ \subseteq\ <_{sn2}^* \circ <_{cut}$,
as previously.
Supposing $t >_{cut} u >_{sn2} v$,
the only difficult case is where a proper subterm $u'$ of $u$ 
is rewritten to get a corresponding subterm of $v$, 
and $u'$ matches 
a non-variable subterm of the right-hand side of a rule for $<_{g}$.
The only case where this happens is in rule (\ref{31g1}), where 
$(x + a)$ can be rewritten to get $x$ or $a$.
In these cases, $t >_g v$ by rules (\ref{31g2}) or (\ref{31g3}):
these rules are included only for this reason.

It is easy to see that Condition~\ref{rpc1} is satisfied, and so
the rewrite system terminates by Theorem~\ref{thm:all-sn}.
}
\subsection{Recursive Path Orderings} \label{s-rpo}

To show that our theorem is at least as general as the recursive path
orderings we now derive their termination.

Given a well-founded ordering $<_\sigma$, we use the derived
lexicographic ordering $\lex\ \sigma$, which is restricted to
fixed-length sequences, and so is well-founded.

Given a well-founded ordering $<_\rho$ on function symbols,
the lexicographic path ordering $\lpo\ \rho$,
also written $<_{lpo}$ \cite[Defn~4.22]{dersh-har},
is then defined as below (omitting reference to $lpo$-equivalent terms,
and where $<_{lex}$ is $\lex\ (\lpo\ \rho)$
$$
\frac {
s_i \geq_{lpo} t } { f(s_1, \ldots, s_m) >_{lpo} t }
\qquad
\frac {
f >_\rho g \qquad \forall i \in \{1, \ldots, n\}.\ f(s_1, \ldots, s_m) >_{lpo} t_i
 } { f(s_1, \ldots, s_m) >_{lpo} g(t_1, \ldots, t_n) }
 $$ 
 
 $$
\frac {
(s_1, \ldots, s_m) >_{lex} (t_1, \ldots, t_m) \qquad 
  \forall i \in \{1, \ldots, m\}.\ f(s_1, \ldots, s_m) >_{lpo} t_i
 } { f(s_1, \ldots, s_m) >_{lpo} f(t_1, \ldots, t_m) }$$

We note that the definition of the multiset path ordering,
and the proof that it is well-founded, correspond closely to what
follows.

The following lemma is actually an easy consequence of the transitivity 
of $>_{lpo}$, but that result is much more difficult to prove.
\begin{lemma} \label{lem-subt-lpo}
If $s >_{lpo} t$ and $t'$ is a subterm of $t$ then $s >_{lpo} t'$.
\end{lemma}
\begin{proof}
It is enough to show that 
if $s >_{lpo} t = g(t_1, \ldots, t_n)$ then $s >_{lpo} t_j$ where
$j \in \{1, \ldots, n\}$.
We show this by induction on the size (or structure) of $s$.
If $s >_{lpo} t$ by the second or third rules, 
then it is immediate that $s >_{lpo} t_j$.
If $s = f (s_1, \ldots, s_m) >_{lpo} t$ by the first rule, 
then for some $s_i$,
either $s_i >_{lpo} t$ and so $s_i >_{lpo} t_j$ by induction,
or $s_i = t >_{lpo} t_j$ by the first rule, 
and then $s >_{lpo} t_j$ by the first rule.
\qed \end{proof}

\begin{theorem}
For a well-founded ordering $<_\rho$ on function symbols,
the derived lexicographic path ordering is well-founded.
\end{theorem}

\begin{proof}

We first define $<_{cut}$ using 
$<_h$ as the ordering of terms according to the head symbol and
defining another relation $<_{lw1}$ as below:
\begin{itemize}
\item $f(\overline{s}) >_h g(\overline{t})$ iff $f >_\rho g$
\item if $((\overline{t}), (\overline{s})) \in \lex\ (\fwf\ 
  (\lpo\ r))$, then $f(\overline{t}) <_{lw1} f (\overline{s})$
\item   $<_{cut}\ =\ (<_h \cup <_{lw1})$.  
\end{itemize}

The idea behind the definition is similar to the way the definition
of $<_{sn1}$ requires the $<_{sn1}$-greater term to be strongly normalising.
As $\fwf\ (\lpo\ r)$ is \linebreak[4] well-founded,
$\lex\ (\fwf\ (\lpo\ r))$ and so
$<_{lw1}$ are well-founded.  Clearly also
\linebreak[4] \mbox{$<_h \circ\ <_{lw1} \, \subseteq\ \, <_h$},
so $<_{cut}$ is well-founded, by Lemma~\ref{wf-rs}.
Further, $<_{sn1}\ \subseteq <_{lw1}$, so $<_{cut} \cup <_{sn1}\ =\ 
<_{cut}$ is well-founded.

To show that the rewrite relation 
$<_{lpo}$ satisfies Condition~\ref{rpc},
suppose $(r', l)$ is given,
where $r <_{lpo} l$ and $r'$ is a subterm of $r$.
Then, by Lemma~\ref{lem-subt-lpo}, $r' <_{lpo} l$.

If $l = f(s_1, \ldots, s_m) >_{lpo} r'$ by the first rule, 
then some $s_i >_{lpo} r'$.
Now assuming that $s_i \in \SN$, we have $r' \in \SN$.

Now suppose $l >_{lpo} r'$ by the second or third rules.
Again, we are assuming that all proper subterms of $l$ are strongly
% normalising, and under this assumption we have $r' <_{cut} l$.
normalising, and then $r' <_{cut} l$.
\qed \end{proof}

It may be noted that using our theorem as above actually proves that
$\ctxt\ (\lpo\ \rho)$ is well-founded --- 
in fact, since $\lpo\ \rho$ is closed under
context this point is of no significance.
The proof that the multiset path ordering 
$<_{mpo}$ \cite[Defn~4.24]{dersh-har}
is well-founded is very similar.
In the ``status-based'' recursive path ordering, 
lists of arguments to a function symbol are compared using
the lexicographic, multiset or other derived ordering $\phi(\_)$,
depending on the function symbol.
This is well-founded also, by a similar proof.
The necessary properties for such an ordering $\phi(\_)$ are the following:
that $\phi(\sigma)$ is well-founded if $\sigma$ is, 
and that if $s_i' <_\sigma s_i$ then 
 $(s_1, \ldots, s_i', \ldots, s_m) <_{\phi(\sigma)} 
 (s_1, \ldots, s_i, \ldots, s_m)$.
This second property is used above in the step $<_{sn1}\ \subseteq
<_{lw1}$.

\subsection{The Knuth-Bendix Ordering}
\label{sec:knuth-bend-order}

For a rewrite system (with rules containing variables), the
Knuth-Bendix ordering $<_{kb}$ is based on a strict well-founded order
$<$ on function symbols and, additionally, a weight function $w$ on
function symbols and variables.  Since our approach is based on a
relation $\rho$ (which amounts to the rewrite rules after all possible
substitutions for variables), we describe the Knuth-Bendix ordering in
this context.  Weights are natural numbers, and the weight of any
constant or object language variable is positive: thus every subterm
has positive weight.  At most one unary function symbol (call it $k$)
can have zero weight, and then $k > f$ for any other function symbol
$f$.  The weight of a term is the sum of the weights of the function
symbols and variables in it.  Then we have that $s >_{kb} t$ iff $w(s)
\geq w(t)$ and one of
\begin{eqnarray}
&& \label{kbo-h1} w(s) > w(t) \\
\label{kbo-hn} && s = k^n(t) \mbox{ for some } n > 0 \\
\label{kbo-fg} 
  && s = f(\overline{s}) \mbox{ and } t = g(\overline{t}) \mbox{ where
  } f > g\\
\label{kbo-lex} 
  && s = f(\overline{s}), t = f(\overline{t}) 
 \mbox{ and } (\overline{t}, \overline{s}) \in \lex\ (<_{kb})
\end{eqnarray}

\begin{theorem}
The Knuth-Bendix ordering is well-founded.
\end{theorem}

\begin{proof}
The proof that $<_{kb}$ is well-founded is similar to that in \S\ref{s-rpo},
and so is somewhat abbreviated here.
We define $s >_{cut} t$ iff $w(s) \geq w(t)$ and either one of the
rules (\ref{kbo-h1}), (\ref{kbo-hn}), (\ref{kbo-fg}) 
holds or $s >_{kw1} t$ holds, where
$<_{kw1}$ is defined by:
\begin{eqnarray}
 f(\overline{t}) <_{kw1} f(\overline{s}) 
 & \mathrm{ iff }
 & (\overline{t}, \overline{s}) \in \lex\ (\fwf\ (<_{kb}))
\end{eqnarray}

To show $<_{cut}$ is well-founded, we have that each individual rule 
provides a well-founded relation and it is easy to apply Lemma~\ref{wf-rs}
to show that their union is well-founded,
noting that if (\ref{kbo-fg}) applies then $g \not= k$.
As in the case of the lexicographic path order $<_{sn1} \subseteq <_{kw1}$.

To show that Condition~\ref{rpc} is satisfied, suppose that $l >_{kb}
r$ and that $r'$ is a subterm of $r$.  Assume that all proper subterms
of $l$ are in \SN, in which case, if $l >_{kb} r'$ then $l >_{cut} r'$. 
We show by induction on the structure of $l$, that $r' <_{kb} l'$ 
for some subterm $l'$ of $l$.
Then if $l'$ is a proper subterm of $l$, 
Condition~\ref{rpc1}\ref{rpc-srp} is satisfied;
if $l' = l$ then $r' <_{kb} l$ and so $r' <_{cut} l$,
so Condition~\ref{rpc1}\ref{rpc-cut} is satisfied.
% which is enough to satisfy either
% , in the case of a proper subterm
% $l'$, or Condition~\ref{rpc1}\ref{rpc-cut} if $l' = l$.

If $w(r') < w(r)$ or $w(r) < w(l)$ then $w(l) > w(r')$ and $l >_{kb} r'$.
If $r' = r$ then $l >_{kb} r'$.
If $w(l) = w(r) = w(r')$ and $r'$ is a proper subterm of $r$, then 
$r = k^n(r')$ for some $n > 0$,
and so $l >_{kb} r$ by either (\ref{kbo-hn}) or (\ref{kbo-lex})
(as the $g$ of (\ref{kbo-fg}) cannot be $k$).
If $l >_{kb} r$ by (\ref{kbo-hn}) then $l >_{kb} r'$ by (\ref{kbo-hn}).
If $l >_{kb} r$ by (\ref{kbo-lex}), then, for some $l_1, r_1$, 
$l = k(l_1)$, $r = k(r_1)$, $l_1 >_{kb} r_1$ and $r'$ is a subterm of $r_1$,
so by induction we have that $r' <_{kb} l'$ for some $l'$ 
which is a subterm of $l_1$ and so of $l$.
\qed \end{proof}

\subsection{Dependency Pairs}\label{s-dps}
Arts \& Giesl \cite{dps00} describe a method of establishing termination using
``dependency pairs''.
They distinguish function symbols which appear at the head of the left-hand
side of a rewrite rule (``defined symbols'') and those which do not
(``constructor symbols'').
They follow the convention that for a rule $l \to r$ of a rewrite system, 
$l$ is not a lone variable, and any variable in $r$ is also in $l$.
For each defined symbol $d$ they introduce a new corresponding ``tuple symbol''
$d^\sharp$.
From a term $t$ we obtain a term $t^\sharp$ by changing the head symbol of $t$
to the corresponding tuple symbol.

Previously we have considered a ``rule'' $l \to r$ after substitution,
and the variables in our analyses have been metavariables where, for
example, we might have considered a rule $g(x) \to x$ with $l = g(x)$, $r = x$,
and $r'$ a proper subterm of $x$.  This approach no longer holds: $l
\to r$ will mean a rule before substitution, and we will use $\sigma$
for a substitution.

For a rewrite rule $l \to r$, and subterm $r'$ of $r$, 
if the head of $r'$ is a defined symbol then  $l^\sharp \to r'^\sharp$
is a \emph{dependency pair}.
We now state and prove the ``sufficiency'' part of Theorem~7 of \cite{dps00}.

\begin{theorem}
If there is a well-founded quasi-ordering $\leq$
which is closed under context and 
where both $\leq$ and $<$ are closed under substitution, 
such that
\begin{enumerate}
\item \label{dpt-rule} $l \geq r$ for all rules $l \to r$, and
\item \label{dpt-dp} $s > t$ for all dependency pairs $s \to t$
\end{enumerate}
then the rewrite system terminates.
\end{theorem}

\begin{proof}
Assume $>$ is minimal such that the conditions hold.
Then there is no instance of $c^\sharp(x) > d^\sharp(y)$ or $c(x) > d(y)$ 
where $c$ is a constructor symbol and $d$ is a defined symbol,
as neither \ref{dpt-rule} nor \ref{dpt-dp} nor the requirement that
$\leq$ be closed under context require it, whence 
the transitivity of $\leq$ cannot require it.

We define $<_{cut}$ by 
\begin{eqnarray}
\label{dp-sh} & s^\sharp < t^\sharp \Longrightarrow
  s\sigma <_{cut} t\sigma & \\
\label{dp-cd} & c(x) <_{cut} d(y) &
\end{eqnarray}
for any substitution $\sigma$, constructor symbol $c$ and defined symbol $d$.

Then $<_{cut}$ is well-founded because $<$ is and because,
as remarked above, there is no instance of 
$c^\sharp(x) > d^\sharp(y)$ or $c(x) > d(y)$.

To show that $<_{cut} \cup <_{sn1}$ is well-founded,
we use Lemma~\ref{wf-rs}\ref{tco}, showing
that $<_{cut} \circ <_{sn1} \ \subseteq\ <_{cut}$.
Suppose that $t >_{cut} u >_{sn1} v$.
If $t >_{cut} u$ by rule (\ref{dp-cd}) then $t >_{cut} v$ by the same rule.
If $t >_{cut} u$ by rule (\ref{dp-sh}) then $t^\sharp > u^\sharp$,
where a proper subterm $u'$ of $u$ is rewritten to 
a corresponding subterm $v'$ of $v$.
Since $u' \geq v'$ by assumption \ref{dpt-rule} because $\leq$ is
closed under substitution, 
we have $u^\sharp \geq v^\sharp$ since $\leq$ is closed under context,
and so $t^\sharp > v^\sharp$ and $t >_{cut} v$.

Finally, we show that Condition~\ref{rpc1} is satisfied.
For a rule $l \to r$ and substitution $\sigma$,
so $(r \sigma, l \sigma) \in \rho$,
and subterm $r'$ of $r \sigma$, 
there are three cases for $r'$:
\begin{itemize}
\item the head of $r'$ is a constructor symbol in $r$,
  in which case $l \sigma >_{cut} r'$ by (\ref{dp-cd})
\item the head of $r'$ is a defined symbol in $r$,
  in which case $r' = r_1 \sigma$ for some subterm $r_1$ of $r$,
  $l^\sharp \to r_1^\sharp$ is a dependency pair, and
  $l \sigma >_{cut} r_1 \sigma = r'$ by (\ref{dp-sh})
\item $r'$ is a subterm of $x \sigma$ for some variable $x$ in $r$,
  in which case $r'$ is a proper subterm of $l \sigma$,
  since any variable in $r$ appears as a proper subterm of $l$.
\end{itemize}
\end{proof}

\section{Observations and Conclusion}

In \S\ref{s-diff} we had the somewhat paradoxical situation that it
was necessary to add additional rewrite rules to enlarge the relation
$\rho$ to prove termination. An interesting question is whether we can
reformulate Theorem~\ref{thm:all-sn} to avoid this need since, the
larger $\rho$ is, the more difficult it should be to prove
termination.

It is interesting to consider further questions of a similar nature.
We prove the well-foundedness of $\ctxt\ \rho$ based on certain
conditions on $\rho$.  Since $\ctxt\ (\ctxt\ \rho) = \ctxt\ \rho$ and
assuming we can apply Theorem~\ref{thm:all-sn} to $\rho$, can we also
apply it to $\ctxt\ \rho$ using the same or a different choice of
$<_{cut}$~?  In fact, we can, and with the same choice of $<_{cut}$.
Suppose $\rho$ satisfies Condition~\ref{rpc}.  Consider $(C[r], C[l])
\in \ctxt\ \rho \setminus \rho$, where $(r, l) \in \rho$, and let $r'$
be a subtree of $C[r]$.  If $r' = C[r]$, then $r' <_{sn1} C[l]$ under
the assumption that all proper subtrees of $C[l]$ are in \SN.  If $r'$
is a subtree of $r$, then Condition~\ref{rpc1}\ref{rpc-srp} holds for
$(r', C[l])$ because $l$ is a proper subtree of $C[l]$, $l$ reduces to
$r$, and $r'$ is a subtree of $r$.  Thus $l$, $r$ and $r'$ are in \SN.
Finally, $r'$ could be $C'[r]$, where $C'[l]$ is a proper subterm of
$C[l]$.  If $C'[r] = C'[l]$ then $l$ is in a different part of $C[l]$
from $C'[l]$ so $r' = C'[l]$ is a proper subterm of $C[l]$;
otherwise $r'$ is the reduction of $C'[l]$, and
Condition~\ref{rpc1}\ref{rpc-srp} holds.

Likewise, rewriting with $\rho$ terminates if and only if rewriting
with $\rho^+$ terminates: this is because $\ctxt\ \rho \subseteq
\ctxt\ \rho^+ \subseteq (\ctxt\ \rho)^+$ and $\ctxt\ \rho$ is
well-founded if and only if $(\ctxt\ \rho)^+$ is.  Now, when we can
apply Theorem~\ref{thm:all-sn} to $\rho$, can we also apply it to
$\rho^+$~?  
So far we have shown that if 
$\ctxt\ \rho$ satisfies Condition~\ref{rpc1}, 
then so does $(\ctxt\ \rho)^+$ (with the same $<_{cut}$),
provided that $\ctxt\ \rho$ is well-founded.
The proof is a complex triple induction.
% In general, this does not seem to be so, but it might
% be possible if the conditions for Theorem~\ref{thm:all-sn} were
% reformulated or generalised.

If we ask how powerful Theorem~\ref{thm:all-sn} is, that is, 
which terminating rewrite systems can it handle, then we find
that it can handle all of them, but this result is unhelpful.
For given $\rho$, where $\ctxt\ \rho$ is well-founded, then,
writing $\leq_{sub}$ for the subterm relation, 
we can define $<_{cut} = \rho\ \circ <_{sub}$.
Then Condition~\ref{rpc1}\ref{rpc-srp} holds, trivially.
Further, it can be shown that $\ctxt\ \rho\ \cup <_{sub}$ is well-founded:
though, as we have seen, $\ctxt\ (\rho\ \cup <_{sub})$ need not be.
Since $<_{dt} \subseteq (\ctxt\ \rho\ \cup <_{sub})^+$, we have
$<_{dt}$ is well-founded.
That is, where $\ctxt\ \rho$ is well-founded, we can always find an
appropriate relation $<_{cut}$.  But it may be no easier to show 
$<_{cut}$ well-founded than to show $\ctxt\ \rho$ well-founded.

We have described a proof of the termination of a rewrite system (or
any relation closed under context) which provides simple proofs of
the termination of a range of rewrite systems. It provides a
reasonably easy proof of the well-foundedness of the lexicographic and
multiset path orderings (which are simplification orderings), 
but it is not limited to simplification orderings.
It can also be used to prove the termination
of Knuth-Bendix orderings and a key theorem for the method of
dependency pairs.

There are several termination results for orderings which are
not necessarily closed under context, but contain a rewrite ordering,
such as the results of Ferreira \& Zantema \cite{fz},
Dershowitz \& Hoot \cite{nat-term} and 
Borralleras, Ferreira \& Rubio \cite{bfr}.
We are currently exploring the linkage between our results 
and these termination results.

\paragraph{Acknowledgements}
We wish to thank Linda Buisman for investigating some of the examples,
and researching the criteria for well-foundedness of a union of
well-founded orderings. We also wish to thank Jean Goubault-Larrecq
and Hubert Comon for pointers to the literature.
Finally, we thank some anonymous referees for very helpful comments.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \bibliography{/home/users/rpg/bib/ce,/home/users/rpg/bib/fm,/home/users/rpg/bib/modal,/home/users/rpg/bib/mtl,/home/users/rpg/bib/logic,/home/users/rpg/bib/tl,/home/users/rpg/bib/paracon,/home/users/rpg/bib/linear,/home/users/rpg/bib/algebra,/home/users/rpg/bib/relevant,/home/users/rpg/bib/dl,/home/users/rpg/bib/atp,/home/users/rpg/bib/tphols}

\bibliographystyle{plain}

\begin{thebibliography}{1}

\bibitem{dps00}
Thomas Arts and J\"urgen Giesl.
Termination of Term Rewriting Using Dependency Pairs.
Theoretical Computer Science 236 (2000), 133-178, 2000.

\bibitem{bfr}
Cristina Borralleras, Maria Ferreira and Albert Rubio.
Complete Monotonic Semantic Path Orderings.
In Proc. 17th Conference on Automated Deduction (CADE-17),
LNCS 1831, 346--364, Springer, 2000.


\bibitem{dawson-gore-machine-checked-strong-normalisation}
Jeremy~E.~Dawson and Rajeev Gor{\'e}.
A New Machine-checked Proof of Strong Normalisation for Display Logic. 
In Computing: The Australasian Theory Symposium, 2003, Electronic Notes in
Theoretical Computer Science 78, 16--35, Elsevier.

\bibitem{dawson-gore-formalised-cut-admissibility}
Jeremy~E.~Dawson and Rajeev Gor{\'e}.
\newblock Formalised cut admissibility for display logic.
\newblock In 
  Proc. 15th International Conference on Theorem Proving in Higher
  Order Logics (TPHOLs02), LNCS 2410, 131--147, Springer, 2002.

\bibitem{33ex}
Nachum Dershowitz.  33 Examples of Termination.
Proc. French Spring School of Theoretical Computer Science (1993),
LNCS 909, 16--25, Springer 1995.

\bibitem{nat-term}
Nachum Dershowitz \& Charles Hoot.  Natural Termination.
Theoretical Computer Science 142 (1995), 179-207.

\bibitem{dersh-har}
Nachum Dershowitz \& David A.~Plaisted.
Rewriting.  In Alan Robinson \& Andrei Voronkov, eds, 
Handbook of Automated Reasoning, 535--610, Elsevier, 2001.

\bibitem{dvk}
Henk Doornbos \& Burghard Von Karger.
On the Union of Well-Founded Relations.  L. J. of the IGPL 6 (1998), 195-201.

\bibitem{fz}
M~C~F~Ferreira and H~Zantema.
Well-foundedness of Term Orderings.
In Conditional Term Rewriting Systems (CTRS-94)
ed N. Dershowitz, LNCS 968, 106--123, 1995.

\bibitem{jgl}
Jean Goubault-Larrecq. Well-founded recursive relations. 
In Computer Science Logic (CSL'2001), 
LNCS 2142, 484--497, 2001.

\bibitem{kl}
Sam Kamin \& Jean-Jacques L\'evy.
Two generalizations of the recursive path ordering.
Unpublished, Department of Computer Science, University of Illinois, 1980.

\bibitem{pfenning-structural-lics94}
Frank Pfenning.
Structural Cut Elimination,
Proc.\ LICS 94, 1994.

\end{thebibliography}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: