\appendix

\begin{center} \large APPENDIX \end{center}


\input{appendix-preliminaries}
\input{appendix-free-cut-elim}
\input{appendix-arithmetic}
\input{appendix-bc}
\input{appendix-bc-convergence}
\input{appendix-wfm}



%
%\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}
%
