Index: CSL17/intro.tex
===================================================================
--- CSL17/intro.tex	(revision 225)
+++ CSL17/intro.tex	(revision 226)
@@ -6,14 +6,14 @@
 Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.
 
 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.
-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 quantiiers 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 can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Leivant94:found-delin-ptime} and subsystems of linear logic   \cite{Girard94:lll} \cite{Lafont04} .
+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 quantiiers 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 can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or 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 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}. 
   
-  Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It aims to relate certain computing disciplines which with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 
-  Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (\cite{Hofmann00,Hofmann03}, \cite{Marion11} etc.).  However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra or of a type system extended with a non-logical feature.} 
+  Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It aims to relate certain computing disciplines with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 
+  Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (e.g. \cite{Hofmann00,Hofmann03}, \cite{Marion11}).  However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra \cite{bellantoni1995fph} or of a type system extended with a non-logical feature \cite{GaboardiMarionRonchi12}.} 
   
  Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}). 
 % But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes.
Index: CSL17/preliminaries.tex
===================================================================
--- CSL17/preliminaries.tex	(revision 225)
+++ CSL17/preliminaries.tex	(revision 226)
@@ -1,7 +1,7 @@
 
 \section{Preliminaries}
 \label{sect:prelims}
-We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimization \cite{bellantoni1995fph}.
+We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimisation \cite{bellantoni1995fph}.
 
 %\anupam{Should recall polymax bounded functions and the polychecking lemma, e.g.\ from Bellantoni's FPH paper or thesis. Quite important, even if proof not given.}
 
@@ -151,12 +151,12 @@
 	\begin{itemize}
 	\item The boolean predicates $\notfn (;x)$,  $\andfn(;x,y)$, $\orfn(;x,y)$, $\equivfn(;x,y)$ can all be defined on safe arguments, simply by computing by case distinction using the conditional function.
 	%\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;1010)=0$.
+	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1011)=0$.
 	
 	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:
 	\begin{eqnarray*}
 	\shorten(\epsilon;x) &=&x\\
-	\shorten(li;x) &=&p(;\shorten(l;x))
+	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))
 	\end{eqnarray*}
 	Then we define $\bit(l;x)$  as follows:
 	$$\bit(l;x)=C(;\shorten(pl;x),\epsilon,0,1).$$ 
@@ -166,15 +166,15 @@
 
 %\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}
 
-\subsection{Bellantoni's characterisation of $\fphi{i}$ using predicative minimization}
+\subsection{Bellantoni's characterisation of $\fphi{i}$ using predicative minimisation}
 
-Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimization: 
+Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimisation: 
 \begin{definition}[$\mubc$ and $\mubc^i$ programs]
 The algebra $\mubc$ is generated from $\bc$ by the following additional operation:
 
 \begin{enumerate}
 			\setcounter{enumi}{7}
-	\item Predicative minimization. If $h$ is in $\mubc$, then so is $f$ defined by
+	\item Predicative minimisation. If $h$ is in $\mubc$, then so is $f$ defined by
 	$$f(\vec u; \vec x):= \begin{cases}
 	s_1 \mu y.(h(\vec u; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\
 	0  & \mbox{ otherwise,}
@@ -184,7 +184,7 @@
 where $\mu y.(h(\vec u; \vec x , y)\mod 2 = 0)$ is the least $y$ such that the equality holds.
 %We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.
 
- For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimization.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program.} So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.
+ For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimisation.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program.} So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.
 
  \end{definition}
  
@@ -217,7 +217,7 @@
  A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.
  \end{definition}
  One then has:
- \begin{lemma}[Bounded Minimization, \cite{BellantoniThesis}]
+ \begin{lemma}[Bounded minimisation, \cite{BellantoniThesis}]
  	\label{lem:bounded-minimisation}
 If  $f(\vec u; \vec x,y)$ is a polynomial checking function on $\vec u$ and $q$ is a threshold, then for any $\vec u$ and $\vec x$ we have:
 $$ (\exists y.   f(\vec u; \vec x,y)\mbox{ mod } 2=0) \Rightarrow (\exists y.  (\size{y}\leq q(\size{\vec{x}})+2) \mbox{ and } f(\vec u; \vec x,y) \mbox{ mod } 2=0) .$$
@@ -229,7 +229,7 @@
  	\label{lem:polychecking}
  Let $\Phi$ be a class of polymax bounded polynomial checking functions. If $f(\vec u; \vec x)$ is in $\mubc(\Phi)$, then $f$ is  a polymax bounded function  polynomial checking function on $\vec u$.
  \end{lemma}
- The following property follows from \cite{BellantoniThesis, Bellantoni95}]
+ The following property follows from \cite{BellantoniThesis, Bellantoni95}:
  \begin{proposition}
   If $\Phi$ is a class of polymax bounded polynomial checking functions, then  $\mubc(\Phi)$ satisfies the properties of Thm \ref{thm:mubc}.
  \end{proposition}
Index: CSL17/appendix-completeness.tex
===================================================================
--- CSL17/appendix-completeness.tex	(revision 225)
+++ CSL17/appendix-completeness.tex	(revision 226)
@@ -5,7 +5,7 @@
 
 The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 
 \paragraph*{Predicative minimisation}
-Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. 
+Suppose $f(\vec u ; \vec x)$ is defined by predicative minimisation from $g$ (we then denote $f$ as as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$). 
 By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,
 \[
 \arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)
