\subsubsection{The replacement relations \texttt{seqRep} and \texttt{seqReps}:}
\cc{start of rep.tex} 

% We define a relation \texttt{strRep} between two structures, and a 
% corresponding relation between two sequents.
We define a relation between two sequents.
For boolean \texttt{b}, structures \texttt{X}, \texttt{Y} 
and sequents \texttt{seq1} and \texttt{seq2},
the expression \texttt{seqRep b X Y seq1 seq2} is true if 
\texttt{seq1} and \texttt{seq2} are the same, except that (possibly)
one or more occurrences of \texttt{X} in \texttt{seq1} are replaced by 
corresponding occurrences of \texttt{Y} in \texttt{seq2},
where such differences occur only in succedent [antecedent] positions,
according as \texttt{b} is \texttt{True} [\texttt{False}]. 
For two lists \texttt{seql1} and \texttt{seql2}, 
\texttt{seqReps b X Y seql1 seql2} holds if each member of  
\texttt{seql1} is related to the corresponding member of \texttt{seql2}
by \texttt{seqRep b X Y}.

The following are the main theorems used to develop the mechanised proof 
based on applying this procedure.
Several of them use the relation \texttt{seqRep pn (Structform A) Y}, since
\texttt{seqRep pn (Structform A) Y seqa seqy} holds 
when \texttt{seqa} and \texttt{seqy} are
correpsonding sequents in the trees $\Pi_L$ and $\Pi_L[A \,?\!= Y]$.

\begin{theorem}[\texttt{seqExSub1}]
If \texttt{pat}
is formula-free and does not contain any structure
variable more than once, and can be instantiated to 
get \texttt{seqa}, and 
\texttt{seqRep pn (Structform A) Y seqa seqy} holds, then \texttt{pat} can
be instantiated to get \texttt{seqy}.
\end{theorem}

\begin{verbatim}
seqExSub1 = 
  "[| ~ seqCtnsFml ?pat; seqSubst (?fs, ?suba) ?pat = ?seqa;
      noDups (seqSVs ?pat);
      seqRep ?pn (Structform ?A) ?Y ?seqa ?seqy |]
   ==> EX suby. seqSubst (?fs, suby) ?pat = ?seqy" 
\end{verbatim}

The reason \texttt{pat} must be formula-free is that, supposing for example
that \texttt{pat} were \texttt{Structform (FV ``B``)}, it could be
instantiated to \texttt{Structform A}, but not to an arbitrary 
structure \texttt{Y}.

The stronger result \texttt{seqExSub2} is similar to \texttt{seqExSub1},
except that the antecedent [succedent] of the sequent 
\texttt{pat} may contain a formula,
provided that the whole of the antecedent [succedent] is that formula.

The result \texttt{seqExSub2}
is used in proceeding up the derivation tree $\Pi_L$,
changing $A$ to $Y$:
if \texttt{pat} is the conclusion of a rule, which, instantiated with
\texttt{(fs, suba)}, is used in $\Pi_L$, then that rule, instantiated with 
\texttt{(fs, suby)}, is used in $\Pi_L[A \,?\!= Y]$.
This is expressed in the theorem \texttt{extSub2}, which is one step in the 
transformation of $\Pi_L$ to $\Pi_L[A \,?\!= Y]$.

To explain the theorem \texttt{extSub2} we first define a
property \texttt{bprops} of rules:
\texttt{bprops rule} holds if the rule \texttt{rule} 
satisfies three properties, which are related 
(but do not exactly correspond) to Belnap's conditions
 -- this is discussed further in \S\ref{Bel-props}.
The three properties are
\begin{itemize}
  \item the conclusion of \texttt{rule} has no repeated structure variables
  \item if a structure variable in the conclusion of \texttt{rule}
    is also in a premise,
    then it has the same ``cedency'' (ie antecedent or succedent) there
  \item if the conclusion of \texttt{rule} has formulae,
    they are displayed (ie the whole of one side)
\end{itemize}


\begin{theorem}[\texttt{extSub2}]
\renewcommand\theenumi{\roman{enumi}}
\renewcommand\labelenumi{(\theenumi)}
Given rule \texttt{rule}
and an instantiation \texttt{ruleA} of it,
and given a sequent \texttt{conclY},
such that 
\begin{enumerate}
\item \texttt{seqRep pn (Structform A) Y (conclRule ruleA) conclY} holds,
\item \texttt{bprops rule} holds,
\item \label{extc}
if the conclusion of \texttt{rule}
has a displayed formula on one side,
then \texttt{conclrule ruleA} and \texttt{conclY} are the same on that side
\end{enumerate}
then there exists \texttt{ruleY}, an instantiation of \texttt{rule}, 
whose conclusion is \texttt{conclY} and whose premises \texttt{premsY}
are, respectively, related to \texttt{premsRule ruleA} by 
\texttt{seqRep pn (Structform A) Y}.
\end{theorem}

\begin{verbatim}
extSub2 =
  "[| conclRule rule = Sequent pant psuc ;  
      conclRule ruleA = Sequent aant asuc ;
      conclY = Sequent yant ysuc ;  
      (strIsFml pant & aant = Structform A --> aant = yant) ;  
      (strIsFml psuc & asuc = Structform A --> asuc = ysuc) ;  
      ruleMatches ruleA rule ; bprops rule ;  
      seqRep pn (Structform A) Y (conclRule ruleA) conclY |]
    ==> (EX subY. conclRule (ruleSubst subY rule) = conclY &  
        seqReps pn (Structform A) Y (premsRule ruleA)  
        (premsRule (ruleSubst subY rule)))"
\end{verbatim}

This theorem is used to show that, when a node of the tree $\Pi_L$
is transformed to the corresponding node of $\Pi_L[A \,?\!= Y]$,
then the next node(s) above can be so transformed. 
But this does not hold at the node whose conclusion is 
$X' \vdash A$ (see Fig.\ref{fig-cut-p}); 
condition (\ref{extc}) above reflects this limitation.

\subsubsection{Turning one cut into several left-principal cuts}

To turn one cut into several left-principal cuts
we use the procedure described above.
This uses \texttt{extSub2} to transform $\Pi_L$ to $\Pi_L[A \,?\!= Y]$
up to each point where $A$ is introduced, and then inserting an instance 
of the (cut) rule (or, in the case where $A$ is introduced by the axiom
$A \vdash A$, using the $\Pi_R$ alone, as in Fig.\ref{fig-cut-p}).
It is to be understood that the derivation trees have no 
(unfinished) premises.

\begin{theorem}[\texttt{makeCutLP}] 
Given cut-free derivation tree \texttt{ptAY}
  deriving (\texttt{A} $\vdash $ \texttt{Y})
  and \texttt{ptA} deriving \texttt{seqA},
  and given \texttt{seqY}, where
  \texttt{seqRep True (Structform A) Y seqA seqY} holds
  (ie, \texttt{seqY} and \texttt{seqA}
  are the same except (possibly)
  that $A$ in a succedent position in \texttt{seqA} is replaced by $Y$ 
  in \texttt{seqY}),
  there is a derivation tree deriving \texttt{seqY} whose 
  cuts are all left-principal on $A$.
\end{theorem}

\begin{verbatim}
makeCutLP =
  "[| allPT (cutOnFmls {}) ?ptAY; allPT (frb rls) ?ptAY;
      allPT wfb ?ptAY; conclPT ?ptAY = (?A |- $?Y);
      allPT (frb rls) ?ptA; allPT wfb ?ptA;
      allPT (cutOnFmls {}) ?ptA;
      seqRep True (Structform ?A) ?Y (conclPT ?ptA) ?seqY |]
   ==> EX ptY.
          conclPT ptY = ?seqY & allPT (cutIsLP ?A) ptY &
          allPT (frb rls) ptY & allPT wfb ptY" 
\end{verbatim}

\texttt{makeCutRP} is basically the symmetric variant of \texttt{makeCutLP} ;
  so \texttt{ptAY} is a cut-free derivation tree deriving ($Y \vdash A$).  
  But with the extra hypothesis that $A$ is introduced
  at the bottom of \texttt{ptAY}, the result is that 
  there is a derivation tree deriving \texttt{seqY} whose
  cuts are all (left- and right-) principal on $A$.
  

These were the most difficult to prove of any of theorems required
for this cut-elimination proof. 
The proofs proceed by structural induction on the initial derivation tree,
where the inductive step involves an application of \texttt{extSub2},
except where the formula $A$ is introduced.
If $A$ is introduced by an introduction rule, then the inductive step
involves inserting an instance of (cut) into the tree, and then applying the
inductive hypothesis.
If $A$ is introduced by the axiom (\textit{id}), then 
(and this is the base case of the induction)
the tree \texttt{ptAY} is substituted.

\begin{definition}
Two derivation trees 
are \emph{equivalent} if
% \begin{itemize}
% \item 
they have the same conclusion (root) sequent.
% \item both are well-formed,
% \item both use rules in the set \texttt{rls}, and
% \item both have no premises (ie, unproved leaves).
% \end{itemize}
\end{definition}

Next we have the theorem expressing the transformation of the whole 
derivation tree, as shown in the diagrams.

\begin{theorem}[\texttt{allLP}]
Given a valid derivation tree \texttt{pt} containing just one cut,
which is on formula $A$ and 
is at the root of \texttt{pt}, there is an equivalent valid tree,
all of whose cuts are left-principal and are on $A$. 
\end{theorem}

\begin{verbatim}
allLP = 
  "[| cutOnFmls {?A} ?pt; allPT wfb ?pt; allPT (frb rls) ?pt;
      allNextPTs (cutOnFmls {}) ?pt |]
   ==> EX ptn.
          conclPT ptn = conclPT ?pt & allPT (cutIsLP ?A) ptn &
          allPT (frb rls) ptn & allPT wfb ptn" 
\end{verbatim}

\texttt{allLRP} is a similar theorem where we start with a single 
left-principal cut, and produce a tree whose cuts are (left- and right-) 
principal.

\cc{end of rep.tex}