\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 
%display calculi enjoy cut-elimination (Thm. \ref{thm:cutad}):
display calculi enjoy cut-admissibility (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}



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

