\documentclass{lecture}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{proof}
\usepackage{exptrees}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{condition}{Condition}

\newcommand{\pordered}[3]{#1 <_{\scriptsize #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{\SN}{\textit{SN}}
% \newcommand{\ISN}{\textit{ISN}}
\newcommand{\SN}{\ensuremath{S\!N}}
\newcommand{\ISN}{\ensuremath{I\!S\!N}}
\newcommand{\lpo}{\textit{lpo}}
\newcommand{\lex}{\textit{lex}}
\newcommand{\fwf}{\textit{fwf}}

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

%\input{/home/discus/disk1/rpg/papers/relalg/csl96/defs}

\newcommand{\comment}[1]{}
\newcommand{\mytilde}{\scriptstyle\sim}

\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

%%%%% Rule Forming Commands

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

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


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

\newcommand{\Drel}{\mbox{\bf DRA }}
\newcommand{\Lg}[1]{\mbox{$\bf #1$}}

\newcommand{\Fml}{\mbox{$\mathbf{Fml}$}}
\newcommand{\LAlg}{\mbox{$\mathfrak{Fml}/\!\!\equiv$}}

\newcommand{\stc}{\bullet}

\newcommand{\blob}{\bullet}

\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}

\newcommand{\mcal}[1]{\mbox{$\cal #1$}}

\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}

\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }

\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}
\newcommand{\eqded}{\dashv \vdash}

\newcommand{\id}{
\idrule{(id)}{$p \vdash p$}
}

\newcommand{\cut}{
\brule{(cut)}
      {$X \vdash A$} 
      {$A \vdash Y$} 
      {$X \vdash Y$} 
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modal Axioms

\definecolor{altmagenta}{rgb}{1,0,1}
\definecolor{altyellow}{rgb}{1,1,0}
\definecolor{altcyan}{rgb}{0,1,1}
\definecolor{darkmagenta}{rgb}{0.5,0,0.5}
\definecolor{darkyellow}{rgb}{0.5,0.5,0}
\definecolor{darkcyan}{rgb}{0,0.5,0.5}
\definecolor{darkgreen}{rgb}{0,0.5,0}
\definecolor{darkblue}{rgb}{0,0,0.5}
\definecolor{darkred}{rgb}{0.5,0,0}

\begin{document}


\title{ }
\begin{slide}
  \begin{Heading}
A General Theorem on Termination of Rewriting
  \end{Heading}

\begin{center}
\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\multicolumn{2}{c}{Jeremy E.\ Dawson and Rajeev Gor\'{e}}
\\ \\
Logic \& Computation Programme      & Automated Reasoning Group 	\\
National ICT Australia 		&  Computer Sciences Laboratory   \\
& Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\  \\
& {Australian National University}                    \\
\texttt{http://rsise.anu.edu.au/{\small$\mytilde$}jeremy} &
		      \texttt{http://rsise.anu.edu.au/{\small$\mytilde$}rpg} \\
\end{tabular*}
\end{center}

\begin{itemize}
\small 
\item[ ] % supported by an Australian Research Council Large Research Grant.
\end{itemize}

\end{slide}

\comment{
\begin{slide}
  \begin{Heading}
    {Colours}
  \end{Heading}
 
 \color{yellow} yellow
 \color{cyan} cyan
 \color{magenta} magenta
 \color{altyellow} altyellow
 \color{altcyan} altcyan
 \color{altmagenta} altmagenta
 \color{darkyellow} darkyellow
 \color{darkcyan} darkcyan
 \color{darkmagenta} darkmagenta
 \color{green} green
 \color{blue} blue
 \color{red} red
 \color{darkgreen} darkgreen
 \color{darkblue} darkblue
 \color{darkred} darkred

\end{slide}
}

\begin{slide}
  \begin{Heading}
    {Overview and Motivation}
  \end{Heading}

  \begin{description}
  \item[Display Calculi:] Generalised sequent framework due to Nuel
    Belnap 

   Single cut-elimination proof if rules
    satisfy 8 easily checked conditions

  \item[Isabelle/HOL:] Logical framework that allows us to formalise
    mathematics 

  \item[Cut elimination:] We used Isabelle/HOL
    to check the cut-elimination theorem of Belnap:
    repeatedly transform derivation, 
    focusing on a top-most cut

  \item[Strong Normalisation:] You can attack a cut other than a top-most cut
    -- must it terminate?
    We tried to check a published proof of strong normalisation.

  \item[Actual outcome:] problem with proof, found and checked a new proof,
  tricky as each step changes or removes one cut,
    but can duplicate others

  \item[Rewriting:] can formulate this proof in terms of a set of rewriting
  rules, proving strong normalisation (termination) of the rewriting procedure

  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Reducing a Left-and-Right Principal Cut}
  \end{Heading}
  
  \begin{itemize}
  \item A cut on $A$ is \emph{left- [right-] principal} if the left [right]
    inference immediately above the cut introduces $A$ via a logical
    rule, written $(\vdash A)$ [$(A \vdash)$]


  \item[ ]
         \begin{center}{\small
         \vpf
         \bpf
           \A "$\Pi_{L}$"
           \U "$X \vdash A$" "($\vdash A$)"
           \A "$\Pi_{R}$"
           \U "$A \vdash Y$" "($A \vdash$)"
           \B "$X \vdash Y$"
         \epf
         }\end{center}

  \item C8: All left-and-right principal cuts can be replaced by cuts
    on strictly smaller subformulae of $A$


   \item Base Case:
   \brule{(cut)}
         {$p \vdash p$}
         {$p \vdash p$}
         {$p \vdash p$} reduced to just $p \vdash p$

    \item Similar cases for $\btop$, $\bbot$
%    \item Similar cases for $\btop$, $\mtop$, $\bbot$, $\mbot$
    
      
  \end{itemize}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Example of a Principal reduction (C8 condition)}
  \end{Heading}
  
{\small
\vpf
\bpf
\A "\color{darkgreen} $\Pi_{ZAB}$"
\U "\color{darkgreen} $Z \vdash A, B$"
\U "$Z \vdash A \bor B$" "($\vdash \bor $)"
\A "\color{darkgreen} $\Pi_{AX}$"
\U "\color{darkgreen} $A \vdash X$"
\A "\color{darkgreen} $\Pi_{BY}$"
\U "\color{darkgreen} $B \vdash Y$"
\B [1em] "$A \bor B \vdash X, Y$" "($\bor \vdash $)"
\B [2em] "$Z \vdash X, Y$" "($cut$)"
\U ['] "Principal cut on formula $A \bor B$"
\epf
\hfill
\vpf
\bpf
\A "\color{darkgreen} $\Pi_{ZAB}$"
\U "\color{darkgreen} $Z \vdash A, B$"
\U "$*A, Z \vdash B$" "(dp)"
\A "\color{darkgreen} $\Pi_{BY}$"
\U "\color{darkgreen} $B \vdash Y$"
\B [2em] "$*A, Z \vdash Y$" "($cut$)"
\U "$Z \vdash A, Y$" "(dp)"
\U "$Z, *Y \vdash A$" "(dp)"
\A "\color{darkgreen} $\Pi_{AX}$"
\U "\color{darkgreen} $A \vdash X$"
\B [2em] "$Z, *Y \vdash X$" "($cut$)"
\U "$Z \vdash X, Y$" "(dp)"
\U ['] "Transformed derivation uses cuts only on $A$ and $B$"
\epf
}

\vfill

Must exhibit and hard-wire such transformations for every logical connective

So if cut is \emph{not} left-and-right principal then we try to make
it so ...

\end{slide}

\begin{slide}
  \begin{heading}
    {A Parametric Reduction --- making a cut left-right-principal}
  \end{heading}
  
  \begin{itemize}

  \item Given a derivation ending in a non left-and-right principal
    cut on formula $A$, we trace the ancestor occurrences of this $A$
    up $\Pi_{L}$:

  \item Let $\Pi[A := Y]$ mean ``replace all 
    (non-principal) ancestors of $A$ with $Y$'' 

  \item[]
    \begin{center}
    \vspace{-2ex}
      {\small
      \bpf
      \A "\color{darkgreen} $\Pi^{1}_{L}$"
      \U "\color{darkgreen} $V \vdash A $" "($\vdash A$)"
      \U "$\Pi^{2}_{L}$" "($\pi$)"
      \U "$X \vdash A $" "($\rho$)"
      \A "\color{darkgreen} $\Pi_R$"
      \U "\color{darkgreen} $A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "\color{darkgreen} $\Pi^{1}_{L}$"
      \U "\color{darkgreen} $V \vdash A $" "($\vdash A$)"
      \A "\color{darkgreen} $\Pi_R$"
      \U "\color{darkgreen} $A \vdash Y$" 
      \B [2em] "$V \vdash Y$" "($cut$)"
      \U "$\Pi^{2}_L[A := Y]$" "($\pi$)"
      \U "$X \vdash Y $" "($\rho$)"
      \epf
      }
    \end{center}

  \item New cut is left-principal (similarly make it also right principal)

  \item If $\Pi_L$ branches ($A$ introduced at multiple places), more complex
  (!) \\
  If $\Pi^{1}_{L}$ is empty, $A$ introduced
  by $A \vdash A$, no new cuts needed.
  \end{itemize}
\end{slide}


\begin{slide}
  \begin{Heading}
    {Strong Normalisation}
  \end{Heading}
  
Cut-admissibility proceeds by eliminating the top-most cut

Strong normalisation: define reduction steps, eliminate \emph{any} cut that
can be reduced, and prove that this cut-elimination procedure terminates:
\begin{itemize}
\item $\Pi_n < \Pi_{n-1} < \cdots < \Pi_2 < \Pi_0$
\item $\Pi_n$ is cut-free
\item $n$ is finite
\item weak-normalisation (attacking top most cut) is an instance of this method
\end{itemize}

Usually define reductions as either a parametric or principal move,
with proviso that we must not cross a cut in a parametric move

\end{slide}

\begin{slide}
  \begin{Heading}
    {Why Formalise (in Isabelle) ?}
  \end{Heading}

Strong-normalisation proofs are notoriously difficult involving many cases

We tried to formalise Heinrich Wansing's proof of strong-normalisation
for display logic, but got stuck at one particular case

Found a problem ... Wansing assumes that $\Pi^1_L$ is unchanged! 

      \hfill $V_A$ is $(*A \comma X)$ \hfill 
      $V_Y$ is $(*Y \comma X)$ \hfill \mbox{}


    \begin{center}
      {\small
      \bpf
      \A "\color{darkgreen} $\Pi^{1}_{L}$"
      \U "\color{darkgreen} $V_A \vdash A $" "($\vdash A$)"
      \U "$X \vdash A, A$" "(dp)"
      \U "$X \vdash A $" "(ctr)"
      \A "\color{darkgreen} $\Pi_R$"
      \U "\color{darkgreen} $A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "\color{red} $\Pi'^{1}_{L}$"
      \U "\color{red} $V_Y \vdash A $" "($\vdash A$)"
      \A "\color{darkgreen} $\Pi_R$"
      \U "\color{darkgreen} $A \vdash Y$" 
      \B [2em] "$V_Y \vdash Y$" "($cut$)"
      \U "$X \vdash Y, Y$" "(dp)"
      \U "$X \vdash Y $" "(ctr)"
      \epf
      }
    \end{center}

% Can construct counter-examples where his proof goes into loops: a
% given cut is reduced to itself ... his procedure will not terminate

\end{slide}

\begin{slide}
\begin{heading}
  { Branch in left subtree --- before and after}
\end{heading}
\begin{center}
\bpf
\A "\color{darkgreen} $\Pi'$"
\U "\color{darkgreen} $X' \vdash A $" "(intro-$A$)"
\A "\color{darkgreen} $\Pi''$"
\U "\color{darkgreen} $X'' \vdash A $" "(intro-$A$)"
\B [1em] "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $A \vdash Y$"
\B [0em] "$X \vdash Y$" "($cut$)"
\epf

\bpf
\A "\color{darkgreen} $\Pi'$"
\U "\color{darkgreen} $X' \vdash A $" % "(intro-$A$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $A \vdash Y$"
\B [1em] "$X' \vdash Y$" "($cut$)"
\A "\color{darkgreen} $\Pi''$"
\U "\color{darkgreen} $X'' \vdash A $" % "(intro-$A$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $A \vdash Y$"
\B [1em] "$X'' \vdash Y$" "($cut$)"
\B [1em] "$\Pi_L[A := Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- before and after }
\end{heading}

\begin{center}
\bpf
\A "\color{darkgreen} $\Pi$"
\U "\color{darkgreen} $X, B \vdash * B $" "($\rho$)"
\U "\color{darkgreen} $X, B \vdash \lnot B $" "($\vdash \lnot$)"
\U "$*\lnot B, X \vdash *B $" "(dp)"
\U "$*\lnot B, X \vdash \lnot B $" "($\vdash \lnot$)"
\U "$X \vdash \lnot B, \lnot B $" "(dp)"
\U "$X \vdash \lnot B $" "($\vdash \mbox{cont}$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $\lnot B \vdash Y$"
\B [1em] "$X \vdash Y$" "($cut$)"
\epf
\hspace{-2em}
\comment{
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- after }
\end{heading}
\begin{center}
}
\bpf
\A "\color{darkgreen} $\Pi$"
\U "\color{darkgreen} $X, B \vdash * B $" "($\rho$)"
\U "\color{darkgreen} $X, B \vdash \lnot B $" "($\vdash \lnot$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $\lnot B \vdash Y$"
\B [1em] "\color{red} $X, B \vdash Y $" "($cut$)"
\U "\color{red} $*Y, X \vdash * B $" "(dp)"
\U "\color{red} $*Y, X \vdash \lnot B $" "($\vdash \lnot$)"
\A "\color{darkgreen} $\Pi_R$"
\U "\color{darkgreen} $\lnot B \vdash Y$"
\B [-2em] "$*Y, X \vdash Y $" "($cut$)"
\U "$X \vdash Y, Y $" "(dp)"
\U "$X \vdash Y $" "($\vdash \mbox{cont}$)"
\epf
\end{center}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Various Binary Orderings -- $\cutord{}{}$}
  \end{Heading}

We define a well-founded ordering $\cutord{}{}$.

For cut-elimination, $\cutord{\Pi_1}{\Pi_0}$ iff 
(informally, the cut at the bottom of $\Pi_1$ is closer to being eliminated
than that at the bottom of $\Pi_0$) 
iff any of

  (a) the bottom inference of $\Pi_1$ is
    not cut, but that of $\Pi_0$ is

  (b) the size of the cut-formula of
    $\Pi_1$ is smaller than that of $\Pi_0$, or

  (c) $\Pi_1$ and $\Pi_0$ have the same cut-formula, and either 
    
    \quad (i) the cut in $\Pi_1$ is left-
    \emph{or} right-principal, and the cut in $\Pi_0$ is neither, or

  % (c) (ii) 
    % $\Pi_1$ and $\Pi_0$ have the same cut-formula,
    \quad (ii) the cut in $\Pi_1$ is \emph{both} left- \emph{and}
    right-principal, and the cut in $\Pi_0$ is not.
  % both left- and right-principal.

Clearly $\cutord{}{}$ is well-founded.

\comment{
\begin{enumerate}
  \item\label{defn:porders-dt-1} the bottom inference of $\Pi_1$ is
    not cut, but that of $\Pi_0$ is
  \item\label{defn:porders-cut-1} the size of the cut-formula of
    $\Pi_1$ is smaller than that of $\Pi_0$, or
  \item\label{defn:porders-LRP-1}
    $\Pi_1$ and $\Pi_0$ have the same cut-formula,
    the cut in $\Pi_1$ is left-principal
    or right-principal, and the cut in $\Pi_0$ is neither, or
  \item\label{defn:porders-LRP-2} 
    $\Pi_1$ and $\Pi_0$ have the same cut-formula,
    the cut in $\Pi_1$ is (left- and
    right-)principal, and the cut in $\Pi_0$ is not (left- and
    right-)principal.
\end{enumerate}
}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Generalise to Term Rewriting}
  \end{Heading}

 Have a language for defining first-order ``terms'', such as
   $f (a, g (b, c))$ 

 Have a collection of rewrite rules:
  $\{ l_1 \rightarrow r_1, \cdots , l_n \rightarrow r_n\}$
  in which can substitute for variables

  We consider the rewrite relation \emph{after} substitution -- 
  call it $\rho$

  \emph{closure} under \emph{contexts}
  of relation $\rho$ \quad(eg, if $l \stackrel\rho\longrightarrow r$ then 
  $C[l] \longrightarrow C[r]$) 

 Question: Does this rewriting process terminate for all terms?

 An ordering $<_{cut}$ must be defined, depending on the problem. \\
Typically, it looks at or near the head of the term (root of the tree)).

 \comment{
 Example: Ackermann's function: 

 \begin{eqnarray*}
 A(0, y) & \longrightarrow & S(y) \\
 A (S(x), 0) & \longrightarrow & A(x, S(0)) \\
 A (S(x), S(y)) & \longrightarrow & A(x, A (S(x), y)) 
 \end{eqnarray*}
 }
 
\end{slide}

\begin{slide}
  \begin{heading}
    {Defining Reductions}
    {and Strongly Normalising Terms}
  \end{heading}

  \begin{definition}
    Assuming a relation $\rho$,
    term $t_0$ \emph{reduces} to term
    $t_1$ if either
  % \begin{itemize}
  % \item[(a)] 
  
 (a)  $(t_1, t_0) \in \rho$, or
  % \item[(b)]
  
  (b) $t_0$ and $t_1$ are identical except that exactly one
       proper subterm of $t_0$ reduces to the
       corresponding proper subterm of $t_1$.
  % \end{itemize}
  \end{definition}

 % We shall later define $\rho$ as a system of rewriting rules 
 % $\{(r_1, l_1), (r_2 , l_2), \cdots \}$

    {(this is the closure of $\rho$ under context)}
\comment{
 Intuition: a reduction is due to a rewrite $l \rightarrow r$ at the
 top level or happens at some deeper level.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Strongly Normalising Terms}
  \end{Heading}
  }
  
  \begin{definition}
    The set \emph{$\SN$} is the {smallest} set of terms
    such that:
  % \begin{itemize}
  % \item[(a)] 

  (a) if $t_0$ cannot be reduced then $t_0 \in \SN$ 
  % \item[(b)] 
  
  (b) if every term $t_1$ to which $t_0$ reduces is in $\SN$ then $t_0 \in \SN$
  % \end{itemize}
  
  A term is \emph{strongly normalising} iff it is a member of $\SN$.
  \end{definition}

  Usual definition is: a term $t$ is in $\SN$ iff there is no infinite
  sequence of reductions starting with $t$.  
  These two definitions are equal in classical logic.
\end{slide}

\begin{slide}
  \begin{heading}
    {Various Binary Orderings -- $\snoneord{}{}$, etc}
  \end{heading}

\begin{enumerate}

\item\label{defn:porders-sn1} $\snoneord{t_1}{t_0}$ 
  if $t_0$ and $t_1$ are the same except that one of the \emph{immediate} 
  subterms of  $t_0$ is strongly normalising and reduces to the 
  corresponding \emph{immediate} subterm of $t_1$.
  
\item\label{defn:porders-sn2} ${t_1} <_{sn2} {t_0}$ -- as above,
  except put \emph{proper} for \emph{immediate}

\item\label{defn:porders-dt} 
  $\dtord{t_1}{t_0}$\quad iff 
   \quad$\cutord{t_1}{t_0}$\quad or \quad$\snoneord{t_1}{t_0}$.

\end{enumerate}

  Despite notation, these relations need \textit{not} be transitive.  
  
  Intuitively, $t_1 <_{dt} t_0$ means that
  $t_1$ is closer to a normal form (being cut-free)
  (in some sense) than is $t_0$.

Necessarily, $<_{sn1} \subseteq <_{sn2}$, both are well-founded.

We need to be able to prove that 
  $\dtord{}{}\ =\ \cutord{}{} \cup \snoneord{}{}$
is well-founded.

Use lemma on the union of well-founded orderings.

\end{slide}

\begin{slide}
\begin{Heading}
{Union of Well-Founded Relations}
\end{Heading}
\begin{lemma} \label{wf-rs}
Let $\tau$ and $\sigma$ be well-founded relations.
Then each of the following implies that 
$\tau \cup \sigma$ is 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}

{(d)} is from Doornbos \& von Karger; other conditions imply {(d)}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Conditions on the rewrite relation $\rho$}
  \end{Heading}
  
\begin{condition}\label{rpc}
For all $(r, l) \in \rho$,
if all proper subterms of $l$ are in \SN\ then, \\
for all subterms $r'$ of $r$, either 
\comment{
  $$ (a) \quad r' \in \SN 
    \qquad \qquad \mbox{or} \qquad \qquad
  (b) \quad r' <_{dt}^+ l$$
  }

  (a)$ \quad r' \in \SN $
  \qquad \mbox{or} \qquad 
  (b)$ \quad r' <_{dt}^+ l$
\end{condition}

Condition~\ref{rpc1} is simpler and implies Condition~\ref{rpc}
\begin{condition}\label{rpc1}
For all $(r, l) \in \rho$,
for all subterms $r'$ of $r$, either 

  (a)\quad  $r'$ is a proper subterm of $l$ 
  % (or is a subterm of a reduction of a proper subterm of $l$)
  (or is a reduction of a proper subterm of $l$)

  (b)\quad  $r' <_{cut} l$

  (c)\quad  $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm.

\comment{
\begin{enumerate}
  \item \label{rpc-srp} $r'$ is a proper subterm of $l$ \\
  % (or is a subterm of a reduction of a proper subterm of $l$)
  \item \label{rpc-cut} $r' <_{cut} l$
  \item \label{rps} 
  $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm.
\end{enumerate}
}
\end{condition}

For assuming that all proper subterms of $l$ are in \SN\,
then Condition~\ref{rpc1}(a) implies that $r' \in \SN$, and
\ref{rpc1}(c) implies that $r' <_{sn1} l$, so
$r' <_{dt}^+ l$.

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

\begin{slide}
  \begin{Heading}
    {Key Properties of Cut-Elimination Reductions}
  \end{Heading}
  
  When we apply a reduction to a cut at the bottom of a tree
  $\Pi_0$, obtaining $\Pi_1$,
  then every subtree $\Pi_1^s$ of $\Pi_1$ which has cut at the bottom
  satisfies one of
  \begin{itemize}
  \item $\Pi_1^s$ is a proper subtree of $\Pi_0$
    (any cut-formula, any number of copies),
    (Condition~\ref{rpc1}(a)) or 
  \item $\cutord{\Pi_1^s}{\Pi_0}$ (Condition~\ref{rpc1}(b)),
  because
  \begin{itemize}
  \item (principal reduction) 
   the cut-formula of $\Pi_1^s$ is smaller than that of $\Pi_0$
  \item (parametric reduction) 
   $\Pi_1^s$ and $\Pi_0$ have the same cut-formula and
    ${\Pi_1^s}$ is principal on more sides than ${\Pi_0}$.
  \end{itemize}
  \end{itemize}
\end{slide}

  \comment{
  \begin{Heading}
    {Generalisation}
  \end{Heading}
  Instead of tree, any term $f (a, g (b, c))$ 

  Relation $\rho$ (eg, $l \longrightarrow r$),
  and its \emph{closure} under \emph{contexts}
  ($C[l] \longrightarrow C[r]$) 

  This is a rewrite relation \emph{after} substitution
  }

\begin{slide}
  \begin{Heading}
    {Inductive Strong Normalisation}
  \end{Heading}

Recall $t \in \SN$ iff $t$ is strongly normalising. 

We define \ISN:\\
$t \in \ISN$ 
if $t$ inherits strong normalisation from its immediate subterms.

\begin{definition}
  $t \in \ISN$ iff: if all the immediate subterms
  of $t$ are strongly normalising then $t$ is strongly
  normalising.
\end{definition}


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

Proof: The immediate subterm relation is well-founded. \\
The result is proved using well-founded induction.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Strong-Normalisation Proof -- outline}
  \end{Heading}
  
  \begin{lemma}\label{dtho}
  Assume that the rewrite relation satisfies Condition 1 or 2.
    For a given term $t_0$, if all terms
    ${t'} <_{dt}^+ {t_0}$ are in \ISN, then so is $t_0$.
  \end{lemma}

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

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

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

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

\noindent and we show that $t_0 \in \SN$.
To show this, let $t_0$ reduce to $t_1$, show $t_1 \in \SN$. \ldots

\begin{theorem} \label{thm:all-sno}
    If $\rho$ satisfies Condition~\ref{rpc}
    and $\dtord{}{} \ = \ \cutord{}{} \cup \snoneord{}{}$
    is well-founded, then 
    every term is strongly normalising.
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dtho} that
every term is in \ISN; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}

\begin{slide}
  \begin{Heading}
    {Strong-Normalisation Proof}
  \end{Heading}
  
  \begin{lemma}\label{dth}
  Assume that the rewrite relation satisfies Condition 1 or 2.
    For a given term $t_0$, if all terms
    $\dtord{t'}{t_0}$ are in \ISN, then so is $t_0$.
  \end{lemma}

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

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

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

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

\noindent and we show that $t_0 \in \SN$.
To show this, let $t_0$ reduce to $t_1$, show $t_1 \in \SN$.

Two cases:
reduction occurs in a proper subterm of $t_0$, 
or of $t_0$ as a whole.

Reduction in a proper subterm of $t_0$ (which is in \SN, by (b)): 

So $\snoneord{t_1}{t_0}$ and $\dtord{t_1}{t_0}$.
Therefore $t_1 \in \ISN$ by assumption (a). %~\ref{ass1}. 

\end{slide}

\begin{slide}
  \begin{heading}
    {Strong-Normalisation Proof (ctd)}
  \end{heading}
Now each immediate subterm of $t_1$ is equal to, or is a reduction of,
an immediate subterm of $t_0$,
which itself is in \SN\ by assumption (b). %~\ref{ass2}.

All immediate subterms of $t_1$ are therefore in \SN. \\
Then, as $t_1 \in \ISN$, we have $t_1 \in \SN$.

$({t_1}, {t_0}) \in \rho$:
By Condition~\ref{rpc},
subterms of $t_1$ are either in \SN\ \\
or are $<_{dt}^+$-smaller than $t_0$ (and so in \ISN, by (a)).

That is, every subterm $t_1^s$ of $t_1$ (including
$t_1$ itself) is in \ISN, \\
so $t_1 \in \SN$ by Lemma~\ref{hereds-sn}.

\begin{theorem} \label{thm:all-sn}
    If $\rho$ satisfies Condition~\ref{rpc}
    and $\dtord{}{} \ = \ \cutord{}{} \cup \snoneord{}{}$
    is well-founded, then 
    every term is strongly normalising.
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dth} that
every term is in \ISN; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}

\begin{slide}
 \begin{Heading}
   {Multiset Order}
 \end{Heading}
 \begin{description}
 \item[$\rho$:] is an irreflexive relation on some given set $E$
 \item[$A, B, C$:] finite multisets of elements of $E$
 \item[$A \sqcup B$:] means multiset union
 \item[$<_{m1}$:] % $(\forall C)(\forall b \in E)$
		     if $\forall c \in C, c <_{\rho} b$,
		     then $C \sqcup A <_{m1} \{b\}\sqcup A$
 \item[Multisets as trees:] two types of nodes $I$nternal and $L$eaf nodes
 \item[Rewrite:] $L(b) \longrightarrow I(L(c_1), \cdots , L(c_k))$
 \item[$<_{cut}$:]\qquad $L(x) >_{cut} L(y)$ iff $x >_{\rho} y$ 
		   \qquad \qquad 
		   $L(x) >_{cut} I(y)$
 \item[Theorem:] For $\rho$ well-founded, derived $<_{m1}$ is
 well-founded on finite multisets.
 \end{description}


\end{slide}

\begin{slide}
  \begin{Heading}
    {Example - Ackermann's function}
  \end{Heading}
\begin{eqnarray*}
A(0, y) & \longrightarrow & S(y) \\
A (S(x), 0) & \longrightarrow & A(x, S(0)) \\
A (S(x), S(y)) & \longrightarrow & A(x, A (S(x), y)) 
\end{eqnarray*}
We define $<_{cut}$ by
\begin{eqnarray}
\label{Acut1} A(x, y) & >_{cut} & S(z) \\
\label{Acut2} A (S(x), y) & >_{cut} & A(x, z) \\
\label{Acut3} A (x, S(y)) & >_{cut} & A(x, y) 
\end{eqnarray}
Clearly $>_{cut}$ is well-founded
using the lexicographic ordering on arguments.

% For each $(r', l)$, 
For $l \rightarrow r$ and $r'$ a subterm of $r$, 
either $l >_{cut} r'$ or $r'$ is a proper subterm of $l$.

\end{slide}

\begin{slide}
  \begin{heading}
    {Ackermann's function -- $<_{cut} \cup <_{sn2}$ is well-founded}
  \end{heading}

To show $<_{cut} \cup <_{sn1}$ is well-founded, 
we show $<_{cut} \cup <_{sn2}$ (larger) is well-founded,
using Lemma~\ref{wf-rs}\ref{tco} --
we show $<_{cut} \circ <_{sn2} \ \subseteq\ 
  <_{sn2}^* \circ <_{cut}$.

For suppose $t >_{cut} u >_{sn2} v$.
If $t >_{cut} u$ by rule (\ref{Acut1}),
$t = A(x, y)>_{cut} S(z) >_{sn2} S(z') = v$ and so
$t >_{cut} v$ (by rule (\ref{Acut1}))

If $t >_{cut} u$ by rule (\ref{Acut2}), 
$t = A (S(x), y) >_{cut} A(x, z) = u$.  
Cases for $u >_{sn2} v$:

$u = A (x, z) >_{sn2} A(x, z') = v$ where $z \longrightarrow z'$, in which case $t >_{cut} v$, or 

$u = A (x, z) >_{sn2} A(x', z) = v$ where $x \longrightarrow x'$ % WRONG and $x \in \SN$,
by reducing a $SN$ subterm of $x$,
in which case $t = A (S(x), y) >_{sn2} A (S(x'), y) >_{cut} A(x', z) = v$.

The case for rule (\ref{Acut3}) is similar.

So $<_{cut} \cup <_{sn2}$ is well-founded,
by Lemma~\ref{wf-rs}\ref{tco}.
Therefore the system terminates by Theorem~\ref{thm:all-sn}.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Example - Distributive and Associative laws}
  \end{Heading}

$$
\begin{array}{rcl@{\qquad}rcl}
D(x + y) & \longrightarrow & Dx + Dy &
(x \times y) \times z & \longrightarrow & x \times (y \times z) \\
D(x \times y) & \longrightarrow & x \times Dy + Dx \times y &
(x + y) + z & \longrightarrow & x + (y + z) \\
x \times (y + z) & \longrightarrow & x \times y + x \times z & & &
\end{array}
$$
To use our proof, add
the following simplification rules as rewrite rules:
$$
x + y \longrightarrow x \qquad
x + y \longrightarrow y \qquad
x \times y \longrightarrow x \qquad
x \times y \longrightarrow y
$$
  
Define $<_{cut}$ by 
$<_{cut} \ = \ <_h \cup <_\times \cup <_+$, where

$\bullet$
$D(x) >_h y \times z \qquad D(x) >_h y + z \qquad x \times y >_h z + w$ 

$\bullet$
for an immediate subterm $x'$ of $x$, 
$x + y >_+ x' + z$ and $x \times y >_\times x' \times z$
% \item $<_{cut} = (<_h \cup <_\times \cup <_+)$.

Clearly $<_{cut}$ is well-founded.

\end{slide}

\begin{slide}
  % \begin{heading}
    % {Example - Distributive and Associative laws (ctd)}
  % \end{heading}

To show $<_{cut} \cup <_{sn1}$ is well-founded, 
we show $<_{cut} \cup <_{sn2}$ (larger) is well-founded,
using Lemma~\ref{wf-rs}\ref{tco} --
we show $<_{cut} \circ <_{sn2} \ \subseteq\ 
  <_{sn2}^* \circ <_{cut}$.

Suppose $t >_{cut} u >_{sn2} v$.
If $t >_h u$ then clearly $t >_h v$.

If $x \times y >_\times x' \times z >_{sn2} x' \times w$, then 
$x \times y >_\times x' \times w$.

If $x \times y \ >_\times \ x' \times z >_{sn2} w' \times z$,~
then, for some $w$, \\ 
~~ $x \times y >_{sn2} w \times y \ >_\times \ w' \times z$ ~
(would not hold for $>_{sn1}$)

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

Look at all pairs $(r', l)$,
where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$. 

Mostly $l >_h r'$, or $r'$ is a proper subterm of $l$.

For the associative rewrite rules 
$l >_\times r$ or $l >_+ r$, by definition. 

Cases like $(r', l) = (D(x), D(x + y))$ : 
Since $x + y \longrightarrow x$, and \\
proper subterm $x + y$ of $l$ is assumed \SN,
have $D(x + y) >_{sn1} D(x)$.

Thus the system terminates by Theorem~\ref{thm:all-sn}.

\end{slide}

% \newcommand{\cons}{\textit{cons}}
\newcommand{\cons}{}
% \newcommand{\nil}{\textit{nil}}
\newcommand{\nil}{{[\ ]}}
\newcommand{\sort}{\textit{sort}}
\newcommand{\ins}{\textit{insert}}
\newcommand{\choo}{\textit{choose}}
\begin{slide}
  \begin{Heading}
    {Example - insertion sort}
  \end{Heading}
  \vspace{-5ex}
\begin{eqnarray*}
\sort\ (\nil) & \longrightarrow & \nil \\
\sort\ (\cons x : y) & \longrightarrow & \ins \ (x, \sort \ (y)) \\
\ins \ (x, \nil) & \longrightarrow & \cons x : \nil \\
\ins \ (x, \cons v : w) & \longrightarrow &
  \choo \ (x, \cons v : w, x, v) \\
\choo \ (x, \cons v : w, y, 0) & \longrightarrow &
  \cons x : \cons v : w \\
\choo \ (x, \cons v : w, 0, s(z)) & \longrightarrow &
  \cons v : \ins \ (x, w) \\
\choo \ (x, \cons v : w, s(y), s(z)) & \longrightarrow &
  \choo \ (x, \cons v : w, y, z) 
\end{eqnarray*}
\comment{
\begin{eqnarray*}
\sort\ (\nil) & \longrightarrow & \nil \\
\sort\ (\cons \ (x, y)) & \longrightarrow & \ins \ (x, \sort \ (y)) \\
\ins \ (x, \nil) & \longrightarrow & \cons \ (x, \nil) \\
\ins \ (x, \cons \ (v, w)) & \longrightarrow &
  \choo \ (x, \cons \ (v, w), x, v) \\
\choo \ (x, \cons \ (v, w), y, 0) & \longrightarrow &
  \cons \ (x, \cons \ (v, w)) \\
\choo \ (x, \cons \ (v, w), 0, s(z)) & \longrightarrow &
  \cons \ (v, \ins \ (x, w)) \\
\choo \ (x, \cons \ (v, w), s(y), s(z)) & \longrightarrow &
  \choo \ (x, \cons \ (v, w), y, z) 
\end{eqnarray*}
}
To define $>_{cut}$, first define $>_h \ \subseteq \ >_{cut}$,
depending on the head symbol,
using this (transitive) order on symbols:
$\sort > \{\ins, \choo\} > \cons$.

As the rules define \ins\ and \choo\ in terms of each other, we define
$$
\begin{array}{c}
\ins \ (x, w) >_{cut} \choo \ (y, w, a, b) >_{cut} \ins \ (x, w') \\
\choo \ (y, w, a, b) >_{cut} \choo \ (y', w, a', b') 
\end{array}
$$
where % $>_{cut}$ is transitive and
$w',a'$ are immediate subterms of $w,a$.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Example - insertion sort, ctd}
  \end{Heading}
It is easy to see that $>_{cut}$ is well-founded.

We add a simplification rule 
$\qquad \cons \ x : y \longrightarrow y$
%  where $l = \sort\ (\cons \ (x, y)) >_{sn1} \sort \ (y) = r'$.

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

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

Compare the ordering $<_{cut}$ with Example 13 in 
Hirokawa \& Middeldorp, Dependency Pairs Revisited, RTA-04.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Example - the modified factorial example}
  \end{Heading}

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

$>_h$ (transitive), on terms, based on head symbol: $ F > \times > + > S$.

If $s >_{h} t$, then $s >_{cut} t$; also 
$$F(S(x)) >_{cut} F(P(S(x))) \qquad F(S(x)) >_{cut} F(P(x))$$

Cannot use simplification ordering as
rule $P(x) \longrightarrow x$ gives non-termination.

We do, however, add the rule $S(x) \longrightarrow x$.

\end{slide}

\begin{slide}
  \begin{Heading}
    {modified factorial -- checking the rules}
  \end{Heading}

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

Now for each $(r', l)$ where 
$l \rightarrow r$ and $r'$ is a subterm of $r$, 
\begin{itemize}
\item $r'$ is a proper subterm of $l$
\item $r' <_h l$
\item $r'$ is $l$, but with $S$ removed from a subterm
  (to give $r' <_{sn1} l$)
\item $r'$ is $F(P(S(x)))$ and $l$ is $F(S(x))$
  (so $r' <_{cut} l$).
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    {modified factorial -- $<_{cut} \cup <_{sn2}$ is well-founded}
  \end{heading}

Clearly $<_{cut}$ is well-founded.
To show that $<_{cut} \cup <_{sn2}$ is well-founded
use Lemma~\ref{wf-rs}\ref{dvk}.
We show 
$<_{cut} \circ <_{sn2} \ \subseteq\ (<_{sn2}^* \circ <_{cut}) \cup <_{sn2}^+$.

Suppose $t >_{cut} u >_{sn2} v$.
If $t >_h u$ then clearly $t >_h v$.  Otherwise:

Suppose $t = F(S(x))$ and $u = F(P(S(x)))$ or $u = F(P(x))$. \\
If $u >_{sn2} v$ by reducing $x$ in $u$ to $x'$,
% (reducing a strongly normalising subterm of $x$),
then % we have $x \in \SN$ and so 
$t = F(S(x)) >_{sn2} F(S(x')) >_{cut} v$.

Otherwise we need to consider specific cases:
$$
\begin{array}{c@{}c@{}c@{}c@{}c@{\quad}c}
t & >_{cut} & u & >_{sn2} & v & \\[1ex]
F(S(x)) & & F(P(S(x))) & & F(P(x)) & t >_{cut} v \\[1ex]
F(S(x)) & & F(P(S(x))) & & F(x) & t >_{sn2} v \\[1ex]
F(S(S(y))) & & F(P(S(y))) & & F(y) & t >_{sn2}^+ v 
\end{array}
$$
\comment{
\begin{itemize}
\item $u = F(P(S(x)))$, $S(x) \longrightarrow x$ where $S(x) \in \SN$,
  $v = F(P(x))$:
  then $t >_{cut} v$
\item $u = F(P(S(x)))$, $P(S(x)) \longrightarrow x$ where $P(S(x)) \in \SN$,
  $v = F(x)$: here, as $S(x) \longrightarrow x$ and $S(x) \in \SN$,
  we have $t >_{sn2} v$
\item $u = F(P(x))$, where $x = S(y)$, 
  $P(S(y)) \longrightarrow y$ and $P(S(y)) \in \SN$, $v = F(y)$:
  here, as $S(y) \longrightarrow y$ and $S(y) \in \SN$,
  we have $t = F(S(S(y)) >_{sn2} F(S(y)) >_{sn2} F(y) = v$.
\end{itemize}
}

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

\end{slide}

\begin{slide}
  \begin{heading}
    {Recursive Path Orderings}
  \end{heading}

Lexicographic ordering $lex\ \sigma$
(fixed-length sequences), well-founded if $\sigma$ is.

Given well-founded partial order $\rho$ on function symbols,
the lexicographic path ordering $lpo\ \rho$ or $<_{lpo}$
defined by (where $<_{lex}$ is $lex\ (lpo\ \rho)$)
$$
\frac {
s_i \geq_{lpo} t } { f(s_1, \ldots, s_m) >_{lpo} t }
\qquad
\frac {
f >_\rho g \qquad \forall i \in \{1, \ldots, n\}.\ f(s_1, \ldots, s_m) >_{lpo} t_i
 } { f(s_1, \ldots, s_m) >_{lpo} g(t_1, \ldots, t_n) }
 $$ 
 
 $$
\frac {
(s_1, \ldots, s_m) >_{lex} (t_1, \ldots, t_m) \qquad 
  \forall i \in \{1, \ldots, m\}.\ f(s_1, \ldots, s_m) >_{lpo} t_i
 } { f(s_1, \ldots, s_m) >_{lpo} f(t_1, \ldots, t_m) }$$

Definition and proof for the multiset path ordering similar.

\begin{lemma} \label{lem-subt-lpo}
If $s >_{lpo} g(t_1, \ldots, t_n)$ then $s >_{lpo} t_j$,
for all $j \in \{1, \ldots \, n\}$.
\end{lemma}
(follows from transitivity of $>_{lpo}$, but we don't prove that) \\
Proof: Induction on the size (or structure) of $s$.

\end{slide}
\begin{slide}

\begin{theorem}
If $\rho$ (on function symbols) is well-founded, then so is $<_{lpo}$.
\end{theorem}

Proof:
We first define $<_{cut}$ using 
$<_h$ as usual, and defining $<_{lw1}$:
\begin{itemize}
\item $f(\overline{s}) >_h g(\overline{t})$ iff $f >_\rho g$
\item if $((\overline{t}), (\overline{s})) \in lex\ (f\!w\!f\ 
  (lpo\ r))$, then $f(\overline{t}) <_{lw1} f (\overline{s})$ \\
\item   $<_{cut}\ =\ (<_h \cup <_{lw1})$.  
\end{itemize}

$f\!w\!f\ (lpo\ r)$ means reducing only SN terms, like in $<_{sn1}$, \\
so $f\!w\!f\ (lpo\ r)$, $lex\ (f\!w\!f\ (lpo\ r))$ and 
$<_{lw1}$ are well-founded. 

As \mbox{$<_h \circ\ <_{lw1} \, \subseteq\ \, <_h$},
$<_{cut}$ is well-founded, by Lemma~\ref{wf-rs}.
Further, $<_{sn1}\ \subseteq <_{lw1}$, so $<_{cut} \cup <_{sn1}\ =\ 
<_{cut}$ is well-founded.

\end{slide}

\begin{slide}

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

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

Now suppose $l >_{lpo} r'$ by the second or third rules. \\
Assuming that proper subterms of $l$ are in \SN, we have $r' <_{cut} l$.

Thus the system terminates by Theorem~\ref{thm:all-sn}.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Applications of the theorem}
  \end{Heading}

Can use the theorem to prove termination 
\begin{itemize}
\item of recursive path orderings
\item of Knuth-Bendix orderings
\item where dependency pairs method applies 
(conversely, lemmas used in dependency pairs work
give short proof of our result) 
\end{itemize}
  
\end{slide}

\begin{slide}
  \begin{Heading}
    {Extension to non-monotonic orderings}
  \end{Heading}

Consider a relation $\rho$ \emph{not} necessarily monotonic 
(closed under contexts).
So ``strongly normalising'' and ``\SN'' mean for $\rho$, not its closure
under contexts.

\begin{condition}\label{cond-nr}
For all $(r, l) \in \rho$,
if all proper subterms of $l$ are in \SN\ then, \\
for all subterms $r'$ of $r$, either 

  (a)$ \quad r' \in \SN $ (eg, $(r', l') \in \rho^*$ for some proper subterm
  $l'$ of $l$)
  % \qquad \mbox{or} \qquad 

  (b)$ \quad r' <_{cut} l$
\end{condition}

\begin{theorem} \label{thm:all-sn-nr}
    If $\rho$ satisfies Condition~\ref{cond-nr}
    and $\cutord{}{}$ is well-founded, then 
    $\rho$ is well-founded.
\end{theorem}
\end{slide}

\end{document}