% AUTOMATICALLY GENERATED FILE - DO NOT EDIT
% GENERATED OMITTING TAGS math change


\section{A Proof of Strong Normalization}
\label{s-sn}
\cc{sn.tex}
\cc{s-sn}

We provide a proof of strong normalization which overcomes the
problems described in \S\ref{s-wsn}.

We use the same definition of reduction as does Wansing
\cite[\S4.2, \S4.3]{wansing-displaying-modal-logic}.
Given a derivation tree with (\emph{cut}) at its root, 
changes can be made to the tree to deal with that particular cut;
we call these ``cut-reductions''.
Following Wansing \cite[\S 4.2]{wansing-displaying-modal-logic},
we can classify these cut-reductions as 
primitive or parametric.
We define and discuss these later.
More generally, we can change a tree by performing a cut-reduction
on any subtree; we call such changes \emph{reductions}.

\begin{definition}[\texttt{reduces}] 
Assuming a relation \texttt{cutReduces} (to be defined later)
a derivation tree $\Pi_0$ \texttt{reduces} to a 
derivation tree $\Pi_1$ if either
\begin{enumerate}
\item $\Pi_0$ \texttt{cutReduces} to $\Pi_1$, or
\item $\Pi_0$ and $\Pi_1$ are the same, except that
exactly one of the immediate subtrees of $\Pi_0$ reduces to 
the corresponding immediate subtree of $\Pi_1$
\end{enumerate}
\end{definition}



Wansing \cite[p.~52]{wansing-displaying-modal-logic}
defines a \emph{strongly normalizable} derivation tree as
a tree from which every sequence of reductions is finite.
We define inductively the set of strongly normalizable derivation trees.
\footnote{What
   about, let \texttt{sn\_set} be the smallest set such that for every
   derivation $\Pi_0$, as soon as every one step reduct $\Pi_1$ is in 
 \texttt{sn\_set}, $\Pi_0$ itself is in \texttt{sn\_set}~?
 HOW ABOUT MINE ?}



\begin{definition}[\texttt{sn\_set}] 
A derivation tree $\Pi_0$ is \emph{strongly normalizable} if it is
a member of \texttt{sn\_set}, which we define to be the smallest set of 
trees such that
\begin{enumerate}
\item If $\Pi_0$ cannot be reduced to another tree $\Pi_1$, 
  then $\Pi_0 \in \texttt{sn\_set}$.
\item If, for every tree $\Pi_1$ to which $\Pi_0$ can be reduced,
  $\Pi_1 \in \texttt{sn\_set}$,
  then $\Pi_0 \in \texttt{sn\_set}$.
\end{enumerate}
\end{definition}

This definition uses Isabelle's inductive definition feature.
This defines the minimal set closed under the given rules.
For example, defining a set $\mathcal S$ of natural numbers 
using the rules $\{0 \in \mathcal S, n \in \mathcal S \Longrightarrow 
n+2 \in \mathcal S\}$ defines the set of even naturals
(although the set of all naturals also satisfies the rules).
For more details, see \cite[\S 2.10]{IsLogHOL}
\footnote{We could move this para above the definition}



To prove that every derivation tree is strongly normalizable, we first
define a binary relation \texttt{dtorder} on derivation trees,
and show that it is well-founded. 


\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{\texttt{\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{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}

\begin{definition}[\texttt{LRPorder}, \texttt{cutorder}, 
  \texttt{sn1order}, \texttt{dtorder}]
  \label{defn:porders}
We define four binary relations, 
\texttt{LRPorder}, \texttt{cutorder}, 
\texttt{sn1order} and \texttt{dtorder}
on derivation trees. 
We define them, as sets of ordered pairs, by:
\begin{enumerate}

\item\label{defn:porders-LRP} $\LRPord{\Pi_1}{\Pi_0}$ if the
  bottom inferences of derivations $\Pi_1$ and $\Pi_0$ are both
  (\emph{cut}), and either
  \begin{enumerate}
  \item\label{defn:porders-LRP-1} 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} the cut in $\Pi_1$ is (left- and
    right-)principal, and the cut in $\Pi_0$ is not.
  \end{enumerate}
%then $(\Pi_1, \Pi_0) \in \texttt{LRPorder}$.
%then $\pordered{\Pi_1}{LRP}{\Pi_0}$.
\item\label{defn:porders-cut} $\cutord{\Pi_1}{\Pi_0}$ if the
  bottom inferences of derivations  $\Pi_1$ and $\Pi_0$ are both
  (\emph{cut}), and if either
  \begin{enumerate}
  \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-cut-2} each derivation has the same cut-formula,
%and $(\Pi_1, \Pi_0) \in \texttt{LRPorder}$,
    and $\LRPord{\Pi_1}{\Pi_0}$.
  \end{enumerate}
%then $(\Pi_1, \Pi_0) \in \texttt{cutorder}$.
%  then $\pordered{\Pi_1}{cut}{\Pi_0}$.
\item\label{defn:porders-sn1} $\snoneord{\Pi_1}{\Pi_0}$ if
$\Pi_0$ and $\Pi_1$ are the same\footnote{Do they have to end in cut? NO}
except that one of the immediate subtrees of $\Pi_0$ is strongly
normalizable and reduces to the corresponding immediate subtree of
$\Pi_1$.
%, then
%  $(\Pi_1, \Pi_0) \in \texttt{sn1order}$.
%  $\pordered{\Pi_1}{sn1}{\Pi_0}$.
\item\label{defn:porders-dt}
%$(\Pi_1, \Pi_0) \in \texttt{dtorder}$ iff any
$\dtord{\Pi_1}{\Pi_0}$ iff any
  of the following hold:
\begin{enumerate}
\item\label{defn:porders-dt-1} the bottom inference of $\Pi_1$ is not
(\emph{cut}),
but that of $\Pi_0$ is
% \item $(\Pi_1, \Pi_0) \in \texttt{cutorder}$
% \item $(\Pi_1, \Pi_0) \in \texttt{sn1order}$
\item\label{defn:porders-dt-2} $\cutord{\Pi_1}{\Pi_0}$
\item $\snoneord{\Pi_1}{\Pi_0}$.
\end{enumerate}




\end{enumerate}
\end{definition}



We can then prove in turn the following theorems,
which are relatively straightforward.
Note that, despite the terminology, these relations are not 
reflexive, and not all transitive.
But the intuition is that
$(\Pi_1, \Pi_0) \in \texttt{dtorder}$ means that $\Pi_1$ is closer
to being cut-free (in some sense) then $\Pi_0$.\footnote{added - JED}

\begin{theorem}[\texttt{wf\_LRPorder, wf\_cutorder, wf\_sn1order}]
The relations 
\texttt{LRPorder}, \texttt{cutorder} and 
\texttt{sn1order} are well-founded.
\end{theorem}



To prove that \texttt{dtorder} is well-founded, we first 
need a result on the interaction between \texttt{cutorder} and
\texttt{sn1order}:


\begin{lemma}[\texttt{sntr'}]
\label{lemma:sntrprime}
If
$\pordered{\Pi_2}{cut}{\Pi_1}$ and
$\pordered{\Pi_1}{sn1}{\Pi_0}$ then
$\pordered{\Pi_2}{cut}{\Pi_0}$.
\end{lemma}



\begin{proof} \footnote{second proof - yours, you also left in a modified
version of my proof}
First note that the bottom inference of $\Pi_1$ is (\emph{cut}), and
$\pordered{\Pi_1}{sn1}{\Pi_0}$, so that the bottom inference of
$\Pi_0$ is (\emph{cut}) and has the same cut-formula.  Secondly,
$\cutord{\Pi_2}{\Pi_1}$ means either that $\Pi_2$ has a smaller
cut-formula than does $\Pi_1$, or that $\LRPord{\Pi_2}{\Pi_1}$.
Therefore, if $\pordered{\Pi_2}{cut}{\Pi_1}$ by virtue of the sizes
of their cut-formulae, then $\pordered{\Pi_2}{cut}{\Pi_0}$ for the
same reason.

Suppose, on the other hand, that $\pordered{\Pi_2}{LRP}{\Pi_1}$.
Since $\pordered{\Pi_1}{sn1}{\Pi_0}$, one immediate subtree
$\Pi_0^s$ of $\Pi_0$ reduces to a corresponding subtree of $\Pi_1$.
We consider cases for where this reduction took place:
\begin{itemize}

\item If the reduction is in a proper subtree of $\Pi_0^s$, then the
  reduction does not affect the lowest inference of $\Pi_0$, which
  we know to be a (\emph{cut}). Since $\Pi_1$ and $\Pi_0$ are
  identical except for this reduction, $\Pi_1$ is left-
  (right-)principal iff $\Pi_0$ is so.  Hence
  $\pordered{\Pi_2}{LRP}{\Pi_0}$.

\item If, on the other hand, $\Pi_0^s$ is the left (right) immediate
  subtree of $\Pi_0$ and therefore has (\emph{cut}) as its lowest
  inference, then $\Pi_0$ is not left- (right-) principal.
  Therefore if $\Pi_0^s$ is reduced to turn $\Pi_0$ into $\Pi_1$,
  and $\LRPord{\Pi_2}{\Pi_1}$, it
  follows that $\pordered{\Pi_2}{LRP}{\Pi_0}$.
\end{itemize}

In both cases,
$\pordered{\Pi_2}{cut}{\Pi_0}$.

\qed \end{proof}



\begin{theorem}[\texttt{wf\_dtorder}]
\texttt{dtorder} is well-founded.
\end{theorem}

\begin{proof}
It is easy to see that an infinite
\texttt{dtorder}-decreasing chain
$\Revdtord{\Pi_0}{\Revdtord{\Pi_1}{\Revdtord{\Pi_2}{\cdots}}}$
must contain either 
an infinite \texttt{sn1order}-decreasing chain
of trees whose bottom inference is not (\emph{cut}),
or an infinite chain
$\Pi_0, \Pi_1, \Pi_2, \ldots$
of trees whose bottom inference is (\emph{cut}) and
for each pair  $(\Pi_{i+1}, \Pi_i) $, either 
$\snoneord{\Pi_{i+1}}{\Pi_i}$ or
 $\cutord{\Pi_{i+1}}{\Pi_i}$.

As \texttt{sn1order} is well-founded, 
there is no infinite \texttt{sn1order}-decreasing
chain; therefore the chain contains infinitely many
pairs 
$\cutord{\Pi_{i+1}}{\Pi_i}$.
But intermediate pairs in \texttt{sn1order}
may be ``absorbed'' -- for example if also
$\snoneord{\Pi_i}{\Pi_{i-1}}$,
then by Lemma~\ref{lemma:sntrprime}, we have
$\cutord{\Pi_{i+1}}{\Pi_{i-1}}$.
Thus there is 
an infinite \texttt{cutorder}-decreasing chain,
contradicting that \texttt{cutorder} is well-founded. 
\qed \end{proof}



We next define \texttt{snHered}, a property of derivation trees, so
named for the idea that such a tree inherits strong normalization from
its immediate subtrees.

\begin{definition}[\texttt{snHered}] \label{snHered} 
A derivation tree $\Pi$ satisfies the property \texttt{snHered} iff
the following holds:
\begin{quote}
if all the immediate subtrees of $\Pi$ are
strongly normalizable then $\Pi$ is strongly normalizable.
\end{quote}
\end{definition}



The next lemma follows from this definition.

\begin{lemma}[\texttt{hereds\_sn}] \label{hereds-sn}
  A derivation tree $\Pi$ is strongly normalizable iff
  every subtree of $\Pi$ has the property \texttt{snHered}.
\end{lemma}



We intend to define cut-reduction in such a way as to enable us to
make some assertions about cut-reductions.  We first define properties
\texttt{nparRedP} and \texttt{c8redP} of reductions (which in fact
apply to parametric and primitive reductions respectively).
The definitions do not require that the bottom inference of the derivation be
\cut, but they are used only where this is so.

\begin{definition}[\texttt{nparRedP}]
\label{defn:nparRedP}
A derivation tree reduction from $\Pi_0$ to $\Pi_1$ satisfies \texttt{nparRedP}
if, for each subtree $\Pi_1^s$ of $\Pi_1$ 
whose bottom inference is (\emph{cut}), either 
\begin{enumerate}
\item $\Pi_1^s$ is a proper subtree of $\Pi_0$, or 
\item\label{defn:nparRedP-2} % $(\Pi_1^s, \Pi_0) \in \texttt{LRPorder}$,
    $\LRPord{\Pi_1^s}{\Pi_0}$,
and they have the same cut-formula.
\end{enumerate}
\end{definition}

It can be seen that, in the case of the
reductions shown in Figs.~\ref{fig-cut-br} and \ref{fig-cut-succ},
the cuts visible in those figures satisfy
Definition~\ref{defn:nparRedP}\ref{defn:nparRedP-2}.

\begin{definition}[\texttt{c8redP}]
\label{defn:c8redP}
Let the bottom inference of $\Pi_0$ be \cut.
A reduction from $\Pi_0$ to $\Pi_1$ satisfies \texttt{c8redP}
if, for each subtree $\Pi_1^s$ of $\Pi_1$ 
whose bottom inference is (\emph{cut}), either 
\begin{enumerate}
\item $\Pi_1^s$ is a proper subtree of $\Pi_0$, or 
\item\label{defn:c8redP-2} 
  the cut-formula of $\Pi_1^s$ is smaller than that of $\Pi_0$.
\end{enumerate}
\footnote{Presumably
  you mean ``than that of the lowest cut of $\Pi_0$''? the BOTTOM CUT}

\end{definition}

Note that both
Definition~\ref{defn:c8redP}\ref{defn:c8redP-2}
and Definition~\ref{defn:nparRedP}\ref{defn:nparRedP-2}
imply $(\Pi_1^s, \Pi_0) \in \texttt{dtorder}$.



We now define a \emph{cut-reduction} (being either parametric or primitive)
as satisfying one of the properties 
\texttt{nparRedP} and \texttt{c8redP}, as well as some further simple
conditions which help the proof.

\begin{definition}[\texttt{cutReduces}]
The derivation tree $\Pi_0$ \emph{cut-reduces} to $\Pi_1$ 
if the following hold:
\footnote{Is this a conjunction or disjuntion? CONJ
Also, does (c) imply (f)? ONLY IN A WELL-FORMED TREE}
\begin{enumerate}
\item $\Pi_0$ and $\Pi_1$ satisfy either 
\texttt{nparRedP} (for a parametric reduction) 
or \texttt{c8redP} (for a primitive reduction) 
\item $\Pi_0$ and $\Pi_1$ have the same conclusion
\item the bottom rule of $\Pi_0$ is (\emph{cut})
\item $\Pi_0$ $\not =$ $\Pi_1$
\item $\Pi_1$ does not consist solely of %an unproved leaf
      a non-axiomatic leaf
\item $\Pi_0$ has at least one immediate subtree 
\end{enumerate}
\end{definition}



Note that for the purposes of the proof of strong normalization, 
we have defined cut-reduction weakly in that,
for example, we do not require that
the new derivation tree \texttt{ptn} be well-formed 
(\texttt{allPT wfb ptn}) or use rules which belong to the calculus
(\texttt{allPT (frb rls) ptn}).
However the definition is also strong in that it requires that either
\texttt{nparRedP} or \texttt{c8redP} holds.
Later we will show that the reductions in which we are interested do
satisfy \texttt{nparRedP} or \texttt{c8redP}.
The result of this is that we prove strong normalization
for a larger class of reductions than we are really interested in.
(Clearly strong normalization for a larger class of reductions
implies strong normalization for a smaller class).



\begin{lemma}[\texttt{dth}] \label{dth}
\label{sn-siord}
For a given derivation $\Pi_0$, if all derivation trees
$\dtord{\Pi'}{\Pi_0}$ have the property \texttt{snHered}, then so
does $\Pi_0$.
\end{lemma}

\begin{proof}
\footnote{I've also changed this to use subscripts, except to avoid
  ambiguity - your version uses $\Pi'$ for two different things}
Given $\Pi_0$, assume that 
\begin{enumerate}
% \renewcommand\theenumi{(A\arabic{enumi})}
% \renewcommand\labelenumi{\theenumi}
\item \label{ass1}
  all derivation trees $\dtord{\Pi'}{\Pi_0}$ satisfy \texttt{snHered}, and 
\item \label{ass2}
  all immediate subtrees of $\Pi_0$ are strongly normalizable.
\end{enumerate}
We have to prove that $\Pi_0$ is strongly
normalizable, whence, by Definition~\ref{snHered},
it satisfies \texttt{snHered}.  Consider
possible cases for a reduction of $\Pi_0$, giving a tree $\Pi_1$.

Firstly, suppose that the bottom inference of $\Pi_0$ is not cut.
Then any reduction is in an immediate (strongly normalizable)
subtree of $\Pi_0$, and so $\snoneord{\Pi_1}{\Pi_0}$ 
and hence $\dtord{\Pi_1}{\Pi_0}$ by definition
\footnote{What ordering is $<$ DT and by which
  definition? DEFN OF dtorder}. 
Since all immediate subtrees of $\Pi_1$ are strongly normalizable 
(as they are equal to or are a reduction of immediate subtrees of $\Pi_0$,
which are strongly normalizable by assumption \ref{ass2}),
and \texttt{snHered} holds for $\Pi_1$ (by assumption \ref{ass1}), the
derivation $\Pi_1$ is strongly normalizable.

Secondly, suppose that the bottom inference of $\Pi_0$ is cut, and
consider a reduction.  This reduction is either parametric or
primitive. If it is in an immediate subtree, by the previous
argument, $\Pi_1$ is strongly normalizable.  If it is a reduction of
the bottom cut, we get the new tree $\Pi_1$ whose cuts are either in
copies of (strongly normalizable) proper subtrees of $\Pi_0$ or are
cuts which are smaller (in \texttt{dtorder})
than the bottom cut of $\Pi_0$ 
(see the remark following 
Definitions \ref{defn:nparRedP} and \ref{defn:c8redP}).
Thus every subtree $\Pi_1^s$ of $\Pi_1$ (including $\Pi_1$ itself)
satisfies one of the following:
\begin{enumerate}
\item $\Pi_1^s$ is a subtree of a proper subtree of $\Pi_0$
\item $\dtord{\Pi_1^s}{\Pi_0}$
\end{enumerate}

Now a subtree $\Pi_1^s$ satisfying (a) is strongly normalizable, and a
subtree $\Pi_1^s$ satisfying (b) satisfies \texttt{snHered}.  Thus
every $\Pi_1^s$ satisfies \texttt{snHered}.
% following seems wrong
% Since $\Pi_1$ was obtained
% via an arbitrary reduction, by structural induction, $\Pi_1$ is
% strongly normalizable.
Since $\Pi_1^s$ is
an arbitrary subtree of $\Pi_1$, 
if follows from Lemma~\ref{hereds-sn} that $\Pi_1$ is
strongly normalizable.

Thus in either case $\Pi_1$ is strongly normalizable.
Since $\Pi_1$ was obtained
via an arbitrary reduction from $\Pi_0$, it follows that 
$\Pi_0$ is strongly normalizable.
Thus we have that \texttt{snHered} holds for $\Pi_0$. 
\qed \end{proof}



\begin{theorem}[\texttt{all\_sn}]
Every derivation tree is strongly normalizable.
\end{theorem}

\begin{proof}
By well-founded induction, it follows from Lemma~\ref{dth} that
every derivation tree satisfies \texttt{snHered};
the result follows from Lemma~\ref{hereds-sn}.
\qed \end{proof}



At this point we have actually shown using Isabelle that
a class of reductions which we have defined is strongly
normalizing.  
We need to show that this class of reductions contains the ones
we are interested in.

\comment{
So far we have just asserted that this class of reductions
contains those which are described by Wansing
and for which he states a strong normalization theorem.

This assertion can never be proved in Isabelle,
but we can prove 
that there is a set of reductions which is contained in the
class defined and which is sufficient to achieve cut-elimination.
In fact we prove that the reductions discussed earlier 
meet these requirements.
}

% We first define a predicate \texttt{ncLP}.
Recall that the parametric reduction
involves tracing up the derivation tree, 
from a premise of the cut being reduced,
to all points where the cut-formula $A$ is introduced.
As Wansing describes \cite[p.~49]{wansing-displaying-modal-logic}
this portion of the derivation tree cannot contain another cut
(if this were allowed, and infinite sequence of reductions \emph{would}
be possible).

\begin{definition}[\texttt{ncLP}]
The exact definition of \texttt{ncLP} is given below,
but the ``intention'' of the definition is that 
\texttt{ncLP seqY ptA} holds iff
calculating the tree \texttt{mLP ptAY seqY ptA}
does not involve traversing another cut; 
\texttt{ncRP} has analogous meaning.
\end{definition}



The actual and ``intended'' definitions are equivalent for a well-formed
derivation tree, which are the only ones we are really interested in.


% The next result says that provided the predicate 
% \texttt{ncLP} is satisfied, a parametric reduction
% which uses \texttt{mLP} satisfies the predicate
% \texttt{nparRedP}.

In the following we will assume a cut as in 
Fig.~\ref{fig-cut-p}, ie,
with conclusion $X \vdash Y$ and cut-formula $A$.

\begin{theorem}[\texttt{pRedLP}]

  Consider a parametric reduction of a cut which proceeds by
  transforming the left subtree (to change its conclusion from $X
  \vdash A$ to $X \vdash Y$), using the function \texttt{mLP}.
  Assume that the
  subtree satisfies the condition \texttt{ncLP} (in effect, that the
  transformation can be performed without traversing another cut), and
  assume the cut is not already left-principal.  Then the reduction
  satisfies the condition \texttt{nparRedP}.
\end{theorem}



The following result is similar, but says that the parametric reduction
is a cut-reduction, ie, it
satisfies the predicate \texttt{cutReduces}.
The results requires stronger conditions, but these are
satisfied in the circumstances when we perform this reduction.

\begin{theorem}[\texttt{cutRedLP}] \label{cutRedLP}
If a cut, at the root of a tree $\Pi$ (\texttt{pt}), is not left-principal 
(and also the left branch is not an unproved leaf),
and
\begin{enumerate}
\item $\Pi$ is well-formed,
\item $\Pi$ uses rule set \texttt{rls}, and 
\item obtaining a new tree $\Pi'$
by calculating \texttt{mLP} of the left branch of $\Pi$
(to change its conclusion from $X \vdash A$ to $X \vdash Y$)
 does not traverse another cut
\end{enumerate}
then the reduction from $\Pi$ to $\Pi'$ is a cut-reduction.
\end{theorem}



The following results, \texttt{allLPm} and \texttt{allLRPm},
are similar to the corresponding
results \texttt{allLP} and \texttt{allLRP},
proved earlier, the difference being that these results
additionally prove that the new derivation tree either is equal to 
the old one or is a cut-reduction of it.

The proofs of these results use 
Theorem~\ref{cutRedLP} (\texttt{cutRedLP}) and \texttt{cutRedRP}
(which is a ``mirror-image''
analogue of \texttt{cutRedLP}, using \texttt{mRP}).
They therefore use the parametric reductions defined in terms
of \texttt{mLP} and \texttt{mRP}.

\begin{theorem}[\texttt{allLPm}] \label{allLPm}
Given a tree $\Pi_0$ with one cut, at the bottom, with cut-formula $A$,
such that 
\begin{enumerate}
\item \label{item1} $\Pi_0$ is well-formed,
\item $\Pi_0$ uses rule set \texttt{rls}, and 
\item \label{item3} $\Pi_0$ has no premises (unproved leaves)
\end{enumerate}
then $\Pi_0$ cut-reduces to a tree $\Pi_1$ such that 
\begin{itemize}
\item $\Pi_1$ has the same conclusion 
as $\Pi_0$,
\item $\Pi_1$ satisfies \ref{item1} to \ref{item3} above, and
\item all cuts in $\Pi_1$ are left-principal, with cut-formula $A$
\end{itemize}
\end{theorem}



\begin{theorem}[\texttt{allLRPm}] \label{allLRPm}
As for Thm.~\ref{allLPm}, except that the cut at the root of $\Pi_0$
is left-principal, and all cuts in $\Pi_1$ are (left- and right-) principal.
\end{theorem}



We have also shown that the primitive reductions described in \S\ref{s-deal}
satisfy \texttt{c8redP}, and are in fact cut-reductions.
For each logical connnective we considered the reduction 
analogous to that in Fig.~\ref{fig-idcut}
(which was used to prove \texttt{orC8} and analogous results), and
showed that it satisfies \texttt{c8redP}.
These results (one for each logical connnective) were combined 
to give Theorem~\ref{formC8W}.

\begin{theorem}[\texttt{formC8W}] \label{formC8W}
  Given a valid\footnote{This is a well-defined semantic term. We must
    not overload it to mean something else. Is there not some other
    term we could use?} tree $\Pi_0$ with one cut, which is principal
  and is at the bottom of $\Pi_0$, there exists a valid tree $\Pi_1$
  such that the relation \texttt{c8redP} holds between $\Pi_0$ and
  $\Pi_1$, and $\Pi_1$ has the same conclusion as $\Pi_0$.
\end{theorem}



We have now shown that our earlier
proof of cut-elimination used, or could have used) only cut-reductions.
This is enough to demonstrate a cut-elimination procedure 
using cut-reductions.
However we now proceed to complete a proof of cut-elimination using
the concept of strong normalization.

We use convenient abbreviations to describe the sorts of trees 
and reductions we are interested in.
Recall that a \emph{valid} derivation tree is one which is well-formed,
uses rules from \texttt{rls}, and has no premises.

\begin{definition}[\texttt{validRed}]
A \emph{valid reduction} is a reduction of tree $\Pi_0$ to tree $\Pi_1$,
where $\Pi_1$ is a valid tree which has the same conclusion as $\Pi_0$.
\end{definition}



% now results from SNCE.ML
\begin{theorem}[\texttt{cutEXred}]
For any valid tree which 
has exactly one cut, at the bottom,
there is available a cut-reduction to another 
valid tree with the same conclusion.
\end{theorem}

\begin{proof}
The proof of theorem uses Theorems \ref{allLPm} and \ref{allLRPm}
for the cases where parametric reductions are required,
and Theorem \ref{formC8W} where primitive reductions are required. \qed
\end{proof}



Given any derivation tree containing a cut, we can apply the theorem
above to a top-most cut.

\begin{theorem}[\texttt{ExRed}]
For any valid tree which contains a cut, 
there is available a valid reduction.
\end{theorem}



The outline of the proof from here is clear:
since every tree with a cut admits a reduction, and 
there is no infinite sequence of reductions, so
an effective cut-elimination procedure is to repeatedly
perform any reduction until it is no longer possible.

\begin{theorem}[\texttt{validRed\_min}]
For any derivation tree $\Pi$
there exists a tree $\Pi^r$
obtained from $\Pi$
such that $\Pi^r$ cannot be further validly reduced.
\end{theorem}



\begin{theorem}[\texttt{redNoCut}]
For any valid tree $\Pi$,
there exists a cut-free valid tree $\Pi^r$,
obtained from $\Pi$ by repeated valid reductions,
such that $\Pi^r$ has the same conclusion
as $\Pi$.
\end{theorem}



That is to say, given a derivation tree, there is a cut-free
equivalent obtained by repeated reductions.
Therefore we have the cut-elimination result, proved using a
strong normalization approach.

Although an Isabelle proof
cannot guarantee that we have encoded 
Wansing's definition of reduction correctly, 
this result shows that we have
defined a class of reductions which is large enough to 
permit cut-elimination, while being small enough to be strongly normalizing.

\begin{theorem}[\texttt{cutElim\_SN}]
  If a sequent can be derived using rules \texttt{rls}, then it can be
  derived from those rules omitting (\emph{cut}).\footnote{Are you
    sure that you do not need extra rules?  For example, if
    \texttt{rls} does not contain contraction, we may require it to
    reduce the number of copies of a formula in order to obtain
    cut-elimination. ANS \texttt{rls} is fixed, the rules of \dRA}
\end{theorem}