Index: CSL17/tech-report/appendix-completeness.tex
===================================================================
--- CSL17/tech-report/appendix-completeness.tex	(revision 252)
+++ CSL17/tech-report/appendix-completeness.tex	(revision 253)
@@ -38,7 +38,7 @@
 	%\begin{proof}
 	%\end{proof}
 	\begin{proof}
-	This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i+1}$ (see \cite{Buss86book}, Thm 20, p. 58).
+	This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i}$ (see \cite{Buss86book}, Thm 20, p. 58).
 	
 	Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:
 	$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$
@@ -60,15 +60,14 @@
 Moreover we have: $A(a) \cand B(a,b,c) \cimp c\leq a$.
 From these three statements we deduce:
 $$(A(a) \cand a \neq 0 \cand b<|a| \cand \exists x^{\safe} \leq a. B(a,b,x)) \cimp \exists x^{\safe } \leq a.B(a,\succ{} b,x).$$
+Note that here we have used the fact that we are in classical logic.
+
 The formula $\exists x\leq a. B(a,b,c)$ is in $\Sigma^{\safe}_{i}$, so by $\Sigma^{\safe}_{i}$-LIND on the formula $\exists x\leq a. B(a,b,c)$, with the variable $b$ which is in $\normal$,  we obtain:
 $$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$
-\patrick{Anupam, is it a valid instance of LIND? I think it is.}
-
 But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:
 $$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$
 which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.
 	\end{proof}
-%	\patrick{Examining it superficially, I think indeed the proof of Buss can be adapted to our setting. But we should probably look again at that with more scrutiny.}
 	
 	Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:
 	\[
Index: CSL17/tech-report/intro.tex
===================================================================
--- CSL17/tech-report/intro.tex	(revision 252)
+++ CSL17/tech-report/intro.tex	(revision 253)
@@ -7,7 +7,7 @@
 
 To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.
 But a perhaps more important distinction is whether the constraints on the logic or theory are
-\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantifiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra  \cite{Cobham}  for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one there are various systems of \textit{implicit computational complexity}, for instance function algebras based on \emph{ramification} or \emph{safe recursion} \cite{BellantoniCook92,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \cite{Leivant94:found-delin-ptime} and subsystems of \emph{linear logic} \cite{Girard94:lll} \cite{Lafont04} .
+\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantifiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra  \cite{Cobham}  for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category there are various systems of \textit{implicit computational complexity}, for instance function algebras based on \emph{ramification} or \emph{safe recursion} \cite{BellantoniCook92,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \cite{Leivant94:found-delin-ptime} and subsystems of \emph{linear logic} \cite{Girard94:lll} \cite{Lafont04} .
 
  Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc. 
  %It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}. 
Index: CSL17/tech-report/preliminaries.tex
===================================================================
--- CSL17/tech-report/preliminaries.tex	(revision 252)
+++ CSL17/tech-report/preliminaries.tex	(revision 253)
@@ -142,6 +142,7 @@
 
 %\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }
 
+We denote $|x|=\ulcorner \log(x+1) \urcorner.$
 \begin{example}
 	[Some simple functions]
 	\label{ex:simple-bc-fns}
@@ -153,7 +154,7 @@
 	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.
 	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1101)=0$.
 	
-	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|+1$ prefix of $x$, as follows:
+	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:
 	\begin{eqnarray*}
 	\shorten(0;x) &=&x\\
 	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))
Index: CSL17/preliminaries.tex
===================================================================
--- CSL17/preliminaries.tex	(revision 252)
+++ CSL17/preliminaries.tex	(revision 253)
@@ -157,7 +157,7 @@
 	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:
 	\begin{eqnarray*}
 	\shorten(0;x) &=&x\\
-	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x)) \mbox{ if $l\neq 0$.}
+	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x)) 
 	\end{eqnarray*}
 	Then we define $\bit(l;x)$  as follows:
 	$$\bit(l;x)=C(;\shorten(l;x),0,1).$$ 
