\section{Proofs and further remarks for Sect.~\ref{sect:free-cut-elim}}

\paragraph*{Discussion on Dfn.~\ref{def:anchoredcut}}
 Our first idea would be to consider as anchored  a cut whose cut-formulas  $A$ in the two premises are both principal for their rule, and at least one of these rules is non-logical. Now, the problem with this tentative definition is that a rule (R) of  $\mathcal T$ can contain several principal formulas  (in $\Sigma'$, $\Delta'$) and so we would like to allow an anchored cut on each of these principal formulas.
  % Consider for instance the following derivation, where we have underlined principal formulas:
  Consider the following derivation, where principal formulas are underlined:
\[
\vlderivation{
\vliin{\cut_2}{}{\seqar \Pi}{
\vliin{\cut_1}{}{\seqar C \land D}{
\vlin{\rigrul{\lor}}{}{ \seqar\underline{ A \lor B} }{\vlhy{\seqar A,B}}
}{
\vlin{(R)}{}{ \underline{A\lor B} \seqar \underline{C\land D} }{ \vlhy{\Sigma \seqar \Delta} }
}
}{
\vlin{\lefrul{\land}}{}{ \underline{C\land D} \seqar \Pi }{\vlhy{C, D \seqar \Pi}}
}
}
\]

  Here $cut_1$ is anchored in this sense, but not $cut_2$. This is why we need the more general definition of \emph{hereditarily principal formula}.


 \begin{proof}
 	[Proof of Lemma~\ref{lem:hereditaryprincipalnonlogical}]
 	Assume that $A$ is an occurrence of formula on the LHS of the sequent and hereditarily principal for a non-logical rule (R), then a direct ancestor of this formula is principal for (R) and thus by condition 4. $A$ cannot be of the form $?A'$. The other case is identical.
 \end{proof}

     Define the  \textit{degree} of a formula as the number of logical connectives or quantifiers in it.  Let us first state an easy building-block of the proof, which comes from standard linear logic:
    \begin{lemma}[Logical non-exponential cut-elimination steps]\label{lem:logical steps}
    Any cut $c$ whose cut-formulas $A$ are both principal formulas of logical rules distinct from $?$, $!$, $wk$, $cntr$ rules can be replaced in one step by cuts on formulas of strictly lower degree (0, 1 or 2 cuts).
    \end{lemma}
    \begin{proof}
    This is exactly as in plain linear logic. Just note that the case of a quantifier formula involves a substitution by a term $t$ throughout the proof, and this is where we need condition 3 on non-logical rules requiring that they are closed by substitution.
    \end{proof}

Now we have all the necessary lemmas to proceed with the proof of the main theorem.
    \begin{proof}[Proof of Thm  \ref{thm:free-cut-elim}]
    Given a cut rule $c$ in a proof $\pi$, we call  \emph{degree} $\deg( c)$  the number of connectives and quantifiers of its  cut-formula. Now the \emph{degree} of the proof $\deg( \pi)$ is the multiset of the degrees of its non-anchored formulas. The degrees will be compared with the multiset ordering.
       The demonstration proceeds by induction on the degree  $\deg( \pi)$.  For a given degree we proceed with a sub-induction on the \textit{height} $\height{\pi}$ of the proof.
    
    Consider a proof $\pi$ of non-null degree. We want to show how to reduce it to a proof of strictly lower degree. Consider a top-most non-anchored cut $c$ in $\pi$, that is to say such that there is no non-anchored cut above $c$.  Let us call $A$ the cut-formula, and $(S_1)$ (resp. $(S_2)$) the rule above the left (resp. right) premise of $c$.  
\[    
     \vliinf{c \; \; \cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \vlinf{S_1}{}{\Gamma \seqar \Delta, A}{} }{\vlinf{S_2}{}{\Sigma, A \seqar \Pi}{}}
\]
    Intuitively we proceed as follows: if $A$ is not hereditarily principal in one of its premises  we will try to commute $c$ with the rule along its left premise  $(S_1)$, and if it is not possible commute it   with the rule along its right premise  $(S_2)$, by using Lemmas \ref{lem:hereditaryprincipalnonlogical}, \ref{lem:standardcommutations} and \ref{lem:keycommutations}; if $A$ is hereditarily principal in both premises we proceed with a cut-elimination step, as in standard linear logic. For this second step, the delicate part is the elimination of exponential cuts, for which we use a big-step reduction; it works well because the contexts in the non-logical rules $(R)$ are marked with $!$ (resp. $?$) on the LHS (resp. RHS). 
    
    So, let us distinguish the various cases:
       \begin{itemize}
    \item \textbf{First case}: the cut-formula $A$ on the LHS of  $c$ is not hereditarily principal. 
    
\begin{itemize}
\item Consider first the situation where $(S_1)$ is not one of the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$.

In this case the commutation of $c$ with $(S_1)$ can be done in the usual way, by using Lemma \ref{lem:standardcommutations}. Let us handle as an example the case where $(S_1)=(\rigrul{\laand})$.

\[
\begin{array}{cc}
& \vlderivation{
\vliin{c}{}{ \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi }{ \vliin{S_1=\rigrul{\vlan}}{}{\Gamma  \seqar B_1\vlan B_2, \Delta, A}{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{\Gamma  \seqar  B_2,\Delta, A}}}{ \vlhy{ \Sigma, A \seqar  \Pi} }
} \\
\noalign{\bigskip}
\to\qquad\qquad  
& \vlderivation{
\vliin{\rigrul{\vlan}}{}{  \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi  }{
\vliin{c_1}{}{\Gamma,\Sigma \seqar B_1, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }
}{
\vliin{c_2}{}{\Gamma,\Sigma \seqar B_2, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_2, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }
}
}
\end{array}
\]


Observe that here $c$ is replaced by two cuts $c_1$ and $c_2$. Call $\pi_i$ the sub-derivation of last rule $c_i$, for $i=1,2$. As for $i=1, 2$ we have
$\deg{\pi_i}\leq \deg{\pi}$ and $\height{\pi_i}< \height{\pi}$ we can apply the induction hypothesis, and reduce $\pi_i$ to a proof $\pi'_i$ of same conclusion and with
$\deg{\pi'_i} < \deg{\pi_i}$. Therefore  by replacing $\pi_i$ by $\pi'_i$ for $i=1, 2$ we obtain a proof $\pi'$ such that $\deg{\pi'}<\deg{\pi}$.  

The case (S)=($\lefrul{\laor}$) is identical, and the other cases are simpler. % (see the Appendix for more examples). 

\item Consider now the case where $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$. Let us also assume that the cut-formula is hereditarily principal in its RHS premise, because if this does not hold we can move to the second case below. 

First consider  $(S_1)=(\rigrul{!})$. As $A$ is not principal in the conclusion of $(\rigrul{!})$ it is of the form $A=?A'$. By assumption we know that  $A=?A'$ in the conclusion of $(S_2)$ is hereditarily principal on the LHS, so by Lemma \ref{lem:hereditaryprincipalnonlogical} it cannot be hereditarily principal for a non-logical rule, so by definition of hereditarily principal we deduce that $(S_2)$ is not an $(R)$ rule. It cannot be an  $(\rigrul{!})$ rule either because then $?A'$ could not be a principal formula in its conclusion. Therefore the only possibility is that 
 $(S_2)$ is an  $(\lefrul{?})$ rule. So the RHS premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$ and by Lemma \ref{lem:keycommutations} the commutation on the LHS is possible. We can conclude as previously. The case where  $(S_1)=(\lefrul{?})$ is the same.
 
 Now consider the case where $(S_1)=(R)$.  As $A$ is not hereditarily principal in the conclusion of $(R)$, it is a context formula and it is on the RHS, so by definition of $(R)$ rules it is  the form $A=?A'$. So as before by Lemma \ref{lem:hereditaryprincipalnonlogical} we deduce that   $(S_2)=(\lefrul{?})$, and  so the RHS premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$.  By Lemma \ref{lem:keycommutations} the commutation on the LHS is possible, and so again we conclude as previously.
 \end{itemize}
    \item \textbf{Second case}: the cut-formulas on the LHS and RHS of  $c$ are both not hereditarily principal. 
    
   After the first case we are here left with the situation where  $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$.
   \begin{itemize}
    \item Consider the case where  $(S_1)$=$(\rigrul{!})$, $(\lefrul{?})$, so $A$ is of the form $A=?A'$. All cases of commutation of $c$ with $(S_2)$ are as in standard linear logic, except if $(S_2)=(R)$. In this case though we cannot have $A=?A'$ because of the shape of rule $(R)$. So we are done. 
    \item Consider  $(S_1)=(R)$. Again as $A$ is not principal in the conclusion of $(S_1)$ and on the RHS of the sequent it is a context formula, and thus of the form  $A=?A'$. As $?A'$ is not principal in the conclusion of $(S_2)$, it is thus a context formula on the LHS of sequent, and therefore $(S_2)$ is not a rule $(R)$. So $(S_2)$ is a logical rule. If it is not an $(\rigrul{!})$ or an $(\lefrul{?})$ it admits commutation with the cut, and we are done. If it is equal to $(\rigrul{!})$ or $(\lefrul{?})$ it cannot have $?A'$ as a context formula in the LHS of its conclusion, so these subcases do not occur.  
   \end{itemize}
 
   
    \item \textbf{Third case}: the cut-formulas on the LHS and RHS of  $c$ are both  hereditarily principal.
     
    By assumption $c$ is non anchored, so none of the two cut-formulas is hereditarily principal for a non-logical rule $(R)$. We can deduce from that
    that the LHS cut-formula is principal for $(S_1)$ and the RHS cut-formula is principal for $(S_2)$. Call $\pi_1$ (resp. $\pi_2$) the subderivation
    of last rule $(S_1)$ (resp. $(S_2)$).
     
    Then we consider the following sub-cases, in order:
     \begin{itemize}
         \item \textbf{weakening sub-case}: this is the case  when one of the premises of $c$ is a $wk$ rule. Without loss of generality assume that it is the left premise of $c$ which is conclusion of $\rigrul{\wk}$, with principal formula $A$. We eliminate the cut by keeping only the LHS proof $\pi_1$, removing the last cut $c$ and last    $\rigrul{\wk}$ rule    on $A$, and by adding enough
        $\rigrul{\wk}$, $\lefrul{\wk}$ rules to introduce all the new formulas in the final sequent.  The degree has decreased.

      \item \textbf{exponential sub-case}: this is when one of the premises of $c$ is conclusion of a $cntr$, $\rigrul{?}$ or $\lefrul{!}$ rule on a formula $?A$ or $!A$, and the other one is not a conclusion of $\wk$.
      
       Assume without loss of generality that it is the right premise which is conclusion of $\lefrul{\cntr}$ or $\lefrul{!}$ on $!A$, and thus the only possibility for the left premise is to  be conclusion of $\rigrul{!}$.  This is rule $(S_1)$ on the picture, last rule of the subderivation $\pi_1$, and we denote its conclusion as $!\Gamma' \seqar ?\Delta', !A$. We will use here a global rewriting step. For that consider in $\pi_2$ all the top-most direct ancestors of the cut-formula $!A$, that is to say direct ancestors which do not have any more direct ancestors above. Let us denote them as $!A^{j}$ for $1\leq j \leq k$. Observe that each $!A^{j}$ is principal formula of a rule $\lefrul{!}$ or $\lefrul{wk}$. Denote by $\rho$ the subderivation
       of $\pi_2$ which has as leaves the sequents premises of these  $\lefrul{!}$ or $\lefrul{wk}$ rules with conclusion containing $!A^{j}$.
       Let $\rho'$ be a derivation obtained from $\rho$ by renaming if necessary eigenvariables occurring in premises of rules $\lefrul{\exists}$, $\rigrul{\forall}$, $(R)$  so that none of them belongs to $FV(!\Gamma', ?\Delta')$, where we recall that $!\Gamma' \seqar ?\Delta',!A$ is the LHS premise of the cut $c$.
  Now, let $\pi'_1$ be the immediate subderivation of $\pi_1$, of conclusion       $!\Gamma' \seqar ?\Delta',A$.  We then define the derivation 
  $\rho''$ obtained from   $\rho'$ in the following way:
  \begin{itemize}
  \item add a cut $c_j$ with (a copy) of $\pi'_1$ on $A^j$ at each leaf which is premise of a rule  $\lefrul{!}$;
  \item add to each sequent coming from $\rho'$  an additional context $!\Gamma'$ on the LHS and an additional context $?\Delta'$ on the RHS, and additional $wk$ rules to introduce these formulas below the $\lefrul{wk}$ rules on formulas $!A^{j}$;
  \item introduce suitable $\lefrul{cntr}$ and $\rigrul{cntr}$ rules after multiplicative binary rules $\rigrul{\land}$, $\lefrul{\lor}$  in such a way to replace $!\Gamma', !\Gamma'$ (resp. $?\Delta', ?\Delta'$) by  $!\Gamma'$ (resp. $?\Delta'$). 
  \end{itemize}
  
  It can be checked that  $\rho''$ is a valid derivation, because all the conditions for context-sensitive rules $(\rigrul{\forall})$, $(\lefrul{\exists})$, $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied. In particular the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied because the contexts have been enlarged with $!$ formulas on the LHS of the sequents ($!\Gamma'$) and ?  formulas on the RHS. of the sequents ($?\Gamma'$).  
  
  Now, let $\pi'$ be the derivation obtained from $\pi$ by removing the cut $c$ and replacing the subderivation $\rho$ by $\rho''$. The derivation $\pi'$ is a valid one, it has the same conclusion $!\Gamma', \Sigma \seqar ?\Delta', \Pi$ and with respect to $\pi$ we have replaced one non-anchored cut $c$ with at most $k$ ones $c_j$, but which are of strictly lower degree. So $\deg(\pi')<\deg(\pi)$ and we are done.

      
      \item \textbf{logical sub-case}: we are now left with the case where both premises of $c$ are conclusions of rules others than $?$, $!$, $wk$, $cntr$. We can thus apply Lemma \ref{lem:logical steps}.
         If one of the premises is an axiom $\lefrul{\bot}$, $\id$ or $\rigrul{\bot}$, then $\pi$ can be rewritten to a suitable proof $\pi'$ by removing $c$ and the axiom rule. Otherwise both premises introduce the same connective, either  $\land$, $\lor$, $\laor$, $\laand$, $\forall$ or $\exists$. In each case a specific rewriting rule replaces the cut $c$ with one cut of strictly lower degree. 
      %See the Appendix.
           \end{itemize}
     \end{itemize}
     \end{proof}
     
     
%\begin{remark}
%[Complexity]
%The exponential sub-case replaces a cut of degree $d$ by at most $|\pi|$ cuts of degree $d-1$, and also at most squares the size of the proof. 
%\end{remark}

%\section{Some cut-elimination cases}
%We work in a one-sided calculus for full linear logic. When working in the affine setting we simply drop the condition that weakened formulae are $?$-ed.
%
%As well as all usual rules, we have the induction rule:
%\[
%\vlinf{\indr}{(x \notin FV (\Gamma) )}{? \Gamma, A^\perp (0) , A(t)}{? \Gamma , A^\perp (x) , A(s x) }
%\]
%
%We give all the various cut-reduction cases in the following section but first we give a simple cut-elimination argument.
%
%\subsection{A basic (free-)cut elimination argument}
%We give an argument that easily scales to free-cut elimination, i.e.\ in the presence of non-logical rules.
%
%\newcommand{\anarrow}[2]{\overset{#1}{\underset{#2}{\longrightarrow}}}
%\newcommand{\cutredlin}{\mathit{ma}}
%\newcommand{\cutredexp}{exp}
%
%\begin{definition}
%	Let $\anarrow{}{\cutredexp}$ denote the reduction steps concerning exponential cuts, and $\anarrow{}{\cutredlin}$ be the set of cut-reduction steps concerning multiplicative and additive cuts.
%\end{definition}
%
%\newcommand{\rk}{\mathsf{rk}}
%	\renewcommand{\deg}{\mathsf{deg}}
%\begin{definition}
%	[Measures]
%	For a $\anarrow{}{\cutredlin}$-redex $r$, let its \emph{degree} $\deg( r)$ be the number of logical connectives or quantifiers in its cut-formula. For a proof $\pi$, its \emph{degree} $\deg( \pi)$ is the multiset of the degree of its redexes.
%\end{definition}
%
%\begin{proposition}
%If $\pi$ is not $\anarrow{}{\cutredlin}$-normal then there is a derivation $L:\pi \anarrow{*}{\cutredlin} \pi'$ such that $\deg(\pi')< \deg(\pi)$.
%\end{proposition}
%\begin{proof}
%	First let us show the statement in the special case that $\pi$ contains precisely one $\cut$-inference as its final step, by induction on $|\pi|$. Each commutative $\anarrow{}{\cutredlin}$-step results in us being able to apply the inductive hypothesis to smaller proofs,- in the case of $\vlan $ two smaller proofs. Each key $\anarrow{}{\cutredlin}$-case strictly reduces the degree of the proof. Consequently we can eventually transform $\pi$ to a proof $\pi'$ which has possibly several cuts of smaller degree, as required.
%	
%	Now to the general case, we simply apply the above procedure to the subproof above a topmost cut in $\pi$.
%\end{proof}
%\begin{corollary}
%	$\anarrow{}{\cutredlin}$ is weakly normalising.
%\end{corollary}
%
%
%\newcommand{\cntdown}{\mathit{cn}}
%\begin{definition}
%	[Lazy contraction]
%	Let $\anarrow{}{\cntdown}$ comprise of the following reduction steps:
%	\begin{enumerate}
%		\item The commuting steps,
%			\[
%			\vlderivation{
%				\vlin{\rho}{}{\Gamma', ?A, }{
%					\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ? A, ? A}}
%				}
%			}
%			\quad\to \quad
%			\vlderivation{
%				\vlin{\cntr}{}{\Gamma', ?A}{
%					\vlin{\rho}{}{\Gamma', ?A, ?A}{\vlhy{\Gamma, ? A, ? A}}
%				}
%			}	
%			\]
%			for each unary rule $\rho$.
%			\item 
%			The key steps:
%			\[ 	
%			\begin{array}{rcl}
%			\vlderivation{
%				\vlin{\cntr}{}{\Gamma, ?A}{
%					\vlin{\wk}{}{\Gamma, ?A, ?A}{\vlhy{\Gamma, ?A}}
%				}
%			}
%			\quad &\to & \quad
%			\Gamma, ?A 
%%			\]
%%			and
%%			\[
%\\
%\noalign{\smallskip}
%				\vlderivation{
%					\vlin{\wk}{}{\Gamma, ?A, ?A}{
%						\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ?A, ?A}}
%					}
%				}
%				\quad &\to& \quad
%				\Gamma, ?A, ?A
%							\end{array}
%			\].
%\item The commuting steps,
%\[
%	\vlderivation{
%		\vliin{\rho}{}{\Gamma ,?A}{
%			\vlin{\cntr}{}{\Gamma_1, ?A}{\vlhy{\Gamma_1, ?A, ?A}}
%		}{\vlhy{\Gamma_2}}
%	}
%	\quad \to \quad
%	\vlderivation{
%		\vlin{\cntr}{}{\Gamma, ?A}{
%			\vliin{\rho}{}{\Gamma,?A, ?A}{\vlhy{\Gamma_1, ?A, ?A}}{ \vlhy{\Gamma_2} }
%		}
%	}
%\]
%%\[
%%\begin{array}{rcl}
%%	\vlderivation{
%%		\vliin{\land}{}{\Gamma, \Delta, ?A, B\land C}{
%%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}
%%		}{\vlhy{\Delta, C}}
%%	}
%%	\quad &\to &\quad
%%	\vlderivation{
%%		\vlin{\cntr}{}{\Gamma, \Delta, ?A, B\land C}{
%%			\vliin{\land}{}{\Gamma, \Delta, ?A, ?A, B\land C}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, C} }
%%		}
%%	}
%%%	\]
%%%	
%%%	\[
%%\\
%%\noalign{\smallskip}
%%	\vlderivation{
%%		\vliin{\cut}{}{\Gamma, \Delta, ?A}{
%%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}
%%		}{\vlhy{\Delta, \lnot{B}}}
%%	}
%%	\quad &\to& \quad
%%	\vlderivation{
%%		\vlin{\cntr}{}{\Gamma, \Delta, ?A}{
%%			\vliin{\cut}{}{\Gamma, \Delta, ?A, ?A}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, \lnot{B}} }
%%		}
%%	}
%%\end{array}
%%\]
%for each binary rule $\rho \in \{ \land, \cut \}$.
%\item The commuting step:
%	\[
%	\vlderivation{
%		\vliin{\vlan}{}{\Gamma, ?A, B\vlan C}{
%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}
%		}{\vlhy{\Gamma, ?A, B}}
%	}
%	\quad \to \quad
%	\vlderivation{
%		\vlin{\cntr}{}{\Gamma, ?A, B\vlan C}{
%			\vliin{\vlan}{}{\Gamma, ?A, ?A, B\vlan C}{\vlhy{\Gamma, ?A, ?A, B}}{
%				\vlin{\wk}{}{\Gamma, ?A, ?A, C}{\vlhy{\Gamma, ?A, C}}
%			}
%		}
%	}
%	\]
%	\end{enumerate}
%	For binary rules:
%
%\end{definition}
%\begin{proposition}
%	$\anarrow{}{\cntdown}$ is weakly normalising
%	, modulo $\cntr$-$\cntr$ redexes,
%	and degree-preserving. 
%	If $\pi$ is $\anarrow{}{\cutredlin}$-normal and $\pi \downarrow_\cntdown \pi'$, then so is $\pi'$.
%\end{proposition}
%\begin{proof}
%	By induction on the number of redexes in a proof. Start with bottommost redex, by induction on number of inference steps beneath it.
%\end{proof}
%
%\begin{remark}
%	Only weakly normalising since $\cntr$ can commute with $\cntr$, allowing cycles.
%\end{remark}
%
%\begin{proposition}
%	If $\pi$ is $\anarrow{}{\cutredexp}$-reducible but $\anarrow{}{\cutredlin}$- and $\anarrow{}{\cntdown}$-normal then there is a derivation $H:\pi \anarrow{*}{\cutredexp} \pi'$ such that $\deg (\pi')<\deg(\pi)$.
%\end{proposition}
%
%
%
%\subsection{Base cases}
%
%\[
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,a }{ \vlhy{\Gamma,a} }{ \vlin{\id}{}{a,a^\bot}{ \vlhy{} } }
%}
%\quad\to\quad
%\vlderivation{
%\Gamma,a
%}
%\]
%
%\[
%\vlderivation{
%\vliin{\cut}{}{\Gamma}{ \vlin{\bot}{}{ \Gamma,\bot }{ \vlhy{\Gamma} } }{ \vlin{1}{}{1}{ \vlhy{} } }
%}
%\quad\to\quad
%\vlderivation{
%\Gamma
%}
%\]
%
%\[
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,\Delta,\top }{ \vlin{\top}{}{ \Gamma,\top,0 }{ \vlhy{} } }{ \vlhy{\Delta , \top } }
%}
%\quad\to\quad
%\vlinf{\top}{}{ \Gamma,\Delta,\top }{}
%\]
%
%\subsection{Commutative cases}
%These are the cases when the principal formula of a step is not active for the cut-step below.
%
%\begin{enumerate}
%\item The cut-step is immediately preceded by an initial step. Note that only the case for $\top$ applies:
%\[
%\vlderivation{
%\vliin{\cut}{}{\Gamma,\Delta,\top}{ 
%\vlin{\top}{  }{ \Gamma,\top,A }{ \vlhy{} }
% }{ \vlhy{\Delta,A^\bot } }
%}
%\quad\to\quad
%\vlinf{\top}{}{ \Gamma,\Delta,\top }{}
%\]
%%Notice that this commutation eliminates the cut entirely and preserves the height of all cuts below.
%\item\label{CaseCommOneStep} A cut-step is immediately preceded by a step $\rho$ with exactly one premiss:
%\[
%\vlderivation{
%\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}
%}
%\]
%We have three subcases:
%\begin{enumerate}
%\item\label{subcase:unary-commutation-vanilla} 
%%$\Delta$ consists of only $?$-ed formulae or 
%If $\rho \notin \{! , \indr \}$ then we can simply permute as follows:
%\begin{equation}
%\label{eqn:com-case-unary-simple}
%\vlderivation{
%\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}
%}
%\quad \to \quad
%\vlderivation{
%\vlin{\rho}{}{\Gamma',\Delta}{
%\vliin{\cut}{}{\Gamma,\Delta}{\vlhy{\Gamma,A}}{\vlhy{A^\bot , \Delta}}
%}
%}
%\end{equation}
%(If $\rho$ was $\forall$ then we might need to rename some free variables in $\Delta$.)
%\item $\rho $ is a $!$-step. Therefore $\Gamma$ has the form $? \Sigma , B$ and $A$ has the form $?C$, yielding the following situation:
%\[
%\vlderivation{
%\vliin{\cut}{}{? \Sigma, !B, \Delta }{
%\vlin{!}{}{? \Sigma, !B , ?C}{\vlhy{?\Sigma , B , ?C}  }
%}{
%\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}
%}
%}
%\]
%Now, if $!C^\perp$ is principle for $\rho'$ then $\rho'\in \{! , \indr\}$ and so $\Delta $ must be $?$-ed; in this case we are able to apply the transformation \eqref{eqn:com-case-unary-simple}. Otherwise $A^\perp$ is not principal for $\rho'$ and so $\rho' \notin \{! , \indr \}$, which means we can apply \ref{subcase:unary-commutation-vanilla} along this side of the subproof.
%\item $\rho$ is a $\indr$-step. Therefore $\Gamma$ has the form $? \Sigma , B^\perp(x), B(s x) $ and $A$ has the form $?C$, and the argument is similar to the case above.
%% yielding the following situation:
%%\[
%%\vlderivation{
%%	\vliin{\cut}{}{? \Sigma, B^\perp (0) , B(t), \Delta }{
%%		\vlin{\indr}{}{? \Sigma, B^\perp (0) , B(t) , ?C}{\vlhy{?\Sigma , B^\perp(x) , B(s x) , ?C}  }
%%	}{
%%	\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}
%%}
%%}
%%\]
%\end{enumerate}
%
%
%
%\item A cut-step is immediately preceded by a $\vlte $-step:
%\[
%\vlderivation{
%\vliin{\cut}{}{\Gamma,\Delta,\Sigma,A\vlte B }{
%\vliin{\vlte}{}{\Gamma,\Delta,A\vlte B,C }{\vlhy{\Gamma,A,C}}{\vlhy{\Delta,B}}
%}{\vlhy{ \Sigma , C^\bot  }}
%}
%\quad\to\quad
%\vlderivation{
%\vliin{\vlte}{}{\Gamma,\Delta,\Sigma,A\vlte B}{
%\vliin{\cut}{}{\Gamma,\Sigma,A}{\vlhy{\Gamma,A,C}}{\vlhy{\Sigma,C^\bot}}
%}{\vlhy{\Delta,B}}
%}
%\]
%%Notice that this commutation might increase the height of any cuts below along the right branch of the indicated cut, but decreases the height along the left branch.
%\item\label{CommCaseAmpersand} A cut-step is immediately preceded by a $\vlan$-step.
%\[
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,\Delta,A\vlan B }{ \vliin{\vlan}{}{\Gamma,A\vlan B,C}{ \vlhy{\Gamma,A,C} }{\vlhy{\Gamma,B,C}}}{ \vlhy{\Delta, C^\bot} }
%}
%\quad\to\quad
%\vlderivation{
%\vliin{\vlan}{}{\Gamma,\Delta,A\vlan B }{
%\vliin{cut}{}{\Gamma,\Delta,A }{ \vlhy{\Gamma,A,C} }{ \vlhy{ \Delta,C^\bot } }
%}{
%\vliin{ \cut }{}{\Gamma,\Delta,B}{ \vlhy{\Gamma,B,C } }{ \vlhy{\Delta,C^\bot} }
%}
%}
%\]
%\item (No rule for cuts commuting with cuts.)
%%A cut-step is immediately preceded by another cut-step:
%\[
%\vlderivation{
%	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{
%		\vliin{\cut}{}{\Gamma, \Delta, B}{\vlhy{\Gamma, A}}{\vlhy{\Delta, \lnot{A}, B}}
%		}{\vlhy{\Sigma, \lnot{B}}}
%	}
%	\quad\to\quad
%\vlderivation{
%	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{\vlhy{\Gamma, A}}{
%		\vliin{\cut}{}{\Delta, \Sigma, \lnot{A}}{\vlhy{\Delta, \lnot{A}, B}}{\vlhy{\Sigma, \lnot{B}}}
%		}
%	}
%\]
%\end{enumerate}
%
%
%
%\subsection{Key cases: structural steps}
%%[THIS SECTION MIGHT NOT BE NECESSARY]
%We attempt to permute cuts on exponential formulae over structural steps whose principal formula is active for the cut. 
%
%We use the commutative case \ref{CaseCommOneStep} to assume that the topmost cut-step in a sequence has already been permuted up to its origin on the $!$-side. 
%
%We have two cases.
%\begin{enumerate}
%\item\label{StructStepCont} The structural step preceding the cut is a weakening:
%\[
%\vlderivation{
%\vliin{\cut}{}{?\Gamma,\Delta}{ \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} } }{ \vlin{w}{}{ ?A^\bot }{ \vlhy{\Delta	} } }
%}
%\quad\to\quad
%\vlinf{w}{}{?\Gamma,\Delta}{ \Delta }
%\]
%%\item The structural step preceding the cut is a contraction:
%%\[
%%\vlderivation{
%%\vliin{\cut}{}{ ?\Gamma,\Delta }{
%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }
%%}
%%\quad\to\quad
%%\vlderivation{
%%\vliq{c}{}{?\Gamma, \Delta}{
%%\vliin{\cut}{}{?\Gamma, ?\Gamma,\Delta }{
%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%%}{
%%\vliin{\cut}{}{?\Gamma,?A^\bot , \Delta }{
%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }
%%}
%%}
%%}
%%\]
%%OR use a multicut:
%%\[
%%\vlderivation{
%%\vliin{\cut}{}{ ?\Gamma,\Delta }{
%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }
%%}
%%\quad\to\quad
%%\vlderivation{
%%\vliin{\multicut}{}{?\Gamma,?A^\bot , \Delta }{
%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }
%%}
%%\]
%\item The structural step preceding a cut is a contraction:
%\[
%\vlderivation{
%	\vliin{\cut}{}{?\Gamma, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{
%		\vlin{\cntr}{}{ ?A,\Sigma }{ \vlhy{ ?A,?A,\Sigma } }
%	}
%}
%\quad\to\quad
%\vlderivation{
%	\vliq{\cntr}{}{ ?\Gamma,\Sigma }{
%		\vliin{\cut}{}{ ?\Gamma,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{
%			\vliin{\cut}{}{ ?A,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,\Sigma } }
%		}
%	}
%}
%\]
%%\item The structural step preceding a cut is a parallel contraction:
%%\[
%%\vlderivation{
%%\vliin{\cut}{}{?\Gamma,?\Delta, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{
%%\vlin{}{}{ ?A,?\Delta,\Sigma }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }
%%}
%%}
%%\quad\to\quad
%%\vlderivation{
%%\vlin{}{}{ ?\Gamma,?\Delta,\Sigma }{
%%\vliin{\cut}{}{ ?\Gamma,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{
%%\vliin{\cut}{}{ ?A,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }
%%}
%%}
%%}
%%\]
%\end{enumerate}
%
%\subsection{Key cases: logical steps}
%Finally, once all cuts have been permuted maximally on both sides, we have the cases when the cut-formula is principal for a preceding logical step on both sides. We have three cases, one for every pair of connectives.
%\begin{enumerate}
%\item The cut-formula is multiplicative:
%\[
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{
%\vliin{\vlte}{}{ \Gamma,\Delta,A\vlte B }{ \vlhy{\Gamma,A} }{ \vlhy{\Delta,B} }
%}{ \vlin{\vlpa}{}{ \Sigma, A^\bot \vlpa B^\bot }{ \vlhy{\Sigma , A^\bot , B^\bot} } }
%}
%\quad\to\quad
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{ \vlhy{\Gamma,A} }{
%\vliin{\cut}{}{ \Delta,\Sigma,A^\bot }{ \vlhy{\Delta,B} }{ \vlhy{\Sigma , A^\bot,B^\bot } }
%}
%}
%\]
%\item The cut-formula is additive,
%\[
%\vlderivation{
%\vliin{\cut}{}{ \Gamma,\Delta }{ 
%\vliin{\vlan}{}{ \Gamma,A\vlan B }{ \vlhy{\Gamma,A} }{ \vlhy{\Gamma,B} }
% }{ \vlin{\vlor}{}{ \Delta,A^\bot\vlor B^\bot }{ \vlhy{\Delta, A^\bot } } }
%}
%\quad\to\quad
%\vliinf{\cut}{}{ \Gamma,\Delta }{ \Gamma,A }{ \Delta,A^\bot }
%\]
%where the case for the other $\vlor$-rule is symmetric.
%\item The cut-formula is exponential.
%\[
%\vlderivation{
%\vliin{\cut}{}{ ?\Gamma,\Delta }{
% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }
%}{
%\vlin{?}{}{ \Delta,?A^\bot }{ \vlhy{\Delta, A^\bot } }
%}
%}
%\quad\to\quad
%\vliinf{\cut}{}{ ?\Gamma,\Delta }{ ?\Gamma,A }{ \Delta,A^\bot }
%\]
%\item The cut-formula is quantified.
%\[
%\vlderivation{
%	\vliin{\cut}{}{\Gamma, \Delta}{
%		\vlin{\forall}{}{\Gamma, \forall x. A(x)}{\vltr{\pi(a)}{\Gamma, A(a)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}}
%		}{
%		\vlin{\exists}{}{\Delta, \exists x . \lnot{A}(x)}{\vlhy{\Delta, \lnot{A}(t)}}
%		}
%	}
%	\quad \to \quad
%	\vlderivation{
%		\vliin{\cut}{}{\Gamma, \Delta}{
%			\vltr{\pi(t)}{\Gamma, A(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
%			}{\vlhy{\Delta, \lnot{A}(t)}}
%		}
%\]
%\end{enumerate}

