%%
%%
\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}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble


\newcommand{\SN}{\textit{SN}}
\newcommand{\SNo}{{SN}^\circ} % needs math mode 
\newcommand{\SNSig}{\textit{SN}^\Sigma}
\newcommand{\ISN}{\textit{ISN}}
\newcommand{\btl}{\blacktriangleleft}
\newcommand{\btr}{\blacktriangleright}
\newcommand{\vtl}{\vartriangleleft}
\newcommand{\vtr}{\vartriangleright}
\newcommand{\vtlo}{\vartriangleleft^\circ}
\newcommand{\vtro}{\vartriangleright^\circ}
\newcommand{\vtluo}{\vtl \cup \vtlo}
\newcommand{\gindy}{\texttt{gindy}}
\newcommand{\indy}{\texttt{indy}}
\newcommand{\gbars}{\texttt{gbars}}
\newcommand{\bars}{\texttt{bars}}
\newcommand{\wfp}{\textit{wfp}}
\newcommand{\wruvo}{\wfp\ (\rho\ \cup \vtlo)}
\newcommand{\subt}{\textit{subt}}
\newcommand{\isubt}{\textit{isubt}}
\newcommand{\psubt}{\textit{psubt}}
\newcommand{\gpo}{\textit{gpo}}
\newcommand{\lpo}{\textit{lpo}}
\newcommand{\lex}{\textit{lex}}
\newcommand{\fwf}{\textit{fwf}}
\newcommand{\tyof}{\textit{tyof}}
\newcommand{\ctxt}{\textit{ctxt}}
\newcommand{\constrict}{\textit{constrict}}
\newcommand{\cons}{\textit{cons}}
\newcommand{\nil}{\textit{nil}}
\newcommand{\Img}{\ \grave{\ }\grave{\ }\ }
\newcommand{\rsmin}{\texttt{rsmin}}

\newcommand\cfile{}

\newcommand\comment[1]{} 
\newcommand\isabelle[0]{} 
\newcommand\notcsl[0]{} 
% \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}}

\setcounter{secnumdepth}2
\setcounter{tocdepth}2
\newtheorem{condition}{Condition}

% 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{Machine-checked Termination Proofs for Abstract Reduction Systems}

\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
Dept 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
\\ \texttt{Jeremy.Dawson@nicta.com.au} \ \ \texttt{Rajeev.Gore@anu.edu.au}
}

\date{\today}

%% Title
\maketitle

\begin{abstract}
\comment{ old abstract
  We take our previous theorem showing the well-foundedness (termination)
  of certain rewrite orderings, 
  and generalise this to abstract reduction relations.
  We show how this implies a very general theorem of Goubault-Larrecq.
  We consider constricting derivations,
  which provide an alternative proof of our theorem for monotonic orderings,
  and we show how our theorem covers the general path ordering of 
  Dershowitz \& Hoot.
  Next, we show how to adapt our proof to prove Goubault-Larrecq's
  second general theorem for higher-order path orderings.
  Finally, we discuss how our theorem applies to the termination of 
  reduction of well-typed combinator expressions, and how it can be adapted
  to show the strong normalisation of the simply-typed $\lambda$-calculus.
  }
  
  We present a general theorem capturing the conditions required for
  the termination of abstract reduction systems and describe how we
  machine-checked its proof using the interactive theorem prover
  Isabelle/HOL. We show that our theorem properly generalises two
  other similar general theorems about termination of such systems. We
  apply our theorem to give interesting proofs of termination for
  typed combinatory logic and the simply-typed lambda calculus.  Thus,
  our method can handle most path-orderings in the literature as well
  as the reducibility method typically used for typed combinators, and
  can be modified to handle the simply-typed $\lambda$-calculus.
  We then give applications of our theorem to prove termination of
  constricting derivations and the general path ordering. 
  Finally we show how to use our techniques to prove an even more
  general theorem due to Jean Goubault-Larrecq.
  All proofs have been formally machine-checked using the 
  theorem prover Isabelle/HOL and we describe some of the encoding at
  appropriate places.
  \\
  {\bf Keywords}: rewriting, termination, well-founded ordering,
  strong normalisation, $\beta$-reduction, simply-typed $\lambda$-calculus

\end{abstract}

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

We address the general problem of termination of rewriting which can
be informally posed as follows.  Assume that we have a fixed set of
``objects'' defined according to some formal syntax.  Suppose we are given
a binary relation $\rho$ on these objects, where $(t, s) \in \rho$
expresses that object $s$ may be transformed into object $t$.  Let us
call such a transformation a \emph{reduction}.  Consider repeatedly
reducing an object in any way possible.  We are interested to know
whether such repeated reduction necesarily terminates -- formally,
whether or not there is an infinite sequence $t = t_0, t_1, \ldots$,
where each $(t_{i+1}, t_i) \in \rho$.  If there is not, we say that
$t$ is strongly normalising, $t \in \SN$.  

The difficulty of the problem arises from the totally general notion
of ``reduction'' and so we also show how we formalise and
machine-checked all our theorems and proofs using Paulson's
interactive theorem prover Isabelle/HOL \cite{isabelle-book}.

In the common special case of a term rewriting system (TRS), an object
is a term of some first-order language, and the reduction relation is
described by a 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. Here, rewriting is also usually \emph{monotonic}
\cite{bfr}, or \emph{closed under context} \cite{hm-dpr}, in that
if $C[\_]$, a term with a ``hole'', is the context, and $l$ reduces
to $r$, then $C[l]$ reduces to $C[r]$.  
There are several general methods capturing termination of such term
rewriting systems
% in this common case where rewriting can be performed at any ``sub-object'':
% that is, where the reduction relation is assumed to be ``closed under
% contexts'' or monotonic
\cite{dps00,nat-term,dggt}.

Recently, Jean Goubault-Larrecq \cite{jgl} has proved termination
results for the more general setting of an 
abstract reduction system (ARS) where this
monotonicity assumption does not hold and where objects need not have
a term structure.  He replaces the notion of subterm with an arbitrary
well-founded relation.  His Theorem~1 is the result of ``chasing
generalizations and simplifications'' of earlier work and ``subsumes
\ldots most path-orderings of the literature'' \cite{jgl}.

While the theorems from \cite{dggt} and \cite{jgl} use remarkably
similar ideas, it was frustrating to see that none actually subsumed
the other, even though \cite{dggt} applies to TRSs and \cite{jgl}
applies to ARSs.  Indeed, there is something in common between the two
results: a more general theorem that properly subsumes both.

We first present our generalised theorem and its proof in
\S\ref{s-tt}.  We then show that it generalises \cite[Theorem~1]{jgl}
and \cite[Theorem~2]{dggt} in \S\ref{s-opr}.  Finally, in
\S\ref{s-snst}, we show how to use our new theorem to obtain two
different proofs of strong normalisation for well-typed combinator
terms and how our proof method can be adapted to show strong
normalisation for the simply-typed $\lambda$-calculus.  In these
cases, although the objects have a term structure, our proofs use the
ARS setting and show the well-foundedness of larger, non-monotonic,
relations.  The combinator case shows that our theorem properly
generalises \cite[Theorem~1]{jgl}. Thus, our theorem handles most
path-orderings in the literature and the reducibility method typically
used for typed combinators. But, for the simply-typed
$\lambda$-calculus, it requires modifications to reason indirectly
about substitutions.

In Sections~\ref{s-cd} and \ref{s-gpo}, we apply our theorem to
constricting derivations and the general path ordering of
Dershowitz \& Hoot
\cite{nat-term}. We also use our techniques to give a different proof
of Goubault-Larrecq's much more complicated Theorem~2 \cite{jgl} in
Section~\ref{jgl-ho}. His theorem generalises \cite[Theorem~1]{jgl},
handles the reducibility argument, and encompasses explicit reasoning
about substitutions for handling the simply-typed $\lambda$-calculus.
% of Jouannaud \& Rubio
%\cite{jr-horpo}.

Our proofs have been formalised and machine-checked in the
theorem prover Isabelle/HOL: 
see \url{http://web.rsise.anu.edu.au/~jeremy/isabelle/snabs/}.

\comment{following replaced 
We address the general problem of termination of rewriting
which can be informally posed as follows.
Assume that we have a fixed set of ``objects''
defined according to some formal syntax.
Suppose we have a binary relation $\rho$ on these objects,
where $(t, s) \in \rho$
expresses that object $s$ may be transformed into object $t$.
Let us call such a transformation a \emph{reduction}.
Consider repeatedly reducing an object in any way possible.
We are interested to know whether such repeated reduction necesarily
terminates -- formally, whether or not there is an infinite sequence 
$t = t_0, t_1, \ldots$, where each $(t_{i+1}, t_i) \in \rho$.
If there is not, we say that $t$ is strongly normalising, $t \in \SN$.
The difficulty of the problem arises from the totally general notion
of ``reduction'', and there are several specialisations of this notion.

There are many different techniques in the literature for proving 
termination of rewriting, but few general theorems which unify these
different proofs.

In the common special case of a term rewriting system (TRS),
an object is a term of some first-order language, and the
reduction relation is described by giving a 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.
% When a relation is defined by a set of rewrite rules, 
Rewriting is also usually \emph{monotonic} \cite{bfr},
or \emph{closed under context} \cite{hm-dpr},
in that where $C[\_]$ is a context (a term with a ``hole''),
and $l$ reduces to $r$, then $C[l]$ reduces to $C[r]$.
% Such a relation is commonly called a \emph{reduction}, such as
% the ``$\beta$-reduction'' of the lambda calculus.

For example, if the ``objects'' are the terms of the simply-typed
$\lambda$-calculus, and the ``reductions'' are the usual 
$\beta$- and $\eta$-reductions,
then the monotonicity assumption is valid and our question becomes the problem
of the strong normalisation of the simply-typed $\lambda$-calculus.

There are several quite general theorems about termination of rewriting in this
common special case where rewriting can be performed at any ``sub-object'':
that is, where the reduction relation 
is assumed to be ``closed under contexts'' or monotonic.
More recently, various authors have investigated the problem of termination
of rewriting when this assumption does not hold.

However it is important to note that in our Isabelle treatment of TRSs
our reduction relation can be any relation that is closed under context.
We make no assumption that it is obtained by substituting a set of rules.
This simplifies the Isabelle formalisation, 
as we have no need to formalise the concept of substitution for a variable.  
Thus when a TRS based on such a set of rules is under consideration,
as in \S\ref{appl-rewr}, 
our relation $\sigma$ refers to the set of all substitution instances of the
set of rules, and $\rho$ is its closure under context.

The most common example is that of an abstruct reduction system (ARS)
where objects need not have a term structure.
Jean Goubault-Larrecq \cite{jgl} has proved termination results
which apply to the more general setting of an ARS. 
% abstract reduction relation.
He replaces the notion of subterm with an arbitrary well-founded relation. 
His Theorem~1 is the result of
``chasing generalizations and simplifications'' of earlier work
and ``subsumes \ldots most path-orderings of the literature'' (\cite{jgl}).

In \cite{dggt} we proved a theorem about the well-foundedness of
a monotonic relation on first-order terms, which applies to
the termination of systems of rewrite rules in a term rewriting system (TRS). 
Our theorem has some similarity to Theorem~1 of \cite{jgl},
but neither subsumes the other.
Motivated by his paper, 
we reformulated our previous theorem and its proof,
in the setting of an ARS, % abstract reduction relation,
incorporating generalisations suggested by his work.
The result of this was to produce a theorem which subsumes 
both our previous theorem and his Theorem~1.

We first present our generalised theorem.
We then give various applications of it to the
well-foundedness of abstract reduction relations on sets of objects 
which need not have a term structure.

We show directly how our result implies the 
termination of the general path ordering of Dershowitz \& Hoot
\cite{nat-term}, and relate our result to work on constricting derivations.

Goubault-Larrecq's Theorem~2 is even more general than his Theorem~1, 
extending the higher-order path ordering of Jouannaud \& Rubio \cite{jr-horpo}.
In Section~\ref{jgl-ho} we show how to
adapt and extend our proof to prove this result.

Finally, we show how our theorem can be used to prove the termination
of reduction of well-typed combinator terms,
and how our proof method can be adapted to show
the strong normalisation of the simply-typed $\lambda$-calculus.
In these cases, although the objects have a term structure, 
our proofs use the ARS setting in that they
show the well-foundedness of larger, non-monotonic, relations.
}

\subsection{Isabelle and the HOL Logic}

Isabelle is a logical framework written in ML \cite{}. It provides
basic facilities for interactively carrying out goal-directed
reasoning in which inference rules are applied backwards to reduce
conclusions to premises. The objects from which premises and
conclusions are built can be defined by the user. For example, if we
want to mimic a sequent calculus then the inference rules are built
from sequents. But if we want to reason axiomatically then they could
be built from formulae of a particular logic. 

Isabelle/HOL is a particular instantiation of this methodology in
which the inference rules are built using formulae of the classical
higher-order logic of Church called HOL \cite{}. Thus the syntax of
this logic contains the usual logical connective like 
implication \verb|-->|,
conjunction \verb|&|,
disjunction \verb!|!,
existential quantification \verb|EX|,
universal quantification \verb|ALL|.

Since Isabelle uses goal-directed reduction it also has a meta-level
logic which is higher-order intuitionistic logic with meta-level
connectives like
implication \verb|==>|,
conjunction \verb|;|,
universal quantification \verb|!!|. For example, the connective 
\verb|==>| is the horizontal line that usually separates premises from
conclusions.

Finally, there are  type-theoretic notions like 
the natural numbers \verb|nat|,
lists \verb|list|,
sets \verb|set|,
list concatenation \verb|head#tail|,
and $\lambda$-abstraction \verb|%|.

We have tried to explain parts of the encoding in the relevant parts
of this paper. The paper can be read without any background in
Isabelle as we have included English prose for almost all proofs. We
have extracted the code exactly and sometimes there is a mismatch
between the variable names used in the English prose and the actual
code. We could have renamed all the code but thought it best to leave
it as it is: we would be grateful for any advice the reviewers have in
regard to our presentation.

\subsection{Notation, Terminology, Definitions and Basic Lemmas} \label{s-ntd}

\comment{ moved earlier 
Assume that we have a fixed set of ``objects''.
Suppose we have a binary relation $\rho$ on these objects,
where $(t, s) \in \rho$
expresses that object $s$ may be transformed into object $t$.
Let us call such a transformation a \emph{reduction}.
Consider repeatedly reducing an object in any way possible.
We are interested to know whether such repeated reduction necesarily
terminates -- formally, whether or not there is an infinite sequence 
$t = t_0, t_1, \ldots$, where each $(t_{i+1}, t_i) \in \rho$.
If there is not, we say that $t$ is strongly normalising, $t \in \SN$.
end of comment moved earlier }

For an irreflexive binary relation $\rho$, we will write
$(r, t) \in \rho$, $(r, t) \in\ <_\rho$,
$r <_\rho t$ or $t >_\rho r$ interchangeably.
We prefer $<_\rho$ over the more traditional $\to_\rho$ because the latter is
typically used in TRSs and our setting is more abstract than TRSs.
For a symbol that suggests a direction, we will write
$(r, t) \in\ \vtl$, $(t, r) \in\ \vtr$,
$r \vtl t$ or $t \vtr r$ interchangeably.
Relations are assumed irreflexive unless the contrary is stated,
but are not assumed transitive even when written using $<_\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 objects,
and $\rho$ is \emph{well-founded} (or \emph{Noetherian})
if every $r \in \SN$.
We write $\leq_\rho$ or $\rho^=$, $<_\rho^+$ or $\rho^+$, and
$<_\rho^*$ or $\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$
that is, $(r, s) \in \sigma \circ \rho$
if there exists $t$ such that 
$(r, t) \in \rho$ and $(t, s) \in \sigma$.

\comment{ moved earlier 
In the common special case of a term rewriting system (TRS),
an object is a term of some first-order language, and the
reduction relation is described by giving a 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.
% When a relation is defined by a set of rewrite rules, 
It is also usually taken that it is \emph{monotonic},
or \emph{closed under context},
in that where $C[\_]$ is a context (a term with a ``hole''),
and $l$ rewrites to $r$, then $C[l]$ rewrites to $C[r]$.
% Such a relation is commonly called a \emph{reduction}, such as
% the ``$\beta$-reduction'' of the lambda calculus.
end of comment moved earlier }

In our formal treatment in Isabelle/HOL 
we used the following inductive definition
for the set \SN\ of strongly normalising objects,
and we proved, 
in the HOL logic, which is classical and contains the Axiom of Choice,
that this definition is equivalent to the standard definition given above.

\begin{definition}[Strongly Normalising -- HOL]
\label{defn:SN}
For a reduction relation $\rho$,
the set \SN\ of strongly normalising objects is the 
(unique) smallest set of objects
such that: if every object $t$ to which $s$ reduces 
% (ie, $(t, s) \in \rho$, ie $t >_\rho s$)
is in \SN\ then $s \in \SN$.
% 
% That is: for all $s$,
% if $\forall t.\,(t, s) \in \rho \Rightarrow t \in \SN$,
% then $s \in \SN$.
% 
% It follows that if $s$ cannot be reduced then $s \in \SN$.
% 
\end{definition}

Our previous work \cite{dggt}, on term rewriting systems, 
dealt with the well-founded-ness of the closure under context of
a relation called $\rho$.
By contrast, we are dealing here with an abstract reduction system,
usually calling the reduction relation $\rho$.
So 
%it is to be understood that 
concepts such as ``strongly
normalising'', ``reduction'', etc, relate to $\rho$, 
and not, even when discussing structured terms,
to the closure of $\rho$ under context.
Furthermore, in the ARS setting, we use an arbitrary relation 
as the counterpart of the immediate subterm relation
used in the TRS setting.
% as in \cite{jgl}, we call this arbitrary relation $\vtl$.
% Therefore if $t \in \SN$ it does not follow that
% subterms of $t$ are in \SN.

In \cite{dggt} %the term rewriting setting, 
we defined the set \ISN\ of ``inductively strongly
normalising'' terms as the set of terms that are in \SN\ if
their immediate subterms are in \SN\ \cite[\S 2.2]{dggt}.
Clearly, $\SN \subseteq \ISN$.
% We now generalise this definition to apply to the arbitrary relation $\vtl$
% in place of the immediate subterm relation \isubt.
We now define \gindy\ as a generalised notion of ``inductively'' for
an arbitrary relation $\sigma$ in place of the immediate subterm
relation \isubt, and then generalise the function \bars\ from
\cite{jgl} by defining \gbars\ inductively.  We encode \gbars\ in
Isabelle/HOL as an ``inductively defined set'': that is, the set
defined is the unique smallest possible set such that the introduction
rules are satisfied.  We also use this feature to define \gindy. In
both cases, Isabelle automatically generates a number of convenient
lemmas.

\begin{definition}[\gindy] \label{def-gindy} 
  For a relation $\sigma$ and set $S$, 
  an object $t \in \gindy\ \sigma\ S$ iff: \\
  if $\forall u.\ (u, t) \in \sigma \Rightarrow u \in S$, 
  then $t \in S$.
\begin{verbatim}
inductive "gindy ?r ?S"
  I "(ALL dts. (dts, ?dt) : ?r --> dts : S) --> ?dt : S 
    ==> ?dt : gindy ?r ?S"
\end{verbatim}
\end{definition}

The questions marks in front of \verb|?r| indicates that this is a
free variable, which is instantiated when we use the inductive
definition. The symbol \texttt{I} is just a label which allows us to
refer to this particular clause when required, and allows the reader
to find it in the actual code. The colon \verb|:|
encodes the usual membership symbol $\in$
so that 
\texttt{(dts, ?dt) : ?r} encodes
$(u, t) \in \sigma$.
The HOL \verb|-->|
connective encodes the implication $\Rightarrow$, and the Isabelle
double arrow \verb|==>| encodes the ``if ... then'' part of our
definition. Thus this definition is a rule of inference with one
premise and one conclusion which allows us to reduce the goal
\texttt{?dt : gindy ?r ?S} to the given premise.

\begin{definition}[\gbars] \label{def-gbars-isa} 
For sets of objects $Q$ and $S$, and relation $\sigma$,
$\gbars\ \sigma\ Q\ S$ is the (unique) smallest set such that:
\begin{enumerate}
\item \label{gbars-inI} $S \subseteq \gbars\ \sigma\ Q\ S$
\item \label{gbars-gbarsI} 
  if $t \in Q$ and
  $\forall u.\ (u, t) \in \sigma \Rightarrow u \in \gbars\ \sigma\ Q\ S$,
  then $t \in \gbars\ \sigma\ Q\ S$.
\end{enumerate}
\end{definition}

\begin{verbatim}
inductive "gbars ?r ?Q ?S"
inI     "dt : ?S ==> dt : gbars ?r ?Q ?S"
gbarsI  "[| dt : ?Q  ; 
          (ALL dtn. (dtn, dt) : ?r --> dtn : gbars ?r ?Q ?S) |] 
	 ==> dt : gbars ?r ?Q ?S"
\end{verbatim}

Here, the 
clauses 
\verb!inI! and 
\verb|gbarsI| encode 
\ref{gbars-inI} and \ref{gbars-gbarsI}, respectively.
Also, the
brackets
\verb![|! and \verb!|]! 
delineate the list of premises in the second rule of inference.
The next lemma gives another characterisation of \gbars\ which is
provably equivalent in classical logic using the Axiom of Choice: $t
\in \gbars\ \sigma\ Q\ S$ iff every downward $\sigma$-chain starting
from $t$ is within $Q$ until it hits $S$ or it terminates.

\begin{lemma}[\gbars -alternative] \label{def-gbars} 
For sets of objects $Q$ and $S$, and relation $\sigma$,
object $t \in \gbars\ \sigma\ Q\ S$ iff: 
for every downward $\sigma$-chain 
$t = t_0 >_\sigma t_1 >_\sigma t_2 >_\sigma \ldots$,
either the chain is finite and all $t_i \in Q$, or 
for some member $t_n$ of the chain,
both $t_n \in S$ and $\{t_0, t_1, t_2, \ldots, t_{n-1}\} \subseteq Q$.
\end{lemma}

\comment{
\begin{verbatim}
 gbars_char = "(?x : gbars ?r ?Q ?S) =
   ((ALL f.  f 0 = ?x & (ALL i. (f (Suc i), f i) : ?r) --> (EX i. f i : ?S)) &
   (ALL f n.  f 0 = ?x & (ALL i<n. (f (Suc i), f i) : ?r) -->
     (ALL j<=n. f j ~: ?S) --> f n : ?Q))" : thm 
\end{verbatim}
}

Definition \ref{def-wfp,bars} captures the notions
of ``$S$ \emph{bars} $s$ in $\sigma$'' and of
``$s$ is \emph{accessible} in $\sigma$, or
  $s$ is in the \emph{well-founded part} of $\sigma$''
as defined in \cite{jgl}.

\begin{definition}[\wfp, \bars] \label{def-wfp,bars} 
Let $\mathcal{U}$ be the universal set of objects.  Then
\begin{enumerate}
\item $s \in \bars\ \sigma\ S$ iff
  $s \in \gbars\ \sigma\ \mathcal{U}\ S$
\hfill (``$S$ \emph{bars} $s$ in $\sigma$'')
\item $s \in \wfp\ \sigma$ iff
  $s \in \bars\ \sigma\ \emptyset$
% \hfill (``$s$ is \emph{accessible} in $\sigma$ '').
  \hfill (``$s$ is in the \emph{well-founded part} of $\sigma$'').
\end{enumerate}
\end{definition}

Thus $\SN = \wfp\ \rho$ and $\ISN = \gindy\ \isubt\ \SN$.

Our Lemma~\ref{gindy-gbars} below generalises \cite[Lemma~2]{dggt}.
It relies on the \gbars-induction principle, 
which is analogous to the principles of well-founded induction,
and of \bars-induction (see \cite[Proposition~1]{jgl}).
It is generated automatically by the Isabelle theorem prover from
the inductive definition of \gbars\ above.
We write $\mathcal P\ s$ to mean that object $s$ satisfies property 
$\mathcal P$.

\begin{proposition}[\gbars-induction]\label{gbars-ind}
For sets $Q$ and $S$, and any property $\mathcal P$, if
 Let $Q$ and $S$ be sets of objects.
 Then, for every property $\mathcal P$, if
\begin{enumerate}
\item \label{gi-in} for every $s \in S$, we have $\mathcal P\ s$, and
\item \label{gi-rec} for every $s \in Q$, if 
  $\forall t.\ (t, s) \in \sigma \Rightarrow \mathcal P\ t$,
   then $\mathcal P\ s$
\end{enumerate}
then every $s \in \gbars\ \sigma\ Q\ S$ satisfies $\mathcal P$.
\end{proposition}

\begin{verbatim}
gbars.induct = 
 "[| !!dt. dt : ?S ==> ?P dt ;
     !!dt. [| dt : ?Q ;
	ALL dtn. (dtn, dt) : ?r --> dtn : gbars ?r ?Q ?S & ?P dtn |] 
	==> ?P dt |] 
  ==> ?xa : gbars ?r ?Q ?S ==> ?P ?xa" : thm
\end{verbatim}

This induction principle is a theorem with three assumptions,
of which the second is a compound one, having itself two assumptions
and a conclusion.
Recall that the notation \verb|!!dt.| denotes meta-level universal
quantification. The appellation
\texttt{: thm}
at the end indicates that this statement has been accepted by the
Isabelle proof engine as a theorem.\footnote{
A careful reading shows that there is an extra
occurrence of  
\texttt{dtn : gbars ?r ?Q ?S}
in the succedent of this second assumption, but we have omitted it
from the prose since it is not essential but is automatically
generated by Isabelle.}

\begin{lemma}\label{gindy-gbars}
  $S = \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S $
\end{lemma}

\begin{verbatim}
gindy_gbars = "gbars ?r (gindy ?r ?P) ?P = ?P" : thm 
\end{verbatim}

\begin{proof} 
$\subseteq$: this is trivial, 
from Definition~\ref{def-gbars-isa}\ref{gbars-inI},
by letting $Q$ be $\gindy\ \sigma\ S$.
 -- if $t \in S$, this is the case $n = 0$ in Definition~\ref{def-gbars}.

$\supseteq$: Let $\mathcal P\ s = s \in S$.
We use Proposition~\ref{gbars-ind} with $Q = \gindy\ \sigma\ S$.
Condition~\ref{gi-in} of Proposition~\ref{gbars-ind} holds trivially,
and condition~\ref{gi-rec} is given by
Definition~\ref{def-gindy}.
 So Proposition~\ref{gbars-ind} gives the result.
\qed \end{proof}

\begin{lemma}\label{l2}
\begin{enumerate}
\item \label{gindy-bars}
  if all objects are in $\gindy\ \sigma\ S$, then $\bars\ \sigma\ S = S$,
  whence, if $\sigma$ is well-founded, then every object is in $S$, and
\item \label{bars-wfp}
  $\bars\ \sigma\ (\wfp\ \sigma) = \wfp\ \sigma$
\end{enumerate}
\end{lemma}

\begin{verbatim}
gindy_bars =
 "[| ?c : bars ?r ?B; !!dts. dts : gindy ?r ?B |] ==> ?c : ?B" : thm
bars_wfp = "bars ?r (wfp ?r) = wfp ?r" : thm
\end{verbatim}

\begin{proof}
\ref{gindy-bars} follows from Lemma~\ref{gindy-gbars};
\ref{bars-wfp} holds as every object is in
$\gindy\ \sigma\ (\wfp\ \sigma)$.
\end{proof}

\section{The Termination Theorem} \label{s-tt}

 We now have enough terminology to prove termination, 
 but we require some further properties of $\rho$.
 
 \subsection{Properties we require of $\rho$} \label{s-rho-props}

Given a reduction relation $\rho$, our general termination result requires 
relations $\vtl$ and $\ll$ which satisfy certain properties.
These relations play a role similar to the relations $\vtl$ and $\ll$
in \cite{jgl}, and, where convenient, we express our conditions so as to 
enable easy comparisons with \cite{jgl}.
The most general version of the properties that $\vtl$ and $\ll$
must satisfy is Condition~\ref{conds-defs}\ref{rpc0} below, 
but in practice we often use the simpler and stronger conditions
\ref{rpc} to \ref{rpc2}.

\begin{condition}\label{conds-defs}
\begin{enumerate}
\item \label{rpc0}
If $\forall s' \vtl s.\ s' \in \SN$, 
then $s \in  \bars\ \rho\ (\gbars \vtl \{u\:|\ u \ll s\}\ \SN)$

\item \label{rpc}
For all $(t, s) \in \rho$,
if $\forall s' \vtl s.\ s' \in \SN$, 
then $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$

\item \label{rpca}
For all $(t, s) \in \rho$,
$t \in \gbars \vtl \{u\:|\ u \ll s\}\ 
  \{v\:|\ (v, s) \in (\vtl \circ\ \rho)\}$

\item \label{rpc1}
$\vtl$ is well-founded and, for all $(t, s) \in \rho$,
if $\forall s' \vtl s.\ s' \in \SN$, then, \\
for all $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$

\item \label{rpc2}
$\vtl$ is well-founded and, for all $(t, s) \in \rho$ and
for all $t' \vtl^* t$, \\ either
  $(t', s) \in (\vtl \circ\ \rho^*)$ or 
   $t' \ll s$.
\end{enumerate}
\end{condition}

\begin{verbatim}
"red_props_bgb ?rho ?isub ?cuto ?S ?dt == 
  (ALL dts. (dts, ?dt) : ?isub --> dts : ?S) --> 
    ?dt : bars ?rho (gbars ?isub {dtc. (dtc, ?dt) : ?cuto} ?S)" : thm 

"red_props_gbscf ?rho ?isub ?cuto ?S ?dt == 
  (ALL dts. (dts, ?dt) : ?isub --> dts : ?S) -->
  (ALL dtn. (dtn, ?dt) : ?rho --> 
    dtn : gbars ?isub {dtc. (dtc, ?dt) : ?cuto} ?S)" : thm

"red_props_dtaf ?rho ?isub ?cuto ?S ?dt == 
  (ALL dts. (dts, ?dt) : ?isub --> dts : ?S) -->
  (ALL dtn.  (dtn, ?dt) : ?rho --> (ALL dts.
    (dts, dtn) : ?isub^* --> dts : ?S | (dts, ?dt) : ?cuto))"
\end{verbatim}

\begin{lemma} \label{conds-lemma}
Each of Conditions~\ref{conds-defs}\ref{rpc} to \ref{rpc2}
implies Condition~\ref{conds-defs}\ref{rpc0}.
\end{lemma}

\begin{verbatim}
bgb_gbsnf = "red_props_gbscf ?rho ?isub ?cuto ?S ?dt ==>
    red_props_bgb ?rho ?isub ?cuto ?S ?dt" : thm

dta_gbscf = "[| wf ?isub; red_props_dtaf ?rho ?isub ?cuto ?S ?dt |]
      ==> red_props_gbscf ?rho ?isub ?cuto ?S ?dt" : thm
\end{verbatim}

\begin{proof}
It is easy to see that Condition~\ref{conds-defs}\ref{rpc} implies
Condition~\ref{conds-defs}\ref{rpc0}. 

To show that Condition~\ref{conds-defs}\ref{rpc1} implies
Condition~\ref{conds-defs}\ref{rpc}, 
assume \ref{rpc1} holds.
Then, as $\vtl$ is well-founded, there is no infinite descending $\vtl$-chain.
Any descending $\vtl$-chain from $r$ is contained in 
$\{t'\:|\ t' \ll s\} \cup \SN$.
In other words, members of such a chain are contained in $\{t'\:|\ t' \ll s\}$
until the chain reaches a member of \SN.
That is, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$, 
and so \ref{rpc} holds.

To show that Condition~\ref{conds-defs}\ref{rpc2} implies
Condition~\ref{conds-defs}\ref{rpc1}, 
and likewise, that Condition~\ref{conds-defs}\ref{rpca} 
implies Condition~\ref{conds-defs}\ref{rpc}, 
assume that $\forall s' \vtl s.\ s' \in \SN$.
Then, if $(t', s) \in (\vtl \circ\ \rho^*)$ because $t' <_\rho^* s' \vtl s$, 
then we have $s' \in \SN$ and so $t' \in \SN$.
Note that in Condition~\ref{conds-defs}\ref{rpca}
we could have $(\vtl \circ\ \rho^*)$ in place of $(\vtl \circ\ \rho)$.
\qed \end{proof}

 \subsection{The Proof of Termination}

Our key lemma, Lemma~\ref{dth} below, corresponds to \cite[Lemma~3]{dggt}, 
but is considerably simpler.
We thank an unnamed referee for pointing out
that our proof and that of \cite[Lemma~3]{dggt}
 bears considerable resemblance to the proof by 
resembles the proof by 
Buchholz \cite{buchholz-pta} of the well-foundedness of the lexicographic 
path ordering, although it was obtained independently.

\comment{
\begin{lemma} \label{dth}
For any object $s$, 
if $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, 
then $s \in \gindy \ll (\gindy \vtl \SN)$.
 If all objects ${t' \ll s}$ are in $\gindy \vtl \SN$, 
 then $s \in \gindy \vtl \SN$.
\end{lemma}
}

\begin{lemma} \label{dth}
If object $s$ satisfies  
Condition~\ref{conds-defs}\ref{rpc0}, 
then \mbox{$s \in \gindy \ll (\gindy \vtl \SN)$}.
 If all objects ${t' \ll s}$ are in $\gindy \vtl \SN$, 
 then $s \in \gindy \vtl \SN$.
\end{lemma}

\begin{verbatim}
dth_dti_bgb = "red_props_bgb ?rho ?isub ?cuto (wfp ?rho) ?dt ==>
    ?dt : gindy ?cuto (gindy ?isub (wfp ?rho))" : thm
\end{verbatim}

\begin{proof} 
Given $s$, assume that 
$\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0} and that

(a) $\forall {u} \ll {s}.\ u \in \gindy \vtl \SN$.

\noindent We then need to show $s \in \gindy \vtl \SN$, so we assume that 

(b) $\forall {s'} \vtl {s}.\ s' \in \SN$

\noindent and we show that $s \in \SN$.
By Lemma~\ref{l2}\ref{bars-wfp},
it suffices to show $s \in \bars\ \rho\ \SN$.
 To show that $s \in \SN$, it is enough to show 
 $s \in \bars\ \rho\ \SN$ by Lemma~\ref{l2}\ref{bars-wfp}.

 By Condition~\ref{conds-defs}\ref{rpc0} 
 (whose antecedent condition holds by assumption (b))
The antecedent of Condition~\ref{conds-defs}\ref{rpc0}
holds by assumption (b),
and so $s \in \bars\ \rho\ (\gbars \vtl \{u\:|\ u \ll s\}\ \SN)$.
As \bars\ is monotonic in its second argument, it is enough to show
$\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq \SN$.
As $\{u\:|\ u \ll s\} \subseteq \gindy \vtl \SN$ by assumption (a),
and as \gbars\ is monotonic in its second argument, 
we have $\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq
\gbars \vtl (\gindy \vtl \SN)\ \SN = \SN$, by Lemma~\ref{gindy-gbars}.

So we have $s \in \SN$.
Thus, discharging assumptions (b) and then (a),
we have $s \in \gindy \vtl \SN$,
and then $s \in \gindy \ll (\gindy \vtl \SN)$. 
\qed \end{proof}

We now identify the conditions  we need to deduce, from Lemma~\ref{dth},
that guarantee that every object is in \SN.

\begin{theorem} \label{thm-allsn}
Relation $\rho$ is well-founded if
 Suppose that $\rho$, $\vtl$ and $\ll$ satisfy
Condition~\ref{conds-defs}\ref{rpc0} holds and 
\begin{enumerate}
\item \label{ubg} every object is in $\bars \ll (\gindy \vtl \SN)$, and
\item \label{vbs} every object is in $\bars \vtl \SN$.
\end{enumerate}
 Then $\rho$ is well-founded.
\end{theorem}

\begin{proof}
  If $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0},
  then every $s \in \gindy \ll (\gindy \vtl \SN)$ by Lemma~\ref{dth}.
  Then, for any $u$, if $u \in \bars \ll (\gindy \vtl \SN)$ then
  Lemma~\ref{l2}\ref{gindy-bars} gives $u \in \gindy \vtl \SN$.
  Thus every $u \in \gindy \vtl \SN$.
  Then, for any $v$, if $v \in \bars \vtl \SN$ then
  Lemma~\ref{l2}\ref{gindy-bars} gives $v \in \SN$.  
  Thus every $v \in \SN$: that is, $\rho$
  is well-founded.  \qed 
\end{proof}

\comment{
 The two stages of the proof are represented by
 the following Isabelle theorems.
 all_gindy_bgb = "[| All (red_props_bgb ?rho ?isub ?cuto (wfp ?rho));
     ?dt : bars ?cuto (gindy ?isub (wfp ?rho)) |] ==> 
     ?dt : gindy ?isub (wfp ?rho)" : thm
}

\begin{verbatim}
all_wf_bgb = "[| ?dt : bars ?isub (wfp ?rho);
    All (red_props_bgb ?rho ?isub ?cuto (wfp ?rho));
    ALL u. u : bars ?cuto (gindy ?isub (wfp ?rho)) |] ==>
    ?dt : wfp ?rho" : thm
\end{verbatim}

\section{Generalising Previous Results} \label{s-opr}

We now obtain both \cite[Theorem~1]{jgl} and \cite[Theorem~2]{dggt}
from our Theorem~\ref{thm-allsn}.

\subsection{Generalising Goubault-Larrecq's General Theorem for ARSs}

We show that our Theorem~\ref{thm-allsn} properly generalizes 
Theorem~1 of Goubault-Larrecq \cite{jgl}, which itself 
generalizes many results in the literature.
Note that \cite{jgl} uses $<$ where we use $\rho$.
We first require two lemmas.

\begin{lemma} \label{lemma-P2}
Given set $S$ and object $s$, suppose for all $t$ that, if
$(t, s) \in \rho$, then
\begin{enumerate}
\item \label{P2a} $t \in S$, or
\item \label{P2b} $s \gg t$ and, for every $u \vtl t$, 
  either $(u, s) \in \rho$ or $u \in S$.
\end{enumerate}
Assume $\vtl$ is well-founded.
Then $(t, s) \in \rho$ implies  
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$.
\end{lemma}

\begin{verbatim}
"red_props_jglhf ?isub ?S ?rho ?cuto ?s == ALL t.
  (t, ?s) : ?rho --> t : ?S | (t, ?s) : ?cuto & 
    (ALL u. (u, t) : ?isub --> (u, ?s) : ?rho | u : ?S)" : thm

jglhf_gbars = "[| wf ?isub; red_props_jglhf ?isub ?S ?rho ?cuto ?dt |]
         ==> red_props_gbsf ?rho ?isub ?cuto ?S ?dt" : thm 
\end{verbatim}

\begin{proof}
Let $(t, s) \in \rho$.
We prove this result for $t$ by well-founded induction on $\vtl$,
so assume that, for all $v \vtl t$, if $(v, s) \in \rho$
then $v \in \gbars \vtl \{x\:|\ x \ll s\}\ S$.

We consider the two cases \ref{P2a} and \ref{P2b} as above.
Firstly, if $t \in S$, then $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$
by Definition~\ref{def-gbars-isa}\ref{gbars-inI}.
Secondly, if \ref{P2b} holds, we show that 
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$
using Definition~\ref{def-gbars-isa}\ref{gbars-gbarsI}.
We have $t \ll s$, and for any $u \vtl t$, there are again two cases.
In the first case, $(u, s) \in \rho$
 $u <_\rho s$ (from \ref{P2b} above), 
and so, by the inductive hypothesis, 
$u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$.
In the second case, $u \in S$
and so $u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$
by Definition~\ref{def-gbars-isa}\ref{gbars-inI}.
\qed \end{proof}

\begin{lemma} \label{lemma-P1}
Suppose that, whenever $(t, s) \in \rho$, either  
\begin{enumerate}
\item \label{P1a} for some object $u$, $s \vtr u$ and $u \geq_\rho t$, or
\item \label{P1b} $s \gg t$ and, for every $u \vtl t$, $s >_\rho u$.
\end{enumerate}
Suppose also that $\vtl$ is well-founded.
Then Condition~\ref{conds-defs}\ref{rpc} holds.
\end{lemma}

\begin{proof}
We use Lemma~\ref{lemma-P2} with
$S = \{v\:|\ \exists x.\ s \vtr x \mbox{ and } x \geq_\rho v\}$.
To show Condition~\ref{conds-defs}\ref{rpc}, let $(t, s) \in \rho$,
and suppose that $\forall s' \vtl s.\ s' \in \SN$. 
By Lemma~\ref{lemma-P2}, $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$.
We show $S \subseteq \SN$.  
Let $s \vtr x $ and $ x \geq_\rho v$. 
Then $x \in \SN = \wfp\ \rho$ and so $v \in \SN$.
Thus, by the obvious monotonicity of \gbars,
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$, as required for
Condition~\ref{conds-defs}\ref{rpc}.
\comment{
Let $(t, s) \in \rho$ and assume that for all $s' \vtl s$, $s' \in \SN$. 
We prove the result by well-founded induction on $\vtl$,
so assume that for all $v \vtl t$ such that $v <_\rho s$,
$v \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$.

We consider the two cases \ref{P1a} and \ref{P1b}.
Firstly, suppose that $s \vtr u$ and $u \geq_\rho t$.
Then $u \in \SN$, so $t \in \SN$, so 
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$ 
by clause \ref{gbars-inI} of Definition~\ref{def-gbars-isa}.
Secondly, if \ref{P1b} holds, we show that 
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$
using clause \ref{gbars-gbarsI} of Definition~\ref{def-gbars-isa}.
We have $t \ll s$, and for any $u \vtl t$, $u <_\rho s$ (from \ref{P1b}
above), and so, by the inductive hypothesis, 
$u \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$.
Therefore $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$.
}
\qed \end{proof}

\begin{verbatim}
jglh_gbscf = "[| wf ?isub;
    red_props_jglhf ?isub {dts. (dts, ?dt) : ?isub O ?rho^*} 
        ?rho ?cuto ?dt |] ==>
    red_props_gbscf ?rho ?isub ?cuto (wfp ?rho) ?dt" : thm
\end{verbatim}

\begin{corollary}
Theorem~1 of \cite{jgl} holds.
 if the conditions of Lemma~\ref{lemma-P1} hold,
 condition~\ref{ubg} of Theorem~\ref{thm-allsn} holds,
 and $\vtl$ is well-founded, then $\rho$ is well-founded.
\end{corollary}

\begin{proof}
Theorem~1 of \cite{jgl} says:
if Property~1 and conditions (\emph{iii}) and (\emph{iv}) 
(as given in \cite{jgl}) hold, then $\rho$ is well-founded.
 Condition (\emph{iii}) of \cite{jgl} says that $\vtl$ is well-founded.

Condition (\emph{iv}) of \cite{jgl} 
is just 
condition \ref{ubg} of Theorem~\ref{thm-allsn}
because $\underline{SN}$ of \cite{jgl} is $\gindy \vtl \SN$ and 
the words 
``\textit{if every $u \vtl s$ is in SN}'' in \cite{jgl} are redundant.
 is that every object $u$ is in $\bars \ll (\gindy \vtl \SN)$, 
 because $\underline{SN}$ of \cite{jgl} is $\gindy \vtl \SN$. 
 
 Thus, by condition (\emph{iv}) of \cite{jgl} 
 condition \ref{ubg} of Theorem~\ref{thm-allsn} holds.

Condition (\emph{iii}) of \cite{jgl} says that $\vtl$ is well-founded.
Then, for any object $v$ and set $S$ of objects, 
$v \in \bars \vtl S$, and so condition \ref{vbs} of 
Theorem~\ref{thm-allsn} follows.

Property~1 says that for $(t, s) \in \rho$, either  
\ref{P1a} or \ref{P1b} of Lemma~\ref{lemma-P1} holds.
 Finally we show that, in the presence of condition (iii) of \cite{jgl}
 (ie, that $\vtl$ is well-founded),
Finally, Lemma~\ref{lemma-P1} shows that 
if $\vtl$ is well-founded, as ensured by condition (iii) of \cite{jgl},
then Property~1 of \cite{jgl}
 which is \ref{P1a} and \ref{P1b} of Lemma~\ref{lemma-P1},
implies Condition~\ref{conds-defs}\ref{rpc},
whence Condition~\ref{conds-defs}\ref{rpc0} holds.

Thus all the conditions of Theorem~\ref{thm-allsn} hold, 
so $\rho$ is well-founded.  
\qed \end{proof}

\begin{verbatim}
all_wf_gjgl = "[| ALL dt. red_props_jglhf ?isub 
    {dts. (dts, dt) : ?isub O ?rho^*} ?rho ?cuto dt;
  ALL u. u : bars ?cuto (gindy ?isub (wfp ?rho));
  wf ?isub |] ==> ?dt : wfp ?rho" : thm
\end{verbatim}

We explore the extent to which, conversely, 
Theorem~1 of Goubault-Larrecq \cite{jgl} implies our Theorem~\ref{thm-allsn}.
We discuss in detail only whether our Conditions 
\ref{conds-defs}\ref{rpc0} to \ref{rpc2} imply Property~1 of \cite{jgl}.  
First we note a sort of converse to Lemma~\ref{lemma-P2}:
if $(t, s) \in \rho \Leftrightarrow t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$
then, by the definition of \gbars,
\ref{P2a} or \ref{P2b} of Lemma~\ref{lemma-P2} hold,
even after deleting ``\emph{or} $u \in S$'' from \ref{P2b}.

Suppose Condition~\ref{conds-defs}\ref{rpca} holds: that is,
with $S = \{v\:|\ (v, s) \in (\vtl \circ\ \rho)\}$,
we have $(t, s) \in \rho \Rightarrow t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$.
Since \gbars\ is monotonic in its third argument
and $S$ is monotonic in $\rho$,
we can enlarge $\rho$ so that Condition~\ref{conds-defs}\ref{rpca}
holds as an equivalence, giving
\ref{P1a} and \ref{P1b} of Lemma~\ref{lemma-P1}
(\textit{i.e.} Property~1 of \cite{jgl}).

That is, \cite[Theorem~1]{jgl} can be used to prove a weaker version
of our Theorem~1 in which Condition~\ref{conds-defs}\ref{rpca},
rather than Condition~\ref{conds-defs}\ref{rpc0}, is assumed,
and it is assumed that $\vtl$ is well-founded.
On the other hand, in Sections \ref{s-tc} and \ref{s-tc2}, the proofs
of termination use Theorem~\ref{thm-allsn}, and, in particular, use
Condition~\ref{conds-defs}\ref{rpc}.
The difference between Condition~\ref{conds-defs}\ref{rpc}
and Condition~\ref{conds-defs}\ref{rpca} is crucial to these proofs,
which shows that Theorem~\ref{thm-allsn} properly generalises
\cite[Theorem~1]{jgl}.

\subsection{Generalising our Previous Theorem for TRSs}
\label{s-appl-rewr}

We now apply Theorem~\ref{thm-allsn} to the special case of a TRS
on terms of a first-order language $T (\Sigma, V)$
(see \cite[\S 3.1]{baader-nipkow}),
thereby showing that it properly generalises our
main result from \cite{dggt}.
We consider a binary relation $\sigma$, 
which is the set of substitutional instances of a
set of rewrite rules, and so is closed under substitutions.
However $\sigma$ itself is typically not monotonic,
ie, compatible with $\Sigma$-contexts 
(see \cite[Definition~3.1.9]{baader-nipkow}).
 
So we define $\ctxt\ \sigma$ to be the ``closure under contexts''
of $\sigma$:
that is, where $C[\_]$ is a context,  (a term with a ``hole''),
and $(r, l) \in \sigma$, then $(C[r], C[l]) \in \ctxt\ \sigma$. 

\comment{
 \begin{definition}[{closure under contexts}] 
 \footnote{could delete this}
   Given a relation $\sigma$ and terms $s$ and $t$, the
   pair $(t, s) \in \ctxt\ \sigma$ (pronounced ``$s$ reduces to
   $t$'') if either
 \emph{(a)} $(t, s) \in \sigma$, or
 \emph{(b)} $s$ and $t$ are identical except that exactly one
        immediate subterm of $s$ reduces to the
        corresponding immediate subterm of $t$.
 \end{definition}
} 

\comment{ 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$.
}

\isabelle{
For the Isabelle formalisation, we need to define the language of terms.
We do so using a datatype 
\verb|'a rtree|,
which defines ``rose trees'' as shown below:
\begin{verbatim}
 datatype 'a rtree = Node "'a" "'a rtree list"
\end{verbatim}

Thus a term is a tree of nodes where each node contains an object of
type \verb|'a| and has an arbitrary list of subtrees each of which
itself is a rose-tree. We then define the notion of immediate subterm
using an inductively defined set of ordered pairs \verb|isubt| as
shown below:
\begin{verbatim}
isubt :: "('a rtree * 'a rtree) set"
inductive "isubt"
    isubtI "?sdt : set ?sts ==> (?sdt, Node ?a ?sts) : isubt"
\end{verbatim}
The first line above declares \verb|isubt| to consist of a set of
ordered pairs of rose-trees. The next line is an inductive definition
which says that the rose-tree \verb|sdt| is an immediate subtree of
the rose-tree \verb|Node a sts| if \verb|sdt| is in the set 
\verb|set sts| 
of members of the list \verb|sts| of immediate
subtrees of 
\verb|Node a sts|.  
It is then easy to show that \verb|isubt| is well-founded.
Then, the notions of proper subtree and subtree are defined as the
transitive closure and the reflexive-transitive closure of 
\verb|isubt|
respectively: we omit details.

We now refer to rose-trees as terms.
We define 
\verb|oneup|
as a function from a set of ordered pairs of lists of terms to
ordered pairs of terms and define
\verb|oneup r|
as an inductively defined set of ordered pairs of terms:
\begin{verbatim}
oneup :: 
 "('a rtree list * 'a rtree list) set => ('a rtree * 'a rtree) set"
inductive "oneup ?r"
 ouI "(?l1, ?l2) : ?r ==> (Node ?a ?l1, Node ?a ?l2) : oneup ?r"
\end{verbatim}

Thus, two terms 
\verb|Node a l1|
and
\verb|Node a l2|
are in 
\verb|oneup r|
if they share the same root 
\verb|a|
and the ordered pair
(\verb|l1|, \verb|l2|)
formed from their respective
lists of immediate subterms is in 
\verb|r|. 

Two lists of terms 
are related by \verb|onerel r| if they are the same
except that one pair of corresponding members are related by \verb|r| 
as shown below:

\begin{verbatim}
onerel :: "('a * 'a) set => ('a list * 'a list) set"
inductive "onerel ?r"
 onerelI1 "(?a, ?b) : ?r ==> (?a # ?t, ?b # ?t) : onerel ?r"
 onerelI2 "(?al, ?bl) : onerel ?r ==> (?h # ?al, ?h # ?bl) : onerel ?r"
\end{verbatim}

We define \verb|ctxt|, for closure under context, inductively, using 
\verb|oneup| and \verb|onerel|:
\begin{verbatim}
ctxt, sn1order ::
 "('a rtree * 'a rtree) set => ('a rtree * 'a rtree) set"
inductive "ctxt ?r"
 red_cutI  "(?tr, ?t) : ?r ==> (?tr, ?t) : ctxt ?r"
 red_nuI "(?tr, ?t) : oneup (onerel (ctxt ?r)) ==> (?tr, ?t) : ctxt ?r"
\end{verbatim}
The clause
\verb|red_cutI|
is the base case where the whole term
\verb|t|
is reduced to the whole term
\verb|tr|.
The clause
\verb|red_nuI|
is the inductive case where term
\verb|t|
is reduced to term
\verb|tr|
via a reduction of an immediate subterm of
\verb|t|
into a corresponding immediate subterm of
\verb|tr|:
that is, where the two terms 
\verb|t| 
and 
\verb|tr|
are identical at the root but some 
member of the list of immediate subterms of 
\verb|t|
is reduced to give the corresponding 
member of the list of immediate subterms of 
\verb|tr|.

We also define $<_{sn1}$ as \verb|sn1order|, and prove that it is well-founded.

\begin{verbatim}
sn1order_def = "sn1order ?r == oneup (onerel (fwf (ctxt ?r)))"
wf_sn1order  = "wf (sn1order ?r)" : thm 
\end{verbatim}
}

%%  \begin{verbatim}
%%  datatype 'a rtree = Node "'a" "'a rtree list"

%%  inductive "isubt"
%%      isubtI "sdt : set sts ==> (sdt, Node a sts) : isubt"

%%  wf_isubt = "wf isubt" : thm

%%  ctxt, sn1order    ::
%%      "('a rtree * 'a rtree) set => ('a rtree * 'a rtree) set"
%%  onerel        :: "('a * 'a) set => ('a list * 'a list) set"
%%  oneup :: "('a rtree list * 'a rtree list) set =>
%%      ('a rtree * 'a rtree) set"

%%  inductive "onerel r"
%%      onerelI1 "(a, b) : r ==> (a # t, b # t) : onerel r"
%%      onerelI2 "(al, bl) : onerel r ==> (h # al, h # bl) : onerel r"

%%  inductive "oneup r"
%%      ouI "(dtl1, dtl2) : r ==> (Node a dtl1, Node a dtl2) : oneup r"

%%  inductive "ctxt r"
%%      red_nuI "(dtr, dt) : oneup (onerel (ctxt r)) ==>
%%        (dtr, dt) : ctxt r"
%%      red_cutI  "(dtr, dt) : r ==> (dtr, dt) : ctxt r"

%%  "sn1order ?r == oneup (onerel (fwf (ctxt ?r)))" : thm
%%  wf_sn1order = "wf (sn1order ?r)" : thm 
%%  \end{verbatim}
%% }

In \cite{dggt} we dealt with the termination of such rewrite relations.
 We now show that the main theorem there follows from Theorem~\ref{thm-allsn}.
In discussing that work we will use ``$\sigma$'' for the relation there called
``$\rho$'', which is the set of substitutional instances of the rewrite rules.
Then the rewrite relation is $\ctxt\ \sigma$, which here we will call $\rho$.
So $\SN = \wfp\ \rho = \wfp\ (\ctxt\ \sigma)$.
The relation $\vtl$ of the previous sections will now be interpreted 
as the immediate subterm relation.

Recall that in \cite{dggt} we used a relation
$<_{dt}\ =\ <_{cut} \cup <_{sn1}$,
where $<_{cut}$ was chosen by the user, but $<_{sn1}$ was defined
to be the set of those reductions where a strongly normalising immediate
subterm is reduced \cite[Definition 3]{dggt}.
Then we apply Theorem~\ref{thm-allsn} by letting $\ll$ be the relation
$<_{dt}^+$, which is well-founded if and only if $<_{dt}$ is so.
We now reproduce Theorem~2 of \cite{dggt} in our current notation.

\begin{condition}\label{rpc-csl}
For all $(t, s) \in \sigma$,
if $\forall s' \vtl^+ s.\ s' \in \SN$ then,
for all $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$.
\end{condition}

\begin{verbatim}
"red_props_dt ?rho ?cuto == ALL t s.  (t, s) : ?rho --> 
  (ALL dts.  (dts, t) : subt --> set (isubts s) <= sn_set ?rho --> 
    dts : sn_set ?rho | (dts, s) : (?cuto Un sn1order ?rho)^+)" : thm
\end{verbatim}

\begin{theorem} \label{thm-csl}
If $\sigma$ satisfies Condition~\ref{rpc-csl},
$\ll$ contains $<_{sn1}$ and $\ll$ is well-founded,
then every term is strongly normalising \cite{dggt}.
\end{theorem}

\begin{proof}
We apply Theorem~\ref{thm-allsn} to this situation. 
Since $\vtl$ is well-founded and 
we assume $\ll$ is well-founded, 
conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn} are satisfied.
It remains only to check that Condition~\ref{conds-defs}\ref{rpc0} holds.
In fact we can show that the stronger 
Condition~\ref{conds-defs}\ref{rpc1} holds.

Consider $(t, s) \in \rho$,
and assume that $\forall s' \vtl s.\ s' \in \SN$. 
As $\rho = \ctxt\ \sigma$ is closed under context, it follows that
any subterm of a strongly normalising term is strongly normalising,
so we can assume that $\forall s' \vtl^+ s.\ s' \in \SN$.
For the case $(t, s) \in \sigma$, Condition~\ref{rpc-csl} then implies
that for $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$, and so
Condition~\ref{conds-defs}\ref{rpc1} holds in this case.

We also need to consider the case $(t, s) \in \rho \setminus \sigma$:
that is, where a proper subterm of $s$ is reduced, using $\sigma$,
to the corresponding proper subterm of $t$.
Consider any subterm $t'$ of $t$.  
We show that either $t' \in \SN$ or $t' <_{sn1} s$,
whence $t' \ll s$.

If $t' = t$, then $t' <_{sn1} s$ by definition of $<_{sn1}$.
If $t'$ is a proper subterm of $t$,
then if there is a corresponding subterm $s'$ of $s$ such that 
either $t' = s'$ or $(t', s') \in \ctxt\ \sigma$,
then $s'$ and $t'$ are in \SN.
Otherwise, there is a proper subterm $s'$ of $s$,
where $s'$ is reduced to $t''$, so $(t'', s') \in \ctxt\ \sigma$,
and $t'$ is a subterm of $t''$.
Then $s'$, $t''$ and $t'$ are all in \SN.
So Condition~\ref{conds-defs}\ref{rpc1} holds for this case also.
\qed \end{proof}

\begin{verbatim}
dt_abs = "red_props_dt ?sigma ?cuto ==>
  red_props_dtaf (reduction ?sigma) isubt 
    ((?cuto Un sn1order ?sigma)^+) (wfp (reduction ?sigma)) ?x" : thm

all_sn3_abs' = "[| red_props_dt ?sigma ?cuto;
  wf (?cuto Un sn1order ?sigma) |] ==> ?dt : sn_set ?sigma" : thm 
\end{verbatim}

\section{Application to Typed Combinators and the $\lambda$-calculus} 
  \label{s-snst}

 Proofs of the strong normalisation of $\beta$-reduction in typed 
 $\lambda$-calculi tend to be complex, relying on several inductions
 as in \cite{gallier-oncr,david-nr}.
 although there are also short but specialised proofs, as in \cite{david-nr}.

In \cite{jgl} Goubault-Larrecq concludes that
``Theorem~1 seems to be insufficient to show that every 
simply-typed $\lambda$-term terminates''.
He therefore takes notions like
``reducibility'' and ``the substitution of terms for variables''
from the classical strong normalisation proof
of the simply-typed $\lambda$-calculus \cite{glt}
and generalises them to obtain his Theorem~2 
for termination of higher-order path orderings. 
\comment{
The extra complexity of Goubault-Larrecq's Theorem~2 \cite{jgl}
is for higher-order path orderings, 
and, as he describes, uses notions like
``reducibility'' and ``the substitution of terms for variables''
taken from the classical strong normalisation proof
of the simply-typed $\lambda$-calculus \cite{glt}.
He also says ``Theorem~1 seems to be insufficient to show that every 
simply-typed $\lambda$-term terminates''.
}

As the $\lambda$-calculus can be imitated by using the combinators
$S,K,I$ a related problem is to prove the strong normalisation for
well-typed combinator terms.
This result follows easily from 
the strong normalisation of $\beta$-reduction.
But to prove the converse, that strong normalisation of $\beta$-reduction
follows from that of well-typed combinator terms, is not so easy:
one needs a translation from $\lambda$-terms to combinator terms
that preserves reducibility, such as of Akama \cite{akama-trans}.

We now describe two ways to use our Theorem~\ref{thm-allsn}
to prove strong normalisation of well-typed combinator terms.
By Theorem~2.2 of Akama \cite{akama-trans}, this is enough to show 
strong normalisation of $\beta$-reduction.
We also show how to adapt Theorem~\ref{thm-allsn}
to prove strong normalisation of the simply-typed $\lambda$-calculus directly.

Thus, the full power of 
\cite[Theorem ~2]{jgl} is not necessary for these tasks. However, we
have been unable to prove termination of typed combinators using our
\cite[Theorem~2]{dggt} as suggested by an anonymous referee.

\subsection{Reduction of Typed Combinator Expressions} \label{s-tc}
Of the usual combinators, the problematic ones are
\emph{S f g x = f x (g x)} and \emph{W f x = f x x},
since their right-hand-sides duplicate $x$.
Thus, in the untyped setting, these do not satisfy strong normalisation:
for example
\\
\begin{center}
\begin{tabular}{c}
$(S I I) (S I I) \longrightarrow^+ (S I I) (S I I)$
\\
$(W I) (W I) \longrightarrow^+ (W I) (W I)$
\\
$W W W \longrightarrow W W W$
\end{tabular}
\end{center}

In the typed setting,
we can use Theorem~\ref{thm-allsn} to prove strong normalisation
for combinators like $S, I,K,B,C,W$,
but we must actually add extra rules to do so.
Note that some rules are only applied to the whole term, whereas
others can also be applied to any subterm.
We use $\alpha, \beta, \gamma, \ldots$ for type variables,
and the notation $<$ on types for the transitive relation given by:
$\alpha < (\alpha \to \beta)$ and $\beta < (\alpha \to \beta)$.
Let $\tyof\ t$ denote the type of $t$,
and let $t <_{ty} s$ mean $\tyof\ t < \tyof\ s$.

We show in detail how to handle only the $S$ combinator, 
but many other combinators like $I,K,B,C,W$ can be dealt with similarly,
and the proof holds for the single system containing all these combinators.
 as indicated by rule (\ref{tc-others}).
We define the relations $\sigma$ and $\rho$ (as inductively defined sets)
by rules, as shown below for the combinator $S$. 
Note that the extra rules (\ref{Sfg}), (\ref{Sf}) and (\ref{S}) are added
only because the proof uses them:
for clearly, if $\rho \supseteq \rho'$,
and $\rho$ terminates, then so does $\rho'$.
These rules are motivated by the relation $\vtlo$ of \cite[\S 5]{jgl}:
% It is easy to extend the proof to the case where there are 
 several of these combinators.
\comment{
(we show types where there is space).

\begin{eqnarray}
\label{Sfgx} S f g x : \gamma >_\sigma f x (g x) : \gamma & & \\
\label{csr} \ctxt\ \sigma \subseteq \rho & & \\
\label{Sfg} S f g : \alpha \to \gamma >_\rho f x (g x) : \gamma & & 
  \quad\mbox{if $x \in \SN$} \\
\label{Sf} S f : (\alpha \to \beta) \to \alpha \to \gamma >_\rho 
  f x (g x) : \gamma & &  \quad\mbox{if $g,x \in \SN$} \\
\label{S} S >_\rho f x (g x) : \gamma & & 
  \quad\mbox{if $f,g,x \in \SN$} 
\end{eqnarray}
}

\begin{eqnarray}
\label{Sfgx} S f g x >_\sigma f x (g x) & & \\
\label{csr} \ctxt\ \sigma \subseteq \rho & & \\
\label{Sfg} S f g >_\rho f x (g x) & & 
  \quad\mbox{if $x \in \SN$} \\
\label{Sf} S f >_\rho 
  f x (g x) & &  \quad\mbox{if $g,x \in \SN$} \\
\label{S} S >_\rho f x (g x) & & 
  \quad\mbox{if $f,g,x \in \SN$}  \\
 \label{tc-others} 
  I x >_\sigma x, \quad & K x y >_\sigma x, & \mbox{ etc.}
\end{eqnarray}
 where $S,f,g,x$ have types
with types
$S : (\alpha \!\to\! \beta \!\to\! \gamma) \!\to\!
  (\alpha \!\to\! \beta) \!\to\! \alpha \!\to\! \gamma$, 
$f : \alpha \!\to\! \beta \!\to\! \gamma$,
$g : \alpha \!\to\! \beta$, $x : \alpha$.

Note that ``\SN'' means with respect to $\rho$:
that is, $\rho$ is being defined, indirectly, in terms of itself.
However the rule (\ref{Sfgx}) preserves the type of a term:
so, when it is applied to a subterm, the whole term remains well-typed. 
The remaining rules change a well-typed term into a well-typed term of
$<$-smaller type.
Further, where a rule for reducing a term $s$ depends on
another term $s'$ being in $SN$, then we have $s' <_{ty} s$.
 Further, the rules for reducing a term $s$ depend on
 other terms $s'$, where $s' <_{ty} s$, being in $SN$,
For example, in rule (\ref{Sf}), we have 
$S f : (\alpha \!\to\! \beta) \!\to\! \alpha \!\to\! \gamma$,
where $g$ and $x$ have
$<$-smaller types, $g : \alpha \!\to\! \beta$ and $x : \gamma$.

That is, for $s : \alpha$, the set
$\{t\:|\ (t, s) \in \rho\}$ depends on 
$\{s' \in \SN \ |\ \tyof\ s' < \alpha\}$, and for given $\beta < \alpha$,
the set $\{s' \in \SN \ |\ s' : \beta\}$ depends on 
$\{(x, s'') \in \rho \ |\ \tyof\ s' \leq \beta\}$.
 Thus we consider $(t, s) \in \rho$ as being defined in terms of
 whether $s' \in \SN$, which depends on whether $(x, s'') \in \rho$,
 for terms $s'$ and $s''$ where $\tyof\ s'' \leq \tyof\ s' < \tyof\ s$  
 (ie $s'' \leq_{ty} s' <_{ty} s$).
This ensures a consistent definition, as for $\vtlo$ in \cite{jgl}.
In effect, whether $(t, s) \in \rho$ and $u \in \SN$ are defined
inductively on the types of $s$ and of $u$.

We say $t <_{sn1} s$ if $(t, s) \in \ctxt\ \sigma$ via a reduction
in an immediate subterm which is itself in $\wfp\, (\ctxt\ \sigma)$:
that is, where $t$ and $s$ differ only in corresponding immediate subterms
$t'$ and $s'$ with $(t', s') \in (\ctxt\ \sigma)$
and $s' \in \wfp\ (\ctxt\ \sigma)$.  

\begin{lemma} \label{tc-c1}
Let $\ll\ =\ <_{ty} \cup <_{sn1}$,
and let $\vtl$ be the immediate subterm relation.
Then Condition~\ref{conds-defs}\ref{rpc} holds.
\end{lemma}

\begin{proof}
Let $(t, s) \in \rho$ and assume that $\forall s' \vtl s.\ s' \in \SN$. 
If $(t, s) \in \rho$ via rule (\ref{Sfg}) (where $s = S f g$), 
we have $g \in \SN$, so $(t, S f) \in \rho$ by rule (\ref{Sf}).
As $S f \vtl s$, we have $S f \in \SN$, 
so $t \in \SN \subseteq \gbars \vtl \{u\:|\ u \ll s\}\ \SN$.
Similar arguments hold where $(t, s) \in \sigma \subseteq \rho$ 
via rules (\ref{Sfgx}) and (\ref{csr}), 
and where $(t, s) \in \rho$ via rule (\ref{Sf}).
 $(t, s) \in \rho$ by rule (\ref{Sf}).
 Similar arguments hold for 
 $(t, s) \in \sigma$ by rule (\ref{Sfgx}) and (\ref{Sf}).
 $(t, s) \in \rho$ by rule (\ref{Sf}).

If $(t, s) \in \rho$ via rule (\ref{S}), then 
we see that the subterms $f,g$ and $x$ of $t$ are in \SN, 
while the subterms $f x : \beta \to \gamma$, $g x : \beta$ and
$t = f x (g x) : \gamma$ are of $<$-smaller type than $S$.
Thus any $\vtl$-descending chain from $t$ consists of terms in 
$\{u\:|\ u \ll s\}$ until reaching a term in \SN.
That is, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$.

Finally, in the case where 
$(t, s) \in \rho \setminus \sigma$ by rules (\ref{Sfgx}) and (\ref{csr}),
 Here, there are corresponding terms $t' \vtl t$ and $s' \vtl s$
we have $t' \vtl t$ and $s' \vtl s$
such that $(t', s') \in \ctxt\ \sigma$.
Since $s' \in \SN \subseteq \wfp\, (\ctxt\ \sigma)$, 
we have $t <_{sn1} s$ and $t \ll s$.
Now consider any $t'' \vtl t$.
Either $t'' = t'$ and $(t', s') \in \ctxt\ \sigma$ as just discussed, 
in which case $s' \in \SN$ and so $t' \in \SN$,
or $t''$ is an immediate subterm of $s$ 
not affected by the reduction from $s$ to $t$,
whence $t'' \in \SN$.

Therefore $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$.
\qed \end{proof}

\begin{theorem} \label{tc-sn}
Every term is strongly normalising.
\end{theorem}

\begin{proof}
We use Theorem~\ref{thm-allsn}.
Apart from Lemma~\ref{tc-c1}, we need conditions 
\ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn}.
Condition~\ref{vbs} holds as $\vtl$ is well-founded.
Finally, to show condition~\ref{ubg}, we show that $\ll$ is well-founded.
Clearly the ``smaller type'' relation $<$ is well-founded, 
and it is easy to show that $<_{sn1}$ is well-founded.
Then, clearly, $<_{ty} \circ <_{sn1}\ \subseteq\ <_{ty}$,
and so, by \cite[Lemma~1]{dggt}, $<_{ty} \cup <_{sn1}$ is well-founded.
\qed \end{proof}

Our rules (\ref{Sfg}), (\ref{Sf}) and (\ref{S}) were suggested by
the definition of $\vtlo$ given just below Remark~13 in \cite{jgl}.
As in \cite{jgl}, therefore, there is a resemblance between our proof
and the classic reducibility argument: we have, for example, 
that for $S\ f\ g$ to be in \SN, it is necessary that for all 
$x \in \SN$, $S\ f \ g\ x\in \SN$, 
which resembles the condition for reducibility in \cite[\S 6.1]{glt}.
Likewise, reducibility and our \SN\ are both defined by induction on the type.

\isabelle{
\subsection{Formulating the Proof in Isabelle} \label{s-c-isa}

We now describe some intricate details of our formalisation of
combinators and typed $\lambda$-calculi which is aimed at readers
familiar with theorem proving in higher-order logics. Readers without
the necessary background should skip this section.

A certain part of the formalisation is common to the 
typed combinator work and the work on the $\lambda$-calculus.
The set of types is formulated as a datatype \verb|ctype|,
and the set \verb|wty| is declared but not defined.
Note that \verb|(t, ty) : wty| means that \verb|t| is well-typed,
of type \verb|ty|.

\begin{verbatim}
datatype ctype = "->" ctype ctype (infixr 10)
               | OTy nat

wty :: "('tc * ctype) set" 
\end{verbatim}

The formulation of the simultaneous definitions of $\rho$ and of $\SN$ 
caused considerable difficulty. 
For Isabelle allows several ways of making definitions which are sure to 
be sound, but none caters directly for our situation.
For example, we cannot define $\rho$ and $\SN$ simultaneously as 
inductively defined sets because, 
although the definition of $\rho$ in terms of \SN\ is monotonic, 
that of \SN\ in terms of $\rho$ is not -- indeed, when there are more
instances of $\rho$, fewer objects are in \SN.

So we defined functions \verb|redstd| and \verb|redstud|.
For those reductions whose definition depends on some term $s'$ of smaller
type being in \SN, such as (\ref{Sfg}), (\ref{Sf}) and (\ref{S}),
we define \verb|redstd sn ty| to be the set of instances $(t, s)$ 
where $s$ is of type \verb|ty| and where 
\verb|sn| is ``taken to be'' the set of \SN\ objects.
That is, if \verb|sn| were \SN, then \verb|redstd sn ty| would be
the set of instances of rules (\ref{Sfg}) to (\ref{S}).
Separately we define \verb|runul| to be the other reductions such as 
those given by rules (\ref{Sfgx}) and (\ref{csr}).
We then define \verb|redstud sn ty| to be the union of \verb|runul|
with those instances of \verb|redstd sn ty'| where \verb|ty'| $<$ \verb|ty|.

Now we are interested in 
\verb|redstd| \SN\ \verb|ty| and \verb|redstud| \SN\ \verb|ty|,
but we cannot yet define \SN.
But we would get the same answer, respectively, by using
\verb|redstd sn ty| and \verb|redstud sn ty|
for any \verb|sn| which agrees with \SN\ on terms of 
$<$-smaller type than \verb|ty|.
Also, since any reduction either preserves the type of a term or
produces a term of $<$-smaller type, we would also have
\verb|wfp (redstud sn ty)| = \verb|wfp (redstud| \SN\ \verb|ty)|.  

So we now progressively define approximations to \SN.
We define \verb|snu ty| (resp.\ \verb|snl ty|), 
intended to be the set of strongly normalising terms whose type is
$\leq$ \verb|ty| (resp.\ $<$ \verb|ty|).
However the actual definition involves 
\verb|snu ty| being defined as
\verb|snl ty| together with the set of terms of type \verb|ty| which are in 
\verb|wfp (redstud (snl ty) ty|.
We then define \verb|sn_d| and \verb|redd| to be, respectively, the unions
of \verb|snu ty| and \verb|redstud (snl ty) ty| over all types \verb|ty|.

\begin{verbatim}
redstd, redstud :: "('tc * ctype) set => ctype => 'tc relation"
redst1, runul, redd :: "'tc relation" 
snu, snl :: "ctype => ('tc * ctype) set"
\end{verbatim}

We then obtain the following theorems.
\begin{verbatim}
rd1c = "redstd (snl ty) ty = redstd sn_d ty" : thm
rdu1c = "redstud (snl ty) ty = redstud sn_d ty" : thm
wfp_redd_iff' = "(t, ty) : wty ==> 
  (t : wfp redd) = (t : wfp (redstud (snl ty) ty))" : thm
sn_d_wfp = "((t, ty) : sn_d) = (t : wfp redd & (t, ty) : wty)" : thm 
\end{verbatim}

As all the development described above is relevant to both proofs for 
the typed combinators and both proofs for the simply-typed $\lambda$-calculus,
it is done in the context of an axiomatic type class,
depending on the following axioms.
Then, in the four differently defined reduction systems
(in \S\ref{s-tc}, \S\ref{s-tc2}, (\S\ref{s-lc} and \S\ref{s-lc2}) 
we need only show that each one satisfies the axioms for the type class,
and then the theorems for the type class become available.

\begin{verbatim}
runul_tys "(t, s) : runul ==> (EX ty. (s, ty) : wty & (t, ty) : wty)"
redstd_tys "(t, s) : redstd sn ty ==> (s, ty) : wty &
  (EX tyt. (tyt, ty) : subty & (t, tyt) : wty)"
redstd_mono "sn1 <= sn2 ==> redstd sn1 ty <= redstd sn2 ty"
rd1 "redstd sn ty = redstd (sn Int {(t, ty1). (ty1, ty) : psubty}) ty"
wty_unique "(s, ty) : wty ==> (s, ty') : wty ==> ty = ty'"
\end{verbatim}

We now discuss the formalisation of the typed combinator language: see
Figure~\ref{fig:comb}.

At first we tried using the general framework described in \S~\ref{s-appl-rewr},
but that required checks on the typing and reduction rules that 
each combinator had the correct number of arguments,
which was an unnecessary complication.
So we defined the datatypes \verb|comb|, for the set of combinators,
and \verb|tc|, for the set of combinator terms, as shown.
This meant that we also had to define \verb|ctxt|, \verb|isubt|, etc, 
all over again.
However most of the relevant lemmas were much easier to prove for 
this datatype than for the datatype \verb|rtree| of \S~\ref{s-appl-rewr}
because the latter contains lists of arbitrary length.
The set \verb|wty| is also defined inductively: recall that
$(t, ty) \in \texttt{wty}$ means that $t$ is well-typed and of type \verb|wty|.

\begin{verbatim}
datatype comb = I | S | K | B | C | W
datatype tc = Comb comb ctype | App tc tc | Atom nat ctype

inductive "wty"
    AppI "(f, a -> b) : wty ==> (x, a) : wty ==> (App f x, b) : wty"
    wty_Comb "(Comb comb ty, ty) : wty"
    wty_Atom "(Atom n ty, ty) : wty"
\end{verbatim}

We then define the reduction rules and related functions.
In the Isabelle formalisation, 
\verb|sn1c| is $<_{sn1}$, 
\verb|tyless| is $<_{ty}$, 
\verb|ltlt| is $\ll$ and 
\verb|redd| is $\rho$. 
More of the Isabelle code is given in Figure~{fig:comb}.
Requiring that terms be appropriately typed is a complication 
which is glossed over in the written proof.
For example, we use \verb|runul| to mean $\ctxt\ \sigma$, 
but only in the case of a well-typed term.


We then need to prove that all the axioms for the type class, 
given above, hold.
Then we prove the main result.  

\begin{figure}[h] % Figure~{fig:comb}
  \centering
% rr, ltlt :: "tc relation"
% sn1c :: "tc relation => tc relation" 
\begin{verbatim}
inductive "rr"
  (* S : (a -> b -> c) -> (a -> b) -> a -> c *)
  (* SI: S f g x --> f x (g x) *)
  SI "(App (App f x) (App g x), 
  App (App (App (Comb S ((a -> b -> c) -> (a -> b) -> a -> c)) f) g) x) : rr"
  
inductive "redstd sn ty"
  (* SfgI : S f g --> f x (g x) *)
  SfgI "(f, a -> b -> c) : wty ==> (g, a -> b) : wty ==>
    (x, a) : wty Int sn ==> (a -> c) = ty ==> 
    (App (App f x) (App g x),
    App (App (Comb S ((a -> b -> c) -> (a -> b) -> ty)) f) g) : redstd sn ty"

  (* SfI : S f --> f x (g x) *)
  SfI "(f, a -> b -> c) : wty ==> (g, a -> b) : wty Int sn ==>
    (x, a) : wty Int sn ==> ((a -> b) -> a -> c) = ty ==> 
    (App (App f x) (App g x),
      App (Comb S ((a -> b -> c) -> ty)) f) : redstd sn ty"

  (* SI : S --> f x (g x) *)
  SI "(f, a -> b -> c) : wty Int sn ==> (g, a -> b) : wty Int sn ==>
    (x, a) : wty Int sn ==> 
    ((a -> b -> c) -> (a -> b) -> a -> c) = ty ==> 
    (App (App f x) (App g x), Comb S ty) : redstd sn ty"

inductive "runul"
  I "(s, ty) : wty ==> (t, s) : ctxt rr ==> (t, s) : runul"

inductive "sn1c r"
  funI "(t, s) : fwf (ctxt r) ==> (App t a, App s a) : sn1c r"
  argI "(t, s) : fwf (ctxt r) ==> (App f t, App f s) : sn1c r"

inductive "ltlt"
  tylessI "(t, tyt) : wty ==> (s, tys) : wty ==> 
    (tyt, tys) : psubty ==> (t, s) : ltlt" 
  sn1I "(t, s) : sn1c rr ==> (t, s) : ltlt"
\end{verbatim}
  \caption{First Proof for Typed Combinators}
  \label{fig:comb}
\end{figure}

\begin{verbatim}
wf_sn1c = "wf (sn1c ?r)" : thm
wf_ltlt = "wf ltlt" : thm
tc_gbsn = "red_props_gbscf redd isubt ltlt (wfp redd) ?dt" : thm
wfp_redd = "?dt : wfp redd" : thm 
\end{verbatim}

}

\subsection{A Second Proof for Typed Combinator Expressions} \label{s-tc2}
We now present another way of using Theorem~\ref{thm-allsn}
to prove the same result.
This proof was suggested 
by a presentation of the classic reducibility argument
given us by an unnamed referee.
It is of independent interest since,
unlike the proof in \S\ref{s-tc}, it uses a relation $\vtl$ which
is distinct from the usual immediate subterm relation.
We define $\vtl$ and the reduction relation $\rho$.
Again, it is understood that terms are well-typed.
Combinators other than $S$ could be included also.
 
\begin{eqnarray}
\label{onearg} N_i & \vtl & M N_1 \ldots N_i \ldots N_n 
\quad \mbox{ for } 1 \leq i \leq n \\
 N \vtl M & \Rightarrow & N A \vtl M A \\
\label{aa} M & >_\rho & M N \quad\mbox{if $N \in \SN$} \\
 \label{Sfgx2} S f g x >_\sigma f x (g x) & & \\
 \label{csr2} \ctxt\ \sigma \subseteq \rho & & \\
\label{Sfgxy} S f g x y_1 \ldots y_n & >_\sigma & f x (g x) y_1 \ldots y_n \\
\label{inarg} (x'_i, x_i) \in \ctxt\ \sigma & \Rightarrow &
  f x_1 \ldots x_i \ldots x_n >_\rho f x_1 \ldots x'_i \ldots x_n
\end{eqnarray}

Note that rules (\ref{Sfgxy}) and (\ref{inarg}) together 
are equivalent to rules (\ref{Sfgx2}) and (\ref{csr2}).
These definitions are sound as before, 
since again, a reduction preserves type or gives a result of
$<$-smaller type, and reduction from $s$ is defined involving
\SN\ terms of $<$-smaller type.
Note that, by rule (\ref{aa}), if $M,N \in SN$ then $M N \in \SN$.

For this proof we define 
  $f x_1 \ldots x_i \ldots x_n >_{sn1} f x_1 \ldots x'_i \ldots x_n$
  where $(x'_i, x_i) \in \ctxt\ \sigma$  (similar to rule (\ref{inarg}))
  and $x_i \in \wfp\, (\ctxt\ \sigma)$.
That is, as before,
$t <_{sn1} s$ if $(t, s) \in \ctxt\ \sigma$ by means of reduction
in a ``$\vtl$-subterm'' which is itself in $\wfp\, (\ctxt\ \sigma)$.
  
Also as before, let $\ll\ =\ <_{ty} \cup <_{sn1}$.

\begin{theorem} \label{tc2-sn}
Every term is strongly normalising.
\end{theorem}

\begin{proof}
We first show that Condition~\ref{conds-defs}\ref{rpc} holds.
Let $(t, s) \in \rho$ and assume that 
$\forall u \ll s$.\ $u \in \gindy\ \vtl \SN$, and 
$\forall v \vtl s$.\ $v \in \SN$. 
If $(t, s) \in \rho$ via rule (\ref{Sfgxy}),
we have $f,g,x$ and each $y_i \in \SN$,
so the combination $f x (g x) y_1 \ldots y_n \in \SN$.

If $(t, s) = (M N, M) \in \rho$ via rule (\ref{aa}), then 
$t <_{ty} s$, so $t \ll s$, and,
for $K \vtl M N$, either $K = N$ which is in \SN,
or $K \vtl M$ and so $K \in \SN$.

Finally, where $(t, s) \in \rho$ via rule (\ref{inarg}),
the argument is similar to that before:
$t <_{sn1} s$, and for $y \vtl t$, there is $x \vtl s$ such that
$y \leq_\rho x$, so $y \in \SN$.

That is, in each case, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$,
so Condition~\ref{conds-defs}\ref{rpc} holds.

From Condition~\ref{conds-defs}\ref{rpc}, we prove that
every term is in \SN\ as in Theorem~\ref{tc-sn}.
\qed \end{proof}

\isabelle{

\begin{figure}[t] % Figure~\ref{fig:comb1}
  \centering
\begin{verbatim}
onearg :: "tc relation"
fctxt, inarg, ctxt :: "tc relation => tc relation"

inductive "onearg"
    isI "(b, App a b) : onearg"
    xI "(b, e) : onearg ==> (b, App e a) : onearg"

inductive "fctxt r"
    inI "(t, s) : r ==> (t, s) : fctxt r"
    funI "(t, s) : fctxt r ==> (App t a, App s a) : fctxt r"

inductive "inarg r"
    argI "(t, s) : r ==> (App f t, App f s) : inarg r"

inductive "redstd sn ty"
    (* argI: M --> M N *)
    argI "(N, a) : wty Int sn ==> (M, a -> b) : wty ==>
      (a -> b) = ty ==> (App M N, M) : redstd sn ty"

inductive "runul"
  fI "(s, ty) : wty ==> (t, s) : fctxt rr ==> (t, s) : runul"
  fiI "(s, ty) : wty ==> (t, s) : fctxt (inarg (ctxt rr)) ==> (t, s) : runul"

inductive "runul'"
  I "(s, ty) : wty ==> (t, s) : ctxt rr ==> (t, s) : runul'"

runul'_eq = "runul' == runul" : thm

inductive "sn1a r"
  I "(t, s) : fctxt (inarg (fwf (ctxt r))) ==> (t, s) : sn1a r"
\end{verbatim}
  \caption{An Alternative Proof for Typed Combinators}
  \label{fig:comb1}
\end{figure}

The Isabelle code differs from the first proof as shown in
Figure~\ref{fig:comb1}.
Also, \verb|ltlt| uses \verb|sn1a| in place of \verb|sn1c|. 
We use \verb|onearg| for $\vtl$.
We have, where $(t, s) \in \tau$, 
$(t y_1 \ldots y_n, t y_1 \ldots y_n) \in \texttt{fctxt} \tau$,
and $(f\ t, f\ s) \in \texttt{inarg} \tau$.
Thus the two clauses for \verb|runul| correspond to the two rules
(\ref{Sfgxy}) and (\ref{inarg}).
The relation \verb|runul'| is defined as \verb|runul| was before.
The purpose of this is to check that \verb|runul| really is the same
as before, as shown by the theorem \verb|runul'_eq|.

We then get theorems similar to before:
\begin{verbatim}
wf_sn1a = "wf (sn1a ?r)" : thm
val wf_ltlt = "wf ltlt" : thm 
val tc_gbsn = "red_props_gbscf redd onearg ltlt (wfp redd) ?dt" : thm
val wfp_redd = "?dt : wfp redd" : thm 
\end{verbatim}
}

\subsection{Strong Normalisation of the Simply-typed $\lambda$-calculus}
  \label{s-lc}

We now give a proof of the 
strong normalisation of the simply-typed $\lambda$-calculus.
We are not able to present this simply as a corollary of 
Theorem~\ref{thm-allsn}, but we need to adapt its proof.
This also is an interesting application since it uses
for $\vtl$ a relation which is neither the immediate nor the proper
subterm relation.

In our formal treatment we use de Bruijn indices for the variables.
Unlike in some other strong normalisation proofs
 we do not need a way of taking an arbitrary term containing free variables
 and substituting correctly typed terms for some of these free variables,
 as might be expressed by $M [\overline x := \overline A]$.
 We do of course have the $\beta$-reduction rule
 $(\lambda x.\, M)N \longrightarrow M [x := N]$.
 In this case the substitution of $N$ is for the (un)bound variable 
 with index 0 in $M$
 (and correspondingly higher index inside abstractions in $M$).
 The rule (\ref{def-vtlo}) for $\vtlo$ below 
 can be expressed similarly using de Bruijn indices.
 
we consider only closed terms, although of course $\beta$- and $\eta$-reduction
can occur in subterms with free variables.
Since $\lambda$-calculus terms usually may contain free variables, 
where we might say, for example, that $xy$ is strongly normalising, 
we achieve a similar effect by allowing constants, or ``atoms'',
whose types are specified.

\isabelle{
Thus our language is expressed by the Isabelle/HOL datatype
in which a $\lambda$-term is an abstraction 
\texttt{Lam} specifying the type \texttt{ctype} of the 
bound variable, an application \texttt{App},
a variable \texttt{Var} known by its de Bruijn index
of type \verb|nat| (natural number),
or an atom \texttt{Atom} of type \texttt{ctype}.

\begin{verbatim} 
datatype lcnt = Lam ctype lcnt | App lcnt lcnt
              | Atom nat ctype | Var nat 
\end{verbatim} 


\begin{figure}[t]
  \centering
\begin{verbatim}
wtyc :: "(lct * ctype list * ctype) set"

inductive "wtyc"
    AppI "(f, bvts, a -> b) : wtyc ==> (x, bvts, a) : wtyc ==>
      (App f x, bvts, b) : wtyc"
    LamI "rty = (aty -> bty) ==> (b, aty # bvts, bty) : wtyc ==>
      (Lam aty b, bvts, rty) : wtyc"
    VarI "n < length bvts ==> nth bvts n = ty ==>
      (Var n, bvts, ty) : wtyc"
    AtomI "ty1 = ty2 ==> (Atom n ty1, bvts, ty2) : wtyc"

inductive "wty"
    I "(x, [], a) : wtyc ==> (x, a) : wty"

inductive "fvs"
    AppI1 "(f, fvf) : fvs ==> (App f x, fvf) : fvs"
    AppI2 "(x, fvf) : fvs ==> (App f x, fvf) : fvs"
    LamI "(b, Suc m) : fvs ==> (Lam aty b, m) : fvs"
    VarI "n = m ==> (Var n, m) : fvs"

recdef subst "measure ((f,n,t). size f)"
  subst_App "subst (App f x, n, t) =
    App (subst (f, n, t)) (subst (x, n, t))"
  (* substitution only where same type *)
  subst_Var "subst (Var n, m, t) =
    (if m = n then t else Var n)"
  subst_Lam "subst (Lam ty b, m, t) =
    Lam ty (subst (b, Suc m, inc_bvs (t, 0)))"
  subst_Atom "subst (Atom n ty, m, t) = Atom n ty"

inductive "beta"
    I "dec_bvs (subst (b, 0, inc_bvs (x, 0)), 0) = M' ==>
      (M', App (Lam a b) x) : beta"

inductive "eta"
    I "(M, 0) ~: fvs ==> dec_bvs (M, 0) = M' ==>
      (M', Lam a (App M (Var 0))) : eta" 

"inc_bvs (App ?f ?x, ?n) = App (inc_bvs (?f, ?n)) (inc_bvs (?x, ?n))"
"inc_bvs (Var ?n, ?m) = (if ?m <= ?n then Var (Suc ?n) else Var ?n)"
"inc_bvs (Lam ?ty ?b, ?m) = Lam ?ty (inc_bvs (?b, Suc ?m))"
"inc_bvs (Atom ?n ?ty, ?m) = Atom ?n ?ty"
\end{verbatim}
  \caption{Isabelle/HOL Encoding for Typed $\lambda$-Calculi}
  \label{fig:lambda}
\end{figure}

The notion of a well-typed term is now relative to the type
of the free variables, so we have \verb|wtyc| as shown in 
Figure~\ref{fig:lambda}
We define \verb|fvs| to indicate whether a variable is free in a term.
We define substitution, needed to define $\beta$-reduction.
This is done as an Isabelle recursive definition with a 
measure function supplied.
The measure function reflects the fact that in recursive calls to 
\verb|subst|, the first argument gets smaller.
The functions \verb|inc_bvs| and \verb|dec_bvs| increment and decrement
the numbers of bound variables, as required when using deBruijn indices.
Precisely, \texttt{inc\_bvs (t, n)} and \texttt{dec\_bvs (t, n)}
increment and decrement numbers of bound variables greater than \verb|n|.
}

Some notation: 
if $\overline N$ is $ N_1, \ldots, N_n $,
then $M \overline N$ means $M N_1 \ldots N_n $,
and if $\overline x$ is $ x_1, \ldots, x_n $,
then $\lambda \overline x.\, M$
means $\lambda x_1 \ldots x_n.\, M$.

For the reduction rules, we have (naturally),
$\beta$-reduction and $\eta$-reduction,
together referred to as $\beta\eta$-reduction,
which can occur anywhere within a term.
We also write $\beta\eta$ for $\beta \cup \eta$.
But we also use an extra rule (\ref{def-vtlo}), defining $\vtlo$,
which is added to make the proof work.
This trick is due to Goubault-Larrecq \cite{jgl}.

\begin{eqnarray}
\label{def-beta} (\lambda x.\, M)N & >_\beta & M [x := N] \\
\label{def-eta} \lambda x.\, M x & >_\eta & M \quad \mbox{ if
 $x$ is not free in } M \\
\label{def-vtlo} (\lambda x.\, M) & \vtro & 
  M [x := A] \quad \mbox{ if $A$ closed, and in \SN}
\end{eqnarray}

It is understood that all terms referred to are well-typed.
Then the reduction relation $\rho$ is given by: 
$(t, s) \in \rho$ iff $s$ is closed
and $(t, s) \in \ctxt\ \beta\eta\ \cup \vtlo$. 
Although $\rho$ and \SN\ are defined in terms of each other, 
 this is again a circular, and so potentially unsound, definition.
these definitions are sound, as in \S\ref{s-tc},
since a reduction preserves type or gives a result of
$<$-smaller type, and reduction from $s$ is defined involving
\SN\ terms of $<$-smaller type.
\comment{
However, we may note that of these rules, if $(t, s) \in \beta \eta$
then $t$ is of the same type as $s$.
Thus the same is true for $(t, s) \in \ctxt\ \beta \eta$.
On the other hand, if $t \vtlo s$, and $s : \alpha \to \beta$,
then $t : \beta$.
Thus the question of whether $u \in \SN$ depends only on the set
$\{(t, s) : (t, s) \in \rho \land s \leq_{ty} u\}$.
In the rule (\ref{def-vtlo}) for $\vtlo$, $A <_{ty} \lambda x.\, M$, 
so the definition of whether $(t, s) \in \rho$ depends on 
whether $A \in \SN$ where $A <_{ty} s$.
Thus we have definitions of whether $(t, s) \in \rho$ and $u \in \SN$,
inductively on the types of $s$ and of $u$.
}

 Theorem~\ref{thm-allsn} and the theorems of \cite{jgl}
 use a relation $\vtl$ to generalise the notion of subterm.
 Again we use a relation $\vtl$ which is neither the
 immediate subterm relation nor the proper subterm relation,
 but is defined by the following:
Again we use a relation $\vtl$ which is not the usual
immediate subterm relation:
 $M \vtl MN$, $N \vtl M N$, and 
 $N \vtl M \Rightarrow \lambda x.\, N \vtl \lambda x.\, M$.
\[ M \vtl MN \qquad \qquad N \vtl M N \qquad \qquad 
N \vtl M \Rightarrow \lambda x.\, N \vtl \lambda x.\, M
\]
\comment{
\begin{eqnarray}
M \vtl MN & & N \vtl M N \\
N \vtl M & \Rightarrow & \lambda x.\, N \vtl \lambda x.\, M 
\end{eqnarray}
}
Informally, if $s = \lambda \overline{x}.\, MN$, 
then, since any expression of $s$ in this form is unique, we have 
$t \vtl s$ iff $t = \lambda \overline{x}.\, M$
or $t = \lambda \overline{x}.\, N$.
Clearly $\vtl$ is well-founded.

We also need to define a relation $\ll$.
First we let $M' N <_{sn1} M N$ when $M$ 
$\beta\eta$-reduces to $M'$, where
 (ie, $(t, s) \in \ctxt\ \beta\eta$)
 because some proper subterm $s'$ of $s$ $\beta\eta$-reduces 
 to a corresponding proper subterm $t'$ of $t$, with
$M$ itself is strongly normalising w.r.t. $\beta\eta$-reduction:
that is, where
$(M', M) \in \ctxt\ \beta\eta$ and $M \in \wfp\ (\ctxt\ \beta\eta)$.
Likewise $M N' <_{sn1} M N$ if 
$(N', N) \in \ctxt\ \beta\eta$ and $N \in \wfp\ (\ctxt\ \beta\eta)$.
Then let $\ll\ =\ <_{ty} \cup <_{sn1}$.
\comment{
\begin{eqnarray}
t <_{ty} s & \Rightarrow & t \ll s \quad 
  \mbox{ (for $t, s$ closed and well-typed) } \\
t <_{sn1} s & \Rightarrow & t \ll s
\end{eqnarray}
}

By the same argument used in proving Theorem~\ref{tc-sn},
$\ll$ is well-founded.
\comment{
Now (repeating an argument used extensively in \cite{dggt}),
we show that $\ll$ is well-founded.
As in \cite{dggt}, we have that $<_{sn1}$ is well-founded.
Obviously $<_{ty}$ is well-founded,
and $<_{ty} \circ <_{sn1} \ \subseteq\ <_{ty}$.
Therefore, by a well-known result (see \cite{dvk}, or \cite[Lemma~1]{dggt})
$<_{ty} \cup <_{sn1}$ is well-founded.
Thus $\ll$ is well-founded.
}

\begin{verbatim}
inductive "wtri"
    AppI1 "(f, App f x) : wtri"
    AppI2 "(x, App f x) : wtri"
    LamI "(M', M) : wtri ==> (Lam aty M', Lam aty M) : wtri"

inductive "redstd sn ty"
    I "(N, a) : wty ==> (N, a) : sn ==> (M, [a], b) : wtyc ==>
      (a -> b) = ty ==> (M', App (Lam a M) N) : beta ==>
      (M', (Lam a M)) : redstd sn ty"

inductive "runul"
    I "(s, ty) : wty 
       ==> (t, s) : ctxt (beta Un eta) ==> (t, s) : runul"
\end{verbatim}

Our target result corresponds to Lemma~\ref{dth}, but
although its proof is very similar we cannot actually appeal to that lemma.
However we first need some simple preliminary lemmas, 
for some of which we omit the easy proofs.

\begin{lemma} \label{abs-sn-nf}
If $M$ is closed (so $y$ not free in $M$)
and $M \in \SN$, then $\lambda y.\, M \in \SN$.
 and $\lambda \overline{y}.\, M \in \SN$.
\end{lemma}

\begin{verbatim}
abs_wfp = "[| ?t : wfp redd; (?t, 0) ~: fvs |] ==>
    Lam ?ty ?t : wfp redd" : thm 
\end{verbatim}

\begin{proof}
First note that $y$ cannot be free in $M$ since $M$ is closed.
Let $s = \lambda y.\, M$.
As $M \in \SN$, we prove the result by well-founded induction on $M$:
that is, for $N$ such that $(N, M) \in \rho$,
we assume $\lambda y.\, N \in \SN$.

Now consider the possibilities for $(t, s) \in \rho$.
Firstly, let $t = M [y := A] \vtlo \lambda y.\, M = s$.
As $y$ is not free in $M$, so $t = M \in \SN$.
We cannot have $(t, s) \in \eta$ since this would require
 $s = \lambda y.\, Ny$, and $y$ is free in $Ny$.
$M = Ny$, and $y$ is free in $Ny$.
The remaining possibilities are reductions of $M$,
where $t = \lambda y.\, N$, $s = \lambda y.\, M$ 
and $(N, M) \in \ctxt\ \beta \eta$.
In this case our inductive hypothesis gives $t \in \SN$.
Thus, in all cases, $t \in \SN$, so $s \in \SN$.
 
Finally, repeated use of this result gives $\lambda \overline{y}.\, M
\in \SN$.  
\qed
\end{proof} 

\begin{lemma} \label{wtri-subst}
Let $N' \vtl N = M [x := A]$.
Then either there exists $M' \vtl M$ such that $N' = M' [x := A]$ or
$M$ is of the form $\lambda \overline{y}.\, x$, with $x \not \in \overline{y}$.
\end{lemma} 

\begin{verbatim}
wtri_subst2 =
   "[| (?K', ?M') : wtri; ?t : wfp redd; (?t, [], ?tty) : wtyc;
         ?M' = subst (?M, ?n, ?t) |]
      ==> (EX K. (K, ?M) : wtri & ?K' = subst (K, ?n, ?t)) |
      ?M' : wfp redd & (ALL m. (?M', m) ~: fvs)" : thm
\end{verbatim}

\begin{proof}
To obtain $N'$ from $N$, 
we go inside abstractions until we reach the outermost application,
where we then select either the function or the argument.
There are two cases here. 
If this application is within $A$, then $M = \lambda \overline{y}.\,x$
with $x \not \in \overline{y}$, and $N' = \lambda \overline{y}.\, A'$
for some $A' \vtl A$.

Otherwise, the application is in $M$.
Since $M = \lambda \overline{y}.\, M_1 M_2$,
let $N = M [x := A] $\\$ = \lambda \overline{y}.\, N_1 N_2$.
Then, for $i = 1$ or 2, $N' = \lambda \overline{y}.\, N_i$, with  
$M' = \lambda \overline{y}.\, M_i$.
\qed \end{proof}


We now state some lemmas showing how certain reductions can be reordered.

\begin{lemma} \label{reords}
\begin{enumerate}
\item \label{sub-red}
If $(M', M) \in (\ctxt\ \beta\eta)^*$,
then $(M' [x := A], M [x := A]) \in (\ctxt\ \beta\eta)^*$.
Thus $(\ctxt\ \beta\eta \setminus \beta\eta)^* \circ \vtlo\ \subseteq\
  \vtlo \circ\ (\ctxt\ \beta\eta)^*$.
\item \label{pp-eta}
If $(M', M) \in (\ctxt\ \beta\eta)^*$, then 
$(\lambda x.\, M' x, \lambda x.\, M x) \in 
  (\ctxt\ \beta\eta \setminus \beta\eta)^*$,
and $(M', \lambda x.\, M x) \in 
  (\ctxt\ \beta\eta \setminus \beta\eta)^* \circ \eta$.
Thus $\eta \circ (\ctxt\ \beta\eta)^* 
  \subseteq (\ctxt\ \beta\eta \setminus \beta\eta)^* \circ \eta$.
\item \label{eta-vtlo}
$\eta\ \circ \vtlo \ \subseteq\ (\ctxt\ \beta)\ \circ \vtlo$, and also
$\eta\ \circ \vtlo \ \subseteq\ \vtlo \circ\ \beta$.
\end{enumerate} 
\end{lemma} 

\begin{verbatim}
redd_commn = "[| (?N, ?Mr) : redstd ?sn ?ty;
  (?Mr, ?M) : nureddb (beta Un eta); (?M, [], ?mty) : wtyc |] ==>
  EX Ms. (Ms, ?M) : redstd ?sn ?ty & (?N, Ms) : ctxt (beta Un eta)" : thm

nu_eta' = "(?M', Lam ?ty ?b1) : (ctxt (beta Un eta))^* ==> 
  (?M', Lam ?ty ?b1) : (nureddb (beta Un eta))^* O eta^=" : thm 

eta_trio = "[| (?t, ?s) : eta O redstd ?sn ?ty;
  (?s, [], ?sty) : wtyc |] ==> 
  (?t, ?s) : redstd ?sn ?ty O beta" : thm

\end{verbatim}

\comment{
\begin{proof}
Let $(N, M) \in \eta$, and $K \vtlo N$.
So say $M = \lambda x.\, N x$ (with $x$ not free in $N$), and 
$N$ must be of the form $\lambda y.\, N'$, with $K = N' [y := A]$.
(Use $\alpha$-conversion to ensure $y \not = x$).
Then $M = \lambda x.\, (\lambda y.\, N') x$,
so $(\lambda x.\, N' [y := x], M) \in \ctxt\ \beta$ and 
$N' [y := A] = N' [y := x] [x := A] \vtlo \lambda x.\, N' [y := x]$.
Also $(\lambda y.\, N') A = ((\lambda y.\, N') x) [x := A] \vtlo M$ and 
$(N' [y := A], (\lambda y.\, N') A) \in \beta$.
\qed \end{proof}
}

We use the lemmas above to derive the following lemma.
We note that it is analogous to the Lemma in \cite[\S 6.3.2]{glt},
which applies to reducible terms.

\begin{lemma} \label{abs-sn}
A term $\lambda x.\, M$ is in \SN\ if, 
for all $N \in \SN$, $M [x := N] \in \SN$.
\end{lemma}

\comment{
\begin{proof} (abbreviated version) \footnote{what do you think}
Let $a$ be an atom of the same type as $x$.
Then $M [x := a] \in \SN\ \subseteq \wfp\ (\ctxt\ \beta\eta)$,
so $M \in \wfp\ (\ctxt\ \beta\eta)$.
So an infinite chain of reductions from $\lambda x.\, M$
cannot consist entirely of successive reductions of $M$, 
but must eventually reach an instance of $\vtlo$
(possible after an instance of $\eta$, which complicates the detailed proof).
Then, using Lemma~\ref{reords}, the chain of reductions can be 
re-ordered so that the use of $\vtlo$ comes first,
and the result follows.
\qed \end{proof}
}

\begin{verbatim}
abs_sn'' =
   "ALL M' ty. (M', Lam ?vty ?M) : redstd sn_d ty --> M' : wfp redd
      ==> Lam ?vty ?M : wfp redd" : thm 
\end{verbatim}

\begin{proof} 
Consider possible reductions of $\lambda x.\, M$.
There are three cases:
\begin{enumerate}
\item $(\lambda x.\, M', \lambda x.\, M) \in \rho$
  where $(M', M) \in \ctxt\ \beta\eta$
\item $(M, \lambda x.\, M x) \in \eta$
\item $M [x := A] \vtlo \lambda x.\, M$.
\end{enumerate}

Let $a$ be an atom of the same type as $x$.
Clearly $a \in \SN$, so, by our precondition,
$M [x := a] \in \SN\ \subseteq \wfp\ (\ctxt\ \beta\eta)$. 
Then it is easy to see that $M \in \wfp\ (\ctxt\ \beta\eta)$.
Suppose there is an infinite chain of reductions starting from $\lambda x.\, M$.
Then, as $M \in \wfp\ (\ctxt\ \beta\eta)$, the chain
cannot consist entirely of successive reductions of $M$, 
 the body of the abstraction,
but must eventually reach an instance of $\vtlo$ or $\eta$.

Suppose the chain first reaches an instance of $\vtlo$.
Then the chain contains both
$(\lambda x.\, M', \lambda x.\, M) \in 
  (\ctxt\ \beta\eta \setminus \beta\eta)^*$
and $M' [x := A] \vtlo \lambda x.\, M'$.
Then $M [x := A] \vtlo \lambda x.\, M$, and since
$(M', M) \in (\ctxt\ \beta\eta)^*$, Lemma~\ref{reords}\ref{sub-red} gives
$(M' [x := A], M [x := A]) \in (\ctxt\ \beta\eta)^*$.
Since $M [x := A] \in \SN$, we have $M' [x := A] \in \SN$.
This contradicts $M' [x := A]$ being in an infinite chain of reductions.

Suppose the chain reaches an instance of $\eta$ before
an instance of $\vtlo$.
By Lemma~\ref{reords}\ref{pp-eta}, the instance of $\eta$ can be postponed 
beyond further instances of $\ctxt\ \beta\eta$,
which become instances of $\ctxt\ \beta\eta \setminus \beta\eta$. 
So as there is no infinite chain of $\ctxt\ \beta\eta \setminus \beta\eta$,
the chain must reach an instance of $\vtlo$.
Then the chain contains both
$(\lambda x.\, M' x, \lambda x.\, M) \in 
  (\ctxt\ \beta\eta \setminus \beta\eta)^*$
and $(N, \lambda x.\, M' x) \in \eta\ \circ \vtlo$.
By Lemma~\ref{reords}\ref{eta-vtlo},
$(N, \lambda x.\, M' x) \in\ \vtlo \circ\ \beta$, and 
we can deal with this as above.
\qed \end{proof}

\comment{
We summarise the reorderings of reductions described in the proof above.
\footnote{could omit this part if we need the space}
Unlabelled arrows denote the relation $(\ctxt\ \beta\eta)^*$:
$$
\begin{array}{ccccc}
\lambda x. M &\to& \lambda x. M' &\vtro& M' [x := A] \\
\lambda x. M &\vtro& {M [x := A]} &\to& {M' [x := A]} 
\end{array}
$$
$$
\begin{array}{ccccccccccccc}
\lambda x. M &\to& \lambda x. M' &=& 
\lambda x. N x &\to_\eta& N &\to& N' &&&& \\
\lambda x. M &\to& \lambda x. M' &=& 
\lambda x. N x &\to& 
\lambda x. N' x &\to_\eta& N' &=& \lambda y. K &\vtro& K [x := A] \\
\lambda x. M & \multicolumn{5}{c}{\to} & 
\lambda x. N' x &\vtro& N' A &=& (\lambda y. K) A &\to_\beta& K [x := A] 
\end{array}
$$
}

\begin{lemma} \label{dth-lc}
 Suppose $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, 
Every term $s \in \gindy \ll (\gindy \vtl \SN)$.
\end{lemma}

\begin{verbatim}
lc_gindy = "?s : gindy ltlt (gindy wtri (wfp redd))" : thm 
\end{verbatim}

\begin{proof} 
Given $s$, assume that 
 $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0} and that

(a) all terms $u$ such that ${u} \ll {s}$ are in $\gindy \vtl \SN$.

\noindent We need to show $s \in \gindy \vtl \SN$, so we assume that 

(b) all terms $v$ such that ${v} \vtl {s}$ are in $\SN$

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

To show that $s \in \SN$, we show that every term $t$ that can
be obtained from $s$ by a single reduction is in \SN: that is,
$\forall t.\, (t, s) \in \rho \Rightarrow t \in \SN$.

So we must look at cases.
Note that, in all cases, $s$ is closed and well-typed.
\begin{enumerate}

\item[$(i)$] $(t, s) \in \beta$: let $s = (\lambda x.\, M)N$.
Then assumption~(b) gives $\lambda x.\, M \in \SN$ and $N \in \SN$.
As $t \vtlo \lambda x.\, M$ we have $t \in \SN$.

\item[$(ii)$] $(t, s) \in ctxt\ \beta\eta \setminus \beta\eta$,
where $s$ is an application:
let $s = MN$.
So $t$ is either $M'N$ or $MN'$ where $(M', M)$ and $(N', N)$ are in
$ctxt\ \beta\eta$.
Then $M,N \in \SN$ by assumption (b) and so $M', N' \in \SN$.
Thus $s \gg t$ and so $t \in \gindy \vtl \SN$ by assumption (a).
To show from this that $t \in \SN$, we need to show that 
$\forall w \vtl t.\ w \in \SN$.
But this is so as $M,N, M', N' \in \SN$.

\item[$(iii)$] $t \vtlo s$: 
let $s = \lambda x.\, M$ and $t = M [x := A]$, where 
$A$ is well-typed and closed, $A \in \SN$,
$x : \alpha$, $A : \alpha$ and $M : \beta$.
Thus $t : \beta <_{ty} s : \alpha \to \beta$, whence $t \ll s$,
and so $t \in \gindy \vtl \SN$ by assumption (a).
Again, to show $t \in \SN$, unless we can do this directly,
it is enough to show that $\forall w \vtl t.\ w \in \SN$.
Suppose $w \vtl t = M [x := A]$.
Lemma~\ref{wtri-subst} gives two cases.
Firstly, we can have $M = \lambda \overline{y}.\, x$,
where $x \not \in \overline{y}$, and $t = \lambda \overline{y}.\, A$.
Then, as $A$ is closed and in \SN\ we have $t \in SN$ by 
repeated use of Lemma~\ref{abs-sn-nf}.
The second case is that 
we have $M' \vtl M$ such that $w = M' [x := A]$.
Thus $\lambda x.\, M' \vtl \lambda x.\, M = s$, so $\lambda x.\, M' \in \SN$.
As $w = M' [x := A] \vtlo \lambda x.\, M'$, 
we have $w \in \SN$, as required.
 it follows that $w \in \SN$.
 As this holds for each $w \vtl t$, and $t \in \gindy \vtl \SN$
 we have $t \in \SN$.

\item[$(iv)$] $(t, s) \in \rho$, where $s$ is an abstraction
(this includes and uses the previous case,
and is the case where we cannot use Lemma~\ref{dth}):
let $s = \lambda x.\, M$.
As shown above, $M [x := A] \in \SN$ for any $A \in \SN$, 
so, by Lemma~\ref{abs-sn}, $s \in \SN$.
\qed \end{enumerate}
\end{proof}

 It follows that every term is in \SN.

\begin{theorem} \label{thm-allsn-lc}
$\rho$ is well-founded.
\end{theorem}

\begin{verbatim}
lc_wfp_redd = "?c : wfp redd" : thm 
\end{verbatim}

\begin{proof}
By Lemma~\ref{dth-lc} every term is in $\gindy \ll (\gindy \vtl \SN)$.
As $\ll$ and $\vtl$ are well-founded, 
we use Lemma~\ref{l2}\ref{gindy-bars} twice to get that every term is in \SN.
 As $\ll$ is well-founded, 
 by Lemma~\ref{l2}\ref{gindy-bars}, every term is in $\gindy \vtl \SN$.
 Then, as $\vtl$ is well-founded, 
 again by Lemma~\ref{l2}\ref{gindy-bars}, every term is in \SN: ie,
 $\rho$ is well-founded.
\qed \end{proof}

\subsection{A Second Proof for the simply-typed $\lambda$-calculus} 
\label{s-lc2}
We now present an alternative proof inspired by the second proof 
for typed combinator terms given in \S\ref{s-tc2}.

\begin{eqnarray}
\label{lc-onearg} N_i & \vtl & M N_1 \ldots N_i \ldots N_n \\
\label{lc-abs} \lambda x_1 \ldots x_k.\, M_i & \vtl & 
  (\lambda x_1 \ldots x_k.\, M_1 M_2) \overline N \qquad 
    (k \geq 1, i=1,2) \\
\label{lc-aa} M &  >_\rho &  M N \quad\mbox{ if $N$ closed and in \SN} \\
\label{lc-beta} (\lambda x.\, M)N \overline A & >_\sigma & 
  M [x := N] \overline A \\
\label{lc-eta} (\lambda x.\, M x) \overline A & >_\sigma & 
  M \overline A \quad \mbox{ if $x$ not free in } M \\
\label{lc-inhead} (M', M) \in \ctxt\ \sigma & \Rightarrow &
  (\lambda x.\, M) \overline A >_\rho  
  (\lambda x.\, M') \overline A \\
\label{lc-inarg} (x'_i, x_i) \in \ctxt\ \sigma & \Rightarrow &
  f x_1 \ldots x_i \ldots x_n >_\rho f x_1 \ldots x'_i \ldots x_n \\
\label{lc-csr} \sigma & \subseteq & \rho 
\end{eqnarray}

Note that rules (\ref{lc-beta}) to (\ref{lc-csr}) 
give $\ctxt\ \beta\eta = \ctxt\ \sigma \subseteq \rho$.
The mutually recursive definitions of $\rho$ and \SN\ are sound as before.
Also define $<_{sn1}$ and $\ll$ as in \S\ref{s-tc2}.
 Note that, by rule (\ref{aa}), if $M,N \in SN$ then $M N \in \SN$.

\isabelle{
The Isabelle proof in this case turned out to be considerably more difficult.
This was because of the way in which the rules involve lists of arguments,
such as $\overline A$.
Consequently, a number of extra lemmas had to be proved and used at the
relevant points.
For example, \verb|wty_foldl| gives the condition for $M \overline A$ to be 
well-typed, where $(\overline y, \overline x) \in \texttt{allrel}\ \tau$
if each pair of corresponding members $(y_i, x_i)$ is in $\tau$.
As another example, the result \verb|gindy_foldl_App_lem|, shown later,
had to be proved as a consequence of the corresponding result for a single
argument, and there were many similar instances.

The relation $\vtl$ is \verb|wtrib|, whose definition uses the \verb|wtri|
of \S\ref{s-lc}.
As before, $\ll$ is \verb|ltlt|, defined as in \S\ref{s-tc2}.
We defined \verb|runul| as in \S\ref{s-lc},
but we proved and used \verb|ctxt_alt|, 
which gives an alternative characterisation of \verb|ctxt|,
which better reflects the form of the rules.  
It uses \verb|Lam_rel|:
if $(M', M) \in \tau$, then 
$(\lambda x.\ M', \lambda x.\ M) \in \texttt{Lam\_rel}\ \tau$.

\begin{verbatim}
wty_foldl = 
 "((foldl App ?M ?As, ?ty) : wty) = 
  (EX astys. (?As, astys) : allrel wty 
             & (?M, foldr op -> astys ?ty) : wty)" : thm

inductive "redstd sn ty"
 argI "(N, a) : wty Int sn 
        ==> (M, a -> b) : wty 
        ==> (a -> b) = ty 
        ==> (App M N, M) : redstd sn ty"

inductive "wtrib"
 isI "(b, App a b) : wtrib"
 xI  "(b, e) : wtrib ==> (b, App e a) : wtrib"
 fI  "(M', M) : wtri ==> (Lam aty M', Lam aty M) : wtrib"

ctxt_alt = "ctxt ?r =
 fctxt ?r Un fctxt (Lam_rel (ctxt ?r)) Un fctxt (inarg (ctxt ?r))" 
 : thm

\end{verbatim}

}

\begin{lemma} \label{abs-sn2}
\begin{enumerate}
\item \label{iff-app} A term $M$ is in \SN\ iff
  $\forall N \in \SN.\ M N \in \SN$.
\item \label{iff-beta} For $N \in \SN$, 
the term $(\lambda x.\, M) N$ is in \SN\ iff $M [x := N] \in \SN$.
\item \label{iff-sub} A term $\lambda x.\, M$ is in \SN\ iff 
  $\forall N \in \SN.\ M [x := N] \in \SN$.
\end{enumerate}
\end{lemma}

\begin{proof} 
Part \ref{iff-app} follows easily from rule (\ref{lc-aa})
and the fact that $\rho$ 
contains the closure under contexts of the remaining rules.

The proof of \ref{iff-beta} is similar to the proof of Lemma~\ref{abs-sn}.
As $M$ and $N$ are in \SN, 
an infinite chain of reductions must eventually meet an instance of 
$\beta$-reduction,
and the chain of reductions can be re-ordered 
so that the $\beta$-reduction comes first.
The details, including the 
case of an $\eta$-reduction of $(\lambda x.\, M)$,
are omitted.

Part \ref{iff-sub} follows from \ref{iff-app} and \ref{iff-beta}.
\qed \end{proof} 

\begin{verbatim}
App_sn_eq = 
 "(?M, ?a -> ?b) : wty ==> (?M : wfp redd) =
  (ALL N. N : wfp redd --> (N, ?a) : wty --> App ?M N : wfp redd)" 
 : thm 

sn_if_beta_eq_s =
   "[| (?K, App ?M ?N) : beta; (App ?M ?N, ?ty) : wty |] ==>
   (App ?M ?N : wfp redd) = (?K : wfp redd & ?N : wfp runul)"
\end{verbatim}

Lemma~\ref{abs-sn2} shows another similarity of
this proof to the classic reducibility argument:
\ref{iff-app} is analogous to 
condition 3 for reducibility in \cite[\S 6.1]{glt},
and \ref{iff-sub} is analogous to 
the Lemma in \cite[\S 6.3.2]{glt}.

\begin{lemma} \label{avsn}
For atom $a$ and variable $x \in \overline x$,
both $\lambda \overline x.\, a$ and 
$\lambda \overline x.\, x$ are in \SN.
\end{lemma} 

\begin{verbatim}
Lam_Atom_sn = "foldr Lam ?vtys (Atom ?n ?ty) : wfp redd" : thm
Lam_Var_sn = "foldr Lam ?vtys (Var ?n) : wfp redd" : thm
\end{verbatim}

\begin{proof} 
The only possible reductions are to apply the term to a closed
strongly normalising argument, to reduce such an argument,
or to $\beta$-reduce the given term with such an argument,
which, noting that Lemma~\ref{abs-sn-nf} holds also in this system,
gives a strongly normalising result. 
\qed \end{proof} 

\begin{lemma} \label{appsn}
For $\overline x = x_1, \ldots, x_k$ ($k \geq 1$),
$\lambda \overline x.\, M_1 M_2 \in \gindy\ \vtl \SN$.
\end{lemma} 

\begin{verbatim}
Lam_App_sn =
 "foldr Lam (?vty # ?vtys) (App ?N1.0 ?N2.0) : gindy wtrib (wfp redd)"
 : thm 
\end{verbatim}

\begin{proof} 
Assume $\lambda \overline x.\, M_i \in \SN$ for $i = 1,2$.  
By Lemma~\ref{abs-sn2} it is enough to show that if the
arguments $\overline N = N_1, \ldots, N_k$ are in \SN,
then $(M_1 M_2) [\overline x := \overline N]$ is in \SN.
But this follows as, for each $i=1,2$,
$\lambda \overline x.\, M_i \in \SN$, and so
$M_i [\overline x := \overline N] \in \SN$.
\qed \end{proof} 

\begin{lemma} \label{gindy-head}
If $M \in \gindy\ \vtl \SN$, 
then $M \overline N \in \gindy\ \vtl \SN$.  
\end{lemma} 

\begin{verbatim}
gindy_foldl_App_lem = "?f : gindy wtrib (wfp redd) ==>
  foldl App ?f ?As : gindy wtrib (wfp redd)" : thm 
\end{verbatim}

\begin{proof}
Follows from Lemma~\ref{abs-sn2}\ref{iff-app} since
$K \vtl M \overline N$ iff $K$ is in $\overline N$ or $K \vtl M$.
\qed \end{proof} 

\begin{lemma} \label{dth-lc2}
 Suppose $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, 
Every term $s \in \gindy \ll (\gindy \vtl \SN)$.
\end{lemma}

\begin{verbatim}
lc_gindy = "?s : gindy ltlt (gindy wtrib (wfp redd))" : thm 
\end{verbatim}

\begin{proof} 
Assume $\forall u \ll s.\ u \in \gindy \vtl \SN$, and 
$\forall v \vtl s.\ v \in \SN$. 
Let $(t, s) \in \rho$.

If $(t, s) = (M N, M) \in \rho$ via rule (\ref{lc-aa}), then 
$t <_{ty} s$, and, for $K \vtl M N$, either $K = N$ which is in \SN,
or $K \vtl M$ and so $K \in \SN$.

If $(t, s) \in \rho$ via rule (\ref{lc-inarg}),
the argument is similar to that before:
$t <_{sn1} s$, and for $y \vtl t$, there is $x \vtl s$ such that
$y \leq_\rho x$, so $y \in \SN$.

Finally, for $s$ of the form $(\lambda \overline x.\, M) \overline N$,
where $M$ is not an abstraction and $\overline x$ is not null,
Lemmas~\ref{gindy-head}, \ref{avsn} and \ref{appsn}
show that $s \in \gindy\ \vtl \SN$.
\comment{
by Lemma~\ref{abs-sn2}, we need only show that
$M [\overline x := \overline y] \in \SN$
(where, if $n < k$, $y_{n+1}, \ldots, y_k$ are additional \SN\ arguments).
Here, if $M = M_1 M_2$, then we have 
each $\lambda \overline x.\, M_i \vtl s$ and so is in \SN,
so each $M_i [\overline x := \overline y] \in \SN$, and 
$M [\overline x := \overline y] =
M_1 [\overline x := \overline y] M_2 [\overline x := \overline y] \in \SN$.
On the other hand, if $M$ is a variable $z$,
then $M [\overline x := \overline y]$
is either $z$ or some $y_i$, and is in \SN.
}

Since we have, for $(t, s) \in \rho$,
 Therefore for $(t, s) \in \rho$ we have 
either $t \in \SN$ or $s \in \SN$, therefore $s \in \SN$.  as required.
\qed \end{proof}

It follows, by a proof as for Theorem~\ref{thm-allsn-lc},
that every term is in \SN.

\begin{theorem} \label{thm-allsn-lc2}
$\rho$ is well-founded.
\end{theorem}

\comment{
\begin{theorem} \label{thm-allsn-lc2}
$\rho$ is well-founded (using a proof as for Theorem~\ref{thm-allsn-lc}).
\end{theorem}
}

We discuss the differences between the proofs in \S\ref{s-tc} to \S\ref{s-lc2}.
The proof in \S\ref{s-lc} includes in the reduction rules the relation $\vtlo$, 
as in \cite{jgl}.
The proof in \S\ref{s-tc} includes the extra reduction rules 
(\ref{Sfg}), (\ref{Sf}) and (\ref{S}), which are analogous, 
since they consist of adding strongly normalising arguments and 
then reducing.

By contrast, the proofs in \S\ref{s-tc2} and \S\ref{s-lc2}
include the extra rule, (\ref{aa}) and (\ref{lc-aa}) respectively,
which consists of simply adding a strongly normalising argument.
But this requires a different choice for the relation $\vtl$ because
allowing both $M \vtl M N$ and $M >_\rho M N$ 
prevents use of our proof method: 
we would want to show $M \in \SN$ by showing (\emph{inter alia})
that $MN \in \SN$, which, since $M \vtl MN$,
we would want to do using the inductive assumption that 
(\emph{inter alia}) $M \in \SN$. 

\notcsl{
\section{Miscellaneous Applications of our Theorem}

We now consider various applications of our theorem to prove the
termination of particular rewriting systems.

\isabelle{
\subsection{Union of Well-founded Relations}

In many places in our work we had to prove that the union of two
relations is well-founded. We now give a lemma that helps in this
task. 

The following lemma is reproduced from \cite{dggt}.
\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}. 

Before becoming aware of \cite{dvk}, we had proved \ref{tco} and
\ref{otc} in Isabelle.  The proof of these is intuitively quite
simple.  Imagine an infinite descending $(\tau \cup \sigma)$-chain.
As $\tau$ and $\sigma$ are each well-founded, the chain must contain
an infinite number of instances of each of $\tau$ and $\sigma$.  Then,
for \ref{otc}, any instance of $\sigma$ can be brought to the front of
the chain so that it is in front of the first instance of $\tau$.
Repeating this would give an infinite $\sigma$-chain, which is a
contradiction, since $\sigma$ is well-founded.  This argument also
proves Lemma~\ref{util}\ref{wfp-otc} below.

For \ref{tco}, each successive instance of $\sigma$ 
either (i) can be brought to the front or (ii) disappears. 
Since there is no infinite $\sigma$-chain, 
there must be a point after which only (ii) applies,
and this gives an infinite $\tau$-chain, which is also a contradiction.

Translating these arguments into Isabelle proofs was not easy.
We used the following characterisations of well-foundedness and of the
well-founded part:
\begin{verbatim}
wf_eq_minimal = "wf ?r = 
  (ALL Q x. x : Q --> (EX z:Q. ALL y. (y, z) : ?r --> y ~: Q))"
 : thm
wf_eq_minimal' = "wf ?r = (ALL Q x.  x : Q --> 
    (EX z:Q. (z, x) : ?r^* & (ALL y. (y, z) : ?r --> y ~: Q)))"

snwfp_min = "(?x : wfp ?r) =
  (ALL Q. ?x : Q --> (EX z:Q. ALL y. (y, z) : ?r --> y ~: Q))" 
 : thm
\end{verbatim}

For \ref{otc}, we actually have the stronger result that if \ref{otc}
holds and $\tau$ is well-founded, then $\wfp\ (\tau \cup \sigma) =
\wfp\ (\sigma)$.

\begin{proof}

We will frequently use the Isabelle notation for relational image:
$x \in \tau \Img Q$ means $\exists q.\ q \in Q \land (q, x) \in \tau$.

Let $x \in \wfp\ (\sigma)$. Using the characterisation
\texttt{snwfp\_min} of \wfp, we need to show that for any given $Q$
such that $x \in Q$, there is a $z \in Q$ which is $(\tau \cup
\sigma)$-minimal in $Q$.

Using $x \in \wfp\ (\sigma)$ and $x \in \tau^* \Img Q$, % lev 9
we get $z \in \tau^* \Img Q$ which is $\sigma$-minimal in $\tau^* \Img Q$.
Since $z \in \tau^* \Img Q$, there is some  $(xa, z) \in \tau^*$ and $xa \in
Q$.% lev 14 

As $xa \in Q$ and $\tau$ is well-founded, 
\verb|wf_eq_minimal'| gives us some $za \in Q$
which is $\tau$-minimal in $Q$
and such that $(za, xa) \in \tau^*$. % lev 19

Next we show that $za$ is $\sigma$-minimal in $Q$.
For if not, suppose $y \in Q$ and $(y, za) \in \sigma$.
Then $(y, z) \in \tau^* \circ \sigma$. % lev 24
It is easy to see that condition~\ref{otc} implies $\tau^* \circ
\sigma \ \subseteq\ \sigma \circ \tau^*$, and so we have $(y, z) \in
\sigma \circ \tau^*$, giving us a $ya$ such that
$(y, ya) \in \tau^*$ and $(ya, z) \in \sigma$. % lev 27
But $y \in Q$, and so d  u$ya \in \tau^* \Img Q$, which contradicts 
$z$ being $\sigma$-minimal in $\tau^* \Img Q$.
Therefore $za$ is $\sigma$-minimal in $Q$.

We now have that $za$ is $\sigma$-minimal in $Q$ and 
$za$ is $\tau$-minimal in $Q$, so 
$za$ is $(\tau \cup \sigma)$-minimal in $Q$.
\qed \end{proof}

For \ref{tco}, there is no similar stronger result.
The proof is a little more difficult, and uses the definition
$\rsmin\ \sigma\ S = \{x \in S.\ \forall y.\ (y, x) \in \sigma 
  \Rightarrow y \not\in S\}$:
\begin{verbatim}
"rsmin ?r ?S == {x. x : ?S & (ALL y. (y, x) : ?r --> y ~: ?S)}"
\end{verbatim}

\begin{proof}
Given $x \in Q$, we have $x \in \tau^* \Img Q$.
Again, we need to show that there exists $z \in Q$ which is
$(\sigma \cup \tau)$-minimal in $Q$.
Now $\sigma^+$ is well-founded as $\sigma$ is, 
so there exists $z \in \tau^* \Img Q$,
which is $\sigma^+$-minimal in $\tau^* \Img Q$.
That is, $z \in \rsmin\ \sigma^+ (\tau^* \Img Q)$. % lev 12
As $\tau$ is well-founded, there exists 
$za$ that is $\tau$-minimal in $\rsmin\ \sigma^+ (\tau^* \Img Q)$. % lev 19

We now consider cases, according to whether
$\forall y.\ (y, za) \in \tau \Rightarrow y \not\in (\tau^* \Img Q)$.
If so, that is, $za$ is $\tau$-minimal in $\tau^* \Img Q$,
then clearly $za \in Q$. % lev 26
Then, as $za$ is $\tau$-minimal in $\tau^* \Img Q$, 
$za$ is $\tau$-minimal in $Q$. 
Likewise, as $za \in \rsmin\ \sigma^+ (\tau^* \Img Q)$, 
that is, $za$ is $\sigma^+$-minimal in $\tau^* \Img Q$, and $za \in Q$, 
so $za$ is $\sigma^+$-minimal, and hence       $\sigma$-minimal, in $Q$. % lev 27

Now suppose the contrary, that there exists $y$ such that
$(y, za) \in \tau$ and $y \in \tau^* \Img Q$.
As $y \in \tau^* \Img Q$ and $\sigma$ is well-founded, 
by \verb|wf_eq_minimal'| there exists
$zb \in \tau^* \Img Q$ such that $(zb, y) \in \sigma^*$ and 
$zb$ is $\sigma^+$-minimal in $\tau^* \Img Q$.
That is, $zb \in \rsmin\ \sigma^+ (\tau^* \Img Q)$.
It is easy to see that condition~\ref{tco} implies 
$\tau \circ \sigma^* \ \subseteq\ \sigma^* \circ \tau$,
and $(zb, za) \in \tau \circ \sigma^*$. % lev 38
Thus $(zb, za) \in \sigma^* \circ \tau$,
giving some $ya$ such that
$(zb, ya) \in \tau$ and $(ya, za) \in \sigma^*$.

Then, as $zb \in \tau^* \Img Q$, so $ya \in \tau^* \Img Q$.
There are two cases here: if $(ya, za) \in \sigma^+$ then 
this contradicts $za$ being $\sigma^+$-minimal in $\tau^* \Img Q$. % lev 46 
But if $ya = za$ then 
$(zb, za) \in \tau$, which contradicts $za$ being $\tau$-minimal
in $\rsmin\ \sigma^+ (\tau^* \Img Q)$.
\qed \end{proof}
}

\subsection{Constricting Derivations} \label{s-cd}

For a rewrite system on a first-order language
(where the reduction relation is closed under context),
a ``constricting derivation'' has been defined as 
an infinite reduction sequence
where each reduction occurs at a subterm $t$ whose
proper subterms are all strongly normalising \cite{dersh-td}.

For a rewrite relation $\rho = \ctxt\ \sigma$, 
we define a \emph{constricting reduction} by:
$(t, s) \in \constrict\ \sigma$ iff
$(t, s) \in \sigma$ and the proper subterms of $t$ are in $\wfp\ \rho$.
As before, $\vtl$ is the immediate subterm relation, and
$<_{sn1}$ is defined as in \S\ref{s-appl-rewr}.

The following results are easily proved by methods similar to those 
of \cite{dvk}.

\begin{lemma} \label{util}
For all binary relations $\sigma$ and $\tau$:
\begin{enumerate}
\item \label{o-rev} $\sigma \circ \tau$ is well-founded if and only if 
  $\tau \circ \sigma$ is well-founded
\item \label{o-u} if $\tau$ is well-founded then
  $\wfp\ (\tau^* \circ \sigma) = \wfp\ (\sigma \cup \tau)$
\item \label{wfp-otc} if $\tau$ is well-founded and
  $\tau \circ \sigma \subseteq \sigma \circ \tau^*$, then 
  $\wfp\ (\sigma \cup \tau) = \wfp\ \sigma$.
\end{enumerate}
\end{lemma}

\begin{verbatim}
wf_rev_comp_eq = "wf (?r O ?s) = wf (?s O ?r)" : thm 
wf_comp_Unl' = "wf ?r ==> wfp (?r^* O ?s) = wfp (?r Un ?s)" : thm
wfUn_movl' = "[| ?s O ?r <= ?r O ?s^*; wf ?s |] ==>
  wfp (?r Un ?s) = wfp ?r" : thm 
\end{verbatim}

The following theorem encapsulates mostly known results, for example 
Lemma~1 of Hirokawa \& Middledorp \cite{hm-dpr} resembles:
``if (\ref{snocos}) then (\ref{rhowf})'',
\footnote{\cite[Lemma~1]{hm-dpr} starts from a minimal non-terminating
term, refers to $<_\epsilon$ rather than $<_{sn1}$ and assumes a TRS, 
with substitutable rewrite rules.  The notation $<_\epsilon$ 
refers to a rewrite of a proper subterm.}
and Proposition~1 of Borralleras, Ferreira \& Rubio \cite{bfr} is:
``if (\ref{rhowf}) then (\ref{rhous})''.  

\begin{theorem} \label{thm-ctalt}
The following are equivalent, where $\rho = \ctxt\ \sigma$: 
\begin{eqnarray}
\label{cosusn}
 (\constrict\ \sigma\ \circ \vtl^*)\ \cup <_{sn1} && \mbox{ is well-founded} \\
\label{cososn}
 \constrict\ \sigma\ \circ \vtl^* \circ <_{sn1}^* && \mbox{ is well-founded} \\
\label{sosnoc}
 \vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma && \mbox{ is well-founded} \\
\label{snocos}
  <_{sn1}^* \circ\ \constrict\ \sigma\ \circ \vtl^* && \mbox{ is well-founded} \\
 \label{rhoos} \rho\ \circ \vtl^* && \mbox{ is well-founded} \\
\label{rhous} \rho\ \cup \vtl && \mbox{ is well-founded} \\
\label{rhowf} \rho && \mbox{ is well-founded}  \\
 \label{rhotc} \rho^+ && \mbox{ is well-founded} \\
 \label{rhotcs} \rho^+ \cup \vtl && \mbox{ is well-founded} 
\end{eqnarray}
\end{theorem}

\begin{proof}
(\ref{sosnoc}) $\Rightarrow$ (\ref{rhowf}): 
If $t_0$ is not in $\SN = \wfp\ \rho$, then let $t_0'$ be a minimal
subterm of $t_0$ which is not in \SN ---
so the proper subterms of $t_0'$ are in \SN.
Consider any infinite sequence of reductions from $t_0'$ --- 
these cannot all be reductions of proper subterms as the latter are in \SN, 
so find $t_0''$ and $t_1$ in this infinite sequence such that
$(t_0'', t_0') \in (\ctxt\ \sigma \setminus \sigma)^*$ and
$(t_1, t_0'') \in \sigma$.
Now all proper subterms of $t_0'$, of $t_0''$ and of all terms between them
in the reduction sequence are in \SN.
So $(t_1, t_0) \in\ \vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma$,
and as $t_1 \not\in \SN$, a 
($\vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma$)-sequence can be continued.
Similar proofs are in the literature, eg, \cite[Theorem~6]{dps00},
\cite[Lemma~1]{hm-dpr}.

\begin{description}
\item[\rm (\ref{cososn}) $\Leftrightarrow$ 
(\ref{sosnoc}) $\Leftrightarrow$ (\ref{snocos}):]
these follow from Lemma~\ref{util}\ref{o-rev}.

\item[\rm (\ref{cosusn}) $\Leftrightarrow$ (\ref{snocos}):]
 and (\ref{rhoos}) $\Leftrightarrow$ (\ref{rhous}) :
follows from Lemma~\ref{util}\ref{o-u}, since $<_{sn1}$ is well-founded.

\item[\rm (\ref{rhowf}) $\Rightarrow$ (\ref{rhous}):]
 (and (\ref{rhotc}) $\Rightarrow$ (\ref{rhotcs}) is similar) :
follows from Lemma~\ref{util}\ref{wfp-otc}, as 
  $\vtl \circ \rho \subseteq \rho\ \circ \vtl$
  as $\rho$ is monotonic.

 (\ref{rhous}) $\Rightarrow$ (\ref{rhowf}) : trivial, as 
 $\rho \subseteq \rho\ \cup \vtl$

 (\ref{rhotcs}) $\Rightarrow$ (\ref{snocos}) : similarly trivial, as 
 $<_{sn1}^* \circ\ \constrict\ \sigma \subseteq \rho^+$

 (\ref{rhotc}) $\Leftrightarrow$ (\ref{rhowf}) is a standard result

\item[\rm (\ref{rhous}) $\Rightarrow$ all others:]
since every other relation mentioned is contained in
\mbox{$(\rho\ \cup \vtl)^+$}.
\end{description}

\end{proof}

In fact the proofs above show that $\wfp\ (\rho) = \wfp\ 
 (\vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma)$.

\begin{verbatim}
wfp_subt_O_tcl = 
  "wfp (subt O (sn1order ?rho)^* O constrict ?rho) =
    wfp (reduction ?rho)" : thm
wfp_psubt_redn = "wfp (reduction ?r Un psubt) =
  wfp (reduction ?r)" : thm
\end{verbatim}

We now link Theorem~\ref{thm-ctalt} with Theorem~\ref{thm-csl},
by some simple proofs.
Note that Condition~\ref{rpc-csl} simply says:
if $(t', s) \in \constrict\ \sigma\ \circ \vtl^*$ then 
$t' \in \SN$ or $t' \ll s$.

Let $\tau = (\constrict\ \sigma\ \circ \vtl^*)\ \cup <_{sn1}$.
We show $\SN = \wfp\ \rho \subseteq \wfp\ \tau$.
Since $\tau \subseteq (\rho\ \cup \vtl)^+$, 
so $\wfp\ (\rho\ \cup \vtl) \subseteq \wfp\ \tau$.
By Lemma~\ref{util}\ref{wfp-otc}, 
$\wfp\ \rho = \wfp\ (\rho\ \cup \vtl)$.

Then, we can use Theorem~\ref{thm-csl} to prove 
(\ref{cosusn}) implies (\ref{rhowf}).
Let $\ll\ = \tau$.
Then Condition~\ref{rpc-csl} holds trivially, $\ll\ \supseteq\ <_{sn1}$
and $\ll$ is well-founded, which is just (\ref{cosusn}) of
Theorem~\ref{thm-ctalt}.
Hence, by Theorem~\ref{thm-csl}, $\rho$ is well-founded.

The converse is also easy to prove, giving an alternative proof of
Theorem~\ref{thm-csl}.
Assume (\ref{cosusn}) $\Rightarrow$ (\ref{rhowf});
we will prove Theorem~\ref{thm-csl}.
Suppose the assumptions of Theorem~\ref{thm-csl} hold,
and we want to show its conclusion, (\ref{rhowf}).
We show (\ref{cosusn}), ie, that $\tau$ is well-founded.
\comment{ 
Suppose that the assumptions of Theorem~\ref{thm-csl} hold,
and assume that (\ref{cosusn}) implies (\ref{rhowf}).
Then we need to show that $\tau$ is well-founded.
}
Let $(t, s) \in \tau$.
Then, if $(t, s) \in\ <_{sn1}$, then $t \ll s$.
Otherwise, $(t, s) \in \constrict\ \sigma\ \circ \vtl^*$ 
and so $t \in \SN$ or $t \ll s$ by Condition~\ref{rpc-csl}.


Now $\SN \subseteq \wfp\ \tau$, as shown above,
so $(t, s) \in \tau$ implies $t \in \wfp\ \tau$ or $t \ll s$,
where $\ll$ is well-founded.
Thus any $\tau$-descending chain either terminates or hits a member
of $\wfp\ \tau$: that is, every $s \in \bars\ \tau\ (\wfp\ \tau)$.
So, by Lemma~\ref{l2}\ref{bars-wfp}, every $s \in \wfp\ \tau$, 
as required.

\subsection{Application to the General Path Ordering} \label{s-gpo}
The definition of the general path ordering of Dershowitz \& Hoot
\cite{nat-term} presupposes terms in a first-order language,
but the ordering is not necessarily monotonic.
Therefore we deal with it in the context of an ARS.
As noted by Goubault-Larrecq \cite{jgl},
his Theorem~1 can be used to show that 
the general path ordering is well-founded.
We now show how that ordering fits our conditions 
for termination of an ARS presented earlier.
The following treatment is similar to that of the recursive path orderings
in our \cite[\S3.7]{dggt},
but that applied only to the cases where the derived ordering is monotonic
(ie, closed under context).  

The general path ordering $<_{gpo}$ is defined as below 
where $s = f(s_1, \ldots, s_m)$ and $t = g(t_1, \ldots, t_n)$,
and $\Lambda({<_{gpo}})$ (or $<_{\Lambda}$) is an ordering
derived from $<_{gpo}$, where $\Lambda$ satisfies
conditions given later.
We omit defining $<_{gpo}$-equivalent terms.
$$
\frac {
s_i \geq_{gpo} t } { s >_{gpo} t } (G1)
\qquad
\frac {
s >_\Lambda t \qquad 
\forall i \in \{1, \ldots, n\}.\ s >_{gpo} t_i } { s >_{gpo} t } (G2)
 $$ 

In practice, $<_{\Lambda}$, which is derived from $<_{gpo}$,
depends on $<_{gpo}$ applied only to smaller terms, ie,
determining whether $s >_\Lambda t$ depends on whether 
$s'>_{gpo} x$ only for proper subterms $s'$ of $s$
(and arbitrary terms $x$). 
Thus the above rules can be seen as
mutually recursive definitions of $<_{gpo}$ and $<_{\Lambda}$.

However in the formal Isabelle proof a different approach was taken to
ensure a consistent definition: 
$<_{gpo}$ is an inductively defined set, which means that
$s >_{gpo} t$ if and only if it can be shown so using the rules above.
This approach requires that $<_{\Lambda}$ be a monotonic function of $<_{gpo}$.

\comment{
Nonetheless, our proof also requires condition \ref{lam-psubt} below
which amounts, in practice, to the condition that $s >_\Lambda t$ depends on 
whether $s'>_{gpo} x$ only for proper subterms $s'$ of $s$.
}

As in \cite{dggt}, 
we define a function \fwf\ (``from well-founded'') which maps a
binary relation $\sigma$ to a binary relation $\fwf\ \sigma$ thus:
 \begin{definition}
 Given a relation $\sigma$,
$(t, s) \in \fwf\ \sigma$ iff  if and only if
$(t, s) \in \sigma$ and $s \in \wfp\ \sigma$.
 is strongly normalising (for $\sigma$).
 \end{definition}

We can let $\vtl$ be either the immediate subterm relation
or the proper subterm relation --- in the latter case,
the required condition~\ref{lam-psubt} below is weaker.
We now list the conditions on $\Lambda$ required for the Isabelle proof:
\begin{enumerate}
\item \label{lam-mono} ${\Lambda}$ is a monotonic function 
\item \label{lam-wf} 
  if $\sigma$ is well-founded then ${\Lambda (\sigma)}$ is well-founded
\item \label{lam-psubt}
  if all $s' \vtl s$ are in $\wfp\ \sigma$
   strongly normalising (for $\sigma$),
  and if $(t, s) \in \Lambda (\sigma)$, 
  then $(t, s) \in \Lambda (\fwf\ \sigma)$.
\end{enumerate}

In practice, condition \ref{lam-psubt} means that the dependence of 
$\Lambda (\sigma)$ upon $\sigma$ is only as follows:
whether $(t, s) \in \Lambda (\sigma)$ depends solely upon 
whether $(x, s') \in \sigma$ for $s' \vtl s$, and arbitrary $x$,
although $\Lambda (\sigma)$ can also depend on, for example,
a well-founded ordering on the function symbols $\{f, g, \ldots\}$.

A common example for $\Lambda$ uses a well-founded ordering $<$
on the function symbols and a function $\Lambda'$ which takes as argument
an ordering on objects of type $\alpha$ and returns an ordering on
lists of such objects.
Then, if $g < f$, $(g(\overline t), f(\overline s)) \in \Lambda (\tau)$,
and if $(\overline t, \overline s) \in \Lambda' (\tau)$,
$(f(\overline t), f(\overline s)) \in \Lambda (\tau)$.
In this case,
if $\Lambda'$ is either the lexicographic or multiset ordering,
then conditions \ref{lam-mono} to \ref{lam-psubt} are satisfied,
and in addition if $(s'_i, s_i) \in \sigma$ then
$(f (s_1, \ldots, s'_i, \ldots, s_n), 
f (s_1, \ldots, s_i, \ldots, s_n)) \in {\Lambda (\sigma)}$.
This property, which was used in \cite[\S3.7]{dggt},
ensures that ${\Lambda (\sigma)}$ is closed under context,
but is not needed for this more general treatment.

\isabelle{
\begin{figure}[t]
  \centering
\begin{verbatim}
consts
  gpo, gpo2 :: 
     "('a rtree relation => 'a rtree relation) => 'a rtree relation"

inductive "gpo crel" "gpo2 crel"
  cI     "(Node g ts, s) : crel gpot 
           ==> gpot <= gpo crel 
            ==> ALL t: set ts. (t, s) : gpo crel 
             ==> (Node g ts, s) : gpo2 crel"
  gpo2I  "(t, s) : gpo2 crel ==> (t, s) : gpo crel"
  subtI  "si : set ss ==> (si, Node f ss) : gpo crel"
  esubtI "si : set ss 
          ==> (t, si) : gpo crel 
           ==> (t, Node f ss) : gpo crel"

wf_der_def = "wf_der crel == ALL r. wf r --> wf (crel r)"

wf_gpoc_fwf_def = "wf_gpoc_fwf crel == ALL r dt dt'. 
   (ALL x. (x, dt) : psubt --> x : wfp r) 
    --> (dt', dt) : crel r --> (dt', dt) : crel (fwf r)"

gpoc_props_def = 
 "gpoc_props crel == mono crel & wf_der crel & wf_gpoc_fwf crel"
\end{verbatim}
  \caption{Isabelle/HOL Encoding for the General Path Ordering}
  \label{fig:gpo}
\end{figure}

In the Isabelle formalisation, we define two inductive sets
simultaneously as shown in Figure~\ref{fig:gpo}.
The odd hypothesis \texttt{gpot <= gpo crel} in the introduction rule \verb|cI|
is because, for an inductively defined set, the rules must be monotonic:
that is, the (truth of) the hypotheses of the introduction rules must be
monotonic in the sets being defined.
As yet, we do not know that \verb|crel| is monotonic,
though we do assume it subsequently. 
Therefore we could not use \texttt{(Node g ts, s) : crel (gpo crel)}
as the first hypothesis to the rule \verb|cI|.
Note that \verb|crel|, of type 
\texttt{'a rtree relation => 'a rtree relation},
represents the function $\Lambda$.
Its required properties are given by \verb|gpoc_props|.

}

\begin{lemma} \label{lem-subt-gpo}
If $s >_{gpo} t$ and $t'$ is a subterm of $t$ then $s >_{gpo} t'$.
\end{lemma}

\begin{verbatim}
subt_gpo = "[| (?ti, ?t) : subt; (?t, ?s) : gpo ?crel |] ==>
   (?ti, ?s) : gpo ?crel" : thm 
\end{verbatim}

\begin{proof} 
It is enough to show that 
if $s >_{gpo} t = g(t_1, \ldots, t_n)$ then $s >_{gpo} t_j$ for any
$j \in \{1, \ldots, n\}$.
We show it by induction on the size (or structure) of $s$.
If $s >_{gpo} t$ via rule ($G2$), 
then it is immediate that $s >_{gpo} t_j$.
If $s = f (s_1, \ldots, s_m) >_{gpo} t$ via rule ($G1$), 
then for some $s_i$,
either $s_i >_{gpo} t$ and so $s_i >_{gpo} t_j$ by induction,
or $s_i = t >_{gpo} t_j$ by rule ($G1$), 
and then $s >_{gpo} t_j$ by rule ($G1$).
\qed \end{proof}
 
\begin{theorem}
The general path ordering $<_{gpo}$ is well-founded.
\end{theorem}

\begin{verbatim}
gpocwf = "gpoc_props ?crel ==> ?dt : wfp (gpo ?crel)" : thm 
\end{verbatim}

\begin{proof}
Define $\ll\ = \Lambda (\fwf\, (<_{gpo}))$.
Then, as \fwf ($<_{gpo}$) is well-founded, $\ll$ is well-founded by 
condition \ref{lam-wf} above.
As $\vtl$ is well-founded, 
conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn} are satisfied.

Then, to show Condition~\ref{conds-defs}\ref{rpc1}, suppose 
for all $s' \vtl s$ that  (where $\vtl$ is the proper subterm relation),
\mbox{$s' \in \SN = \wfp\, (<_{gpo})$}, 
$t <_{gpo} s$, and $t'$ is a subterm of $t$.
Then Lemma~\ref{lem-subt-gpo} gives $t' <_{gpo} s$.
If $t' <_{gpo} s$ by rule ($G1$), then 
$s_i \vtl s$ and $t' <_{gpo}^* s_i$, so $s_i$ and $t'$ are in \SN.
If $t' <_{gpo} s$ by rule ($G2$), then $(t', s) \in \Lambda (<_{gpo})$.
By condition \ref{lam-psubt}, $(t', s) \in \Lambda (\fwf\, (<_{gpo})) =\ \ll$.
Thus Condition~\ref{conds-defs}\ref{rpc1} is satisfied,
and so $<_{gpo}$ is well-founded.
\qed \end{proof}

\section{Goubault-Larrecq's Theorem for Higher-order Path Orderings}
\label{jgl-ho}

Theorem~2 of Goubault-Larrecq's work \cite{jgl} extends his Theorem~1
so as to allow for the substitution involved in $\beta$-reduction
in the $\lambda$-calculus 
and also extends the higher-order path ordering of Jouannaud \& Rubio
\cite{jr-horpo}.
It involves three more relations $\btl$, $\vtlo$ and $\Sigma$,
in addition to $\vtl$ and $\ll$ used previously.

We give a concrete example of these relations by 
describing how Goubault-Larrecq's result 
is applied to show the strong normalisation of $\beta$-reduction.
We then show how to obtain his general result using our techniques
(but not actually using our Theorem~\ref{thm-allsn}).

Let $\beta$ be the relation of $\beta$-reduction, 
but only of the whole term, not of a proper subterm.
Then let $\vtl$ be the immediate subterm relation, 
let $\btl\ = \beta\ \cup \vtl$, 
let $\ll$ be $\beta$-reduction in a proper subterm,
and let $\lambda x. M \vtro M [x := N]$ for $N \in \SN$.
Finally $(t, s) \in \Sigma$ (in our notation;
\cite{jgl} uses functions $\_\ \cdot\ \sigma$)
if $t$ is obtained by substituting strongly normalising terms 
(of the right type) for variables in $s$.

We now consider this result in the light of our proof of 
Theorem~\ref{thm-allsn}.

In \cite[Theorem~2]{jgl}, $\SNo$ is $\wruvo$,
and $\underline{\SN}^\circ$ is $\gindy\ (\vtluo)\ \SNo$.
The following lemma follows easily from Lemma~\ref{lemma-P2}.
In fact Property~2 of \cite{jgl} could be weakened, 
as it is used only to show conditions \ref{P2a} and \ref{P2b}
of Lemma~\ref{lemma-P2}.
We also use the numbering of conditions, such as $(i)^\circ$,
to correspond to that in \cite{jgl}.

\begin{lemma} \label{prop2}
Assume Property~2 of \cite{jgl} holds: that is,
if $(t, s) \in \rho$ then either
\begin{description}
\item[$(i)^\circ$] for some $u$, $s \btr u$ and $u \geq_\rho t$, or
\item[$(ii)^\circ$] $s \gg t$ and for every $u \vtl t$, 
  either $s >_\rho u$ or for some $v \vtl s$, $v \geq_\rho u$.
\end{description}
Let $S = \{y\:|\ \exists z.\ z\ (\btl \cup \vtl)\ s \mbox{ and }
  (y, z) \in (\rho\ \cup \vtlo)^* \}$.
Then any $t$ such that $(t, s) \in \rho$ 
is in $\gbars \vtl \{x\:|\ x \ll s\}\ S$.
\end{lemma}

\comment{
If we set $S$ in Lemma~\ref{lemma-P2} 
to be $\{y\:|\ \exists z.\ z\ (\btl \cup \vtl)\ s$ and 
$(y, z) \in (\rho\ \cup \vtlo)^* \}$,
then the conditions of Lemma~\ref{lemma-P2} are clearly weaker
then those in Property~2 of \cite{jgl}.
}
Thus, when Property~2 is satisfied, we have that 
\begin{equation} \label{gbS}
\mbox{if } (t, s) \in \rho, \mbox{ then }
t \in \gbars \vtl \{x\:|\ x \ll s\}\ S
\end{equation}

We now use (\ref{gbS}) to show that Condition~\ref{conds-defs}\ref{rpc},
with $\vtl$ replaced by $\vtluo$ and 
$\rho$ by $\rho\ \cup \vtlo$, and so $\SN$ by $\SNo$, holds.
Below we use infix notation to write 
$t'\ (\vtluo)\ s$ for $(t, s) \in (\vtluo)$, for example.  
That is, if (\ref{eqts}) and (\ref{isubs}) then (\ref{gbvtluo}):
\begin{eqnarray}
\label{eqts} && (t, s) \in \rho\ \cup \vtlo \\
 % \label{isubs} && \mbox{for all }s'\ (\vtluo)\ s, \quad s' \in \SNo \\
\label{isubs} && \forall s'.\ s'\ (\vtluo)\ s \Rightarrow s' \in \SNo \\
\label{gbvtluo} && t \in \gbars\ (\vtluo)\ \{x\:|\ x \ll s\}\ \SNo
\end{eqnarray}

\begin{lemma} \label{lem-14-15}
Assume (\ref{gbS}) and conditions $(xiv)$ and $(xv)$ of \cite{jgl}
(shown below).
Alternatively, assume condition $(xiv')$ in place of $(xiv)$:
\begin{description}
\item[$(xiv)$] if $s \gg t \vtro u$, then either $t \vtr u$ or 
$s \vtro v \geq_\rho t$ for some $v$
\item[$(xiv')$] if $s \gg t \vtro u$, then either $t \vtr u$ or 
$s \vtro v \geq_\rho u$ for some $v$
\item[$(xv)$] if $s \btr u$ and 
$\forall v.\ v\ (\vtluo)\ s \Rightarrow v \in \SNo$, then $u \in \SNo$.
\end{description}
Then 
\begin{enumerate}
\item \label{14-15-c1}
  Condition~\ref{conds-defs}\ref{rpc} (as substituted) holds, 
  ie, if (\ref{eqts}) and (\ref{isubs}) then (\ref{gbvtluo}), and
\item \label{14-15-gg} 
  every $s \in \gindy \ll (\gindy\ (\vtluo)\ \SNo)$.
\end{enumerate}
\end{lemma}

\begin{verbatim}
"jgl14f ?cuto ?trio ?isub ?rho ?s == 
    ALL t u.  (t, ?s) : ?cuto --> (u, t) : ?trio -->
      (u, t) : ?isub | (t, ?s) : ?isub Un ?trio O ?rho^*" 

"jgl15f ?btri ?sub ?sn ?dt == 
    (ALL v. (v, ?dt) : ?sub --> v : ?sn) -->
    (ALL u. (u, ?dt) : ?btri --> u : ?sn)" 

dth_dti_jglh_sn = "[| wf ?isub;
  ALL dt.  red_props_jglh ?isub {dts. (dts, dt) : ?btri Un ?isub O ?rho^*}
     ?rho ?cuto dt;
  jgl14f ?cuto ?trio ?isub ?rho ?dt;
  jgl15f ?btri (?isub Un ?trio) (wfp (?rho Un ?trio)) ?dt |] ==>
  ?dt : gindy ?cuto (gindy (?isub Un ?trio) (wfp (?rho Un ?trio)))" : thm 
\end{verbatim}

\begin{proof} \emph{\ref{14-15-c1}}
Suppose $(t, s) \in \rho$ and
assume that for all $s' (\btl \cup \vtl) s$,
$s' \in \SNo$. 
Then if $y \in S$, say $z (\btl \cup \vtl) s$
and $(y, z) \in (\rho\ \cup \vtlo)^*$, then $z \in \SNo$ and $y \in \SNo$, 
so $S \subseteq \SNo$ and, by (\ref{gbS}) and the monotonicity of \gbars, 
we have $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SNo$.

Let $(t, s) \in\ \vtlo$ and
assume that for all $s' \vtlo s$,
$s' \in \SNo$. 
Then $t \in \SNo \subseteq \gbars \vtl \{x\:|\ x \ll s\}\ \SNo$.

Combining these, we get: 
if $(t, s) \in (\rho\ \cup \vtlo)$ and,
for all $s'\ (\btl \cup \vtluo)\ s$, $s' \in \SNo$, then 
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SNo$: 
that is, 
if (\ref{eqts}) and (\ref{isubbs}) then (\ref{gbvtl}).
\begin{eqnarray}
\label{isubbs} 
  && \mbox{for all }s'\ (\btl \cup \vtluo)\ s, \quad s' \in \SNo \\
 && \forall s'.\ s'\ (\btl \cup \vtluo)\ s \Rightarrow s' \in \SNo \\
\label{gbvtl} && t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SNo
\end{eqnarray}

By $(xv)$ we can delete $\btl$ from (\ref{isubbs}), that is, 
(\ref{isubbs}) is equivalent to (\ref{isubs}).
 \begin{equation}
 \label{isubs'} \mbox{for all }s'\ (\vtluo)\ s, \quad s' \in \SNo
 \end{equation}
So now we have: if (\ref{eqts}) and (\ref{isubs'}) then (\ref{gbvtl}),
but we want: if (\ref{eqts}) and (\ref{isubs'}) then (\ref{gbvtluo}).
\comment{
That is, we have: if $(t, s) \in \rho\ \cup \vtlo$ and
for all $s'\ (\vtluo)\ s$, $s' \in \SNo$, then
$t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SNo$.
But we need to show (under these assumptions)
\begin{equation}
\label{gbvtluo} t \in \gbars\ (\vtluo)\ \{x\:|\ x \ll s\}\ \SNo
\end{equation}
}

So assume (\ref{isubs'}) and (\ref{gbvtl}), we will show (\ref{gbvtluo}).
 $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SNo$.
Consider a descending $(\vtluo)$-chain from $t$.
Let the first instance (if any)
of $\vtlo \setminus \vtl$ in it be $t_i \vtro t_{i+1}$,
and assume the chain has not yet reached a member of $\SNo$.
Then $t_i \in \{x\:|\ x \ll s\}$, ie, $t_i \ll s$.
Therefore, using $(xiv)$, since $(t_{i+1}, t_i) \not \in \vtl$,
we have $s \vtro v \geq_\rho t_i$,
so $v \in \SNo$ by (\ref{isubs'}), and $t_i \in \SNo$.
Using $(xiv')$ instead,
$s \vtro v \geq_\rho t_{i+1}$, so $t_{i+1} \in \SNo$.
In each case, (\ref{gbvtluo}) holds.
 Thus $t \in \gbars\ (\vtluo)\ \{x\:|\ x \ll s\}\ \SNo$.

That is, Condition~\ref{conds-defs}\ref{rpc} (as substituted) holds. 

\emph{\ref{14-15-gg}}
From Lemma~\ref{dth} we get every
$s \in \gindy \ll (\gindy\ (\vtluo)\ \SNo)$.
\qed \end{proof}

Note that it would be sufficient in condition $(xiv)$ if
``$s' \vtro v \geq_\rho t$'' were replaced by 
``$s'\ (\vtr \cup \vtro)\ v$ and $(t, v) \in (\rho\ \cup \vtlo)^*$'',
and condition $(xiv')$ could be modified likewise.
Lemma~3 of \cite{jgl} appears to use $(xiv')$ rather than $(xiv)$.

Now, we first consider the simpler case of \cite[Thm~2]{jgl}
where the only $\sigma$ is $\sigma_0$. 
Then, condition $(iv)^\circ$ 
simply says $\underline\SN^\circ$ \textit{bars $s$ in} $\gg$,
ie every $s \in \bars \ll (\gindy\ (\vtluo)\ \SNo)$.
Thus, using Lemma~\ref{l2}\ref{gindy-bars},
it follows from Lemma~\ref{lem-14-15}\ref{14-15-gg} that
every $s \in \gindy\ (\vtluo)\ \SNo$.

We now use condition $(xiii)$ of \cite{jgl} 
(omitting reference to $\sigma$).

\begin{lemma} \label{13ns}
Assume condition $(xiii)$ holds: i.e.\  
for every object $s$, either $s \in \SNo$ or, for every 
$u\ (\vtluo)\ s$, either $u \in \SNo$ or there exists $v \vtl s$
such that $u\ (\leq_\rho\ \cup \vtlo)\ v$.  $(u, v) \in \rho\ \cup \vtlo$.
Then, if $s \in \gindy\ (\vtluo)\ \SNo$, then $s \in \gindy \vtl \SNo$.
\end{lemma}

\begin{verbatim}
"jgl13f ?isub ?trio ?rho ?s == ?s : wfp ?rho | 
  (ALL u. (u, ?s) : ?trio --> 
          u : wfp ?rho | (u, ?s) : ?isub O ?rho^*)"

bars_ext13 = 
 "[| ?s : gindy (?isub Un ?trio) (wfp ?rho)
     ; jgl13f ?isub ?trio ?rho ?s |] 
  ==> ?s : gindy ?isub (wfp ?rho)" : thm
\end{verbatim}

\begin{proof}
Assume that $\forall t \vtl s.\ t \in \SNo$: we need to show $s \in \SNo$.
Firstly, note that if $v \vtl s$ and $u\ (\leq_\rho\ \cup \vtlo)\ v$,
as in the last part of condition $(xiii)$, 
 $(u, v) \in \rho\ \cup \vtlo$,
then $v$, and therefore $u$, are in $\SNo$.
Then, by condition $(xiii)$, 
either $s \in \SNo$, whence $s \in \gindy \vtl \SNo$ trivially,
or, for every $u \vtlo s$ we have $u \in \SNo$ (by the remark above).
Then, as every $u$ such that $u\ (\vtluo)\ s$ is in $\SNo$, 
and $s \in \gindy\ (\vtluo)\ \SNo$, so we have $s \in \SNo$ as required.  
\qed \end{proof}

Finally, as $\vtl$ is well-founded  by condition $(iii)$,
every $s \in \bars \vtl \SNo$;
as every $s \in \gindy \vtl \SNo$, 
every $s \in \SNo$ by Lemma~\ref{l2}\ref{gindy-bars}.

We now extend the foregoing to capture the generality of
\cite[Theorem~2]{jgl}, but our notation differs:
we use a relation $\Sigma$.
In terms of the $S$ of \cite[Theorem~2]{jgl}, 
$(t, s) \in \Sigma$ when $t = s \cdot \sigma$ for some $\sigma \in S$.
Then condition $(xii)$, which is: for some $\sigma_0 \in S$, 
for all $s$, $s \cdot \sigma_0 = s$, becomes: $\Sigma$ contains the identity
relation.

Define a set $\SNSig$ by: $s \in \SNSig$ iff 
for all $v$ such that $(v, s) \in \Sigma$, $v \in \SNo$.

\begin{verbatim}
"jgl13sf ?sig ?isub ?trio ?rho ?s ==  
  ALL t. (t, ?s) : ?sig 
  --> t : wfp ?rho 
      | (ALL u. (u, t) : ?isub Un ?trio -->
                 u : wfp ?rho | (u, ?s) : (?isub O ?sig) O ?rho^*)"

"jgl4sf ?sig ?isub ?trio ?cuto ?rho ?s == 
  (ALL v. (v, ?s) : ?isub O ?sig --> v : wfp ?rho) 
   --> (ALL t. (t, ?s) : ?sig 
        --> t : bars ?cuto (gindy (?isub Un ?trio) (wfp ?rho)))"
\end{verbatim}

\begin{lemma} \label{13s}
Assume condition $(xiii)$ holds: i.e.\  
for every $(t, s) \in \Sigma$, either $t \in \SNo$ or, for every 
$u\ (\vtluo)\ t$, either $u \in \SNo$ or there exist $v'$ and $v$
such that $u\ (\leq_\rho\ \cup \vtlo)\ v' <_\Sigma v \vtl s$.
% Suppose also that for all $v'$ such that $(v', s) \in\ \vtl \circ \Sigma$,
% $v' \in \SNo$.
% Then, if $t \in \gindy\ (\vtluo)\ \SNo$, then $t \in \SNo$.
Suppose that $\forall t <_\Sigma s.\ t \in \gindy\ (\vtluo)\ \SNo$.
Then $s \in \gindy \vtl \SNSig$.
\end{lemma}

\begin{verbatim}
ext13_subs_wf = 
 "[| jgl13sf ?sig ?isub ?trio ?rho ?s
     ; ALL t. (t, ?s) : ?sig --> t : gindy (?isub Un ?trio) (wfp ?rho) |] 
  ==> ?s : gindy ?isub (subs_wf ?sig ?rho)" : thm 
\end{verbatim}

\begin{proof}
Suppose that $\forall v \vtl s.\ v \in \SNSig$.
We need to show $s \in \SNSig$, so suppose $(t, s) \in \Sigma$.
We then need to show $t \in \SNo$.

Firstly, note that if $u\ (\leq_\rho\ \cup \vtlo)\ v' <_\Sigma v \vtl s$,
as in the last part of condition $(xiii)$,
then, as $v \in \SNSig$, it follows that
$v'$, and therefore $u$, are in $\SNo$.
Then, by condition $(xiii)$, 
either $t \in \SNo$ 
or, for every $u$ such that $u\ (\vtluo)\ t$ 
we have $u \in \SNo$ (by the remark above).
Then, as every $u$ such that $u\ (\vtluo)\ t$ is in $\SNo$, 
and $t \in \gindy\ (\vtluo)\ \SNo$ we have $t \in \SNo$, as required.  
\qed \end{proof}

\comment{
Note that condition $(iv)^\circ$ is:
if, for all $v$ such that $(v, s) \in\ \vtl \circ \Sigma$, $v \in \SNo$,
(equivalently, for all $u \vtl s$, $u \in \SNSig$),
and $(t, s) \in \Sigma$, then 
$t \in \bars \ll (\gindy\ (\vtluo)\ \SNo)$.
}

\begin{theorem} \label{jgl2}
Assume all the conditions for Theorem~2 of \cite{jgl} hold.
That is,
\begin{itemize}
\item Property~2 (see Lemma~\ref{prop2})
\item (iii): $\vtl$ is well-founded
\item $(iv)^\circ$:
if $\forall v.\ (v, s) \in \vtl \circ\ \Sigma \Rightarrow v \in \SNo$,
(equivalently, $\forall u \vtl s.\ u \in \SNSig$),
and $(t, s) \in \Sigma$, then 
$t \in \bars \ll (\gindy\ (\vtluo)\ \SNo)$
\item (xii): each $(s, s) \in \Sigma$
\item (xiii) (see Lemma~\ref{13s})
\item (xv) and either (xiv) or (xiv') (see Lemma~\ref{lem-14-15})
\end{itemize}
Then
\begin{enumerate}
\item \label{htgs} $\forall s.\ s \in \gindy \vtl \SNSig$
\item \label{hts} $\forall s.\ s \in \SNo$
\end{enumerate}
\end{theorem}

\begin{verbatim}
sub_wfp = "[| All (jgl13sf ?sig ?r ?trio (?rho Un ?trio));
  All (jgl4sf ?sig ?r ?trio ?ra (?rho Un ?trio));
  All (jglns.jgl14f ?ra ?trio ?r ?rho);
  All (jgl15f ?btri (?r Un ?trio) (wfp (?rho Un ?trio))); wf ?r;
  ALL dt.  red_props_jglh ?r {dts. (dts, dt) : ?btri Un ?r O ?rho^*}
     ?rho ?ra dt; Id <= ?sig |] ==> ?s : wfp (?rho Un ?trio)" : thm
\end{verbatim}

\begin{proof} \emph{\ref{htgs}}
To show $s \in \gindy \vtl \SNSig$, 
we may assume that $\forall u \vtl s.\ u \in \SNSig$.
% We need to show that $s \in \SNSig$.
% we need to show that $s \in \SNo$.
Suppose that $(t, s) \in \Sigma$.
By condition $(iv)^\circ$, % (as explained above),
$t \in \bars \ll (\gindy\ (\vtluo)\ \SNo)$.
It follows from Lemma~\ref{lem-14-15}\ref{14-15-gg} and
Lemma~\ref{l2}\ref{gindy-bars} 
that any such $t$ is in $\gindy\ (\vtluo)\ \SNo$.
% Then, by Lemma~\ref{13s}, $t \in \SNo$.
Then Lemma~\ref{13s} holds and $s \in \gindy \vtl \SNSig$. 
% As this holds for all $t <_\Sigma s$, $s \in \SNSig$, as required.

\emph{\ref{hts}}
% As $\vtl$ is well-founded, every $s \in \bars \vtl \SNSig$;
% so every $s \in \SNSig$ by Lemma~\ref{l2}\ref{gindy-bars};
% as $(s, s) \in \Sigma$ (by $(xii)$), $s \in \SNo$.
As $\vtl$ is well-founded, every $s \in \SNSig$ by
Lemma~\ref{l2}\ref{gindy-bars};
as $(s, s) \in \Sigma$ by $(xii)$, we have $s \in \SNo$.
% \qed
\end{proof}

\footnote{conclusion required here}
}

\section{Observations and Conclusion}

\comment{
In \S\ref{s-tc}, as in \cite[\S3.3]{dggt},
we had the somewhat paradoxical situation that it
was necessary to add additional rules to enlarge the relation
$\rho$ to prove termination.
We would like to extend Theorem~\ref{thm-allsn} to avoid this need since,
the larger $\rho$ is, the more difficult it should be to prove termination.
}

If Condition~\ref{conds-defs}\ref{rpc} holds,
then it also holds if we augment $\rho$ to contain $\vtl$. 
Thus, for fixed $\vtl$,
Theorem~\ref{thm-allsn} does \emph{not} provide a universal
method of proving termination because there are well-founded relations $\rho$
where $\rho\ \cup \vtl$ is not well-founded.

However, if $\rho$ is well-founded
and we can choose $\vtl$ so that $\vtl\ \subseteq \rho$,
then Theorem~\ref{thm-allsn} can be applied trivially.
Let $\ll\ = \ \vtl\ = \rho^+$, which is well-founded.
Then even Condition~\ref{conds-defs}\ref{rpc2} applies.
%% for $\vtl\ \subseteq \rho$ is well-founded and,
%% if $(t, s) \in \rho$ and $t' \vtl^* t$, 
%% then $(t', s) \in \rho^+ =\ \ll$.
Clearly also, conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn}
apply as $\ll$ and $\vtl$ are well-founded.
That is, Theorem~\ref{thm-allsn} is, trivially, a universal method of proving
termination (as are several other orderings in the literature).

%% However, if $\rho$ is well-founded
%% and we can choose $\vtl$ so that $\vtl\ \subseteq \rho$,
%% then Theorem~\ref{thm-allsn} can be applied trivially.
%% Let $\ll\ = \rho^+$, which is well-founded.
%% Then even Condition~\ref{conds-defs}\ref{rpc2} applies, for 
%% $\vtl\ \subseteq \rho$ is well-founded and,
%% if $(t, s) \in \rho$ and $t' \vtl^* t$, 
%% then $(t', s) \in \rho^+ =\ \ll$.
%% Clearly also, conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn}
%% apply as $\ll$ and $\vtl$ are well-founded.
%% That is, Theorem~\ref{thm-allsn} is, trivially, a universal method of proving
%% termination (as are several other orderings in the literature).

\comment{
We have proved a theorem about termination of reduction rules
which generalises the previous quite general theorems, 
in \cite{dggt} and the first theorem in \cite{jgl}. 
% and the general path ordering \cite{nat-term}.
% \footnote{ may omit the general path ordering}
% We have shown how to adapt the framework of our proof to give
% a proof of the complex second theorem in \cite{jgl} for
% higher-order path orderings.
% \footnote{ may omit the second theorem in \cite{jgl}}

Finally, motivated by the complexity of proofs of the termination of
$\beta$-reduction in a typed setting, we show how to use our main
theorem to prove the termination of the reduction of well-typed
combinator expressions, and to adapt its proof to prove the strong
normalisation of the simply-typed $\lambda$-calculus.  } Our proofs
for the simply-typed $\lambda$-calculus 
%have some resemblances to the
differ from 
classic reducibility proofs by circumventing the usual step
that $M [\overline x := \overline A] \in \SN$ for $A \subseteq \SN$.
An open question is whether our indirect method for 
handling
substitutions can be adapted to prove termination for the
higher-order recursive path ordering of
%Jouannaud \& Rubio 
\cite{jr-horpo}. 

The picture that emerges is the following. 
%Goubault-Larrecq's
Theorem~1 from \cite{jgl} can handle ARSs but cannot handle
reducibility arguments like those required for combinators or
the simply-typed $\lambda$-calculus.  Our \cite[Theorem~2]{dggt} 
handles TRSs but also cannot handle such reducibility arguments. Our new
Theorem~1 handles both TRSs and some reducibility arguments, but
must be modified to reason indirectly about substitutions for
the simply-typed $\lambda$-calculus.
An important goal is to find the exact relationship between
\cite[Theorem~2]{jgl} and 
our Theorem~\ref{thm-allsn}.

% \paragraph{Acknowledgements}
% 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}

%\vspace*{-1em}

\bibliographystyle{plain}

\begin{thebibliography}{1}

\bibitem{akama-trans}
Yohji Akama.  A $\lambda$-to-CL Translation for Strong Normalization.
In Proc.\ Typed Lambda Calculi and Applications (TLCA'97),
LNCS 1210, 1--10, Springer, 1997.  

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

\bibitem{baader-nipkow}
Franz Baader and Tobias Nipkow.
Term Rewriting and All That.
CUP, 1998

\bibitem{bfr}
C~Borralleras, M~Ferreira and A~Rubio.
Complete Monotonic Semantic Path Orderings.
In Proc.\ CADE-17, LNCS 1831, 346--364, Springer, 2000.

\bibitem{buchholz-pta}
Wilfried Buchholz.
Proof-theoretic analysis of termination proofs. 
Annals of Pure and Applied Logic 75 (1995), 57--65.

\bibitem{david-nr}
R~David.
Normalization without Reducibility.
APAL 107:121--130, 2001 Elsevier.

\bibitem{dggt}
Jeremy~E~Dawson and Rajeev Gor{\'e}.
A General Theorem on Termination of Rewriting. 
\newblock In 
  Proc.\ Computer Science Logic (CSL 2004),
  LNCS 3210, 100--114, 2004.

\bibitem{dgtars}
J~E~Dawson and R~Gor{\'e}.
Machine-checked  Termination Proofs for Abstract Reduction Systems. 
\newblock \url{http://web.rsise.anu.edu.au/~jeremy/pubs/rewr_term/mcars/}

\bibitem{dersh-td}
N Dershowitz.  Termination Dependencies (Extended Abstract).
In Proc.\ Sixth Int'l Workshop on Termination (WST '03), A~
Rubio, ed., Valencia, Spain, pp. 27--30.

\bibitem{nat-term}
N Dershowitz \& C Hoot.  Natural Termination.
TCS 142 (1995), 179-207.

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

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

\bibitem{gallier-oncr}
Jean Gallier.  On Girard's "Candidats de Reductibilite".
Logic and Computer Science, P.Odifreddi (ed), Academic Press, 1989, 123-203.

\bibitem{glt}
Jean-Yves Girard, Yves Lafont and Paul Taylor.
Proofs and Types.
CUP, 1990.

\bibitem{jgl}
J~Goubault-Larrecq. Well-founded recursive relations. 
In Proc.\ CSL'2001, LNCS 2142, 484--497, Springer, 2001.

 \bibitem{hm-dpr}
 Nao Hirokawa and Aart Middeldorp.
 Dependency Pairs Revisited.
 In Proc.\ Rewriting Techniques and Applications (RTA-04), 
 LNCS 3091, 249--268, Springer, 2004.

\bibitem{jr-horpo}
J-P~Jouannaud and A~Rubio.
The Higher-order Recursive Path Ordering.
In Proc. 14th Logic in Computer Science (LICS'99), 402--411, 1999.

\end{thebibliography}

\end{document}

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