
\section{The system GTD}
This section and the next describe Isabelle proofs of the
cut admissibility of the logic GTD described in \cite{mints-jaegerfest}

\label{s-gtd}
Semantically this system is $K$ with the additional axiom
$\Box A \Leftrightarrow \Box \Box A$.
The sequent inference rules involving $\Box$ are
$$
\frac{\Gamma, \Box \Gamma \vdash A}{\Box \Gamma \vdash \Box A}
(\vdash\Box)
\qquad
\frac{\Gamma, \Box \Gamma \vdash \Box A}{\Box \Gamma \vdash \Box A}
(\Box\vdash)
$$
We first formalised $GTD$ as 
\texttt{glssc GTD}
using a framework which had previously been applied to other logics.
\texttt{GTD} means the rules involving $\Box$, and \texttt{glssc} refers to 
a set of classical logic rules, including explicit weakening and contraction
rules. 

Our formalisation involves sequents consisting of multisets of formulae on
either side of a turnstile. 

\begin{verbatim}
datatype 'a sequent = Sequent "'a multiset" "'a multiset"
\end{verbatim}

Here are the definitions of \texttt{glssc} and \texttt{GTD}
\begin{verbatim}
inductive "GTD"
  intros
    I : "A = B | A = Box B ==>
      ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : GTD"

inductive "glssc glrs"
  intros
    axiom : "([], {#D#} |- {#D#}) : glssc glrs"
    extI : "psc : glne ==> pscmap (extend flr) psc : glssc glrs"
    glrI : "psc : glrs ==> psc : glssc glrs"
\end{verbatim}

The second clause for \texttt{glssc} takes the rules in \texttt{glne}
and adds a context (the same context) to the conclusion and \emph{all}
premises.
This means that the logical rules with two premises are of the context-sharing
form.
The following definitions explain this further.

\begin{verbatim}
types
  'a psc = "'a list * 'a" (* single step inference *)
consts
  pscmap :: "('a => 'b) => 'a psc => 'b psc"
  (* extend a sequent by adding context to conclusion and premises *)
  extend :: "'a sequent => 'a sequent => 'a sequent"
primrec
   pscmap_def "pscmap f (ps, c) = (map f ps, f c)"
defs
  extend_def : "extend fmls seq == seq + fmls"
\end{verbatim}

We reused some code from previous work in which the logical rules 
($\vdash\lor$), ($\land\vdash$) and ($\vdash\lor$)
were of the forms shown (without the context)
$$
\frac{A \vdash}{A \land B \vdash}
\qquad
\frac{B \vdash}{A \land B \vdash}
\qquad
\frac{\vdash A}{\vdash A \lor B }
\qquad
\frac{\vdash B}{\vdash A \lor B }
\qquad
\frac{A \vdash B}{\vdash A \to B }
$$

The rules used for classical logic (before extending them with a context) 
form the set \texttt{glne}: the rule sets 
\texttt{wkrls}, \texttt{ctrrls} $A$, \texttt{glil} and \texttt{glir} 
are the weakening rules, contraction (on $A$) rules, and the left and right
logical introduction rules.

\begin{verbatim}
inductive "glne" (* rules before being extended *)
  intros
    wkI : "(ps, c) : wkrls ==> (ps, c) : glne"
    ctrI : "(ps, c) : ctrrls A ==> (ps, c) : glne"
    ilI : "(ps, c) : glil ==> (ps, c) : glne"
    irI : "(ps, c) : glir ==> (ps, c) : glne"
\end{verbatim}

To prove cut admissibility we actually used induction on a derivation to prove
admissibility of the mix (multicut rule).

\subsection{Framework of our induction proofs} \label{s-induction}
FOLLOWING TEXT FROM OUR LPAR PAPER
Many cut-elimination proofs proceed via two main phases. The first
phase transforms the given derivations using several ``parametric''
steps so that the cut-formula is the principal formula of the final
rule in the resulting sub-derivations.  The ``principal cut'' is then
``reduced'' into cuts which are ``smaller'' in some well-founded
ordering such as size of cut-formula.  We describe how we captured
this two-phase structure of cut-elimination proofs, and present a
widely applicable result that a parametric step is possible under
certain conditions.

We use the following framework for deriving cut-admissibility,
or indeed any property $P$ of pairs of subtrees.
In the diagram below, to prove $P (\MC_{l}, \MC_{r})$, the
induction hypothesis is that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
\MQ_{rj})$ hold for all $i$ and $j$:

\begin{center}
\begin{prooftree}
\AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$\MC_{l}$}
\AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$\MC_{r}$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}
A proof of $P (\MC_{l}, \MC_{r})$ using this induction hypothesis
inevitably proceeds by cases on the actual rules $\rho_l$ and
$\rho_r$, and for a cut-formula $A$, on whether it is principal
in either or both of $\rho_l$ and $\rho_r$.  But we also use
induction on the size of the cut-formula, or, more generally, on some
well-founded relation on formulae.

So we actually consider a property $P$ of a (cut) formula $A$
and (left and right subtree conclusion) sequents $(\MC_l, \MC_r)$.
In proving $P\ A\ (\MC_{l}, \MC_{r})$,
in addition to the inductive hypothesis above, we assume
that $P\ A'\ (\MD_l, \MD_r)$ holds generally for $A'$ smaller than $A$ and
all ``\texttt{rls}-derivable'' sequents $\MD_l$ and $\MD_r$:
\textit{i.e.} derivable from the empty set of
premises using rules from $rls$. These intuitions give  the
following definition \texttt{gen\_step2sr} of
a condition which permits one step of the inductive proof.
Setting out proofs by using a number of lemmas, each stating
\texttt{gen\_step2sr} \ldots for specific cases of the final rules on each side
above the cut enables us to avoid having one huge monolithic proof in the
Isabelle code.

\begin{definition}[\texttt{gen\_step2sr}] \label{d-gen-step2sr}
For a formula $A$, a property $P$,
a subformula relation \texttt{sub},
a set of rules \texttt{rls},
inference rule instances $\MR_l = {(\psl, \MC_l)}$
and $\MR_r = {(\psr, \MC_r)}$,
\texttt{gen\_step2sr} $P\ A$ \texttt{sub rls} $(\MR_l, \MR_r)$
means: %\\%[0.5em]
% if %all the following hold:
\begin{description}
\item[if] forall ${A'}$ such that $(A', A) \in \texttt{sub}$
and all \texttt{rls}-derivable sequents
$\MD_l$ and $\MD_r$,
${P\ A'\ (\MD_l, \MD_r)}$ holds
\item[and] for each ${\MP_{li}}$ in ${\psl}$,
${\MP_{li}}$ is \texttt{rls}-derivable and 
${P\ A\ (\MP_{li}, \MC_r)}$ holds
\item[and] for each ${\MP_{rj}}$ in ${\psr}$,
${\MP_{rj}}$ is \texttt{rls}-derivable and
${P\ A\ (\MC_l, \MP_{rj})}$ holds
\item[and] ${\MC_l}$ and ${\MC_r}$ are \texttt{rls}-derivable.
\item[then] ${P\ A\ (\MC_{l}, \MC_{r})}$ holds.
\end{description}
\end{definition}

\begin{verbatim}
gen_step2sr_simp: "gen_step2sr ?P ?A ?sub ?rls ((?aa, ?ba), ?ab, ?bb) =
    ((ALL A'.  (A', ?A) : ?sub -->
       (ALL dl:derrec ?rls {}.  ALL dr:derrec ?rls {}. ?P A' (dl, dr))) -->
     (ALL pl:set ?aa. pl : derrec ?rls {} & ?P ?A (pl, ?bb)) -->
     (ALL pr:set ?ab. pr : derrec ?rls {} & ?P ?A (?ba, pr)) -->
     ?ba : derrec ?rls {} --> ?bb : derrec ?rls {} --> ?P ?A (?ba, ?bb))"
\end{verbatim}

So the property $P$ we want to prove using this induction framework is that
the final sequents $\MC_l$ and $\MC_r$ can be combined using the mix rule.

The main theorem \texttt{gen\_step2sr\_lem} below for proving an
arbitrary property $P$ states that if the step of the inductive proof
is possible for all cases of final rule instances
 $\MR_l$ and $\MR_r$
  % ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$
   on each side, then $P$ holds in all cases.

\begin{theorem}[\texttt{gen\_step2sr\_lem}] \label{t-gen-step2sr-lem}
 If
 \begin{itemize}
 \item \texttt{A} is in the well-founded part of the subformula relation
 \texttt{sub},
 \item sequents $\MS_l$ and $\MS_r$ are \texttt{rls}-derivable, and
 \item for all formulae $A'$, and all rules $\MR_l$ and $\MR_r$,
%  ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$, 
 our induction step condition
 \texttt{gen\_step2sr} $P\ A'\ \texttt{sub rls}\ (\MR_l, \MR_r)$
 holds
\end{itemize}
 then ${P\ A\ (\MS_l, \MS_r)}$ holds.
\end{theorem}

This enables us to split up an inductive proof, by showing,
separately, that \texttt{gen\_step2sr} holds for particular cases of
the final rules $(\MP_l, \MC_l)$ and $(\MP_r, \MC_r)$ on each side.
For example, the inductive step for the case where the cut-formula $A$ is
parametric, not principal, on the left is encapsulated in the
following theorem where
\mbox{\texttt{prop2 mar erls} $A\ (\MC_l, \MC_r)$} means
that the conclusion of a multicut on \texttt{A} whose premises are
$\MC_l$ and $\MC_r$ is derivable using rules \texttt{erls}.

\begin{theorem}[\texttt{lmg\_gen\_step}]~\label{t-gs2sr}
 For any relation \texttt{sub} and any rule set \texttt{rls},
 given an instance of multicut with left and right subtrees
 ending with rules $\MR_l$ and $\MR_r$:
\begin{description}
 \item[if] weakening is admissible for the rule set \texttt{erls},
 \item[and] all extensions of some rule $(\MP, X \vdash Y)$ are in the rule set
  \texttt{erls},
  \item[and] $\MR_l$ is an extension of $(\MP, X \vdash Y)$,
  \item[and] the cut-formula $A$ is not in $Y$
  (meaning that $A$ is parametric on the left)
%  \end{itemize}
  \item[then] \texttt{gen\_step2sr (prop2 mar erls)} $A$ \texttt{sub rls}
  $(\MR_l, \MR_r)$ holds.
\end{description}
\end{theorem}

Theorem~\ref{t-gs2sr} codifies multi-cut elimination for parametric
cut-formulae, and applies generally to many different
calculi since it holds independently of the values of \texttt{sub} and
\texttt{rls}.  Of course, for a system with explicit weakening rules,
such as $GTD$, weakening is {\it a fortiori} admissible.

The above theorem uses the property \texttt{prop2 mar erls} (for rule set
\texttt{erls}.
We show the definitions of \texttt{prop2} and \texttt{mar} below.

\begin{verbatim}
inductive "mar rls A"
    I : "(Xl + ms_delete {A} Xr |- ms_delete {A} Yl + Yr) : derrec rls {}
      ==> (Xl |- Yl, Xr |- Yr) : mar rls A"

inductive "mas rls A"
    I : "seql : derrec rls {} & seqr : derrec rls {} -->
        (seql, seqr) : mar rls A ==> (seql, seqr) : mas rls A"

prop2_def : "prop2 f rls A seqs == seqs : f rls A"
\end{verbatim}

It may be noticed that \texttt{mar} and \texttt{mas} are similar except that 
\texttt{mas} contains explicitly the condition that the premises of the
putative cut are derivable.  
In the context of induction on derivations, this is true anyway,
so we have the following theorem

\begin{verbatim}
gs2_mas_mar: "gen_step2sr (prop2 mas ?rls) ?A ?sub ?rls =
            gen_step2sr (prop2 mar ?rls) ?A ?sub ?rls"
\end{verbatim}

(Later we will refer to \texttt{car} and \texttt{cas} which are corresponding
concepts for single, rather than multiple, cuts).

Then we get the following theorems:

\begin{verbatim}
glssc_gs2sr_GTD_r :
   "[| (?psa, ?ca) : extrs glne; (?psb, ?cb) : GTD |] ==>
  gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
       ((?psa, ?ca), ?psb, ?cb)"

glssc_gs2sr_GTD_l :
   "[| (?psa, ?ca) : GTD; (?psb, ?cb) : extrs glne |] ==>
   gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
     ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}

That is, with a GTD rule on one side and one of the usual logical rule on the
other, the inductive step is available.  
These results are easy because if the cut-formula is not the principal formula
of the logical rule then Theorem~\ref{t-gs2sr} (and the corresponding result on
the right) apply.
If the cut-formula (which must be boxed)
is the principal formula of the logical rule then the logical rule must be
weakening or contraction, in which case applying multicut to its premise 
gives the required result.

With logical rules on both sides, the following theorem applies:
note that it applies to any logic \texttt{glssc ?R} 
(where $?R$ can stand for any set of rules).

\begin{verbatim}
glssc_gs2sr_ng: 
  "[| c8ger_prop ?psubfml (glssc ?R) ?A (glne - wkrls - UNION UNIV ctrrls);
         (?psa, ?ca) : extrs glne; (?psb, ?cb) : extrs glne |] ==>
   gen_step2sr (prop2 mar (glssc ?R)) ?A ?psubfml (glssc ?R)
     ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}

The property \texttt{c8ger\_prop} says essentially that if \emph{single} cuts 
on subformulae of $A$ are admissible then a single cut on $A$
is admissible where the last rules on either side are logical introduction
rules introducing the cut-formula $A$.

\begin{verbatim}
"c8ger_prop ?isubfml ?drls ?A ?c8rls ==
      ALL ps qs pse qse X Y.
         (ps, 0 |- {#?A#}) : ?c8rls -->
         (qs, {#?A#} |- 0) : ?c8rls -->
         pse = map (extend (X |- Y)) ps -->
         qse = map (extend (X |- Y)) qs -->
         set pse Un set qse <= derrec ?drls {} -->
         (ALL sfa.
             (sfa, ?A) : ?isubfml --> (ALL seqs. seqs : cas ?drls sfa)) -->
         (X |- Y) : derrec ?drls {}"
\end{verbatim}

In the cases of the logical introduction rules proving multicut admissibility
is more difficult than proving single cut admissibility.  
Where introduction of (just one instance of) the cut-formula $A$
is the last step on each side before the cut,
 it is nesessary to perform multicut elimination on $A$ between 
$\MQ_{l1} \ldots \MQ_{ln}$ and $\MC_{r}$, and between
$\MC_{l}$ and $\MQ_{r1} \ldots \MQ_{rm}$;
then one performs single-cut elimination on the sub-formulae of $A$.
These steps are part of the proof of \texttt{c8\_gs2\_mas}.
An example follows.
Note that here (unlike some of the other diagrams) the contexts
$U$ and $Y$ may contain copies of the cut-formula.
Let $Y'$ be $Y$ with copies of $A \land B$ deleted, and 
$U'$ be $U$ with copies of $A \land B$ deleted.

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash A, Y$}
\AxiomC{$X \vdash B, Y$}
\RightLabel{($\vdash \land$)}
\BinaryInfC{$X \vdash A \land B, Y$}
\AxiomC{$U, A, B \vdash V$}
\RightLabel{($\land \vdash$)}
\UnaryInfC{$U, A \land B \vdash V$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$X, U' \vdash Y', V$}
\end{prooftree}
\end{center}

This is replaced by

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash A, Y$}
\AxiomC{$U, A \land B \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$X, U' \vdash A, Y', V$}
\dottedLine
\UnaryInfC{\large (A)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash B, Y$}
\AxiomC{$U, A \land B \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$X, U' \vdash B, Y', V$}
\dottedLine
\UnaryInfC{\large (B)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash A \land B, Y$}
\AxiomC{$U, A, B \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$X, U', A, B \vdash Y', V$}
\dottedLine
\UnaryInfC{\large (C)}
\end{prooftree}
\end{center}

Then (A), (B) and (C) are combined using inductive cuts on the smaller
cut-formulae $A$ and $B$, and the necessary contractions,
 to derive the required sequent {$X, U' \vdash Y', V$}.

\begin{verbatim}
c8_gs2_mas:
   "[| wk_adm ?drls; ?prl = (?ps, 0 |- {#?A#}); ?qrl = (?qs, {#?A#} |- 0);
         ?prl : ?c8rls; ?qrl : ?c8rls;
         ?eprl = pscmap (extend (?Xl |- ?Yl)) ?prl;
         ?eqrl = pscmap (extend (?Xr |- ?Yr)) ?qrl;
         c8ger_prop ?sub ?drls ?A ?c8rls |] ==>
       gen_step2sr (prop2 mas ?drls) ?A ?sub ?drls (?eprl, ?eqrl)"
\end{verbatim}

We proved that \texttt{c8ger\_prop} holds in the following theorem.
\begin{verbatim}
rls_c8: "c8ger_prop ipsubfml (glssc ?rls) ?A
   (glne - wkrls - UNION UNIV ctrrls)"
\end{verbatim}

It remains to look at the case where the final rule on both sides of the
desired cut are instances of the $GTD$ rules.
Here there are two quite distinct cases, depending on which $GTD$ rule is used
as the final step for the left premise of the cut.  

For the first case, the rule on the left is
 the $(\Box \vdash)$ rule as shown,
and for the rule on the right,
only its conclusion matters, and is as shown.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
\RightLabel{$(\Box\vdash)$}
\UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$\textit{ctr}^*\vdash$}
% \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
\AxiomC{$\cdots$}
\UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

we use the inductive hypothesis permitting multicutting $\Box A$ between
$\Gamma, \Box \Gamma \vdash \Box A$ with $\Box A^n, \Box \Delta \vdash \Box B$
then we use weakening and the $(\Box \vdash)$ rule, to get

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
\AxiomC{$\cdots$}
\UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{weak})}
\UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
\RightLabel{($\Box\vdash$)}
\UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

The second case, with the $(\vdash \Box)$ rule on the left as shown,
is more complicated. 
Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash A$}
\RightLabel{$(\Box\vdash)$}
\UnaryInfC{$\Box \Gamma \vdash \Box A$}
\AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
\UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

In this case, from the premise on the right, we perform 
inductive mix on $\Box A$ with the conclusion on the left,
then mix on $A$ with the premise on the left,
contraction(s) on $\Box \Gamma$, and finally an instance of the 
$(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
The result is shown below.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash A$}
\AxiomC{$\Box \Gamma \vdash \Box A$}
\AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

\begin{verbatim}
glssc_gs2sr_GTD_GTD:
   "[| (?psa, ?ca) : GTD; (?psb, ?cb) : GTD |] ==>
   gen_step2sr (prop2 mar (glssc GTD)) ?A ipsubfml (glssc GTD)
       ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}

Finally we combine these results to get the mix admissibility result.

\begin{verbatim}
mas_GTD: "(?seql, ?seqr) : mas (glssc GTD) ?A"
\end{verbatim}

\section{Inductive proof of cut (\emph{not} mix) admissibility for GTD}
\label{s-cut-gtd}
The previous section dealt with a proof of cut admissibility where the
inductive hypothesis was essentially that mix-admissibility is available for
the end-sequents of ``smaller'' pairs of derivations.

We now want to explore what it takes to produce an inductive proof where the
inductive hypothesis is that (specifically) single-cut admissibility is
available for ``smaller'' pairs of derivations.

We define the ordinary logical rules of the differently from the above, 
so that the rules ($\vdash\lor$) and ($\land\vdash$) are 
of the forms shown (without the context)
$$
\frac{A, B \vdash}{A \land B \vdash}
\qquad
\frac{\vdash A, B}{\vdash A \lor B }
$$
In these forms, these rules are invertible.

We define the rules of the system as follows.
The rules used for classical logic (before extending them with a context) 
form the set \texttt{lkxcne}: the rule sets \texttt{idrls},
 \texttt{wkrls}, \texttt{ctrrls} $A$, \texttt{lksil} and \texttt{lksir} 
are the axioms, weakening rules, contraction (on $A$) rules, 
and the left and right logical introduction rules.

\begin{verbatim}
inductive "lkxcss xrls"
  intros
    extI : "psc : lkxcne ==> pscmap (extend flr) psc : lkxcss xrls"
    x : "psc : xrls ==> psc : lkxcss xrls"

inductive "lkxcne"
  intros
    id : "psc : idrls ==> psc : lkxcne" 
    wk : "psc : wkrls ==> psc : lkxcne"
    ctr : "psc : ctrrls A ==> psc : lkxcne" 
    ilI : "psc : lksil ==> psc : lkxcne"
    irI : "psc : lksir ==> psc : lkxcne"
\end{verbatim}

When proving single-cut admissibility, the contraction rule causes a
difficulty, since going up one step in the proof gives us an extra copy of the
cut-formula to deal with, and the inductive hypothesis enables us to use an
inductively available cut only to get rid of one copy of the cut-formula.

The solution is to use the invertibility of the logical introduction rules,
which reduces the problem of cut on a cut-formula $A$ containing a logical
connective to cut on sub-formulae of $A$.

Unfortunately the contraction rule causes the same sort of difficulty here as
it does with the cut rule.
So we have to prove, inductively, a sort of ``multi-invertibilty'' property,
that multiple copies of a formula are invertible according to the introduction
rule for that formula.
Again, we define a predicate indicating that one step of an inductive proof
of this result is available.

Firstly, we define the set of inverses of a sequent according to a rule set:
if $(ps, seq) \in irls$ and $p \in ps$, 
then $p \in \texttt{invs\_of}\ irls\ seq$.

Then the property of interest is that when a sequent is derivable, its
inverses are also derivable.  
The predicate \texttt{inv\_step} describes that this property holds for the 
end-sequent of a derivation, assuming that it holds for the preceding
sequent(s).
Note that there are two rule sets involved, the rules used for derivations and
the rules being shown to be invertible.

In the definition of \texttt{inv\_step}, \texttt{derivs} will be the set of
derivable sequents.
Then \texttt{inv\_step} \ldots means that 
for the last rule $(ps, concl)$ of a derivation:
if the inverses of the premises $ps$ of that rule are derivable,
then the inverses of the conclusion $concl$ are derivable.

Finally, \texttt{gtd\_inv\_step} shows that the logical introduction rules,
with each formula repeated $n$ times, and with contexts, are invertible,
and \texttt{gtd\_inv\_rl} is the invertibility result.

\begin{verbatim}
invs_of_def: "invs_of ?irls ?seq ==
         {x. EX p ps. x = p & p : set ps & (ps, ?seq) : ?irls}"

inv_step.simps: "inv_step ?derivs ?irls (?ps, ?concl) =
   (set ?ps <= ?derivs --> (ALL p:set ?ps. invs_of ?irls p <= ?derivs) -->
	   invs_of ?irls ?concl <= ?derivs)"

gtd_inv_step: "[| ?r : lksil Un lksir; ?x : lkxcss GTD |] ==>
  inv_step (derrec (lkxcss GTD) {}) (extrs (multiples {?r})) ?x"

gtd_inv_rl: "Ball (extrs (multiples lksne)) (inv_rl (lkxcss GTD))"
\end{verbatim}

NOTE: From here the proof of cut admissibility is a single theorem with
one long monolithic proof.  Perhaps I should rearrange it so as to better
enable a description of the intermediate results.

First we need a change in the pattern of proof by induction.
Referring to the diagram in \S\ref{s-induction}, 
the induction hypothesis that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
\MQ_{rj})$ hold for all $i$ and $j$ will not be sufficient.
Rather we will need an assumption that 
$P (\MQ'_{li}, \MC_{r})$ and $P (\MC_{l}, \MQ'_{rj})$ hold whenever 
$\MQ'_{li}$ is derived by a derivation no larger than the derivation
of $\MQ_{li}$ (likewise for $\MQ'_{rj}$).

This means that we need to define the height of a derivation tree, and
therefore that we need to define a derivation tree value whose height can be
defined and calculated. 

FOLLOWING FROM GLS LPAR PAPER - 
WE NEED TO MOVE IT EARLIER SINCE IT APPLIES TO SEVERAL SECTIONS

ALSO DELETE IT FROM THE GLS SECTION LATER

In~\cite{dawson-gore-cut-admissibility}, we modelled a derivation tree
in HOL as a recursive structure which consists of a
root sequent (which should be the conclusion of some rule), and an
associated list of (sub)trees (each of which should derive a premise of
that rule). The type of explicit derivation trees is a recursive
datatype, such as:
\begin{verbatim}
   datatype 'a dertree = Der 'a ('a dertree list)
       | Unf 'a (* unfinished leaf which remains unproved *)
\end{verbatim}
%
We then had to express the property of such a tree, that it
is in fact correctly based on the given rules, and so represents a
valid derivation.

A \textit{valid} tree is one whose inferences are in the set of rules
and which as a whole has no premises.

 Thus we
``mix and match'' a deep embedding of derivation trees with a shallow
embedding of inductively defined sets of derivable sequents.
To ensure the correctness of our ``mixing and matching'' we needed the
following relationship between our definitions of derivability according
to the two embeddings.

\begin{lemma} \label{l-derrec-valid}
  Sequent $X \vdash Y$ is derivable, shallowly,
  from the empty set of premises using rules \texttt{rls}
  (ie, is in \texttt{derrec rls} $\{\}$)
 %(ie, according to the definitions of \S\ref{s-dp})
  iff some explicit derivation tree
  \texttt{dt} is valid wrt.\ \texttt{rls} and has a conclusion
  $X \vdash Y$.
\begin{verbatim}
"(?a : derrec ?rls {}) = (EX dt. valid ?rls dt & conclDT dt = ?a)"
\end{verbatim}
\end{lemma}

We can now define the height of such a tree, as

\begin{verbatim}
primrec (* height (max) of derivation tree *)
  "heightDT (Der seq dts) = Suc (heightDTs dts)"

  "heightDTs [] = 0"
  "heightDTs (dt # dts) = max (heightDT dt) (heightDTs dts)"
\end{verbatim}

Note that we had to use height as defined: we found that our first choice, to
use the number of nodes in a derivation tree, did not work.

So \texttt{height\_step2\_tr} \ldots states that the inductive step
 works for the two derivation trees above the putative cut 
(or whatever property we use this induction pattern for).
Unlike in the case of \texttt{gen\_step2sr}, the (final) argument is a pair of
derivation trees rather than the pair of bottom rules.
Apart from this, \texttt{gen\_step2sr} is a stronger property
(as it uses a weaker induction property), so we get the result
\texttt{gs2\_cas\_hs\_tr} which links the two.
This uses the relation on trees \texttt{casdt}, where cut-admissibility
works between the conclusions of those trees.
We also have a corresponding definition \texttt{masdt}
and result \texttt{gs2\_mas\_hs\_tr} for multicuts. 
And, corresponding to \texttt{gen\_step2sr\_lem},
we use the property by the lemma \texttt{height\_step2\_tr\_lem}.

\begin{verbatim}
height_step2_tr_eq: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
      ((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
       (ALL dtp. (dtp, ?dta) : measure heightDT --> ?P ?A (dtp, ?dtb)) -->
       (ALL dtq. (dtq, ?dtb) : measure heightDT --> ?P ?A (?dta, dtq)) -->
       ?P ?A (?dta, ?dtb))"

inductive "casdt rls A"
  intros
      I : "valid rls dtl & valid rls dtr -->
        (conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"

cas_casdt: "(conclDT ?dtl, conclDT ?dtr) : cas ?rls ?A ==>
  (?dtl, ?dtr) : casdt ?rls ?A

gs2_cas_hs_tr:
   "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)
      ==> height_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"

height_step2_tr_lem: "[| ?A : wfp ?sub; 
  ALL A dta dtb. height_step2_tr ?P A ?sub (dta, dtb) |] ==>
   ?P ?A (?dta, ?dtb)" 
\end{verbatim}

Since we have proved invertibility for the logical introduction rules, 
when the cut-formula is a compound formula, then, regardless of what the 
final rules in the actual derivation trees are, we can use the invertibility
and reduce the problem to that of cuts on smaller formula.

We then use the fact that for all the logical connnectives,
 with their left and right logical introduction rules, 
we can use cuts on the subformulae on the premises of the introduction rules
to achieve the effect of a cut on the whole formula 
on the conclusions of those introduction rules.
This is expressed in the following theorem:

\begin{verbatim}
gprstep_q: "[| All (ctr_adm ?drls); wk_adm ?drls;
   (?ps, {#} |- {#?A#}) : lksir; (?qs, {#?A#} |- {#}) : lksil;
   ?pse = map (extend (?Xl |- ?Yl)) ?ps;
   ?qse = map (extend (?Xr |- ?Yr)) ?qs;
   set ?pse Un set ?qse <= derrec ?drls {};
   ALL sfa.  (sfa, ?A) : ipsubfml --> (ALL Xl Yl Xr Yr.
        (Xl |- mins sfa Yl, mins sfa Xr |- Yr) : cas ?drls sfa);
   extrs lksne <= ?drls |] ==> (?Xl + ?Xr |- ?Yl + ?Yr) : derrec ?drls {}"
\end{verbatim}

There then remains the cases where the cut-formula $A$ is not a compound formula
introduced by the logical introduction rules in the sets 
\texttt{lksil} and \texttt{lksir}.

This means that $A$ is either a boxed formula or a primitive proposition
(or, in our formulation, a formula variable). 
Because the bottom rule on either side may be a contraction on $A$, 
in which case cutting with the premise of that rule is of no help, 
we look upwards on either side to the lowest rule
which is not a contraction on $A$.

We have a lemma \texttt{top\_ctr\_r} which says that you can go up a derivation
tree to a rule which is not contraction on $A$ on the right.
A similar lemma \texttt{top\_ctr\_l} applies to contraction on the left.

\begin{verbatim}
top_ctr_r: "[| ?ctrrl = ([{#} |- {#?A#} + {#?A#}], {#} |- {#?A#});
   valid ?rls ?dt; conclDT ?dt = extend ?flr ({#} |- {#?A#}) |] ==>
   EX dtn n.  botRule dtn ~: extrs {?ctrrl} & valid ?rls dtn &
         heightDT ?dt = heightDT dtn + n &
         conclDT dtn = extend ?flr (times (Suc n) ({#} |- {#?A#}))"
\end{verbatim}

We then look at the final rule of that derivation tree (which is necessarily
not a contraction).
There are cases where the rule is either one of the box rules or is an
extension $\rho'$ of a rule $\rho$ in \texttt{lkxcne},
and in this case the rule may or may not have $A$ as its principal formula.

Where the rule has $A$ (in succedent position) as its principal formula,
it can only be weakening (or the axiom, which is a trivial case).
In this case either there are no contractions following the weakening, in which
case weakening (of $A$) makes the cut-elimination trivial, or
we construct a tree without the weakening step and with one fewer contractions,
and this tree has the same conclusion;
as this tree is smaller, we can apply the inductive hypothesis that 
cut-elimination is available.

% end of rwr_tacs
Next there is the case where the principal formula of the rule $\rho$
is not $A$.  
This case is like the parametric rule case of the simpler cut-elimiation
proofs.

\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A^n$}
\RightLabel{($\rho'$)}
\UnaryInfC{$X \vdash Y, A^n$}
\RightLabel{($\textit{ctr}^* \vdash$)}
\UnaryInfC{$X \vdash Y, A$}
\AxiomC{$A, U \vdash V$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{$X, U \vdash Y, V$}
\end{prooftree}
\end{center}

Here we must apply the requisite number of contractions on $A$ to the premises
of $\rho'$, then apply (using the inductive hypothesis) cut on $A$ to each of
them, and finally apply $\rho''$ which is the appropriate (but different from
$\rho'$) extension of $\rho$.

\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A^n$}
\RightLabel{($\textit{ctr}^* \vdash$)}
\UnaryInfC{$X' \vdash Y', A$}
\AxiomC{$A, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$X', U \vdash Y', V$}
\RightLabel{($\rho''$)}
\UnaryInfC{$X, U \vdash Y, V$}
\end{prooftree}
\end{center}

The remaining case is where the last rule on the left above the contractions on
$A$ is one of the $GTD$ rules. 
But as their conclusion is of the form $\Box \Gamma \vdash \Box A$,
this tells us that there are in fact no contractions following this rule.

We now look at the right side, and again, look for the last rule above a
continuous sequence of contractions on the cut-formula.

Among the cases of the last rule on the right above the contractions,
the cases of axiom or weakening involving $A$, or an extension of
a rule in \texttt{lkxcne} whose principal formula is not $A$, are similar to
those above.

This leaves us the case where the last rules on both sides above any
contractions are the GTD rules.

For the first case, the rule on the left is
 the $(\Box \vdash)$ rule as shown,
and for the rule on the right,
only its conclusion matters, and is as shown.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
\RightLabel{$(\Box\vdash)$}
\UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$\textit{ctr}^*\vdash$}
% \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
\AxiomC{$\cdots$}
\UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

We use the inductive hypothesis permitting cutting $\Box A$ between
$\Gamma, \Box \Gamma \vdash \Box A$ and $\Box A, \Box \Delta \vdash \Box B$
then we use weakening and the $(\Box \vdash)$ rule, to get

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
\AxiomC{$\cdots$}
\UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{weak})}
\UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
\RightLabel{($\Box\vdash$)}
\UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

The second case, with the $(\vdash \Box)$ rule on the left as shown,
is more complicated. 
Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash A$}
\RightLabel{$(\Box\vdash)$}
\UnaryInfC{$\Box \Gamma \vdash \Box A$}
\AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
\UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

In this case, from the premise on the right, we perform contractions on 
$\Box A$, then inductive cut on $\Box A$ with the conclusion on the left,
then contractions on $A$, then cut on $A$ with the premise on the left,
contraction(s) on $\Box \Gamma$, and finally an instance of the 
$(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
The result is shown below.

\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma, \Box \Gamma \vdash A$}
\AxiomC{$\Box \Gamma \vdash \Box A$}
\AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$A^n, \Box A, \Delta, \Box \Delta \vdash B'$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$A, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{$(\textit{ctr}^*\vdash)$}
\UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
\RightLabel{$(\vdash \Box)$ or $(\Box \vdash)$}
\UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
\end{prooftree}
\end{center}

Finally we combine these results to get the cut admissibility result,
in terms of explicit derivation trees, and then in terms of derivability.
\begin{verbatim}
gtd_casdt: "(?dta, ?dtb) : casdt (lkxcss GTD) ?A" : Thm.thm
gtd_cas: "(?cl, ?cr) : cas (lkxcss GTD) ?A" : Thm.thm 
\end{verbatim}

\section{GTD without structural rules} \label{s-cut-gtdns}

We now look at proving cut admissibility for a version of GTD without structural
rules, where the box rules have their conclusions (only) 
extended with an arbitrary context, which permits weakening to be admissible.

We define the rules of the system as follows.
The rules used for classical logic (before extending them with a context) 
form the set \texttt{lksne}: the rule sets \texttt{idrls},
  \texttt{lksil} and \texttt{lksir} 
are the axioms and the left and right logical introduction rules.

\begin{verbatim}
inductive "lkssx xrls"
  intros
    extI : "psc : lksne ==> pscmap (extend flr) psc : lkssx xrls"
    x : "psc : xrls ==> psc : lkssx xrls"

inductive "lksne"
  intros
    axiom : "([], {#A#} |- {#A#}) : lksne"
    ilI : "psc : lksil ==> psc : lksne"
    irI : "psc : lksir ==> psc : lksne"

inductive "extcs rules"
  intros
    I : "(ps, c) : rules ==> (ps, extend flr c) = epsc ==> epsc : extcs rules" 
\end{verbatim}

Then the set of rules of the system is \texttt{lkssx (extcs GTD)}.

First we prove weakening admissibility.
It follows directly from

\begin{verbatim}
wk_adm_extrs_cs: "wk_adm (extrs ?rlsa Un extcs ?rls)"
\end{verbatim}
which is proved in the same way that weakening admissibility is proved for S4.

For contraction admissibility,
first we need to prove invertibility of the logical rules.

SIMILAR to S4.  Uses 

\begin{verbatim}
lks_inv_stepm:
val it = "?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lksne) ?psc"

inv_stepm_disj_cs: 
  "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
  inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl" 

inv_stepm_disj:
   "[| seq_meet ?c ?ic = 0; extrs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
   inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"

inv_stepm_scrls:
   "[| extrs {?srl} = ?rls; ?rl : ?rls; ?srl : scrls; ?irl : scrls;
	snd ?srl = snd ?irl --> ?srl = ?irl |] ==>
    inv_stepm ?rls (extrs {?irl}) ?rl"
\end{verbatim}

The results \texttt{inv\_stepm\_disj\_cs} and \texttt{inv\_stepm\_disj} 
are for the case where the formula to be inverted is in the context of 
the conclusion of the last rule of the derivation:
the first premise gives you that the formula to be inverted is
not the principal formula of the rule, though it is expressed in a way 
which is relevant to a case where the rules in question have more than just one
principal formula.

The result \texttt{inv\_stepm\_scrls} 
(whose proof uses \texttt{inv\_stepm\_disj})
uses the fact that for each formula there is a unique introduction rule,
so an inversion step is either parametric or give syo the premise(s) of the last
rule applied.

Thus we get

\begin{verbatim}
gtdns_inv_rl: "Ball (extrs lksne) (inv_rl (lkssx (extcs GTD)))" 
\end{verbatim}

Then, to prove contraction admissibility,
SIMILAR to S4

we use 

\begin{verbatim}
ctxt_ctr_adm_step1_cs: "[| pg_meet ?concl (?As + ?As) <= ?As;
  ?rl = (?ps, ?concl); (?ps, extend ?flr ?concl) = ?erl;
  extcs {?rl} <= ?rules |] ==> ctr_adm_step1 (derrec ?rules {}) ?erl ?As"
\end{verbatim}
to handle the case where at least one of the copies of the formula to be
contracted arises from the extension of the conclusion of the box rule.

\texttt{ctr\_adm\_step1} is a simplified version of \texttt{ctr\_adm\_step},
without the inductive hypothesis relating to smaller formulae.

Now, for cut admissibility: the difficult cases are where the last rule on both
sides is one of the two box rules.

Since the proof is effectively the same whichever of the two rules is on the
right, we define 

\begin{verbatim}
inductive "s4g prs"
  intros
    I : "A : prs B ==>
      ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : s4g prs"
\end{verbatim}

and we prove the two results

\begin{verbatim}
s4_box_box_lem:
   "[| ?prsl = (%B. {B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)" 

gtd_box_box_lem:
   "[| ?prsl = (%B. {Box B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)" 
\end{verbatim}

For the cut-elimination proof we also use results for the 
parametric cases, that is, where the cut-formula appears in the context of the
last rule on either side above the cut.
This includes cases where that rule is in \texttt{extrs} \ldots 
(where the rule has a context which appears in premises and conclusion)
and where that rule is in \texttt{extcs} \ldots 
(where the rule has a context which appears only in the conclusion).

\begin{verbatim}
lcg_gen_step: "[| wk_adm ?erls; extrs {(?ps, ?U |- ?V)} <= ?erls; ~ ?A :# ?V;
  ?pscl = pscmap (extend (?W |- ?Z)) (?ps, ?U |- ?V) |] ==>
  gen_step2sr (prop2 car ?erls) ?A ?any ?erls (?pscl, ?pscr)"

lcg_gen_steps_extcs:
  "[| wk_adm ?rls; extcs {(?ps, ?c)} <= ?rls; ~ ?A :# succ ?c |] ==>
  gen_step2sr (prop2 car ?rls) ?A ?sub ?rls ((?ps, extend ?flr ?c), ?psr, ?cr)"
\end{verbatim}

Finally we need to deal with the cases of matching instances of the usual
logical introduction rules.
Here we use the general result

\begin{verbatim}
gs2sr_alle: "[| wk_adm ?prls; c8_ercas_prop ?psubfml ?prls ?A ?rls;
  ?rls <= iscrls; idrls <= ?prls; extrs ?rls <= ?prls;
  (?psa, ?ca) : extrs ?rls; (?psb, ?cb) : extrs ?rls |] ==>
  gen_step2sr (prop2 car ?prls) ?A ?psubfml ?prls ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}

This theorem (which incorporates the parametric cases) uses 
\texttt{c8\_ercas\_prop} which says essentially that if both sides of the cut are
logical introduction rules, and cut is admissible on smaller cut-formulae,
then the cut in question is admissible.
The property \texttt{c8sg\_prop} is almost identical ---
the difference is weakening / contraction.

(LATER - on looking back at the previous section I find the result
\texttt{gprstep\_q} shown -
basically that result plus the case of the axiom rules gives you
\texttt{gen\_lksne\_c8sg} below)

Omitting the definition of \texttt{c8\_ercas\_prop},
here is the theorem which uses it:

\begin{verbatim}
c8_ercas_gs2: "[| c8_ercas_prop ?psubfml ?drls ?A ?c8rls;
  ?prl = (?ps, 0 |- {#?A#}); ?prl : ?c8rls;
  ?qrl = (?qs, {#?A#} |- 0); ?qrl : ?c8rls;
  ?eprl = pscmap (extend ?pe) ?prl; ?eqrl = pscmap (extend ?qe) ?qrl |] ==>
  gen_step2sr (prop2 car ?drls) ?A ?psubfml ?drls (?eprl, ?eqrl)"

c8sg_ger: "c8sg_prop ?sub ?rls ?drls ?A ==> c8_ercas_prop ?sub ?drls ?A ?rls"
\end{verbatim}

The key property here is that 

\begin{verbatim}
gtdns_lksne_c8sg: "c8sg_prop ipsubfml (lkssx (extcs GTD)) ?A lksne"
\end{verbatim}

which in turn uses the more general result which is not specific to GTD

\begin{verbatim}
gen_lksne_c8sg: "[| All (ctr_adm ?drls); wk_adm ?drls; extrs lksne <= ?drls |]
         ==> c8sg_prop ipsubfml lksne ?drls ?A"
\end{verbatim}

Finally we get the cut admissibility result:

\begin{verbatim}
gtdns_casdt: "(?dt, ?dta) : casdt (lkssx (extcs GTD)) ?A" 

gtdns_cas:
   "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (lkssx (extcs GTD)) ?A"
\end{verbatim}
