Index: CSL17/completeness.tex
===================================================================
--- CSL17/completeness.tex	(revision 173)
+++ CSL17/completeness.tex	(revision 174)
@@ -40,6 +40,7 @@
 [Minimisation]
 $\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	
 \end{lemma}
+% see Thm 20 p. 58 in Buss' book.
 \begin{proof}
 \todo{}
 \end{proof}
@@ -89,7 +90,7 @@
 & 
 %Seq(z) \cand 
 \exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
-\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_i) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
+\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
 \end{array}
 \right)
 \]
Index: CSL17/main.tex
===================================================================
--- CSL17/main.tex	(revision 173)
+++ CSL17/main.tex	(revision 174)
@@ -12,6 +12,7 @@
 
 \bibliographystyle{plainurl}% the recommended bibstyle
 
+\usepackage[lutzsyntax]{virginialake}
 \input{ph-macros}
 
 % Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Index: CSL17/arithmetic.tex
===================================================================
--- CSL17/arithmetic.tex	(revision 173)
+++ CSL17/arithmetic.tex	(revision 174)
@@ -86,5 +86,113 @@
 \subsection{A sequent calculus presentation}
 \todo{Write out usual first-order sequent calculus}
 
+\begin{figure}
+\[
+\small
+\begin{array}{l}
+\begin{array}{cccc}
+%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}
+%& \vlinf{\id}{}{p \seqar p}{}
+%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}
+%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
+ \vlinf{id}{}{p \seqar p}{}
+& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}
+&&
+\\
+\noalign{\bigskip}
+%\noalign{\bigskip}
+\vliinf{\lefrul{\cor}}{}{\Gamma, A \cor B \seqar \Delta}{\Gamma , A \seqar \Delta}{\Gamma, B \seqar \Delta}
+&
+\vlinf{\lefrul{\cand}}{}{\Gamma, A\cand B \seqar \Delta}{\Gamma, A , B \seqar \Delta}
+&
+%\vlinf{\lefrul{\laand}}{}{\Gamma, A\laand B \seqar \Delta}{\Gamma, B \seqar \Delta}
+%\quad
+\vlinf{\rigrul{\cor}}{}{\Gamma \seqar \Delta, A \cor B}{\Gamma \seqar \Delta, A, B}
+&
+%\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}
+\vliinf{\lefrul{\cimp}}{}{\Gamma, A \cimp B \seqar \Delta}{\Gamma \seqar A, \Delta}{\Gamma, B \seqar \Delta}
+&
+\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}
+&
+
+\vlinf{\rigrul{\cimp}}{}{\Gamma \seqar \Delta, A \cimp B}{\Gamma, A \seqar \Delta,  B}
+&
+
+\vlinf{\lefrul{\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}
+% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&
+\end{array}
+\end{array}
+\]
+\caption{Sequent calculus rules}\label{fig:sequentcalculus}
+\end{figure}
+ We denote sequence as $\Gamma \seqar \Delta$ where $\Gamma$, $\Delta$ are multi sets of formulas. The sequent calculus rules are displayed on Fig. \ref{fig:sequentcalculus},  where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.
+
+We consider \emph{systems} of `nonlogical' rules extending this sequent calculus, which we write as follows,
+ \[
+ \begin{array}{cc}
+    \vlinf{(R)}{}{ \Gamma , \Sigma' \seqar \Delta' , \Pi  }{ \{\Gamma , \Sigma_i \seqar \Delta_i , \Pi \}_{i \in I} }
+\end{array}
+\]
+ where, in each rule $(R)$, $I$ is a finite possibly empty set (indicating the number of premises) and we assume the following conditions and terminology:
+ \begin{enumerate}
+ \item In $(R)$ the formulas of $\Sigma', \Delta'$  are called \textit{principal}, those of $\Sigma_i, \Delta_i$ are called \textit{active}, and those of   
+$ \Gamma,  \Pi$ are called \textit{context formulas}. 
+\item Each rule $(R)$ comes with a list $a_1$, \dots, $a_k$ of eigenvariables such that each $a_j$ appears in exactly one $\Sigma_i, \Delta_i$ (so in some active formulas of exactly one premise)  and does not appear in  $\Sigma', \Delta'$ or $ \Gamma,  \Pi$.
+    \item A system $\mathcal{S}$ of rules must be closed under substitutions of free variables by terms (where these substitutions do not contain the eigenvariables $a_j$ in their domain or codomain).  
+   \end{enumerate}
+ 
+%The distinction between modal and nonmodal formulae in $(R)$ induces condition 1
+ Conditions 2 and 3 are standard requirements for nonlogical rules, independently of the logical setting, cf.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that, in our nonlogical rules, we often need a notion of \textit{bound} variables in the active formulas (typically for induction rules), for which we rely on eigenvariables. Condition 3 is needed for our proof system to admit elimination of cuts on quantified formulas.
+
+
 \subsection{Free-cut free normal form of proofs}
-\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
\ No newline at end of file
+\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
+Since our nonlogical rules may have many principal formulae on which cuts may be anchored, we need a slightly more general notion of principality.
+    \begin{definition}\label{def:anchoredcut}
+  We define the notions of \textit{hereditarily principal formula} and \textit{anchored cut} in a $\system$-proof, for a system $\system$, by mutual induction as follows:
+  \begin{itemize}
+  \item A formula $A$ in a sequent $\Gamma \seqar \Delta$ is \textit{hereditarily principal} for a rule instance (S) if either (i) the sequent is in the conclusion of (S) and $A$ is principal in it, or 
+(ii)  the sequent is in the conclusion of an anchored cut, the direct ancestor of $A$ in the corresponding premise is hereditarily principal for the rule instance (S), and the rule (S) is nonlogical.
+  \item A cut-step is an \textit{anchored cut} if the two occurrences of its cut-formula $A$ in each premise are hereditarily principal for nonlogical steps, or one is hereditarily principal for a nonlogical step and the other one is principal for a logical step.
+  \end{itemize}
+     A cut which is not anchored will also be called a \textit{free-cut}.
+  \end{definition}
+  As a consequence of this definition, an anchored cut on a formula $A$ has the following properties:
+  \begin{itemize}
+  \item At least one of the two premises of the cut has above it a sub-branch of the proof which starts (top-down) with a nonlogical step (R) with $A$ as one of its principal formulas, and then a sequence of anchored cuts in which $A$ is part of the context.
+  \item The other premise is either of the same form or is a logical step with principal formula $A$. 
+  \end{itemize}
+   
+   Now we have (see \cite{Takeuti87}): 
+   \begin{theorem}
+   [Free-cut elimination]
+   \label{thm:free-cut-elim}
+    Given a system  $\mathcal{S}$, any  $\mathcal{S}$-proof $\pi$ can be transformed into a $\system$-proof $\pi'$ with same end sequent and without any free-cut.
+   \end{theorem}
\ No newline at end of file
Index: CSL17/ph-macros.tex
===================================================================
--- CSL17/ph-macros.tex	(revision 173)
+++ CSL17/ph-macros.tex	(revision 174)
@@ -78,4 +78,17 @@
 \newcommand{\ciff}{\equiv}
 
 \newcommand{\size}[1]{|#1|}                        %% length of a word
-\newcommand{\mode}{\; \underline{\mbox{mod}}\;}   %% mod 2^{|x|}
\ No newline at end of file
+\newcommand{\mode}{\; \underline{\mbox{mod}}\;}   %% mod 2^{|x|}
+
+%%%%% RULES %%%%%%
+\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}
+	\newcommand{\rigrul}[1]{#1\text{-}\mathit{r}}
+	\newcommand{\id}{\it{id}}
+	\newcommand{\cut}{\it{cut}}
+	\newcommand{\wk}{\mathit{wk}}
+	\newcommand{\cntr}{\mathit{cntr}}
+	
+% theories
+	\newcommand{\theory}{\mathcal T}
+	\newcommand{\system}{\mathcal S}
+	
