Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\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} and \ref{lem:standardcommutations}; 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}