\section{Introduction}

\label{intro}

A multisuccedent sequent calculus  for intuitionistic logic free of structural rules was presented   in \cite{D88} and a
detailed proof of their admissibility,   based on \cite{D97},  appeared in \cite{NvP01}. A single succedent version of that calculus
was adopted in \cite{TS96}. In all cases the proof of the admissibility of the structural rules relies, as for the classical $ {\bf G3}$ system, on the hight-preserving admissibility of the contraction rule.
When additional atomic rules are added to the calculus the hight-preserving admissibilibility of the contraction rule may fail. Such is the case for example for the following rules
 $\hbox{Ref}$ and $ \hbox{Repl}$   for equality, introduced in \cite{NvP98} and adopted in  the second edition \cite{TS00} of \cite{TS96}
    \[
\begin{array}{clccl}
\underline{t=t,\Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{~Ref}}&~~~~~~~~~~~~~~~~~~~~~&\underline{s=r, P[x/s],P[x/r], \Gamma \Rightarrow \Delta}&\vbox to 0pt{\hbox{~Repl}}\\
\Gamma\Rightarrow \Delta&&&s=r, P[x/s], \Gamma \Rightarrow \Delta&
\end{array}
\]

For example
\[
a=f(a), a=f(a) \Rightarrow  a=f(f(a))
\]
has  derivations of height equal 1  in the systems obtained by adding $\hbox{Ref}$ and $\hbox{Repl}$  to ${\bf G3[mic]}$
 namely
\[
\begin{array}{c}
a=f(a), a=f(a),  a=f(f(a)) \Rightarrow a=f(f(a))\\
\cline{1-1}
a=f(a), a=f(a) \Rightarrow  a=f(f(a))
\end{array}
\]
but $a=f(a)\Rightarrow a=f(f(a))$ cannot have  a derivation of height less than or equal 1 in such a system.

For that reason, in such cases, to prove the admissibility of the structural rules    we  have to  follow a route somewhat different from
the one used in  \cite{NvP98} (see also \cite{NvP01} and \cite{NvP11}),
and from the one followed in \cite{TS00} for extensions of their single succedent ${\bf G3[mic]}$ calculus with  rules for which hight preserving admissibilty of the contraction rule is ensured. The basic idea is to eliminate context-sharing cuts first,  with the eliminability of contraction obtained as a consequence, due to its immediate derivability from context-sharing cut.

Actually we  will show that we can proceed in that way for any set ${\cal R}$ of atomic formulae of the following form:

\[
\begin{array}{cl}
\underline{\vec{Q_1},\Gamma_1\Rightarrow \Delta_1, \vec{Q_1'} ~~\ldots ~~\vec{Q_n},\Gamma_n\Rightarrow \Delta_n, \vec{Q_n'}}&\\
\vec{P}, \Gamma_1,\ldots, \Gamma_n \Rightarrow \Delta_1,\ldots, \Delta_n, \vec{P'}
\end{array}
\]
where $\vec{Q_1}, \vec{Q_1'} ,\ldots, \vec{Q_n},  \vec{Q_n'}, \vec{P},\vec{P'}$ are
 sequences (possibly empty) of  atomic formulae and $\Gamma_1,\ldots, \Gamma_n, \Delta_1,\ldots \Delta_n$  are  finite sequences (possibly empty) of formulae that are not active in the rule.

More precisely,  letting  ${\bf G3[mic]}^{\cal R}$ denote the calculi  obtained by adding to ${\bf G3[mic]}$ the rules in ${\cal R}$  and $Cut_{cs}$   the context-sharing cut rule,  we will show that
 any derivation in  ${\bf G3[mic]}^{\cal R} + Cut_{cs}$ can be transformed into a derivation in the same system
 in which the  rules in ${\cal R}$ and the $Cut_{cs}$ rule are applied before any logical rule. From that it will follow that
if the structural rules are admissible  in the calculus that contains only the initial sequents  and the rules in ${\cal R}$, then they are admissible in  ${\bf G3[mic]}^{\cal R}$ as well.
For ${\cal R}=\emptyset$  we have   that  the height preserving admissibility of the weakening rules and the height-preserving invertibility of the logical rules  suffice for the eliminability of context-sharing cut, without having to obtain the admissibility of contraction first, and, as a  consequence, for the admissibility of the $Cut$-rule in ${\bf G3[mic]}$.
For ${\cal R}= \{ \hbox{Ref},   \hbox{Repl}\}$ we obtain  that the structural rules are admissible in ${\bf G3[mic]}^{\cal R}$, thus extending the result proved in \cite{NvP98} in the case $t,r$ and $s$ are restricted to be constants.

\section{Preliminaries }
\label{Preliminaries}

The sequent calculus ${\bf G3c}$ in \cite{N16} has, in  the notations in \cite{TS00},  the following initial sequents and rules, where $P$ is an atomic formula and $A, B$ stand for any formula in a first order language   (function symbols included) and $\Gamma$ and $\Delta$ are finite multisets of formulae :

\

{\bf Initial sequents}
\[
P,\Gamma \Rightarrow \Delta, P
\]

{\bf Logical rules}

\[
\begin{array}{clccl}
A,B, \Gamma \Rightarrow \Delta&\vbox to 0pt{\hbox{$L\wedge $}}&~~~~~~&\underline{\Gamma\Rightarrow,\Delta, A~~~\Gamma\Rightarrow \Delta, B}& \vbox to 0pt{\hbox{$R\wedge$}}\\
\overline{A\wedge B, \Gamma \Rightarrow \Delta}&&&\Gamma \Rightarrow \Delta, A\wedge B\\

\\
\underline{A,\Gamma\Rightarrow \Delta~~~B,\Gamma \Rightarrow \Delta}& \vbox to 0pt{\hbox{$L\vee $}}&&\Gamma\Rightarrow \Delta, A, B& \vbox to 0pt{\hbox{$R\vee$}}\\
A\vee B, \Gamma \Rightarrow \Delta&&&\overline{\Gamma\Rightarrow\Delta, A\vee B}\\

\\

\\

\underline{\Gamma\Rightarrow \Delta, A~~~B,\Gamma \Rightarrow \Delta}&\vbox to 0pt{\hbox{$L\rightarrow $}}&&A,\Gamma \Rightarrow \Delta, B&\vbox to 0pt{\hbox{$R\rightarrow $}}\\
A\rightarrow B, \Gamma \Rightarrow \Delta&&&\overline{\Gamma \Rightarrow \Delta, A\rightarrow B}&\\
\\

\\
\overline{\bot, \Gamma \Rightarrow \Delta}^{~L\bot}&&&&\\

\\
\\

\underline{A[x/t], \forall x A,\Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{$L\forall $}}&&\underline{\Gamma\Rightarrow \Delta, A[x/a]}&\vbox to 0pt{\hbox{$R\forall $}}\\
\forall xA, \Gamma\Rightarrow \Delta&&&\Gamma\Rightarrow \Delta, \forall x A\\

\\

\\
\underline{A[x/a], \Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{$L\exists $}}&&\underline{\Gamma\Rightarrow \Delta, \exists x A,  A[x/t]}&\vbox to 0pt{\hbox{$R\exists $}}\\
\exists xA, \Gamma\Rightarrow \Delta&&&\Gamma\Rightarrow \Delta, \exists x A

\end{array}
\]

In ${\bf G3i}$ the rules $L\rightarrow$, $R\rightarrow$ and $R\forall$ are replaced by:

\[
\begin{array}{clccl}
\underline{A\rightarrow B, \Gamma \Rightarrow \Delta, A~~~B,\Gamma \Rightarrow \Delta}&\vbox to 0pt{\hbox{$L^i\rightarrow $}}&~~~~~~~~&A,\Gamma \Rightarrow B&\vbox to 0pt{\hbox{$R^i\rightarrow $}}\\
A\rightarrow B, \Gamma\Rightarrow \Delta&&&\overline{\Gamma\Rightarrow\Delta, A\rightarrow B}\\

\\
\\

&&&\Gamma\Rightarrow A[x/a]&\vbox to 0pt{\hbox{$R^i\forall $}}\\
&&&\overline{\Gamma\Rightarrow \Delta, \forall x A}&

\end{array}
\]
In  both ${\bf G3c}$ and ${\bf G3i}$,   $a$ does not occur in the conclusion of $L\exists$ and $R\forall$.

Finally ${\bf G3m}$ is obtained from ${\bf G3i}$ by replacing $L\bot$ by the initial sequents $\bot, \Gamma \Rightarrow \Delta, \bot$.

\

${\bf G3[mic]}$ denotes any of the systems ${\bf G3m}$,   ${\bf G3i}$ or  ${\bf G3c}$.

\

The left and right weakening rules, $LW$ and $RW$ have the form:

\[
\begin{array}{clccl}
\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{$LW$}}&~~~~&\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{$RW$}}\\
\cline{1-1}\cline{4-4}
A,\Gamma\Rightarrow \Delta&&&\Gamma\Rightarrow\Delta,A
\end{array}
\]
The left and right contraction rules, $LC$ and $RC$ have the form:

\[
\begin{array}{clccl}
A.A, \Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{$LC$}}&~~~~&\Gamma\Rightarrow \Delta, A,A&\vbox to 0pt{\hbox{$RC$}}\\
\cline{1-1}\cline{4-4}
 A,\Gamma\Rightarrow \Delta&&&\Gamma\Rightarrow\Delta,A
 \end{array}
\]

The cut rule  and the context-sharing cut rule, $Cut$  and $Cut_{cs}$  have the form:
\[
\begin{array}{clcclccl}
\Gamma\Rightarrow\Delta, A~~~~A,\Lambda \Rightarrow \Theta&\vbox to 0pt{\hbox{$Cut $}}&~~&&~~&&\Gamma\Rightarrow \Delta, A~~~A,\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{$Cut_{cs} $}}\\
\cline{1-1}\cline{7-7}
\Gamma,\Delta\Rightarrow \Lambda,\Theta&&&&&&\Gamma\Rightarrow \Delta\\
\end{array}
\]

\

The additional atomic rules that we will consider are  of the form described in  \ref{intro}.

\subsection{Separated derivations}
\label{sep}

In all the systems considered the weakening rules are height-preserving admissible. For left weakening   it suffices to add $A$ to the antecedent  of every sequent in a given derivation of $\Gamma \Rightarrow \Delta$, modulo a possible renaming of the proper variables in the $L\exists$ and $R\forall$ inferences,  to obtain a derivation of the same height of $A, \Gamma\Rightarrow \Delta$. In the classical case one can proceed in the same way also for right weakening, while in the minimal or intuitionistic case one uses  induction on the height of derivation, taking advantage of the possibility of adding an arbitrary context on the right in the applications of $R^i\rightarrow$ and $R^i\forall$.

\begin{definition}
For a set of additional  atomic rules ${\cal R}$, let ${\bf G3[mic]}^{\cal R}$ be the sequent calculus obtained from  ${\bf G3[mic]}$
by adding  the rules in ${\cal R}$.
With ${\cal R}$ we will denote also the  logic-free subcalculus of  ${\bf G3[mic]}^{\cal R}$, that contains only the initial sequents $P,\Gamma\Rightarrow \Delta, P$  and the rules in ${\cal R}$.
\end{definition}

\begin{definition}
Let ${\cal R}$ be any set of atomic rules. An ${\cal R}$-inference is any application of a rule in ${\cal R}$. An ${\cal R}$-derivation is a derivation in
${\bf G3[mic]}^{\cal R}$.
\end{definition}

\begin{definition}
A derivation in  ${\bf G3[mic]}^{\cal R} +Cut_{cs}$
 is  said to be {\em separated} if no logical inference  precedes an ${\cal R}$  or $Cut_{cs}$-inference.
\end{definition}

Our first goal  is to show that every derivable sequent in ${\bf G3[mic]}^{\cal R} +Cut_{cs}$
has a separated derivation in the same system.
Derivations without  logical inferences are trivially separated. For such derivations we have the following useful fact.

\begin{lemma}\label{atomic}
If $\Gamma\Rightarrow \Delta$ has a derivation ${\cal D}$ in ${\cal R}$, then there is a subsequent $\Gamma^\circ\Rightarrow \Delta^\circ$ of $\Gamma\Rightarrow \Delta$, with atomic formulae only, that has a derivation ${\cal D}^\circ$ in the same system, with only atomic sequents, such that $h({\cal D}^\circ)\leq h({\cal D})$.
\end{lemma}

{\bf Proof} The claim is  proved by a straightforward induction on the height of derivations, thanks to the height-preserving admissibility of the weakening rules. $\Box$

\begin{lemma}\label{invertzero}
If the conclusion of a classical logical rule has a derivation in ${\cal R}$  of height bounded by $h$, then also its premisses have  derivations
 in ${\cal R}$ of height bounded by $h$. The same holds in the minimal  and intuitionistic case with the exception of rules $R\rightarrow$ and $R\forall$.
\end{lemma}
{\bf Proof} By the previous lemma, there is a derivation  ${\cal D}^\circ$ of height bounded by $h$ of an atomic subsequent $\Gamma^\circ\Rightarrow \Delta^\circ$ of the conclusion of the logical inference. Being  atomic  $\Gamma^\circ\Rightarrow \Delta^\circ$  does not contain the principal formula of the logical inference we are interested in and its premiss or premisses can be obtained from  ${\cal D}^\circ$   by weakening. $\Box$

\begin{proposition}\label{invert}
\begin{itemize}
\item[a)]  Hight-preserving separated invertibility of the logical rules in ${\bf G3c}^{\cal R} +Cut_{cs}$

If the conclusion of a logical inference has a separated derivation of height bounded by $h$, then also its  premisses  have  separated derivations of height bounded by $h$.

\item[b)] The same holds for ${\bf G3[mi]}^{\cal R} +Cut_{cs}$, except for the rules  $R^i\rightarrow$ and $R^i\forall$.
\end{itemize}

\end{proposition}

{\bf Proof}  If the given derivation ${\cal D}$ reduces to an initial sequent or to an instance of $L\bot$ or it ends with a logical inference that does not introduce the principal formula of the rule $R$ to be proved invertible, then the argument is the same as for  the ${\bf G3[mic]}$ systems (see \cite{D88},  \cite{NvP01}).
For example if ${\cal D}$ has the form:

\[
\begin{array}{ccc}
{\cal D}_0&~~~&{\cal D}_1\\
E\rightarrow F, A\rightarrow B, \Gamma \Rightarrow \Delta, E&&F, A\rightarrow B, \Gamma\Rightarrow \Delta\\
\cline{1-3}
\multicolumn{3}{c}{A\rightarrow B, E\rightarrow F, \Gamma\Rightarrow \Delta}
\end{array}
\]
and the rule to be proved invertible is an $L^i\rightarrow$ with principal formula $A\rightarrow B$, then a derivation of the same height as ${\cal D}$ of
its first premiss $A\rightarrow B, E\rightarrow F, \Gamma\Rightarrow \Delta, A$ is obtained by height preserving weakening applied to ${\cal D}$.
As far as the second premiss, i.e. $B, E\rightarrow F, \Gamma \Rightarrow \Delta$ is concerned, by  induction hypothesis there is a separated derivation ${\cal D}_0'$ of height bounded by the height of ${\cal D}_0$, of $B, E\rightarrow F, \Gamma \Rightarrow \Delta, E$ and a separated derivation ${\cal D}_1'$,  of height bounded by the height of ${\cal D}_1$, of $B, F,  \Gamma \Rightarrow \Delta$, Then:
\[
\begin{array}{ccc}
{\cal D}_0'&~~~&{\cal D}_1'\\
B, E\rightarrow F, \Gamma\Rightarrow \Delta, E&&B, F,  \Gamma\Rightarrow \Delta\\
\cline{1-3}
\multicolumn{3}{c}{B,  E\rightarrow F, \Gamma\Rightarrow \Delta}

\end{array}
\]is a separated derivation of   $B, E\rightarrow F, \Gamma \Rightarrow \Delta$ with height  bounded by $h({\cal D})$.

 If the last inference does introduce  the principal formula of $R$, we only need, in addition, to note that the subderivations of a separated derivation are themselves  separated.

 If ${\cal D}$ ends with an ${\cal R}$ or  $Cut_{cs}$-inference,  then ${\cal D}$, being separated, does not contain any logical inference, and the previous Lemma applies. $\Box$

\begin{proposition} \label{sepequality}
If the premisses  of an ${\cal R}$-inference $R$ have  a separated derivation, then its conclusion also has a separated derivation.

\end{proposition}

{\bf Proof} If all the separated derivations of the premisses end with an ${\cal R}$ or with a $Cut_{cs}$-inferences, they are all free of logical inferences and it suffices to apply to such premisses the rule $R$ to obtain the desired separated derivation.
Otherwise we select a derivation of a premiss that ends with a logical inference and proceed by a straightforward induction on the sum of the heights of derivations. For example suppose  that $R$ has the following two premisses:
1) $Q_1,\Gamma_1', A\vee B\Rightarrow \Delta_1, Q_1'$, with separated derivation ${\cal E}_1$, that ends with an $L\vee$-inference with principal formula $A\vee B$, and  2) $Q_2,\Gamma_2\Rightarrow \Delta_2, Q_2'$ with separated derivation ${\cal E}_2$
and that the  conclusion of $R$ is  $P,\Gamma_1',A\vee B, \Gamma_2\Rightarrow \Delta_1,\Delta_2, P'$.
${\cal E}_1$ has the form:

\[
\begin{array}{ccc}
{\cal E}_{10}&~~~&{\cal E}_{11}\\
Q_1, \Gamma_1', A\Rightarrow \Delta_1, Q_1'&&Q_1, \Gamma_1', B\Rightarrow \Delta_1, Q_1'\\
\cline{1-3}
\multicolumn{3}{c}{Q_1,\Gamma_1', A\vee B \Rightarrow \Delta_1, Q_1'}
\end{array}
\]

We can apply the induction hypothesis to ${\cal E}_{10}$ paired with ${\cal E}_2$ to obtain a separated derivation of:
$$a)~~~P,\Gamma_1', A, \Gamma_2\Rightarrow \Delta_1,\Delta_2, P'$$ and  to ${\cal E}_{11}$ paired with ${\cal E}_2$ to obtain a separated derivation of:
$$b)~~P,\Gamma_1', B, \Gamma_2\Rightarrow \Delta_1,\Delta_2, P'.$$
Then it suffices to apply the same last  $L\vee$-inference of ${\cal E}_1$ to $a)$ and $b)$ to obtain the desired separated derivation of
$$P,\Gamma_1',A\vee B, \Gamma_2\Rightarrow \Delta_1,\Delta_2, P'.$$
$\Box$

\begin{lemma}
If the premisses $\Gamma \Rightarrow \Delta, A$  and $A, \Gamma\Rightarrow \Delta$ of a $Cut_{cs}$-inference have separated derivations in ${\bf G3c[mic]}^{\cal R} +Cut_{cs}$, one of which is free of logical inferences, then its conclusion $\Gamma\Rightarrow \Delta $ has a separated derivation in the same system.
\end{lemma}

{\bf Proof}  If both derivations are free of logical rules then it suffices to apply a $Cut_{cs}$-inference to their endsequents. Otherwise we distinguish two cases.

 Case 1 ${\cal D}$ is  a derivation without logical inferences of $\Gamma \Rightarrow \Delta, A$ and ${\cal E}$ is  a separated derivation containing logical inferences  of $A, \Gamma\Rightarrow \Delta$, so that it ends with a logical inference.

 We have to find a separated derivation of $\Gamma\Rightarrow \Delta$.  By Lemma \ref{atomic} there is an atomic subsequent $\Gamma^\circ \Rightarrow \Delta^\circ$ of  $\Gamma\Rightarrow \Delta, A$ such that  $\Gamma^\circ \Rightarrow \Delta^\circ$ has  a derivation ${\cal D}^\circ$ without  logical inferences. If $A$ does not occur in  $\Delta^\circ$, then a separated derivation,   actually a derivation without logical inferences, of $\Gamma \Rightarrow \Delta$ can be obtained directly by weakening the conclusion of ${\cal D}^\circ$. On the other hand if $A$ occurs in $\Delta^\circ$, then $A$ is atomic so that  the principal formula of the last logical inference of ${\cal E}$  is different from $A$. We can then apply the induction hypothesis to ${\cal D}^\circ$, appropriately weakened,  and to the immediate subderivation(s) of ${\cal E}$ and then the same last logical inference of ${\cal E}$. For example if ${\cal E}$ has the form:
 \[
 \begin{array}{c}
 {\cal E}_0\\
 A, E, F, \Gamma'\Rightarrow \Delta\\
 \cline{1-1}
 A,E\wedge F, \Gamma'\Rightarrow \Delta
 \end{array}
 \]
by Lemma \ref{atomic} we have a derivation ${\cal D}'$ without logical inferences of $E,F,\Gamma'\Rightarrow \Delta, A$.
 By induction hypothesis applied to ${\cal D}'$ and ${\cal E}_0$ we obtain a separated derivation of $E, F, \Gamma'\Rightarrow \Delta$, from which the desired separated derivation of $E\wedge F, \Gamma'\Rightarrow \Delta$ is obtained by means of the last $L\wedge$-inference of ${\cal E}$.

Case 2.  ${\cal D}$ is  a separated derivation containing logical inferences, so that it ends with a logical inference,  of $\Gamma \Rightarrow \Delta, A$ and ${\cal E}$ is  a  derivation without  logical inferences  of $A, \Gamma\Rightarrow \Delta$. By Lemma \ref{atomic} there is an atomic subsequent of $\Gamma^\circ\Rightarrow \Delta^\circ$ of $A,\Gamma\Rightarrow \Delta$ with a derivation ${\cal E}^\circ$ without logical inferences. If $A$ does not occur in $\Gamma^\circ$, then $\Gamma\Rightarrow \Delta$ can be derived without logical inferences by weakening the conclusion of ${\cal E}^\circ$. Otherwise $A$ is atomic, so that it is not the principal formula
  of the last inference of ${\cal D}$, and we can apply the induction hypothesis to the immediate subderivation(s) of ${\cal D}$ to  conclude as in the previous case. $\Box$

  \begin{proposition} \label{sepcutcs}

  If the  premisses $\Gamma \Rightarrow \Delta, A$  and $A, \Gamma\Rightarrow \Delta$ of a $Cut_{cs}$-inference have separated derivation in
  ${\bf G3c[mic]}^{\cal R} + Cut_{cs}$, then its conclusion has a separated derivation in the same system.
   \end{proposition}

  {\bf Proof} Let ${\cal D}$ and ${\cal E}$ be  separated derivations of $\Gamma \Rightarrow \Delta, A$  and $A, \Gamma\Rightarrow \Delta$  respectively.
  We have to find a separated derivation of $\Gamma\Rightarrow \Delta$.

  By the previous Lemma we can assume that both ${\cal D}$ and ${\cal E}$ end with a logical rule, and  proceed by
  a principal induction  on the height (of the formation tree) of $A$ and a secondary induction  on $h({\cal D})+h({\cal E})$.

{\bf  Classical case}

 Case 1 $A$ is not principal  in (the last inference of) ${\cal D}$.
 If ${\cal D}$ reduces to an instance of $L\bot$, the same holds for $\Gamma\Rightarrow \Delta$.

 Case 1. $L\wedge$. $~ {\cal D}$ is of the form

 \[
 \begin{array}{c}
 {\cal D}_0\\
 E,F,\Gamma'\Rightarrow \Delta, A\\
 \cline{1-1}
 E\wedge F,\Gamma'\Rightarrow \Delta, A
 \end{array}
 \]so that the endsequent of ${\cal E}$ has the form $A,E\wedge F, \Gamma'\Rightarrow \Delta$.
 By Proposition \ref{invert} there is a separated derivation ${\cal E}'$  of $A, E, F, \Gamma'\Rightarrow\Delta$ such that $h({\cal E}')\leq h({\cal E})$.
 By the (secondary) induction hypothesis applied to ${\cal D}_0$ and ${\cal E}'$ there is a separated derivation of $E,F,\Gamma'\Rightarrow \Delta$, from which the required separated derivation of $\Gamma\Rightarrow \Delta$ can be obtained by means of the last $L\wedge$- inference of ${\cal E}$. In the following we will express the argument as follows:
\[
\begin{array}{ccc}
 E,F,\Gamma' \Rightarrow \Delta, A&~~~&\\
 \cline{1-1}
 E\wedge F,\Gamma'\Rightarrow \Delta, A&&A,E\wedge F, \Gamma'\Rightarrow \Delta\\
 \cline{1-3}
 \multicolumn{3}{c}{E\wedge F, \Gamma'\Rightarrow \Delta}
 \end{array}
 \]

 is transformed into:
 \[
 \begin{array}{cccl}
&~~~&A, E\wedge F, \Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{inv}}\\
 \cline{3-3}
 E, F, \Gamma'\Rightarrow\Delta, A&&A, E, F, \Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-3}
 \multicolumn{3}{c}{E,F,\Gamma'\Rightarrow \Delta}\\
  \multicolumn{3}{c}{\overline{E\wedge F,\Gamma'\Rightarrow \Delta}}\
 \end{array}
 \]
In this case the  principal formula of the last logical inference of ${\cal D}$ occurs in the endsequent of ${\cal E}$ where it can be inverted, producing a separated derivation of a sequent identical to the  premiss of the last inference of ${\cal D}$, except that the cut formula $A$ is shifted from the succedent to the antecedent.
We can then apply the secondary induction hypothesis to produce  a sequent to which the last logical inference of ${\cal D}$ can be applied, yielding the required separated derivation.
The same kind of  argument applies to all the remaining cases. For example:

 Case 1. $L\rightarrow$

 \[
 \begin{array}{ccccc}
 \Gamma'\Rightarrow \Delta, E, A&~~&F,\Gamma'\Rightarrow \Delta, A&~~~&\\
 \cline{1-3}
 \multicolumn{3}{c}{E\rightarrow F, \Gamma'\Rightarrow \Delta, A}&&A,E\rightarrow F, \Gamma'\Rightarrow \Delta\\

  \multicolumn{5}{c}{\overline{~~~~~~~~~~~~~~~~~~~ E\rightarrow F, \Gamma'\Rightarrow \Delta~~~~~~~~~~~~~~~~~~~~~~~~~~}}
   \end{array}
 \]
 is transformed into:

 \[
 \begin{array}{ccclcccl}
 &~~&A,E\rightarrow F, \Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{inv}}~~~~&&~~&A,E\rightarrow F, \Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{inv}}\\
 \cline{3-3}\cline{7-7}
 \Gamma'\Rightarrow \Delta, E, A&&A,\Gamma'\Rightarrow \Delta, E&\vbox to 0pt{\hbox{ind}}~~~~~~~& F,\Gamma'\Rightarrow \Delta, A&&A,F,\Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-3}\cline{5-7}
 \multicolumn{3}{c}{\Gamma'\Rightarrow \Delta, E}&&\multicolumn{3}{c}{F,\Gamma' \Rightarrow \Delta}\\
 \multicolumn{7}{c}{\overline{~~~~~~~~~~~~~~~~~~~~~E \rightarrow F, \Gamma' \Rightarrow \Delta~~~~~~~~~~~~~~~~~~~~~~~~~~}}
 \end{array}
 \]

 Case1 $R\rightarrow$
 \[
 \begin{array}{ccc}
 \Gamma, E\Rightarrow \Delta', F, A&~~&\\
 \cline{1-1}
 \Gamma\Rightarrow \Delta', E\rightarrow F, A&&A,\Gamma\Rightarrow \Delta', E\rightarrow F\\
 \cline{1-3}
  \multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F}
 \end{array}
 \]
 is transformed into:

 \[
\begin{array}{cccl}
&&A,\Gamma\Rightarrow \Delta', E\rightarrow  F&\vbox to 0pt{\hbox{inv}}\\
\cline{3-3}
\Gamma,E\Rightarrow \Delta', F, A&&A,\Gamma, E  \Rightarrow \Delta',  F&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}
 \multicolumn{3}{c}{\Gamma, E\Rightarrow \Delta',   F}\\
 \multicolumn{3}{c}{\overline{\Gamma\Rightarrow \Delta', E\rightarrow F}}
\end{array}
\]

 Case 1 $R\forall$

 \[
 \begin{array}{ccc}
 \Gamma\Rightarrow \Delta', E[x/a], A&~~&\\
 \cline{1-1}
 \Gamma \Rightarrow \Delta', \forall x E, A&&A,\Gamma\Rightarrow \Delta', \forall x E\\
 \cline{1-3}
 \multicolumn{3}{c}{ \Gamma\Rightarrow \Delta', \forall x E}
 \end{array}
 \]

 is transformed into:

 \[
 \begin{array}{clcl}
&~~&A,\Gamma\Rightarrow \Delta', \forall x E&\vbox to 0pt{\hbox{inv}}\\
\cline{3-3}
 \Gamma\Rightarrow \Delta', E[x/a], A &&A,\Gamma\Rightarrow \Delta', E[x/a]& \vbox to 0pt{\hbox{ind}}\\
 \cline{1-3}
 \multicolumn{3}{c}{ \Gamma\Rightarrow \Delta', E[x/a]}\\
 \multicolumn{3}{c}{\overline{ \Gamma\Rightarrow \Delta', \forall x E}}
 \end{array}
 \]

 Case 2.  $A$ is not principal  in (the last inference of) ${\cal E}$.
 If ${\cal E}$ reduces to an instance of $L\bot$, the same holds for $\Gamma\Rightarrow \Delta$.
 All the other cases are treated dually to Case 1. For example:

 Case 2. $R\wedge$

 \[
 \begin{array}{ccc}
 &~~&A,E,F,\Gamma'\Rightarrow \Delta\\
 \cline{3-3}
 E\wedge F, \Gamma'\Rightarrow \Delta, A&&A,E\wedge F, \Gamma'\Rightarrow \Delta\\
 \cline{1-3}
 \multicolumn{3}{c}{E\wedge F, \Gamma'\Rightarrow \Delta}
  \end{array}
 \]
  is transformed into:
 \[
 \begin{array}{clcl}
 E\wedge F, \Gamma'\Rightarrow \Delta, A&\vbox to 0pt{\hbox{inv}}~~&&\\
 \cline{1-1}
 E,F,\Gamma'\Rightarrow \Delta, A&&A,E,F,\Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-3}
 \multicolumn{3}{c}{E,F, \Gamma'\Rightarrow \Delta}&\\
 \multicolumn{3}{c}{\overline{E\wedge F, \Gamma'\Rightarrow \Delta}}
 \end{array}
 \]
In   the above cases all  the applications of $\hbox{ind}$ refer to  the secondary induction hypothesis.

 \

 Case 3. $A$ is principal  in (the last inferences of) both $ {\cal D}$  and  ${\cal E}$.

 \

 Case 3. $\wedge$:

 \[
 \begin{array}{ccccc}
 \Gamma\Rightarrow \Delta, B&~~~&\Gamma\Rightarrow \Delta, C&~~~&B, C,\Gamma\Rightarrow \Delta\\
 \cline{1-3}\cline{5-5}
 \multicolumn{3}{c}{\Gamma \Rightarrow \Delta, B\wedge C}&&B\wedge C,\Gamma\Rightarrow \Delta\\
 \cline{1-5}
  \multicolumn{5}{c}{\Gamma \Rightarrow \Delta}

 \end{array}
 \]
is transformed into:

\[
\begin{array}{ccclcl}
&~~&\Gamma\Rightarrow \Delta, B&\vbox to 0pt{\hbox{w}}~~~&&\\
\cline{3-3}
&&C,\Gamma\Rightarrow \Delta, B&&B,C,\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
\cline{3-5}
\Gamma\Rightarrow \Delta, C&&\multicolumn{3}{c}{C,\Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{ind}}\\
\cline{1-5}
 \multicolumn{5}{c}{\Gamma \Rightarrow \Delta}
\end{array}
\]

In this case  the second application of $\hbox{ind}$  refers necessarily to the principal induction hypothesis, which is possible since $h(C)< h(B\wedge C)$,
independently of the height of the separated derivation of the second premiss $C,\Gamma\Rightarrow \Delta$,  previously obtained by the (secondary suffices) induction hypothesis. Of the remaining cases we deal with the  Case 3 $\forall$  in which $A$ is a universal formula, leaving the others to the reader.

\[
\begin{array}{ccc}
\Gamma\Rightarrow \Delta, B[x/a]&~~~&\forall x B, B[x/t],\Gamma\Rightarrow \Delta\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta,\forall x B&&\forall x B,\Gamma\Rightarrow \Delta\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta}
\end{array}
\]
 is transformed into:

 \[
 \begin{array}{clclcl}
 &&\Gamma\Rightarrow \Delta, B[x/a]&&&\\
 \cline{3-3}
 &&\Gamma\Rightarrow \Delta,\forall x B&\vbox to 0pt{\hbox{w}}~~&&\\
 \cline{3-3}
 \Gamma\Rightarrow \Delta, B[x/a]&\vbox to 0pt{\hbox{Sub$[a/t]$}}~~&B[x/t],\Gamma\Rightarrow \Delta, \forall x B&&\forall x B,B[x/t],\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-1}\cline{3-5}
 \Gamma\Rightarrow \Delta, B[x/t]&&\multicolumn{3}{c}{B[x/t], \Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-5}
 \multicolumn{5}{c}{\Gamma\Rightarrow \Delta}
 \end{array}
 \]where $\hbox{Sub$[a/t]$}$ yields the result of replacing $a$ by $t$ throughout the separated derivation of $\Gamma\Rightarrow \Delta, B[x/a]$.
For the result of  such a replacement to be a derivation it is required that the parameters used as proper in the $L\exists$ and $R\forall$-inferences of  the given derivation be renamed, if necessary, so as not to occur in $t$.

{\bf Intuitionistic case}

Case 1. $A$ is not principal in ${\cal D}$.
We only need to replace Case1. $L\rightarrow$, $R\rightarrow$ and   $R\forall$ with the following:

Case 1. $L^i\rightarrow$
\[
\begin{array}{ccccc}
E\rightarrow F, \Gamma'\Rightarrow \Delta, E,  A&~~&F,\Gamma'\Rightarrow \Delta, A&~~&\\
\cline{1-3}
\multicolumn{3}{c}{E\rightarrow F, \Gamma'\Rightarrow \Delta, A}&&A,E\rightarrow F,\Gamma'\Rightarrow \Delta\\
\cline{2-5}
&\multicolumn{4}{c}{E\rightarrow F, \Gamma'\Rightarrow \Delta}
\end{array}
\]
is transformed into:

\[
\begin{array}{ccclcccl}
&&A,E\rightarrow F,\Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{inv}}~~&&&A,E\rightarrow F,\Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{inv}}\\
\cline{3-3}\cline{7-7}
E\rightarrow F, \Gamma'\Rightarrow \Delta, E,  A&~~&A,E\rightarrow F,\Gamma'\Rightarrow \Delta, E&\vbox to 0pt{\hbox{ind}}&F,\Gamma'\Rightarrow \Delta, A&&A, F, \Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}\cline{5-7}
\multicolumn{3}{c}{E\rightarrow F,\Gamma'\Rightarrow \Delta, E}&& \multicolumn{3}{c}{F,\Gamma'\Rightarrow \Delta}\\
\multicolumn{7}{c}{\overline{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ E\rightarrow F, \Gamma'\Rightarrow \Delta ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}}
\end{array}
\]

Case 1. $R^i\rightarrow$

\[
\begin{array}{ccc}
E,\Gamma\Rightarrow F&~~~&\\
\cline{1-1}
\Gamma\Rightarrow \Delta', E\rightarrow F, A&&A,\Gamma\Rightarrow \Delta',E\rightarrow F\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta',  E\rightarrow F}
\end{array}
\]

is transformed into:
\[
\begin{array}{c}
E,\Gamma\Rightarrow F\\
\cline{1-1}
\Gamma\Rightarrow \Delta', E\rightarrow F
\end{array}
\]

Case 1. $R^i\forall$.

\[
\begin{array}{ccc}
\Gamma\Rightarrow E[x/a]&~~&\\
\cline{1-1}
\Gamma\Rightarrow \Delta', \forall x E, A&&A,\Gamma\Rightarrow \Delta', \forall x E\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', \forall x E}

\end{array}
\]

is transformed into:

\[
\begin{array}{c}
\Gamma\Rightarrow E[x/a]\\
\cline{1-1}
\Gamma\Rightarrow \Delta', \forall x E
\end{array}
\]

Case 2  Case 1. does not occur, so that $A$ is principal in the last inference of ${\cal D}$,  and $A$   is not principal in ${\cal E}$ and
If the rule  of the last inference of ${\cal E}$ is invertible in ${\cal D}$ , i.e. if it is not a $R^i\rightarrow$ or $R^i\forall$-inference then we proceed as in Case 2 of the classical case.
If ${\cal E}$ ends with a $R^i\rightarrow$ or $R^i\forall$-inference,  we distinguish cases according to the form of $A$.

\

Case 2. $R^i\rightarrow$, $\wedge$

\[
\begin{array}{ccccc}
\Gamma\Rightarrow \Delta', E\rightarrow F, B&~~&\Gamma\Rightarrow \Delta', E\rightarrow F, C&~~&B\wedge C, E,\Gamma\Rightarrow F\\
\cline{1-3} \cline{5-5}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F, B\wedge C}&&B\wedge C, \Gamma\Rightarrow \Delta', E\rightarrow F\\
\multicolumn{5}{c}{\overline{~~~~~~~~~~~~~~~~~~~~~~~~~~~\Gamma\Rightarrow \Delta', E\rightarrow F~~~~~~~~~~~~~~~~~~~~~~~~~~~}}
\end{array}
\]
is transformed into:

\[
\begin{array}{ccclll}
&&&&B\wedge C, E,\Gamma\Rightarrow F&\\
\cline{5-5}
&~~&\Gamma\Rightarrow\Delta', E\rightarrow F, B&\vbox to 0pt{\hbox{w}}~~&B\wedge C, \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{inv}}\\
\cline{3-3}\cline{5-5}
&&C,\Gamma\Rightarrow\Delta', E\rightarrow F, B&&B,  C, \Gamma\Rightarrow \Delta', E\rightarrow F& \vbox to 0pt{\hbox{ind}}\\
\cline{3-5}
\Gamma\Rightarrow \Delta',E\rightarrow F, C&\multicolumn{4}{c}{~~~~~~~~~~~~C,\Gamma\Rightarrow \Delta', E\rightarrow F~~}& \vbox to 0pt{\hbox{ind}}\\
\cline{1-5}
\multicolumn{4}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F}
\end{array}
\]

Case 2. $R^i\rightarrow$, $\vee$

\[
\begin{array}{ccc}
\Gamma\Rightarrow \Delta', E\rightarrow F, B, C&~~~&B\vee C, E,\Gamma \Rightarrow F\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta', E\rightarrow F, B \vee C&&B\vee C, \Gamma \Rightarrow \Delta',  E\rightarrow F\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F}

\end{array}
\]
is transformed into:

\[
\begin{array}{ccclcl}
&&B\vee C, E, \Gamma\Rightarrow F&&&\\
\cline{3-3}
&~~&B\vee C, \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{inv}}~~&&\\
\cline{3-3}
&& C, \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{w}}&B\vee C, E,\Gamma \Rightarrow F&\\
\cline{3-3} \cline{5-5}
\Gamma\Rightarrow \Delta', E\rightarrow F, B, C&&C, \Gamma\Rightarrow \Delta', E\rightarrow F, B&\vbox to 0pt{\hbox{ind}}&B\vee C, \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{inv}}\\
\cline{1-3}\cline{5-5}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F, B}&&B , \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{ind}}\\

\multicolumn{6}{c}{\overline{~~~~~~~~~~~~~~~~~~~~~~\Gamma\Rightarrow \Delta', E\rightarrow F~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}}

\end{array}
\]

Case 2 $R^i\rightarrow$, $\rightarrow$
\

\[
\begin{array}{ccc}
B,\Gamma\Rightarrow C&~~~&B\rightarrow C, E,\Gamma\Rightarrow F\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow  \Delta', E\rightarrow F,B\rightarrow C&&B\rightarrow C,\Gamma\Rightarrow \Delta',E\rightarrow F\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F}
\end{array}
\]
is transformed into:

\[
\begin{array}{clcl}
B,\Gamma\Rightarrow C&~~~&&\\
\cline{1-1}
\Gamma\Rightarrow F,  B\rightarrow C&\vbox to 0pt{\hbox{w}}&&\\
\cline{1-1}
E,\Gamma\Rightarrow F, B\rightarrow C&&B\rightarrow C, E, \Gamma\Rightarrow F&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}
\multicolumn{3}{c}{E, \Gamma\Rightarrow  F}\\
\multicolumn{3}{c}{\overline{~~ \Gamma\Rightarrow  \Delta',E\rightarrow  F}}

\end{array}
\]

Case 2 $R^i\rightarrow$, $\forall$

\[
\begin{array}{ccc}
\Gamma\Rightarrow B[x/a]&~~~&\forall x B, E, \Gamma\Rightarrow F\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta', E\rightarrow F, \forall x B&&\forall x B, \Gamma\Rightarrow \Delta', E\rightarrow F\\
\cline{1-3}
\multicolumn{3}{c}{~~ \Gamma\Rightarrow  \Delta',E\rightarrow  F}
\end{array}
\]
is transformed into:
\[
\begin{array}{clcl}
\Gamma\Rightarrow B[x/a]&&&\\
\cline{1-1}
\Gamma\Rightarrow F, \forall x B &\vbox to 0pt{\hbox{w}}~~&&\\
\cline{1-1}
E,\Gamma\Rightarrow F, \forall x B&&\forall x B, E, \Gamma\Rightarrow F&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}
\multicolumn{3}{c}{E,  \Gamma\Rightarrow    F}\\
\multicolumn{3}{c}{\overline{~~ \Gamma\Rightarrow  \Delta',E\rightarrow  F}}
\end{array}
\]

Case 2 $R^i\rightarrow$, $\exists$

\

\[
\begin{array}{ccc}
\Gamma\Rightarrow \Delta', E\rightarrow F, \exists xB, B[x/t]&~~&\exists x B, E,\Gamma\Rightarrow  F\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta', E\rightarrow F, \exists x B&& \exists x B, \Gamma\Rightarrow \Delta', E\rightarrow F\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow  \Delta', E\rightarrow  F}
\end{array}
\]
is transformed into:

\[
\begin{array}{ccclcl}
&&&&\exists x B, E,\Gamma\Rightarrow F&\\
\cline{5-5}
&~~&\exists x B, E,\Gamma\Rightarrow  F&~~~~&  \exists x B, \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{inv}}\\
\cline{3-3}\cline{5-5}
\Gamma\Rightarrow \Delta', E\rightarrow F, \exists x B, B[x/t]&& \exists x B, \Gamma\Rightarrow \Delta',E\rightarrow  F, B[x/t]&\vbox to 0pt{\hbox{ind}}&B[x/a], \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{Sub$[a/t]$}}\\
\cline{1-3}\cline{5-5}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta', E\rightarrow F, B[x/t] } && B[x/t], \Gamma\Rightarrow \Delta', E\rightarrow F&\vbox to 0pt{\hbox{ind}}\\
\multicolumn{6}{c}{\overline{~~~~~~~~~~~~~~~~~~~~~~~~~~\Gamma\Rightarrow  \Delta',E\rightarrow  F~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}}

\end{array}
\]

Case 2. $R^i\forall$.  Similar to Case2. $R^i\rightarrow$. For example:

 (Case 2 $R^i\forall$, $\rightarrow$)

 \[
 \begin{array}{ccc}
 B,\Gamma\Rightarrow C&~~~&B\rightarrow C,\Gamma\Rightarrow E[x/a]\\
 \cline{1-1}\cline{3-3}
 \Gamma\Rightarrow \Delta', \forall x E, B\rightarrow C&&B\rightarrow C, \Gamma\Rightarrow \Delta', \forall x E\\
 \cline{1-3}
 \multicolumn{3}{c}{\Gamma\Rightarrow  \Delta',\forall x E}

 \end{array}
 \]
is transformed into:
\[
\begin{array}{cccl}
 B,\Gamma\Rightarrow C&~~~&&\\
 \cline{1-1}
 \Gamma\Rightarrow E[x/a], B\rightarrow C&&B\rightarrow C,\Gamma\Rightarrow E[x/a]&\vbox to 0pt{\hbox{ind}}\\
 \cline{1-3}

 \multicolumn{3}{c}{\Gamma\Rightarrow   E[x/a]}\\
  \multicolumn{3}{c}{\overline{\Gamma\Rightarrow   \Delta', \forall x E}}
\end{array}
\]

and  (Case 2  $R^i\forall$, $\forall$)

\[
\begin{array}{ccc}
\Gamma\Rightarrow B[x/b]&~~~&\forall x B,\Gamma\Rightarrow E[x/a]\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta',\forall x E,\forall x B&&\forall x B,\Gamma\Rightarrow \Delta',\forall x E\\
\cline{1-3}
 \multicolumn{3}{c}{\Gamma\Rightarrow  \Delta', \forall x  E}

\end{array}
\]
is transformed into:

\[
\begin{array}{cccl}
\Gamma\Rightarrow B[x/b] &~~&&\\
\cline{1-1}
\Gamma\Rightarrow E[x/a], \forall x B&&\forall x B, \Gamma\Rightarrow E[x/a]&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow   E[x/a]}\\
  \multicolumn{3}{c}{\overline{\Gamma\Rightarrow   \Delta', \forall x E}}
\end{array}
\]

Case 3. $A$ is principal in both  ${\cal D}$ and ${\cal E}$. The only difference  with respect to the classical case concern $\rightarrow$ and $\forall$.

Case 3i $\rightarrow$

\[
\begin{array}{ccccc}
B,\Gamma\Rightarrow C&~~&B\rightarrow C, \Gamma\Rightarrow \Delta, B&~~&C,\Gamma\Rightarrow \Delta\\
\cline{1-1}\cline{3-5}
\Gamma\Rightarrow \Delta, B\rightarrow C&&\multicolumn{3}{c}{B\rightarrow C,\Gamma \Rightarrow \Delta}\\
\cline{1-5}
\multicolumn{5}{c}{\Gamma\Rightarrow  \Delta}
\end{array}
\]
is transformed into:

\[
\begin{array}{ccclcccl}
B,\Gamma\Rightarrow C&~~&&&B,\Gamma\Rightarrow C&\vbox to 0pt{\hbox{w}} & C,\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{w}}\\
\cline{1-1}  \cline{5-5} \cline{7-7}
\Gamma\Rightarrow \Delta, B,  B\rightarrow C&~~&B\rightarrow C, \Gamma\Rightarrow \Delta, B&  \vbox to 0pt{\hbox{ind}}~~~~& B,\Gamma\Rightarrow \Delta, C&~~&C,B,\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
\cline{1-3}\cline{5-7}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta, B}&&\multicolumn{3}{c}{B, \Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{ind}}\\
\cline{1-7}
\multicolumn{7}{c}{\Gamma\Rightarrow \Delta}
\end{array}
\]

Case 3i $\forall$

\[
\begin{array}{ccc}
\Gamma\Rightarrow B[x/a]&~~~&\forall x B, B[x/t],\Gamma\Rightarrow \Delta\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow \Delta,\forall x B&&\forall x B,\Gamma\Rightarrow \Delta\\
\cline{1-3}
\multicolumn{3}{c}{\Gamma\Rightarrow \Delta}

\end{array}
\]
is transformed into:

\[
\begin{array}{clclclcl}
&&\Gamma\Rightarrow B[x/a]&&&\\
\cline{3-3}
\Gamma\Rightarrow B[x/a]&\vbox to 0pt{\hbox{Sub$[a/t]$}}~~~~~&\Gamma\Rightarrow \Delta, \forall x B&\vbox to 0pt{\hbox{w}}&&\\
\cline{1-1}\cline{3-3}
\Gamma\Rightarrow B[x/t]&\vbox to 0pt{\hbox{w}}~~~&B[x/t], \Gamma\Rightarrow \Delta, \forall x B&~~&\forall x B,B[x/t],\Gamma\Rightarrow \Delta&\vbox to 0pt{\hbox{ind}}\\
\cline{1-1}\cline{3-5}
\Gamma\Rightarrow \Delta, B[x/t]&&\multicolumn{3}{c}{B[x/t], \Gamma\Rightarrow \Delta}&\vbox to 0pt{\hbox{ind}}\\
\cline{1-5}
\multicolumn{5}{c}{\Gamma\Rightarrow \Delta}

\end{array}
\]
$\Box$

From  Proposition \ref{sepequality} and \ref{sepcutcs} by a straightforward induction argument we have the following separation  property
for ${\bf G3[mic]}^{\cal R} + Cut_{cs} $.

\begin{proposition}\label{sep}

Every derivation in ${\bf G3[mic]}^{\cal R} + Cut_{cs} $ can be transformed into a separated derivation of its endsequent.

\end{proposition}

\begin{theorem}\label{teorsep}
If the structural rules  are admissible in ${\cal R}$,  then they are admissible in ${\bf G3[mic]}^{\cal R}$ as well.
\end{theorem}

{\bf Proof}
 Let   ${\cal D}$ be a derivation in ${\bf G3[mic]}^{\cal R} + RLW +RLC+ Cut $.  We have to show that the applications of the $RLW$, $RLC$ and $Cut$ can be eliminated from ${\cal D}$.
  ${\cal D}$   can be transformed into a derivation ${\cal D}'$
in  ${\bf G3[mic]}^{\cal R} + Cut_{cs} $  of the same endsequent.
For,
the application of the $Cut$-rule can be replaced by applications of the weakenings and the $Cut_{cs}$ rule.

The applications of the contraction rules can be replaced by derivations from its premiss and initial sequents using  the $Cut_{cs}$-rule. More precisely,  as far as left contraction is concerned, the subderivations of ${\cal D}$ of the form
\[
\begin{array}{c}
{\cal E}\\
\underline{F, F, \Gamma\Rightarrow \Delta}\\
F, \Gamma\Rightarrow \Delta
\end{array}
\]
can be replaced  by:

\[
\begin{array}{ccc}
{\cal I} &~~~&{\cal E}\\
F,\Gamma\Rightarrow F&&F,F,\Gamma\Rightarrow \Delta\\
\cline{1-3}
\multicolumn{3}{c}{F,\Gamma\Rightarrow \Delta}
\end{array}
\]where, in case $F$ is not atomic, ${\cal I}$ is a derivation in ${\bf G3m}$ or in ${\bf G3i}$.
Similarly for right contraction.

Finally the applications of the weakening rules  can be eliminated by their (heigh-preserving) admissibiity in  all the systems considered.

Thus from ${\cal D}$ we obtain a derivation ${\cal D}'$ in ${\bf G3[mic]}^{\cal R} +Cut_{cs}$, that
by Proposition \ref{sep},  can be transformed into
a separated derivation ${\cal D}''$ of the endsequent  of ${\cal D}$. Thus,  to obtain the desired derivation in ${\bf G3}[mic]^{\cal R}$ of the endsequent of ${\cal D}$,  it suffices to eliminate the applications of $Cut_{cs}$ in the initial subderivations of ${\cal D}''$ belonging to ${\cal R} +Cut_{cs}$, which  is possible if the  contraction and the cut rule are admissible in ${\cal R}$.
$\Box$

\subsection{Admissibility of the Structural Rules}

\begin{corollary}
The structural rules are admissible in ${\bf G3[mic]}$
\end{corollary}

{\bf Proof} By Theorem \ref{teorsep},  with ${\cal R}=\emptyset$,
it suffices to note that the sequents that  can be derived  from
initial sequents by means of the structural rules are themselves initial sequents. $\Box$

\

Following \cite{N16} we let
${\bf G3[mic]}^=$ be   ${\bf G3[mic]}^{\cal R}$  for ${\cal R}=\{\hbox{Ref}, \hbox{Repl}\}$.

\begin{corollary}
The structural rules are admissible in ${\bf G3[mic]}^=$
\end{corollary}

 {\bf Proof}
 For the admissibility of left contraction we proceed by induction on the height of   derivations  to show that a derivation ${\cal D}$ of $A,A,\Gamma\Rightarrow \Delta$ in ${\cal R}$ can be transformed into a derivation of $A,\Gamma \Rightarrow \Delta$ in ${\cal R}$. That is immediate if ${\cal D}$ reduces to an initial sequent.  If $h({\cal D})>0$,  the conclusion is a straightforward consequence of the induction hypothesis except when
  ${\cal D}$ has the form:

 \[
 \begin{array}{cl}
 \underline{s=r, s=r, E[x/r], \Gamma'\Rightarrow \Delta}&\vbox to 0pt{\hbox{Repl}}\\
 s=r, s=r, \Gamma' \Rightarrow \Delta
 \end{array}
 \] and $A$ is $s=r$,  that coincides also  with $E[x/s]$.
We may assume that there is exactly one occurrence of $x$ in $E$.
Then $E$ can have the form $x=r$ or $r$ can have the form $r^\circ[x/s]$ and $E$ the form $s=r^\circ$.
In the former case the induction hypothesis applied to the immediate subderivation ${\cal D}_0$ of  ${\cal D}$,  whose endsequent is
$s=r,s=r,r=r, \Gamma'\Rightarrow \Delta$, yields a derivation
of $s=r, r=r, \Gamma'\Rightarrow \Delta$, from which we obtain $s=r, \Gamma'\Rightarrow \Delta$ by an application of $\hbox{Ref}$.
In the latter case ${\cal D}$ has the form:

\[
\begin{array}{cl}
{\cal D}_0\\
\underline{s=r^\circ[x/s], ~s=r^\circ[x/s],~ s=r^\circ[x/r^\circ[x/s]], ~\Gamma'\Rightarrow \Delta}&\vbox to 0pt{\hbox{Repl}}\\
s=r^\circ[x/s],~ s=r^\circ[x/s], ~\Gamma'\Rightarrow \Delta

\end{array}
\]
and  can be transformed into:

 \[
\begin{array}{cl}
{\cal D}_0&\\
\underline{s=r^\circ[x/s], ~s=r^\circ[x/s],~ s=r^\circ[x/r^\circ[x/s]], ~\Gamma'\Rightarrow \Delta}&\vbox to 0pt{\hbox{Repl}}\\
s=r^\circ[x/s],~ s=r^\circ[x/s], ~\Gamma'\Rightarrow \Delta&\vbox to 0pt{\hbox{w}}\\
\overline{\underline{s=r^\circ[x/s],~s=s,~ s=r^\circ[x/s], ~\Gamma'\Rightarrow \Delta}}&\vbox to 0pt{\hbox{Repl}}\\
\underline{s=r^\circ[x/s],~s=s, ~\Gamma'\Rightarrow \Delta}&\vbox to 0pt{\hbox{Ref}}\\
s=r^\circ[x/s], ~\Gamma'\Rightarrow \Delta
\end{array}
\]
 Since the rules of ${\cal R}$ do not modify the succedent of their premiss, the admissibility of the cut rule follows  by a straightforward induction on the height of the derivation of its first   premiss. $\Box$

\