
\section{Dynamic Topological Logic: the system S4C (without structural rules)}
  \label{s-s4cns}

This section describes Isabelle proofs of the
cut admissibility of the logic S4C described in \cite{mints-jaegerfest}

This system has two ``modal'' operators, $\Box$ and $\circ$.
The $S4$-axioms hold for $\Box$, $\circ$ commutes with the boolean operators,
and the following are given:
\begin{align*}
\circ (A \to B) & \leftrightarrow (\circ A \to \circ B) \\
\circ \bot & \leftrightarrow \bot \\
\circ \Box A & \to \Box \circ A
\end{align*}

The following sequent rules are given for S4C
$$
\frac{\circ^k A, \Gamma \vdash \Delta, \circ^k B}
  {\Gamma \vdash \Delta, \circ^k (A \to B)}(\vdash\to)
\qquad
\frac{\Gamma \vdash \Delta, \circ^k A \quad \circ^k B, \Gamma \vdash \Delta}
  {\circ^k (A \to B), \Gamma \vdash \Delta}(\to\vdash)
$$
$$
\frac{\circ^k A, \Gamma \vdash \Delta}
  {\circ^k \Box A, \Gamma \vdash \Delta}(\Box\vdash)
\qquad
\frac{\Gamma \vdash \Delta}
  {\circ \Gamma \vdash \circ \Delta}(\circ)
\qquad
\frac{\mathcal B \vdash A}{\mathcal B \vdash \Box A}(\vdash\Box)
$$

In the $(\vdash\Box)$ rule, $\mathcal B$ must consist of 
``$\Box$-formulae'', that is, formulae of the form $\circ^k \Box A$.


As this presentation omits the other logical operators, 
we include, for them, the usual logical introduction rules
with the principal and side formulae preceded by $\circ^k$ just 
as with the $(\vdash\to)$ and $(\to\vdash)$ rules shown above.

% The property we will prove inductively is mix (rather than cut) admissibility.
We use a version of the system without structural rules: we prove
invertibility of the logical rules and contraction admissibility.
In fact the presence of the $(\circ)$ rule adds to the complexity of the proof
and is dealt with in a rather similarly to how we dealt with contraction in
proving cut admissibility for GTD.

As we do not have the structural rules,
we use a presentation of the system which 
\begin{itemize}
\item allows an arbitrary context to be added to the conclusion (only) of the
$(\vdash \Box)$ and $(\circ)$ rules
\item uses a version of the $(\Box \vdash)$
rule which includes the principal formula in the premise
\end{itemize}

$$
\frac{\Gamma \vdash \Delta}
  {\Gamma', \circ \Gamma \vdash \circ \Delta, \Delta'}(\circ)
\qquad
\frac{\mathcal B \vdash A}{\Gamma, \mathcal B \vdash \Box A, \Delta}
  (\vdash\Box)
\qquad
\frac{\circ^k \Box A, \circ^k A, \Gamma \vdash \Delta}
  {\circ^k \Box A, \Gamma \vdash \Delta}(\Box\vdash)
$$

We now describe how we formalised the system.
First we define the rules which can be extended by an arbitrary context
in their premises and conclusion.
Without the context, these rules form the set \texttt{s4cnsne}.

Applying \texttt{nkmap} $k$ to a rule applies $\circ^k$ to each formula
appearing in that rule.

\begin{verbatim}
inductive "s4cnsne"
  intros
    id : "psc : idrls ==> psc : s4cnsne"
    circ_il : "rl : lksil ==> nkmap k rl : s4cnsne"
    circ_ir : "rl : lksir ==> nkmap k rl : s4cnsne"
    circ_T : "rl : lkrefl ==> nkmap k rl : s4cnsne"

inductive "lkrefl" 
  intros
    I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"

defs
  nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))"

inductive "s4cns"
  intros
    extI : "rl : s4cnsne ==> pscmap (extend (U |- V)) rl : s4cns"
    extcsI : "(ps, c) : circ Un s4cbox ==> (ps, extend (U |- V) c) : s4cns"

inductive "circ"
  intros
    I : "([seq], seqmap Circ seq) : circ"

inductive "s4cbox"
  intros
    boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cbox"

inductive "msboxfmls"
  intros
    I : "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls"

inductive "boxfmls"
  intros
    I : "funpow Circ k (Box B) : boxfmls"
\end{verbatim}

We first need to prove admissibility of the structural rules, weakening and
contraction.
QUESTION - we did prove contraction admissibility, but is it essential?

Weakening admissibility was straightforward using Lemma~\ref{l-ext-concl-wk}.

Invertibility of the logical introduction rules was dealt with using multiple
lemmas showing various cases of \texttt{inv\_stepm}, as described in
\S\ref{s-s4-inv}: as noted there, a proof of invertibilty can be split up into 
\begin{itemize}
\item the invertibility of various different rules 
\item cases of what the last rule in the derivation, 
from whose conclusion we wish to apply one of the inverted rules
\end{itemize}
As in \S\ref{s-s4-inv}, we make significant use of 
Lemma~\ref{lemma:inv-stepm-monotonic}.

We then prove contraction admissibility.
In part this also makes use of the general result
(NOTE - also used in S4, but not by Jesse as I hadn't done this by then)

This uses predicates and results very similar to Definition~\ref{d-gen-step}
and Lemma~\ref{genstep:lem}, but instantiated to apply to the property of
contraction admissibility.

\begin{verbatim}
gen_ctr_adm_step: "[| ?A : wfp ?sub;
       ALL dt. ALL (ps, concl):?rules.
               ctr_adm_step ?sub (derrec ?rules {}) (ps, concl) dt |]
      ==> ctr_adm ?rules ?A" 

ctr_adm_step_eq: "ctr_adm_step ?sub ?derivs (?ps, ?concl) ?A =
  (ALL As.  ms_of_seq As = {#?A#} -->
    (ALL A'.  (A', ?A) : ?sub --> (ALL As.  ms_of_seq As = {#A'#} -->
      (ALL XY.  XY : ?derivs --> As + As <= XY --> XY - As : ?derivs))) -->
    (ALL p:set ?ps. p : ?derivs & (As + As <= p --> p - As : ?derivs)) -->
    As + As <= ?concl --> ?concl - As : ?derivs)"
\end{verbatim}

We now look at proving \texttt{ctr\_adm\_step} for each possible case for
the last rule of a derivation.

\begin{lemma} \label{l-gen-ctr-adm-step-inv}
If 
\begin{itemize}
\item rule set $lrls$ consists of rules
   which are the identity (axiom) rules $A \vdash A$,
   or are rules with a single formula in their conclusion,
\item all rule in $lrls$ have the ``subformula'' property 
  (which here means that for every premise \emph{other than a premise which
contains the conclusion}, every formula in that premise is a subformula of a
formula in the conclusion
\item the rule set $drls$ (derivation rules) contains the extensions of $lrls$
\item in regard to the derivation rules $drls$, the inverses of extensions of
$lrls$ are admissible
\item rule $(ps, c)$ is an extension of a rule of $lrls$
\end{itemize}
then the contraction admissibility step \texttt{ctr\_adm\_step}
 holds for the final rule $(ps, c)$ and the derivation rule set $drls$:
that is, assuming that
\begin{itemize}
\item contraction on formulae $A'$ smaller than $A$ is admissible, and 
\item contraction on $A$ is admissible in the sequents $ps$
\end{itemize}
 then contraction on $A$ in sequent $c$ is admissible.  
\end{lemma}

\begin{verbatim}
gen_ctr_adm_step_inv:
   "[| ?epsc : extrs ?lrls; ?lrls <= iscrls; extrs ?lrls <= ?drls;
         Ball ?lrls (subfml_cp_prop ?sub);
         Ball (extrs ?lrls) (inv_rl ?drls) |] ==>
   ctr_adm_step ?sub (derrec ?drls {}) ?epsc ?A"

subfml_cp_prop.simps:
   "subfml_cp_prop ?sub (?ps, ?c) =
      (ALL p:set ?ps. ?c <= p |
	(ALL fp. ms_mem fp p --> (EX fc. ms_mem fc ?c & (fp, fc) : ?sub)))" 
\end{verbatim}

Then the other cases of \texttt{ctr\_adm\_step} were proved separately:

\begin{verbatim}
ctr_adm_step_s4cbox:
   "[| ?psc = (?ps, ?c); ?psc : extcs s4cbox; extcs s4cbox <= ?drls |]
      ==> ctr_adm_step ?sub (derrec ?drls {}) ?psc ?A"

ctr_adm_step_circ:
   "[| ?psc = (?ps, ?c); ?psc : extcs circ; extcs circ <= ?drls |]
      ==> ctr_adm_step ipsubfml (derrec ?drls {}) ?psc ?A"
\end{verbatim}

To prove cut admissibility, the basic method is to look for the last rule
application on each side of a rule other than the $(\circ)$ rule.
This resembles the proof described in \S\ref{s-cut-gtd}, where we looked for
the last rule on each side which is not contraction on the cut-formula.
For this we use the theorem \texttt{top\_circ\_ns}.
We also need the fact that in some cases we need the fact that if the bottom
rule is not $(\circ)$, then the tree asserted to exist is actually the original
one.
The function \texttt{forget} exists simply to prevent automatic case splitting
of its argument: logically it does nothing.

\begin{verbatim}
top_circ_ns: "valid ?rls ?dt ==> EX dtn k.
   botRule dtn ~: extcs circ & valid ?rls dtn &
   seqmap (funpow Circ k) (conclDT dtn) <= conclDT ?dt &
   heightDT ?dt = heightDT dtn + k &
   forget ((k = 0) = (botRule ?dt ~: extcs circ) & (k = 0) = (dtn = ?dt))"

forget_def: "forget ?f == ?f"
\end{verbatim}

But one easy case is where the last rule on \emph{both} sides is the $(\circ)$
rule: then we can apply cut (on a smaller formula) to the premises of the
$(\circ)$ rules, and then apply the $(\circ)$ rule.
So when we look at the $(\circ)$ rules on both sides immediately preceding the
cut, we need only bother about the case where the number of those 
$(\circ)$ rules is zero on one side.

First, the case where both rules are the $(\vdash\Box)$ rule.
The fact that the conclusions of both the $(\circ)$ rule and the $(\vdash\Box)$ 
rule may be extended by an arbitrary context complicates matters.
Consider the following diagram of a number of $(\circ)$ rules followed by the
$(\vdash\Box)$ rule.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\Gamma, \M \vdash \Box A, \Delta$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\Gamma', \circ^k \Gamma, \circ^k \M \vdash 
  \circ^k \Box A, \circ^k \Delta, \Delta'$}
\end{prooftree}
\end{center}

In this case we can instead construct the following derivation tree,
which is of the same height.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\end{prooftree}
\end{center}
Thus we can use, in proving an inductive step, the fact that
$\circ^k \M \vdash \circ^k \Box A$ is derivable, and with a derivation
of the same height as that of $\Gamma', \circ^k \Gamma, \circ^k \M \vdash 
  \circ^k \Box A, \circ^k \Delta, \Delta'$.
This will be used in our proofs without further comment.

Now, where the cut-formula is within $\circ^k Y, V$ (where this is the
derivation tree on the left of a desired cut), or within $U, \circ^k X$
(where this tree is on the right), the cut is admissible because we can
start from the derivable sequent $\M \vdash A$ and apply $(\vdash\Box)$ and 
$\circ$ rule without any extra formulae in the conclusions, as discussed above.
In this case we just use weakening admissibility
to obtain the result of the cut.

These situations are covered by the lemmas 
\texttt{s4cns\_cs\_param\_l''} and \texttt{s4cns\_cs\_param\_r''}.

\begin{verbatim}
s4cns_cs_param_l'':
  "[| (?ps, ?cl |- ?cr) : s4cns; botRule ?dtn : extcs {(?ps, ?cl |- ?cr)};
     count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4cns ?dtn |] ==>
   sumh_step2_tr (prop2 casdt s4cns) ?C ?sub 
  (Der (seqmap (funpow Circ ?k) (conclDT ?dtn) + ?flr) ?list,
       Der ?dtr ?lista)" 
\end{verbatim}

A similar pair of results, discussed later,
covers the case where the rule above the $(\circ)$
rules is a base rule which is extended by an arbitrary context in its
conclusion \emph{and} its premises.  

Now we can assume that the cut-formula is within the principal part of the 
rule before the $(\circ)$ rules (noting that for the $(\vdash\Box)$ rule
the ``principal part'' means the entire $\M \vdash \Box A$).
Then there must be zero $(\circ)$ rules on the right side (because if there are 
zero $\circ$ rules on the left, then the cut-formula must be $\Box A$, whence
there would also be zero $(\circ)$ rules on the right.

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

Here we do the cut, by induction, before the $(\vdash\Box)$ rule on the right, 
using a derivation like that on the left, but without any context,
then we apply the $(\vdash\Box)$ rule, introducing the required context.

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

For the other cases, we first consider the ``parametric'' cases,
where the last rule above the $(\circ)$ rules is an extension $\rho'$
of a rule $\rho$ in \texttt{s4cnsne},
and the principal formula of $\rho$ is not the ``de-circled'' cut-formula $A$.

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

Here we must apply the $\circ$ rule the requisite number of times 
to the premise(s) of $\rho'$,
then apply (using the inductive hypothesis) cut on $\circ^k A$ to each of
them, and finally apply $\rho''$ which we get by applying
$\circ^k$ to $\rho$, and then extending it appropriately.

This uses the result that if a rule is in \texttt{s4cnsne}
then so is the result of applying $\circ^k$ to all formulae in its premises and
conclusion.

\begin{verbatim}
s4cnsne_nkmap: "?r : s4cnsne ==> nkmap ?k ?r : s4cnsne"
\end{verbatim}

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

Lemmas \texttt{s4cns\_param\_l'} and \texttt{s4cns\_param\_r'} cover this case.

\begin{verbatim}
s4cns_param_l': "[| (?ps, ?cl |- ?cr) : s4cnsne;
     botRule ?dtn : extrs {(?ps, ?cl |- ?cr)};
     count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4cns ?dtn;
     Suc (heightDTs ?list) = heightDT ?dtn + ?k |] ==>
    sumh_step2_tr (prop2 casdt s4cns) ?C ?sub
       (Der (seqmap (funpow Circ ?k) (conclDT ?dtn) + ?flr) ?list,
        Der ?dtr ?lista)"
\end{verbatim}

It is similar for the parametric case on the right.
The axiom rule is trivial in all cases.

For the $(\vdash \Box)$ rule on the left, where the rule on the right 
is an extension of rule $\rho$ whose principal formula is the ``de-circled''
cut-formula, the only case remaining is where $\rho$ is $(\Box \vdash)$.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash \Box)$}
\UnaryInfC{$X, \M \vdash \Box A, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$X', \circ^k X, \circ^k \M \vdash \circ^k \Box A, \circ^k Y, Y'$}
\AxiomC{$\circ^{k''} A, U \vdash V$}
\RightLabel{$(\Box \vdash)$}
\UnaryInfC{$\circ^{k''} \Box A, U \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^{k' + k''} \Box A, \circ^{k'} U, U' \vdash \circ^{k'} V, V'$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{$X', \circ^k X, \circ^k \M, \circ^{k'} U, U' \vdash 
  \circ^k Y, Y', \circ^{k'} V, V'$}
\end{prooftree}
\end{center}

Here $k' + k'' = k$, but since we also have that $k = 0$ or $k' = 0$,
this means that $k' = 0$ and $k'' = k$.  The following diagram omits
a final use of the admissibility of weakening.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k A$}
\AxiomC{$\M \vdash A$}
\RightLabel{($\vdash \Box$)}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k \Box A, \circ^k A, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\circ^k \M, \circ^k A, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\circ^k \M, \circ^k \M, U \vdash V$}
\RightLabel{(\textit{ctr})}
\UnaryInfC{$\circ^k \M, U \vdash V$}
\end{prooftree}
\end{center}

Next we look at the case of the $(\vdash \Box)$ rule on the right,
but for this, since the cut-formula must be a $\Box$-formula,
all cases have already been dealt with.

Finally, there is the case where the last rules (above the final sequence of
$\circ$-rules) on both sides are extensions of rules in \texttt{s4cnsne}. 
Most of these cases have been covered, ie,
the axiom rules, and 
the ``parametric'' cases, where the ``de-circled'' cut-formula 
is not the principal formula of the rule.

So there remain the cases where the rules on either side are the logical
introduction rules.
For these, the proofs are essentially the same as for other logics generally,
except that we need to allow for a number of circles.
Conceptually it is easiest to imagine that in each case the final $\circ$ rules
are moved upwards to precede the final logical introduction rules,
although we didn't actually prove it this way.

We proved that the usual logical introduction rules,
with $\circ^k$ applied to principal and side formulae (as used in S4C),
satisfy the property \texttt{c8ger\_prop} mentioned in \S\ref{s-induction}.
Recall that this means that assuming cut admissibility on smaller
formulae, you have cut admissibility of a more complex formula where the last
rule on either side is a logical introduction rule.

\begin{verbatim}
s4cns_c8: "c8ger_prop (circrel ipsubfml) s4cns ?A 
    (nkmap ?k ` (lksil Un lksir))"
\end{verbatim}

The following diagrams show an example.
We let $t = k + k' = l + l'$.
In this case we do not make use of the fact that either $k$ or $l$ must be
zero.

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\vdash \land$)}
\BinaryInfC{$X \vdash \circ^{k'} (A \land B), Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t (A \land B), \circ^k Y$}
\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\land \vdash$)}
\UnaryInfC{$U, \circ^{l'} (A \land B) \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U \vdash \circ^k Y, \circ^l V$}
\end{prooftree}
\end{center}

The diagram above is simplified by not including the extra context which
may be introduced in the conclusion of the $(\circ)$ rules.
This is replaced by

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t A, \circ^k Y$}
\AxiomC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U \vdash \circ^t A, \circ^k Y, \circ^l V$}
\dottedLine
\UnaryInfC{\large (A)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t B, \circ^k Y$}
\AxiomC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U \vdash \circ^t B, \circ^k Y, \circ^l V$}
\dottedLine
\UnaryInfC{\large (B)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$\circ^k X \vdash \circ^t (A \land B), \circ^k Y$}
\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t A, \circ^t B \vdash \circ^l V$}
\RightLabel{(\textit{inductive cut})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U, \circ^t A, \circ^t B \vdash 
  \circ^k Y, \circ^l V$}
\dottedLine
\UnaryInfC{\large (C)}
\end{prooftree}
\end{center}

Then (A), (B) and (C) are combined using inductive cuts on the smaller
cut-formulae $\circ^t A$ and $\circ^t B$, and the necessary contractions, to
derive the required sequent
{$\circ^k X, \circ^l U \vdash \circ^k Y, \circ^l V$}.
Again, we can use weakening admissibility to get the extra context which 
was introduced by the $(\circ)$ rules, but omitted from the first diagram.

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}
s4cns_casdt: "(?dta, ?dtb) : casdt s4cns ?A" 
s4cns_cas: "(?cl, ?cr) : cas s4cns ?A"
\end{verbatim}

