\section{Display Calculus}\label{app:display}

%% This appendix will give further details to expand on the proofs 
%% of Secs. \ref{Sec:display} and
%% \ref{Sec:biill_to_fill}
%% regarding the
%% display calculi $\filldc$ and $\biilldc$.

%% First, 
We outline the conditions that are easily checked to confirm that the
display calculi enjoy cut-elimination (Thm. \ref{thm:cutad}):

\begin{definition}[Belnap's Conditions C1-C8]
The set of display conditions appears in various guises in the literature. Here we follow
the presentation given in Kracht~\cite{kracht-power}.
\begin{description}
\item[(C1)] Each formula variable occurring in some premise of a rule $\rho$ is a subformula
of some formula in the conclusion of~$\rho$.
\item[(C2)] \textit{Congruent parameters} is a relation between parameters of the identical structure variable occurring 
in the premise and conclusion sequents. 
%For example, Consider the rule~${\imp}{\DC}$ in Table~\ref{DLMlogical}:
%the parameter~$X$ occurring in the left premise sequent and the conclusion sequent of ${\imp}{\DC}$
%are congruent parameters. Similarly, the parameter~$Y$ occurring in the right premise sequent and 
%the conclusion sequent of ${\imp}{\DC}$ are congruent parameters.
%c;
\item[(C3)] Each parameter is congruent to at most one structure variable in the conclusion. Equivalently,
no two structure variables in the conclusion are congruent to each other.
\item[(C4)] Congruent parameters are either all antecedent or all succedent parts of their respective sequent.
\item[(C5)] A formula in the conclusion of a rule~$\rho$ is either the entire
antecedent or the entire succedent. Such a formula is called a \textbf{principal formula} of~$\rho$.
\item[(C6/7)] Each rule is closed under simultaneous substitution of arbitrary structures for congruent
parameters.
\item[(C8)] If there are rules $\rho$ and $\sigma$ with respective
conclusions $X\turn A$ and $A\turn Y$ with formula $A$ principal in
both inferences (in the sense of C5) and if $cut$ is applied to
yield $X\turn Y$, then either $X\turn Y$ is identical to either
$X\turn A$ or $A\turn Y$; or it is possible to pass from the
premises of $\rho$ and $\sigma$ to $X\turn Y$ by means of inferences
falling under $cut$ where the cut-formula always is a proper
subformula of $A$. 
%
%Remark: The C8 condition sounds as if we can use only cuts here, but
%it is really more like ``(rp) and (drp) inferences and cut as long
%as the cut formula is always a proper subformula of $A$''.
\end{description}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conservativity of BiILL over FILL}\label{app:conserv}

Fig.~\ref{fig:filld} explicitly gives the proof rules for $\filldn$, the nested
sequent calculus with deep inference for FILL. These are easily derived from
$\biilldn$ (Fig.~\ref{fig:fbilld}).

\begin{figure}[t]
{\small

%% $$
%% \infer[id^d]
%% {X[\,Y^l[A] \seq Y^r[A]\,]}{
%% \mbox{
%%   $\begin{array}{c}
%%   X[~] \mbox{ is a hollow context}, \\
%%   Y^l \mbox{ is a left-context} \mbox{ and } 
%%   Y^r \mbox{ is a right-context.}
%%   \end{array}
%%   $
%% }
%% }
%% \infer[cut]
%% {X[\Sc \seq \Tc]}
%% {X_1[\Sc_1 \seq \Tc_1, A] & X_2[\Sc_2, A \seq \Tc_2]}
%% $$

Propagation rules:
%% $$
%% \infer[pl]
%% {X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
%% {
%%  X[\Sc \seq (A, \Sc' \seq \Tc'), \Tc]
%% }
%% \qquad
%% \infer[pr]
%% {X[(\Sc \seq \Tc), \Sc' \seq A, \Tc']}
%% {X[(\Sc \seq \Tc, A), \Sc' \seq \Tc']}
%% $$

$$
\infer[pl_1]
{X[\Gamma, A \seq (\Gamma' \seq \Tc'), \Tc]}
{
 X[\Gamma \seq (A, \Gamma' \seq \Tc'), \Tc]
}
\qquad
\infer[pr_2]
{X[\Gamma \seq \Tc, (\Gamma' \seq \Tc', A)]}
{X[\Gamma \seq \Tc, A, (\Gamma' \seq \Tc')]}
$$

Identity and logical rules: In branching rules, $X[~] \in X_1[~] \merge X_2[~]$
and $\Tc \in \Tc_1 \merge \Tc_2$.
$$
\infer[id^d]
{X[p \seq p, \Vc]}
{\mbox{$X[~]$ and $\Vc$ are hollow.}}
\qquad
\infer[\punit_l^d]
{X[\punit \seq \Vc]}
{\mbox{$X[~]$ and $\Vc$ are hollow. }}
\qquad
\infer[\punit_r^d]
{X[\Gamma \seq \Tc, \punit]}
{X[\Gamma \seq \Tc]}
$$
$$
\infer[\tunit_l^d]
{X[\Gamma, \tunit \seq \Tc]}
{X[\Gamma \seq \Tc]}
\qquad
\infer[\tunit_r^d]
{X[\cdot \seq \tunit, \Vc]}
{\mbox{$X[~]$ and $\Vc$ are hollow. }}
$$
$$
\infer[\ltens_l^d]
{X[\Gamma, A \ltens B \seq \Tc]}
{X[\Gamma, A, B \seq \Tc]}
\qquad
\infer[\ltens_r^d]
{X[\Gamma_1,\Gamma_2 \seq A \ltens B, \Tc]}
{X_1[\Gamma_1 \seq A, \Tc_1] & X_2[\Gamma_2 \seq B, \Tc_2]}
$$
$$
\infer[\limp_l^d]
{X[\Gamma_1,\Gamma_2, A \limp B \seq \Tc]}
{
X_1[\Gamma_1 \seq A, \Tc_1] & X_2[\Gamma_2, B \seq \Tc_2]
}
\qquad
\infer[\limp_r^d]
{X[\Gamma \seq \Tc, A \limp B]}
{X[\Gamma \seq \Tc, (A \seq B)]}
$$
$$
\infer[\parr_l^d]
{X[\Gamma_1,\Gamma_2, A \parr B \seq \Tc]}
{
 X_1[\Gamma_1, A \seq \Tc_1]
 &
 X_2[\Gamma_2, B \seq \Tc_2]
}
\qquad
\infer[\parr_r^d]
{X[\Gamma \seq A \parr B, \Tc]}
{X[\Gamma \seq A, B, \Tc]}
$$
}
\caption{The deep inference system $\filldn$. }
% \caption{The deep inference system $\biilldn$. In branching rules, $X[~] \in X_1[~] \merge X_2[~]$,
% $\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$.}
\label{fig:filld}
\end{figure}

\begin{proof}[Proof of Lemma~\ref{lem:basic_arr}]
This is basic category theory; we give one example to illustrate the techniques
used. Given an arrow $f:A\otimes B\to C$, we get a new arrow $A\to B\limp C$ by
composing $B\limp f$ with the `co-evaluation' arrow $\eta:A\to B\limp(A\otimes
B)$.
\end{proof}

\begin{proof}[Proof of Lemma~\ref{lem:ctxt}]
By induction on the size of $X[~]$. The base case, where $X[~]$ is a hole, is
trivial. The induction case involves a context $\Gamma\seq X[~],\Tc$ and hence
requires an arrow
$$
\Gamma\limp X[S]\parr\Tc \quad\to\quad \Gamma\limp X[T]\parr\Tc.
$$
This exists by the induction hypothesis and the inductive definitions of
Lem.~\ref{def:free}. The validity of $X[S]$ then transfers to $X[T]$ via
composition with the arrow $I\to X[S]$.
\end{proof}

\begin{proof}[Proof of Lemma~\ref{lem:merg_tens}(ii) and (iii)]
(ii): The base case requires an arrow
\begin{equation}\label{eq:mt_2}
(\Gamma_1\limp A\parr\Tc_1)\otimes(\Gamma_2\otimes B\limp \Tc_2)\otimes
\Gamma_1\otimes\Gamma_2\otimes(A\limp B) \quad\to\quad \Tc.
\end{equation}
Applying an evaluation to the left of \eqref{eq:mt_2} gives $(A\parr\Tc_1)
\otimes(\Gamma_2\otimes B\limp \Tc_2)\otimes\Gamma_2\otimes(A\limp B)$; weak
distributivity gives $\Tc_1\parr(A\otimes(\Gamma_2\otimes B\limp \Tc_2)\otimes
\Gamma_2\otimes(A\limp B))$; two more evaluations give $\Tc_1\parr\Tc_2$ and
Lem.~\ref{lem:merg} completes the result.

(iii): The base case requires an arrow
\begin{equation}\label{eq:mt_3}
(\Gamma_1\otimes A\limp \Tc_1)\otimes(\Gamma_2\otimes B\limp \Tc_2)\otimes
\Gamma_1\otimes\Gamma_2\otimes(A\parr B) \quad\to\quad \Tc.
\end{equation}
Two applications of weak distributivity map the left of \eqref{eq:mt_3} to
$$
((\Gamma_1\otimes A\limp \Tc_1)\otimes\Gamma_1\otimes A)\parr
((\Gamma_2\otimes B\limp \Tc_2)\otimes\Gamma_2\otimes B).
$$
Two evaluations and Lem.~\ref{lem:merg} complete the result.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Annotated Sequent Calculi Proofs}

On the next page we present cut-free proofs of the Bierman example
\eqref{eq:Bierman} in the style of the three cut-free annotated sequent calculi
in the literature: that due to Bierman \cite{Bierman:Note}; that due to Bellin
reported in \cite{Bierman:Note}, and that due to Br\"{a}uner and de Paiva
\cite{Brauner:Formulation}. Note that all three proofs contain the same
sequence of proof rules; strip out the annotations and they are MLL proofs
of the sequent. The difference between the calculi lies in the nature of their
annotations, all of which come into play to verify that the final rule
application, of ($\limp R$), is legal. The reader is invited to compare these
proofs to those presented in the paper using display calculus (Fig.
\ref{Fig:Bierman}) and deep inference (Fig. \ref{fig:bierman-deep}).

\newpage
\begin{landscape}
Bierman-style proof; ($\limp R$) is legal because $v$ and $(w\parr x\limp y)
\parr z$ share no free variables.
\begin{prooftree}
\AxiomC{$v:a\turn v:a$}
\AxiomC{$w:b\turn w:b$}
\BinaryInfC{$v\parr w:a\parr b\turn v:a,w:b$}
\AxiomC{$x:c\turn x:c$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c \turn v:a,w:b,x:c$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c \turn v:a,w\parr x:b\parr c$}
\AxiomC{$y:d\turn y:d$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,w\parr x\limp y:b\parr c\limp d\turn v: a,y:d$}
\AxiomC{$z:e\turn z:e$}
\BinaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,(w\parr x\limp y)\parr z:(b\parr c\limp d)\parr e\turn v:a,y:d,z:e$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c,(w\parr x\limp y)\parr z:(b\parr c\limp d)\parr e\turn v:a,y\parr z:d\parr e$}
\UnaryInfC{$(v\parr w)\parr x:(a\parr b)\parr c\turn v:a,\lambda(w\parr x\limp y)\parr z^{(b\parr c\limp d)\parr e}.(y\parr z):(b\parr c\limp d)\parr e\limp d\parr e$}
\end{prooftree}

Bellin-style proof; ($\limp R$) is legal because $r$ is not free in $\mbox{let }
t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v$. We apologise
for the extremely small font size necessary to fit this proof on the page.
{\tiny
\begin{prooftree}
\AxiomC{$v:a\turn v:a$}
\AxiomC{$w:b\turn w:b$}
\BinaryInfC{$u:a\parr b\turn \mbox{let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let }u\mbox{ be -}\parr w\mbox{ in }w:b$}
\AxiomC{$x:c\turn x:c$}
\BinaryInfC{$t:(a\parr b)\parr c \turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w:b,\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x:c$}
\UnaryInfC{$t:(a\parr b)\parr c \turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x):b\parr c$}
\AxiomC{$y:d\turn y:d$}
\BinaryInfC{$t:(a\parr b)\parr c,s:b\parr c\limp d\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)):d$}
\AxiomC{$z:e\turn z:e$}
\BinaryInfC{$t:(a\parr b)\parr c,r:(b\parr c\limp d)\parr e\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)):d,\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z:e$}
\UnaryInfC{$t:(a\parr b)\parr c,r:(b\parr c\limp d)\parr e\turn  \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,(\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)))\parr(\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z):d\parr e$}
\UnaryInfC{$t:(a\parr b)\parr c\turn \mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be }v\parr\mbox{- in }v:a,\lambda r^{(b\parr c\limp d)\parr e}.(\mbox{let } r\mbox{ be }s\parr\mbox{- in }(s(\mbox{let }t\mbox{ be }u\parr\mbox{- in let }u\mbox{ be -}\parr w\mbox{ in }w)\parr(\mbox{let }t\mbox{ be -}\parr x\mbox{ in }x)))\parr(\mbox{let }s\mbox{ be -}\parr z\mbox{ in }z):(b\parr c\limp d)\parr e\limp d\parr e$}
\end{prooftree}
}

Br\"{a}uner and de Paiva-style proof; ($\limp R$) is legal because $(b\parr c
\limp d)\parr e$ is not related to $a$.
\begin{prooftree}
\AxiomC{ \ }\LeftLabel{$(a,a)$\;}
\UnaryInfC{$a\turn a$}
\AxiomC{ \ }\RightLabel{\;$(b,b)$}
\UnaryInfC{$b\turn b$}\LeftLabel{$(a\parr b,a),(a\parr b,b)$\;}
\BinaryInfC{$a\parr b\turn a,b$}
\AxiomC{ \ }\RightLabel{\;$(c,c)$}
\UnaryInfC{$c\turn c$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,b),((a\parr b)\parr c,c)$\;}
\BinaryInfC{$(a\parr b)\parr c \turn a,b,c$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,b\parr c)$\;}
\UnaryInfC{$(a\parr b)\parr c \turn a,b\parr c$}
\AxiomC{ \ }\RightLabel{$(d,d)$}
\UnaryInfC{$d\turn d$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d),(b\parr c\limp d,d)$\;}
\BinaryInfC{$(a\parr b)\parr c,b\parr c\limp d\turn a,d$}
\AxiomC{ \ }\RightLabel{\;$(e,e)$}
\UnaryInfC{$e\turn e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d),((b\parr c\limp d)\parr e,d),((b\parr c\limp d)\parr e,e)$\;}
\BinaryInfC{$(a\parr b)\parr c,(b\parr c\limp d)\parr e\turn a,d,e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,d\parr e),((b\parr c\limp d)\parr e,d\parr e)$\;}
\UnaryInfC{$(a\parr b)\parr c,(b\parr c\limp d)\parr e\turn a,d\parr e$}\LeftLabel{$((a\parr b)\parr c,a),((a\parr b)\parr c,(b\parr c\limp d)\parr e\limp d\parr e)$\;}
\UnaryInfC{$(a\parr b)\parr c\turn a,(b\parr c\limp d)\parr e\limp d\parr e$}
\end{prooftree}

\end{landscape}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The Shallow Nested Sequent Calculus}
\label{apx:shallow}

A structure can be interpreted as a multiset of nested sequents by 
replacing both $>$ and $<$ with the sequent arrow $\seq$, and interpreting the structural
connective `,' (comma) as multiset union, and $\Phi$ as the empty multiset. 
That is, the structure of a nested sequent incorporates implicitly the associativity and
commutativity of comma, and its unit, via the multiset structure. Conversely, a
nested sequent can be translated to an equivalence class of structures (modulo 
the associativity, commutativity and unit laws for `,') 
by replacing sequent arrows in negative positions with $<$, and those in positive positions with $>$. 
Given a nested sequent $X$, we shall write $\seqtodisp{X}$ to denote the corresponding (equivalence class of) 
structure in display calculus. Conversely, give a structure $X$, we write 
$\disptoseq{X}$ to denote the multiset of formulas/sequents that correspond to $X.$
\\

\noindent
{\bf Theorem \ref{thm:biill-sn-eq-dc}.} 
A formula $B$ is cut-free provable in $\biillsn$ iff it is cut-free provable in $\biilldc$. 

\begin{proof}
We show that cut-free $\biillsn$ can simulate cut-free $\biilldc$ and vice versa. To prove this, we need
to generalise slightly the statement to the following:
\begin{itemize}
\item If $(X \vdash Y)$ is cut-free provable in $\biilldc$ then $(\disptoseq{X} \seq \disptoseq{Y})$
is cut-free provable in $\biillsn$.
\item If $(X \seq Y)$ is cut-free provable in $\biillsn$ then $\seqtodisp{X} \vdash \seqtodisp{Y}$
is cut-free provable in $\biilldc.$
\end{itemize}
The first statement is easy, since the rules of $\biillsn$ are more general than $\biilldc.$ 
We show here the other direction. We illustrate here the case for the $\parr_l$ rule. 
For simplicity, we omit applications of structural
rules for associativity, commutativity and unit, and obvious applications of display postulates. 
$$
\infer[\parr_l]
{\Sc, \Sc', A \parr B \seq \Tc, \Tc'}
{\Sc, A \seq \Tc & \Sc', B \seq \Tc'}
\qquad
\leadsto
\qquad
\infer[]
{\seqtodisp{\Sc}, \seqtodisp{\Sc'}, A \parr B \vdash \seqtodisp{\Tc}, \seqtodisp{\Tc'}}
{
\infer[]
{\seqtodisp{\Sc},  A \parr B \vdash \seqtodisp{\Sc'} > (\seqtodisp{\Tc}, \seqtodisp{\Tc'})}
{
 \infer[]
 {\seqtodisp{\Sc},  A \parr B \vdash (\seqtodisp{\Sc'} > \seqtodisp{\Tc'}), \seqtodisp{\Tc}}
 {
  \infer[]
  {  A \parr B \vdash \seqtodisp{\Sc} > ((\seqtodisp{\Sc'} > \seqtodisp{\Tc'}), \seqtodisp{\Tc})}
  {
   \infer[]
   { A \parr B \vdash (\seqtodisp{\Sc} > \seqtodisp{\Tc}), (\seqtodisp{\Sc'} > \seqtodisp{\Tc'})}
   {
    \infer[]
    {A \vdash (\seqtodisp{\Sc} > \seqtodisp{\Tc})}
    {\seqtodisp{\Sc}, A \vdash \seqtodisp{\Tc}}
    &
    \infer[]
    {B \vdash (\seqtodisp{\Sc'} > \seqtodisp{\Tc'})}
    {\seqtodisp{\Sc'}, B \vdash \seqtodisp{\Tc'}}
   }
  }
 }
}
}
$$
\end{proof}

\section{The Equivalence Between Shallow and Deep Inference Calculi}
\label{apx:equiv}

\subsection{From deep inference to shallow inference}
\label{apx:deep-to-shallow}

\begin{lemma}[Weakening of hollow sequents]
\label{lm:weak}
The following rules are cut-free derivable in $\biillsn$:
$$
\infer[w_l]
{X, \Uc \seq \Vc}
{\Uc \seq \Vc}
\qquad
\infer[w_r]
{\Uc \seq \Vc, X}
{\Uc \seq \Vc}
$$
provided $X$ is a hollow sequent.
\end{lemma}
\begin{proof}
By induction on the size of $X.$
\end{proof}

%% \begin{lemma}
%% \label{lm:left-right}
%% The following rule is cut-free derivable in $\biillsn$:
%% $$
%% \infer[lr]
%% {X^l[\Sc] \seq Y^r[\Tc]}
%% {
%% \Sc \seq \Tc
%% }
%% $$
%% where $X^l[~]$ is a left-context and $Y^r[~]$ is a right-context.
%% \end{lemma}
%% \begin{proof}
%% By induction on the size of $X^l[~]$ and $Y^l[~]$, and using Lemma~\ref{lm:weak}. We look at an interesting
%% case where $X^l[~] = (X_1^l[~] \seq \Uc)$ and $Y^r[~] = (\Vc \seq Y_1^r[~])$ where $\Uc$ and $\Vc$ are hollow
%% sequents. 
%% $$
%% \infer[gl]
%% {(X_1^l[\Sc] \seq \Uc) \seq (\Vc \seq Y_1^r[\Tc])}
%% {
%% \infer[gr]
%% {X_1^l[\Sc], ( \sunit \seq \Uc) \seq (\Vc \seq Y_1^r[\Tc])}
%% {
%%  \infer[w_l]
%%  {X_1^l[\Sc], ( \sunit \seq \Uc) \seq (\Vc \seq \sunit), Y_1^r[\Tc]}
%%  {
%%   \infer[w_r]
%%   {X_1^l[\Sc] \seq (\Vc \seq \sunit), Y_1^r[\Tc]}
%%   {
%%    \deduce{X_1^l[\Sc] \seq Y_1^r[\Tc]}{\deduce{\vdots}{\Sc \seq \Tc} }
%%   }
%%  }
%% }
%% }
%% $$
%% \end{proof}

\begin{lemma}
\label{lm:idd}
The rule $id^d$ is cut-free derivable in $\biillsn$.
\end{lemma}
\begin{proof}
We show that $X[\Sc, A \seq A, \Tc]$ is provable in $\biillsn$,
where $X[~]$, $\Sc$ and $\Tc$ are hollow. 
We show the case where $X[~]$ is a positive context; the other case where $X[~]$ is negative
can be proved dually. 
Note that by the display property (Proposition \ref{prop:display}), the sequent $X[\Sc, A \seq A, \Tc]$
is display-equivalent to $\Uc, \Sc, A \seq A, \Tc$ for some $\Uc$.
Clearly the structure $\Uc$ here must be a multiset of hollow sequents. The derivation
is thus constructed as follows: 
$$
\infer[\mbox{Prop. \ref{prop:display} }]
{X[\Sc, A \seq A, \Tc]}
{
\infer[wr;wl]
{\Uc, \Sc, A \seq A, \Tc}
{
 \infer[id]
 {A \seq A}{}
}
}
$$
\end{proof}

\noindent{\bf{Lemma \ref{lm:dist}.}} 
The following rules are derivable in $\biillsn$ without cut:
$$
\infer[dist_l]
{(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2), \Uc \seq \Vc}
{
(\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2), \Uc \seq \Vc
}
\qquad
\infer[dist_r]
{\Uc \seq \Vc, (\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2)}
{
 \Uc \seq \Vc, (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
}
$$
\begin{proof}
We show here a derivation of $dist_l$. The $dist_r$ rule can be derived similarly. 
$$
\infer[rp_2]
{(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2), \Uc \seq \Vc}
{
 \infer[drp_1]
 {(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2) \seq (\Uc \seq \Vc)}
 {
   \infer[drp_2]
   {\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2, (\Uc \seq \Vc)}
   {
    \infer[gl]
    {(\Xc_1, \Xc_2  \seq \Yc_2) \seq \Yc_1, (\Uc \seq \Vc)}
    {
      \infer[rp_2]
      {\Xc_1, (\Xc_2  \seq \Yc_2) \seq \Yc_1, (\Uc \seq \Vc)}  
      {
       \infer[gr]
       {\Xc_1 \seq ((\Xc_2  \seq \Yc_2) \seq \Yc_1, (\Uc \seq \Vc))}  
       {
         \infer[drp_2]
         {\Xc_1 \seq \Yc_1, ((\Xc_2  \seq \Yc_2) \seq (\Uc \seq \Vc))}  
         {
           \infer[rp_1]
           {(\Xc_1 \seq \Yc_1) \seq ((\Xc_2  \seq \Yc_2) \seq (\Uc \seq \Vc))}  
           {
            \infer[rp_1]
            {(\Xc_1 \seq \Yc_1), (\Xc_2  \seq \Yc_2) \seq (\Uc \seq \Vc)}
            {
              {(\Xc_1 \seq \Yc_1), (\Xc_2  \seq \Yc_2), \Uc \seq \Vc}
            }  
           }
         }
      }
     }
    }
    }
 }
}
$$
\end{proof}

\subsection{From shallow inference to deep inference}
\label{apx:shallow-to-deep}

\begin{lemma}
\label{lm:idd-permute}
Suppose the $id^d$ rule is applicable to $X$. Suppose also that $X$ is the premise of
an instance of a rule in $\{rp_1,rp_2,drp_1,drp_2,gl,gr \}$ and suppose $X'$
is the conclusion of the same rule instance. Then $X'$ is derivable in $\biilldn.$
%% Then for every $X'$ such that
%% $$
%% \infer[\rho]
%% {X'}{X}
%% $$
%% where $\rho \in \{rp_1,rp_2,drp_1,drp_2,gl,gr \}$, we have that $X'$ is derivable in $\biilldn.$
\end{lemma}
\begin{proof}
Since $id^d$ is applicable to $X$, it must be the case that
$X = Y[\Sc, A \seq A, \Tc]$ for some $A$, hollow context $Y[~]$, 
and hollow sequents $\Sc$ and $\Tc.$
We do case analyses on how the rule $\rho$ affects $X$. If $\rho$ changes the
structure of $Y[~]$ only, but leave $[\Sc, A \seq A, \Tc]$ intact, 
i.e., $X' = Y'[\Sc, A \seq A, \Tc]$, then obviously $Y'[~]$ must also be
a hollow sequent, so the $id^d$ rule is applicable. 
The interesting case is when $\rho$ affects the subsequent $(\Sc, A \seq A, \Tc)$, i.e.,
when exactly of the $A$'s is moved by $\rho$ to a different nested sequent. 
We show here the interesting cases; the
others can be proved similarly. 
In all cases, these structural rules
can be replaced by propagation rules of $\biilldn.$
\begin{itemize}
\item $\rho$ is
$$
\infer[drp_1]
{(\Sc, A \seq \Uc) \seq A, \Vc}
{
\Sc, A \seq A, \Uc, \Vc
}
$$
where $\Tc = (\Uc, \Vc).$ Then the derivation of $X'$ is as follows:
$$
\infer[pl_2]
{(\Sc, A \seq \Uc) \seq A, \Vc}
{
\infer[id^d]
{A, (\Sc \seq \Uc) \seq A, \Vc}
{}
}
$$

\item $\rho$ is
$$
\infer[rp_1]
{\Uc, A \seq (\Vc \seq A, \Tc)}
{
\Uc, \Vc, A \seq A, \Tc
}
$$
where $\Sc = (\Uc, \Vc).$ The sequent $X'$ is derived as follows:
$$
\infer[pr_2]
{\Uc, A \seq (\Vc \seq A, \Tc)}
{
\infer[id^d]
{\Uc, A \seq (\Vc \seq \Tc), A}
{}
}
$$
\end{itemize}
\end{proof}


%% \begin{proof}
%% Since $id^d$ is applicable to $X$, it must be the case that
%% $X = Y[Z_1^l[A] \seq Z_2^r[A]]$ for some $A$, hollow context $Y[~]$, 
%% left-context $Z_1^l[~]$ and right-context $Z_1^r[~].$
%% We do case analyses on how the rule $\rho$ affects $X$. If $\rho$ changes the
%% structure of $Y[~]$ only, but leave $[Z_1^l[A] \seq Z_2^r[A]$ intact, 
%% i.e., $X' = Y'[Z_1^l[A] \seq Z_2^r[A]]$, then obviously $Y'[~]$ must also be
%% a hollow sequent, so the $id^d$ rule is applicable. 
%% The interesting case is when $\rho$ affects the subsequent $(Z_1^l[A] \seq Z_2^r[A]).$
%% In this case, we only need to show that $X'$ contains a subsequent of the form
%% $(Z_3^l[A] \seq Z_4^r[A])$ for some left-context $Z_3^l[~]$ and
%% right-context $Z_4^r[~].$ 
%% This can be easily verified; we show a few sample cases here. 
%% \begin{itemize}
%% \item $\rho = drp_1$. 
%% In one case, we have:
%% $$
%% \infer[drp_1]
%% {(Z_1^l[A] \seq U^r[A], \Uc) \seq \Vc}
%% {Z_1^l[A] \seq U^r[A], \Uc, \Vc }
%% $$
%% where $Z_2^r[A] = (U^r[A], \Uc, \Vc)$ for some multisets of hollow sequents $\Uc$, $\Vc.$
%% The subsequent we want is $(Z_1^l[A] \seq U^r[A], \Uc)$, i.e., let $Z_3^l[~] = Z_1^l[~]$
%% and let $Z_4^r[~] = (U^r[~], \Uc).$ Obviously $Z_3^l[~]$ is a left-context and
%% $Z_4^r[~]$ is a right-context, and the surrounding context $[~] \seq \Vc$ is hollow, so 
%% the $id^d$ is indeed applicable.

%% The other case is when $A$ is not moved to the subsequent, i.e., 
%% $$
%% \infer[drp_1]
%% {(Z_1^l[A] \seq \Uc) \seq U^r[A], \Vc}
%% {Z_1^l[A] \seq U^r[A], \Uc, \Vc }
%% $$
%% In this case, take $Z_3^l[~] = (Z_1^l[~] \seq \Uc)$, which is a left-context,
%% and $Z_4^r[~] = (U^r[~], \Vc)$, which is a right-context.

%% The cases where $\rho$ is $drp_2$, $rp_1$ or $rp_2$ can be handled similarly. 

%% \item $\rho = gl$: 
%% \begin{itemize}
%% \item $\rho$ is
%% $$
%% \infer[gl]
%% {(Z_1^l[A], \Uc \seq Z_2^r[A]) \seq \Vc}
%% {(Z_1^l[A] \seq Z_2^r[A]), \Uc \seq \Vc}
%% $$
%% In this case, let $Z_3^l[~] = Z_1^l[~]$ and let $Z_4^r[~] = (Z_2^r[~], \Uc)$. 

%% \item $\rho$ is 
%% $$
%% \infer[gl]
%% {(\Vc, U^l[A] \seq \Uc) \seq Z_2^r[A]}
%% {(U^l[A] \seq \Uc), \Vc \seq Z_2^r[A]}
%% $$
%% i.e., $Z^l_1[~] = ((U^l[~] \seq \Uc), \Vc).$
%% In this case, let $Z_3^l[~] = (\Vc, U^l[~] \seq \Uc)$ and $Z_4^r[~] = Z_2^r[~].$
%% \end{itemize}
%% The case where $\rho = gr$ can be handled similarly.
%% \end{itemize}
%% \end{proof}

\begin{lemma}
\label{lm:const}
Suppose the $\punit$ rule (resp. the $\tunit$ rule)is applicable to $X.$ Suppose $X$ is
the premise of an instance of a rule in $\rho \in \{rp_1,rp_2,drp_1,drp_2,gl,gr \}$ and suppose
$X'$ is the conclusion of the same rule. Then $X'$ is derivable in $\biilldn.$
%% Then for every $X'$ such that
%% $$
%% \infer[\rho]
%% {X'}{X}
%% $$
%% where $\rho \in \{rp_1,rp_2,drp_1,drp_2,gl,gr \}$, $X'$ is derivable in $\biilldn$ using the $\punit$ (resp. $\tunit$) rule. 
\end{lemma}

To prove the following lemma, it is useful to consider a generalisation of the rules $gl$, $gr$, $drp_2$ and $rp_2$: 
$$
\infer[eg]
{\Sc, \Sc' \seq \Tc, \Tc'}
{(\Sc \seq \Tc), \Sc' \seq \Tc'}
\qquad
\infer[ig]
{\Sc, \Sc' \seq \Tc, \Tc'}
{
\Sc \seq (\Sc' \seq \Tc'), \Tc
}
$$
These two rules can be derived using $gl$, $gr$, $drp_2$ and $rp_2$ as follows:
$$
\infer[drp_2]
{\Sc, \Sc' \seq \Tc, \Tc'}
{
\infer[gl]
{(\Sc, \Sc' \seq \Tc) \seq \Tc'}
{
\Sc', (\Sc \seq \Tc) \seq \Tc'
}
}
\qquad
\qquad
\infer[rp_2]
{\Sc, \Sc' \seq \Tc, \Tc'}
{
\infer[gr]
{\Sc \seq (\Sc' \seq \Tc, \Tc')}
{
\Sc \seq (\Sc' \seq \Tc'), \Tc
}
}
$$
Conversely, $gl$, $gr$, $drp_2$ and $rp_2$ can be derived using $drp_1,rp_1,eg$ and $ig$:
$$
\infer[gl]
{(\Sc, \Tc \seq \Sc') \seq \Tc'}
{(\Sc \seq \Sc'), \Tc \seq \Tc'}
\qquad
\leadsto
\qquad
\infer[drp_1]
{(\Sc, \Tc \seq \Sc') \seq \Tc'}
{
 \infer[eg]
 {\Sc, \Tc \seq \Sc', \Tc'}
 {
  (\Sc \seq \Sc'), \Tc \seq \Tc'
 }
}
$$
$$
\infer[gr]
{\Sc \seq (\Sc' \seq \Tc', \Tc)}
{
 \Sc \seq (\Sc' \seq \Tc'), \Tc
}
\qquad
\leadsto
\qquad
\infer[rp_1]
{\Sc \seq (\Sc' \seq \Tc', \Tc)}
{
 \infer[ig]
 {\Sc, \Sc' \seq \Tc', \Tc}
 {
  \Sc \seq (\Sc' \seq \Tc'), \Tc
 }
}
$$
Note that $drp_2$ and $rp_2$ are just special cases of $eg$ and $ig.$
Lemma~\ref{lm:permute} then follows from the following lemma. 

\begin{lemma}
%\noindent{\bf Lemma \ref{lm:permute}.} 
The rules $drp_1,rp_1,eg$ and $ig$ permute up over all logical rules of $\biilldn.$
\end{lemma}
\begin{proof}
In the following, we omit trivial cases where the structural rule being applied does not affect
the (sub)sequent where the principal formula of the logical rule resides. 

For permutation over the propagation rules, the non-trivial cases are those where the structural rule enables
the propagation to happen. We look at some non-trivial cases here; the others are similar. In all cases,
the propagation may need to be replaced by one or more propagation rules, or may be absorbed 
by the structural rule. 
\begin{itemize}
\item $pl_1$ over $drp_1$: 
$$
\infer[drp_1]
{(\Sc, B \seq \Tc) \seq (\Uc \seq \Vc), \Tc'}
{
 \infer[pl_1]
 {\Sc, B \seq \Tc, (\Uc \seq \Vc), \Tc' }
 {
  \Sc \seq \Tc, (B, \Uc \seq \Vc), \Tc, \Tc'
 }
}
\qquad
\leadsto
\qquad
\infer[pl_2]
{(\Sc, B \seq \Tc) \seq (\Uc \seq \Vc), \Tc'}
{
 \infer[pl_1]
 {B, (\Sc \seq \Tc) \seq (\Uc \seq \Vc), \Tc'}
 {
  \infer[drp_1]
  {(\Sc \seq \Tc) \seq (B, \Uc \seq \Vc), \Tc'}
  {
    \Sc \seq \Tc,  (B, \Uc \seq \Vc), \Tc'
  }
 }
}
$$

\item $pl_1$ over $rp_1$:
$$
\infer[rp_1]
{\Sc, B \seq (\Tc \seq (\Uc \seq \Vc), \Tc')}
{
\infer[pl_1]
{\Sc, B, \Tc \seq (\Uc \seq \Vc), \Tc'}
{
 {\Sc, \Tc \seq (B, \Uc \seq \Vc), \Tc'}
}
}
\qquad
\leadsto
\qquad
\infer[pl_1]
{\Sc, B \seq (\Tc \seq (\Uc \seq \Vc), \Tc')}
{
\infer[pl_1]
{\Sc \seq (\Tc, B \seq (\Uc \seq \Vc), \Tc')}
{
\infer[rp_1]
{\Sc \seq (\Tc \seq (B, \Uc \seq \Vc), \Tc')}
{
 {\Sc, \Tc \seq (B, \Uc \seq \Vc), \Tc'}
}
}
}
$$

\item $pl_1$ over $ig$:
$$
\infer[ig]
{\Sc, B, \Sc' \seq \Tc, \Tc'}
{
\infer[pl_1]
{\Sc, B \seq (\Sc' \seq \Tc'), \Tc}
{
\Sc \seq (B, \Sc' \seq \Tc'), \Tc
}
}
\qquad
\leadsto
\qquad
\infer[ig]
{\Sc, B, \Sc' \seq \Tc, \Tc'}
{
\Sc \seq (B, \Sc' \seq \Tc'), \Tc
}
$$

\item The cases for permutation over $pr_1$ can be done similarly; 
replacing left-propagation rules ($pl_1$, $pl_2$)
with right-propagation rules ($pr_1$, $pr_2$).  

\item The cases for permutation over $pl_2$ are mostly straightforward.
The only non-trivial case is the following: 
$$
\infer[eg]
{\Sc, B, \Sc' \seq \Tc, \Tc'}
{
 \infer[pl_2]
 {(\Sc, B \seq \Tc), \Sc' \seq \Tc'}
 {
  B, (\Sc \seq \Tc), \Sc' \seq \Tc'
 } 
}
\qquad
\leadsto
\qquad
\infer[eg]
{\Sc, B, \Sc' \seq \Tc, \Tc'}
{B, (\Sc \seq \Tc), \Sc' \seq \Tc'}
$$
\item The cases for permutation over $pr_2$ can be done similarly to the cases
for $pl_2.$
\end{itemize}

Permutation over non-branching logical rules is trivial, as the sequent structure of the conclusion 
of a logical rule is preserved in the premise. 
For the branching rules, we look at the case with $\limp_l$, which is slightly non-trivial.
The rest can be proved similarly. 

In the following, we show only non-trivial interactions between the structural rules
and $\limp_l$, i.e., those in which the principal formula of $\limp_l$ is moved
by the display rule.

\begin{itemize}
\item $\limp_l$ over $drp_1$: 
\[
\infer[drp_1]
{(\Sc, C \limp B \seq \Tc) \seq \Uc}
{
\infer[\limp_l]
{\Sc, C \limp B \seq \Tc, \Uc}
{
{\Sc_1 \seq C, \Tc_1, \Uc_1}
&
{\Sc_2, B \seq \Tc_2, \Uc_2}
}
}
\qquad
\leadsto
\]
\[
\qquad
\infer[\limp_l]
{(\Sc, C \limp B \seq \Tc) \seq \Uc}
{
\infer[drp_1]
{(\Sc_1 \seq C, \Tc_1) \seq \Uc_1}
{\Sc_1 \seq C, \Tc_1, \Uc_1}
&
\infer[drp_1]
{(\Sc_2, B \seq \Tc_2) \seq \Uc_2}
{\Sc_2, B \seq \Tc_2, \Uc_2}
}
\]

\item $\limp_l$ over $rp_1$:
\[
\infer[rp_1]
{\Sc, C \limp B \seq (\Tc \seq \Uc)}
{
\infer[\limp_l]
{\Sc, C \limp B, \Tc \seq \Uc}
{
 {\Sc_1, \Tc_1 \seq C, \Uc_1}
&
 {\Sc_2, B \seq \Tc_2, \Uc_2}
}
}
\qquad
\leadsto
\]
\[
\qquad
\infer[pl_1]
{\Sc, C \limp B \seq (\Tc \seq \Uc)}
{
 \infer[\limp_l]
 {\Sc \seq (C \limp B, \Tc \seq \Uc)}
 {
  \infer[rp_1] 
  {\Sc_1 \seq (\Tc_1 \seq C, \Uc_1)}
  {\Sc_1, \Tc_1 \seq C, \Uc_1}
  &
  \infer[rp_1]
  {\Sc_2 \seq (\Tc_2, B \seq \Uc_2)}
  {\Sc_2, \Tc_2, B \seq \Uc_2}
 }
}
\]
Notice that we need to use the propagation rule $pl_1$ to push $rp_1$ over $\limp_l$.
The only other case where a propagation rule is used is when permuting 
$drp_1$ over $\excl_r$; in this case the propagation rule needed is $pr_1$. 

\item $\limp_l$ over $eg$:
$$
\infer[eg]
{\Sc, C \limp B, \Sc' \seq \Tc, \Tc'}
{
 \infer[\limp_l]
 {(\Sc, C \limp B \seq \Tc), \Sc' \seq \Tc'}
 {
  {(\Sc_1 \seq C, \Tc_1), \Sc_1' \seq \Tc_1'}
  &
  {(\Sc_2, B \seq \Tc_2) \seq \Tc_2'}
 }
}
$$
$$
\leadsto
\qquad
\infer[\limp_l]
{\Sc, C \limp B, \Sc' \seq \Tc, \Tc'}
{
 \infer[eg]
 {\Sc_1, \Sc_1' \seq C, \Tc_1, \Tc_1'}
 {(\Sc_1 \seq C, \Tc_1), \Sc_1' \seq \Tc_1'}
 &
 \infer[eg]
 {\Sc_2, \Sc_2', B \seq \Tc_2, \Tc_2'}
 {(\Sc_2, B \seq \Tc_2), \Sc_2' \seq \Tc_2'}
}
$$

\item $\limp_l$ over $ig$:
$$
\infer[ig]
{\Sc, \Sc', C \limp B \seq \Tc, \Tc'}
{
 \infer[\limp_l]
 {\Sc \seq (\Sc', C \limp B \seq \Tc'), \Tc}
 {
  {\Sc_1 \seq (\Sc_1' \seq C, \Tc_1'), \Tc_1}
  &
  {\Sc_2 \seq (\Sc_2', B \seq \Tc_2'), \Tc_2}
 }
}
$$
$$
\leadsto
\qquad
\infer[\limp_l]
{\Sc, \Sc', C \limp B \seq \Tc,\Tc'}
{
 \infer[ig]
 {\Sc_1, \Sc_1' \seq C, \Tc_1, \Tc_1'} 
 {\Sc_1 \seq (\Sc_1' \seq C, \Tc_1'), \Tc_1}
 &
 \infer[ig]
 {\Sc_2, \Sc_2', B \seq \Tc_2, \Tc_2'}
 {\Sc_2 \seq (\Sc_2', B \seq \Tc_2'), \Tc_2'}
}
$$
\end{itemize}
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Proof that BiILL and FILL  are NP-complete}
\label{apx:np}

\begin{lemma}
The tautology problem for BiLLL is in NP
\end{lemma}
\begin{proof}
We shall utilise the deep inference system $\biilldn$ to prove this. 
To show membership in NP, it is sufficient to show that every proof of a formula $B$ in $\biilldn$
can be checked in polynomial time. 
So suppose we are given a proof $\Pi$ of a formula $B$ in $\biilldn$.
We first establish show that the size of $\Pi$ is bounded polynomially by $|B|$, and show
that checking validity of each inference step of $\Pi$ is decidable in PTIME in the size of $|B|.$


We assume a representation of formulas as ordered trees, with nodes
labelled with connectives and propositional variables. 
A nested sequent is represented
as an unordered tree of ordered pairs of lists of formulae. 
The edges are labelled with polarity information ($+$ or $-$)
to indicate whether a child node of a parent node is nested to the left or the right of the sequent
represented by the parent node. 
We further assume that each occurrence of $\limp$ and $\excl$ in $B$ is labelled with a unique
identifier. Such a labelling only introduces at most a polynomial overhead of 
the size of $B$, so is inconsequential
as far as proving the upper bound in NP is concerned. Since each sequent arrow is created (reading the rules
upwards) by decomposing exactly one occurrence of $\limp$ or $\excl$, we can assume w.l.o.g. that
each node in a nested sequent is similarly uniquely labelled. Given this, it is easy to see 
that checking whether two trees of ordered pairs of lists 
represent the same nested sequent can be done in PTIME in the size of the trees. An inspection
on the rules of $\biilldn$ shows that the size of each nested sequent in $\Pi$ is bounded
by $|B|$, since each introduction rule replaces one formula connective with
zero or one structural connective. So checking equality between two nested sequents (or contexts) in $\Pi$ 
can be done in PTIME in the size of $B.$ 
We need to further show that, in the branching rules in $\Pi$, that merging of contexts and
sequents happen only along the same labelled nodes. 
So, checking whether the merging relation holds 
between three sequents (or contexts) in a branching rule in $\Pi$
can also be decided in PTIME in the size of $B.$

Notice that every occurrence of 
a  propositional variable or a constant in $B$ appears exactly once in either an $id^d$ rule or a 
constant rule, so the number of leaves in $\Pi$ is bounded by $|B|.$
That means that the number of branches in $\Pi$ is bounded by  $|B|.$ 
In every branch in $\Pi$, the number of logical rules is bounded by $|B|$, because each
connective is introduced exactly once in $\Pi.$
Now we need also to account for the number of propagation rules. Notice that the propagation rules
are non-invertible, and each formula occurrence can be propagated at most $k$ times, where $k$ is
the number of $\limp$ and $\excl$ occurring in $B$. The number of formula occurrences in
a nested sequent in $\Pi$ is bounded by $|B|$, so there can be at most $k \times |B|$ propagation
rules that can be successively applied to a nested sequent. 
The length of each branch in $\Pi$ is bounded by $|B| + (|B|/2) \times k \times |B|$, i.e.,
the number of logical rules, plus the number of propagation rules in between every pair
of logical rules. So the length of each branch is bounded by $O(|B|^3).$
That means that number of nodes in $\Pi$ is bounded by  $O(|B|^4)$. 
Now the size of each sequent in the node is obviously bounded by $B$, so
the total size of $\Pi$ is bounded by $O(|B|^5)$. It remains to show that
checking whether each inference in $\Pi$ is valid is decidable in PTIME in the size of $B$. 
The slightly non-trivial
bit is to decide whether the splitting of the contexts in branching rules are valid, e.g.,
whether $X[~] \in X_1[~] \merge X_2[~]$, etc. As discussed above, this can be done in PTIME as well
given our unique labelling assumption. 
\end{proof}

\begin{lemma}
The tautology problem for $\filldn$ is NP-hard. 
\end{lemma}
\begin{proof}
  We show how to encode constants-only multiplicative
  linear logic (COMLL), which is MLL without any propositional
  variables and is known to be NP-complete~\cite{Lincoln94}. Since
  COMLL has no propositional variables, every COMLL formula in nnf
  has no negation (or implication) in it. So it is
  enough to show that every COMLL formula in nnf is valid iff it is
  provable in $\filldn$. The restriction of $\filldn$ to the COMLL
  connectives gives us exactly COMLL, since without implication
  (negation), the proof system degenerates into the usual classical
  sequent calculus for COMLL. 
\end{proof}

\section{Conservativity via Schellinx's sequent calculus}
\label{apx:conserv-schellinx}

We give here an alternative proof that $\biill$ is conservative over FILL via
the sequent calculus for FILL that was proposed by Schellinx~\cite{Schellinx:Some}.
The rules of this calculus are those for MLL, except 
that the $\limp$-right rule is replaced with: 
$$
\infer[]
{\Gamma \vdash C \limp B}
{\Gamma, C \vdash B}
$$
We show that every derivation of a formula in $\filldn$ can be translated to a derivation
of the same formula in Schellinx's calculus, possibly using cuts.

We shall assume that formulas are equivalent modulo associativity and commutativity
of $\ltens$ and $\parr$. This is not necessary but it helps to simplify the proof. 
Formally this just means that there are implicit cuts in the following constructions that
we omit, i.e., those needed to allow replacement of a formula with its equivalent one. 
Given this convention, we shall omit parentheses when writing a tensor (par) of multiple
formulas, e.g., $(B_1 \ltens B_2 \ltens B_3).$
Given $\Gamma = \{B_1,\dots,B_n\}$, 
we shall write $\ltens(\Gamma)$ to denote  the formula
$(B_1 \ltens \cdots \ltens B_n)$, and similarly, $\parr(\Gamma)$
denotes $(B_1 \parr \cdots \parr B_n).$ 

In the following proofs, we shall be working with formula interpretations of nested
sequents, using the translation functions $\tau^a$ and $\tau^s$ defined
in Definition~\ref{def:tau_nested}.
%% The translation functions $\tau^s$ and $\tau^a$ that apply to structures
%% are adapted to nested sequents in the obvious way, by treating their images 
%% as equivalence classes of formulas (modulo associativity, commutativity and unit laws
%% for $\ltens$ and $\parr$). 
%% Formally, they are defined as follows:
%% $$
%% \begin{array}{l}
%% \tau^s(B_1,\dots,B_k, X_1,\dots,X_l \seq C_1,\dots,C_m, Y_1,\dots,Y_n) \\
%% = 
%% (B_1 \ltens \cdots \ltens B_k \ltens \tau^a(X_1) \ltens \cdots \ltens \tau^a(X_l)) 
%% \limp
%% (C_1 \parr \cdots \parr C_m \parr \tau^s(Y_1) \parr \cdots \parr \tau^s(Y_n)).
%% \end{array}
%% $$
%% $$
%% \begin{array}{l}
%% \tau^a(B_1,\dots,B_k, X_1,\dots,X_l \seq C_1,\dots,C_m, Y_1,\dots,Y_n) \\
%% = 
%% (B_1 \ltens \cdots \ltens B_k \ltens \tau^a(X_1) \ltens \cdots \ltens \tau^a(X_l)) 
%% \excl
%% (C_1 \parr \cdots \parr C_m \parr \tau^s(Y_1) \parr \cdots \parr \tau^s(Y_n)).
%% \end{array}
%% $$
%% Notice that $\tau^s$ and $\tau^a$ differ in the interpretation of the top most 
%% sequent symbol: in the former it is interpreted as linear implication, while in the latter
%% it is exclusion. 
%% The recursive parts, i.e., the interpretaion of $X_1,\dots,X_l$ and $Y_1,\dots,Y_n$, are
%% are translated in the same way in both cases. 
%% Essentially, whenever a sequent occurs immediately to the left of a sequent symbol, it 
%% is interpreted negatively (i.e., its topmost sequent symbol is interpreted as exclusion); and dually
%% when it occurs on the right. 
%% When $n = 0$, $B_1\ltens \cdots \ltens B_n$ is interpreted as $\tunit$ (the unit of tensor);
%% similarly $B_1 \parr \cdots \parr B_n$ is interpreted as $0.$
Strictly speaking, the empty sequent $\sunit \seq \sunit$ would be interpreted (positively) as 
$\tunit \ltens \tunit \limp 0 \parr 0$, because of the way we separate formulas from sequents in the
definition of $\tau$. But when using the translation function $\tau$, 
we shall treat $\tunit \ltens \cdots \ltens \tunit$ as simply $\tunit$, to simplify
presentation. This is harmless as they are logically equivalent (alternatively we could write
a more complicated translation function just to take care of this minor syntactic bureaucracy). 

\begin{lemma}
\label{lm:conserv-merge}
Let $X$ and $Y$ be FILL sequents. If $Z \in X \merge Y$, then
the formula
$$
\tau^s(X) \parr \tau^s(Y) \limp \tau^s(Z)
$$
is provable in FILL.
\end{lemma}
\begin{proof}
By induction on the structure of $Z.$
So suppose $Z$ is 
$$
(\Gamma, \Delta \seq \Gamma', \Delta', Z_1, \dots, Z_n)
$$
and $X$ and $Y$ are, respectively,  
$$
(\Gamma \seq \Gamma', X_1, \dots, X_n) \qquad (\Delta \seq \Delta', Y_1, \dots, Y_n)
$$
where $Z_i \in X_i \merge Y_i$, for every $i \in \{1,\dots,n\}.$
By the induction hypothesis, we have for each $i$: $\tau^s(X_i) \parr \tau^s(Y_i) \limp \tau^s(Z_i).$
To prove $\tau^s(X) \parr \tau^s(Y) \limp \tau^s(Z)$ it is enough to show that the following
sequent is derivable in FILL:
$$
\begin{array}{l}
\ltens(\Gamma) \limp \parr(\Gamma',\tau^s(X_1),\dots,\tau^s(X_n)), 
\ltens(\Delta) \limp \parr(\Delta',\tau^s(Y_1),\dots,\tau^s(Y_n)),  
\Gamma, \Delta  \\
\vdash
\Gamma', \Delta', \tau^s(Z_1), \dots, \tau^s(Z_n).
\end{array}
$$
This is easily provable, using cut formulas $\tau^s(X_i) \parr \tau^s(Y_i) \limp \tau^s(Z_i).$
\end{proof}

\begin{lemma}
\label{lm:conserv-hollow}
For every hollow FILL sequent $X$, the formula $\punit \limp \tau^s(X)$ 
is provable in FILL.
\end{lemma}

\begin{lemma}
\label{lm:conserv-id}
Let $X[~]$ be a hollow positive FILL context, let $\Sc$ be a multiset
of hollow FILL sequents. Then each of the following formulas
is provable in FILL: 
$$
\tau^s(X[A \seq \Sc, A])
\qquad
\tau^s(X[\punit \seq \sunit])
\qquad
\tau^s(X[\sunit \seq \tunit])
$$
\end{lemma}
\begin{proof}
By induction on $X[~]$, and utilising Lemma~\ref{lm:conserv-hollow}. 
\end{proof}

\begin{lemma}
\label{lm:conserv-non-branching}
Suppose $F \limp G$ is provable in FILL. 
Then for every positive FILL context $X[~]$,
the formula $\tau^s(X[F]) \limp \tau^s(X[G])$ is provable in FILL.
\end{lemma}

\begin{lemma}
\label{lm:conserv-branching}
Suppose $F \ltens G \limp H$ is provable in FILL.
Then for every positive FILL context $X_1[~], X_2[~], X[~]$ such
that $X[~] \in X_1[~] \merge X_2[~]$, we have that
$$
\tau^s(X_1[F]) \ltens \tau^s(X_2[G]) \limp \tau^s(X[H])
$$
is also provable in FILL.
\end{lemma}
\begin{proof}
By induction on the structure of $X[~].$
Suppose $X[~]$
is
$$
\Gamma, \Delta \seq \Sc, X'[~]
$$
and $X_1[~]$ and $X_2[~]$ are, respectively, 
$$
(\Gamma \seq \Sc_1, X_1'[~])
\qquad
(\Delta \seq \Sc_2, X_2'[~])
$$
where $X'[~] \in X_1'[~] \merge X_2'[~]$ and
$\Sc \in \Sc_1 \merge \Sc_2.$
By the induction hypothesis, we have 
$$
\tau^s(X_1'[F]) \ltens \tau^s(X_2'[G]) \limp \tau^s(X'[H]).
$$
To prove $\tau^s(X_1[F]) \ltens \tau^s(X_2[G]) \limp \tau^s(X[H])$ it is enough
to prove the following sequent:
\begin{equation}
\label{eq:seq1}
\begin{array}{l}
\ltens(\Gamma) \limp \parr(\tau^s(\Sc_1), \tau^s(X_1'[F])), 
\ltens(\Delta) \limp \parr(\tau^s(\Sc_2), \tau^s(X_2'[G])), 
\Gamma, \Delta \\
\vdash 
\tau^s(\Sc), \tau^s(X'[H])
\end{array}
\end{equation}
By Lemma~\ref{lm:conserv-merge}, we can show that
$\tau^s(\Sc_1) \parr \tau^s(\Sc_2) \limp \tau^s(\Sc).$ Therefore, to prove 
sequent (\ref{eq:seq1}) it is enough to prove the following sequent:
$$
\begin{array}{l}
\ltens(\Gamma) \limp \parr(\tau^s(\Sc_1), \tau^s(X_1'[F])), 
\ltens(\Delta) \limp \parr(\tau^s(\Sc_2), \tau^s(X_2'[G])), 
\Gamma, \Delta \\
\vdash 
\tau^s(\Sc_1), \tau^s(\Sc_2), \tau^s(X'[H])
\end{array}
$$
which is provable by straightforward applications of logical rules
and the cut rule with the cut formula 
$\tau^s(X_1'[F]) \ltens \tau^s(X_2'[G]) \limp \tau^s(X'[H])$
(which is provable by the induction hypothesis). 
\end{proof}

Now we are ready to prove the statement of Theorem~\ref{thm:filldn-conserv}: 
For every FILL formula $B$, $B$ is provable in FILL if and only if
it is provable in $\filldn.$
\begin{proof}
One direction, from FILL to $\filldn$, follows from the fact that any FILL derivation
is also a derivation in $\biillsn$, and Theorem~\ref{thm:separation}.
For the reverse direction, we show that every derivation of $X$ in $\filldn$ corresponds to 
a derivation of $\vdash \tau^s(X)$ in FILL; hence every valid formula in $\filldn$ is also
valid in FILL. We do this by induction on the height of derivations in $\filldn.$
The base cases where the derivation ends with $id^d$, $\punit^d_l$ or $\tunit^d_r$ follow
from Lemma~\ref{lm:conserv-id}. 
For the inductive cases, we first show that every rule in $\biilldn$ corresponds to
a valid sequent in FILL. 
For a non-branching rule, with premise $U$ and conclusion $V$, the corresponding
implication is $\tau^s(U) \vdash \tau^s(V)$. For a branching rule, with premises
$U$ and $V$, and conclusion $W$, the corresponding implication is 
$\tau^s(U), \tau^s(V) \vdash \tau^s(W).$
Thus given a derivation of $X$ ending with a branching rule:
$$
\infer[\rho]
{X}
{\deduce{X_1}{\vdots} & \deduce{X_2}{\vdots}}
$$
the translation takes the form:
$$
\infer[cut]
{\vdash \tau^s(X)}
{
\deduce
{\vdash \tau^s(X_1)}
{(1)}
&
\infer[cut]
{\tau^s(X_1) \vdash \tau^s(x)}
{
 \deduce{\vdash \tau^s(X_2)}{(2)}
 &
 \deduce{\tau^s(X_1), \tau^s(X_2) \vdash \tau^s(X)}{(3)}
}
}
$$
Sequents (1) and (2) are provable by the induction hypothesis, so it is enough
to show we can always prove sequent (3). We show here a case where the derivation
in $\filldn$ ends with $\limp_l$; the other cases are similar. 
So suppose the derivation in $\filldn$ ends with: 
$$
\infer[\limp_l^d]
{X[\Gamma, \Delta, A \limp B \seq \Tc]}
{
X_1[\Gamma \seq A, \Tc_1] & X_2[\Delta, B \seq \Tc_2]
}
$$
where $\Tc, \Tc_1$ and $\Tc_2$ are multisets of intuitionist formulas/sequents,
$X[~] \in X_1[~] \merge X_2[~]$, and $\Tc \in \Tc_1 \merge \Tc_2.$
By Lemma~\ref{lm:conserv-branching}, 
it is enough to show that the following formula is valid in FILL:
$$
(\ltens(\Gamma) \limp A \parr \tau^s(\Tc_1))
\ltens
(\ltens(\Delta) \ltens B \limp \tau^s(\Tc_2))
\limp
(\ltens(\Gamma, \Delta, A \limp B) \limp \tau^s(\Tc)).
$$
This in turn reduces to proving the sequent:
$$
\ltens(\Gamma) \limp A \parr \tau^s(\Tc_1), 
\ltens(\Delta) \ltens B \limp \tau^s(\Tc_2),
\Gamma, \Delta, A \limp B 
\vdash
\tau^s(\Tc).
$$
This sequent can be proved (in a bottom-up fashion) by 
a cut with the provable formula (by Lemma~\ref{lm:conserv-merge})
$\tau^s(\Tc_1) \parr \tau^s(\Tc_2) \limp \tau^s(\Tc)$, followed
by straightforward applications of introduction rules.
$$
\infer[\mbox{Lem. \ref{lm:conserv-merge}}]
{\ltens(\Gamma) \limp A \parr \tau^s(\Tc_1), 
\ltens(\Delta) \ltens B \limp \tau^s(\Tc_2),
\Gamma, \Delta, A \limp B 
\vdash
\tau^s(\Tc)}
{
\infer[\limp_l]
{
\ltens(\Gamma) \limp A \parr \tau^s(\Tc_1), 
\ltens(\Delta) \ltens B \limp \tau^s(\Tc_2),
\Gamma, \Delta, A \limp B 
\vdash
\tau^s(\Tc_1), \tau^s(\Tc_2)
}
{
\deduce{\ltens(\Gamma) \limp A \parr \tau^s(\Tc_1), 
\Gamma \vdash  A, \tau^s(\Tc_1)}{(4)}
&
\deduce{
\ltens(\Delta) \ltens B \limp \tau^s(\Tc_2),
\Delta, B 
\vdash
\tau^s(\Tc_2)
}{(5)}
}
}
$$
The derivations for sequents (4) and (5) are easy and omitted here. 
\end{proof}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 

