Index: arithmetic.tex
===================================================================
--- arithmetic.tex	(revision 227)
+++ arithmetic.tex	(revision 228)
@@ -165,6 +165,7 @@
 \begin{figure}
 	\[
 	\small
+	\hspace{-1.5em}
 	\begin{array}{l}
 	\begin{array}{cccc}
 	%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}
@@ -172,12 +173,37 @@
 	%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}
 	%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
 	\vlinf{id}{}{\Gamma, p \seqar p, \Delta }{}
-	& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}
-	&&
+	& \vliinf{cut}{}{\Gamma, \Sigma \seqar \Delta, \Pi }{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
+	&	\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}
+	&
+	
+	\vlinf{\rigrul{\neg}}{}{\Gamma, \seqar \neg A, \Delta}{\Gamma, A \seqar  \Delta}
+		\\
+		
+		\noalign{\bigskip}
+		%\text{Structural:} & & & \\
+		%\noalign{\bigskip}
+		
+		\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
+		&
+		\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}
+		&
+		\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
+		&
+		\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
+		\\
+		\noalign{\bigskip}
+		\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}
+		&
+		\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}
+		&
+		\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}
+		&
+		\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) }
 	\\
 	\noalign{\bigskip}
 	%\noalign{\bigskip}
-	\vliinf{\lefrul{\cor}}{}{\Gamma, A \cor B \seqar \Delta}{\Gamma , A \seqar \Delta}{\Gamma, B \seqar \Delta}
+	\vliinf{\lefrul{\cor}}{}{\Gamma, \Sigma, A \cor B \seqar \Delta, \Pi}{\Gamma , A \seqar \Delta}{\Sigma, B \seqar \Pi}
 	&
 	\vlinf{\lefrul{\cand}}{}{\Gamma, A\cand B \seqar \Delta}{\Gamma, A , B \seqar \Delta}
 	&
@@ -187,47 +213,8 @@
 	&
 	%\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A\laor B}{\Gamma \seqar \Delta, B}
 	%\quad
-	\vliinf{\rigrul{\cand}}{}{\Gamma \seqar \Delta, A \cand B }{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, B}
-	\\
-	\noalign{\bigskip}
-	
-	\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}
-	&
-	
-	\vlinf{\lefrul{\neg}}{}{\Gamma, \seqar \neg A, \Delta}{\Gamma, A \seqar  \Delta}
-	&
-	&
-	%\vliinf{\lefrul{\cimp}}{}{\Gamma, A \cimp B \seqar \Delta}{\Gamma \seqar A, \Delta}{\Gamma, B \seqar \Delta}
-	%&
-	%
-	%\vlinf{\rigrul{\cimp}}{}{\Gamma \seqar \Delta, A \cimp B}{\Gamma, A \seqar \Delta,  B}
-	
-	
-	\\
-	
-	\noalign{\bigskip}
-	%\text{Structural:} & & & \\
+	\vliinf{\rigrul{\cand}}{}{\Gamma, \Sigma \seqar \Delta, \Pi, A \cand B }{\Gamma \seqar \Delta, A}{\Sigma \seqar \Pi, B}
 	%\noalign{\bigskip}
-	
-	%\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
-	%&
-	\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}
-	%&
-	%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
-	&
-	\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
-	&
-	&
-	\\
-	\noalign{\bigskip}
-	\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}
-	&
-	\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}
-	&
-	\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}
-	&
-	\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) } \\
-	%\noalign{\bigskip}
 	% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&
 	\end{array}
 	\end{array}
@@ -344,4 +331,9 @@
 \end{theorem}
 
 Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$. The latter is a consequence of the former already in $\basic$.
-The proof of this result also relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible typing on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.
\ No newline at end of file
+The proof of this result also relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.
+
+As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae immediately below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
+
+Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, e.g.\
+\todo{}
\ No newline at end of file
