Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 259)
+++ CSL17/tech-report/arithmetic.tex	(revision 260)
@@ -198,7 +198,7 @@
 
 \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
 
-We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
+We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  \vec x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
  
 Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:
 \begin{itemize}
@@ -207,7 +207,7 @@
 %\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
 \item Conditional $C$: 
 $$\begin{array}{ll}
-\forall x^{\safe} , y_{\epsilon}^{\safe}, y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
+\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
                                                                                                    & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
                                                                                                    & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
 \end{array}
Index: CSL17/tech-report/completeness.tex
===================================================================
--- CSL17/tech-report/completeness.tex	(revision 259)
+++ CSL17/tech-report/completeness.tex	(revision 260)
@@ -53,7 +53,8 @@
 	\right) \\
 	\cor & \left(
 	\begin{array}{ll}
-	z\neq 0 
+	%z\neq 0
+	z=\succ{1} p z 
 	& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
 	& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
 	\end{array}
@@ -111,7 +112,9 @@
 	Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.
 	We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$. 
 	%\todo{verify $z\neq 0$ disjunct.} 
-	Then $z \neq 0$ holds. Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
+	%Then $z \neq 0$ holds. 
+	Then $z=\succ{1} p z$ holds.
+	Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
 	$\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that
 	$\exists y^\safe .  (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce 
 	$\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction
Index: CSL17/tech-report/ph-biblio.bib
===================================================================
--- CSL17/tech-report/ph-biblio.bib	(revision 259)
+++ CSL17/tech-report/ph-biblio.bib	(revision 260)
@@ -5,16 +5,7 @@
 	note={\url{http://www.anupamdas.com/fph-unbounded-arithmetic.pdf}}
 	}
 
-@incollection{bellantoni1995fph,
-	title={Predicative recursion and the polytime hierarchy},
-	author={Bellantoni, Stephen},
-	booktitle={Feasible Mathematics II},
-	pages={15--29},
-	year={1995},
-	publisher={Springer}
-}
 
-
 @inproceedings{Lasson11,
   author    = {Marc Lasson},
   title     = {Controlling Program Extraction in Light Logics},
Index: CSL17/tech-report/preliminaries.tex
===================================================================
--- CSL17/tech-report/preliminaries.tex	(revision 259)
+++ CSL17/tech-report/preliminaries.tex	(revision 260)
@@ -195,7 +195,7 @@
 $\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.
  \end{theorem}
 
-In what follows we will recall some of the intermediate results and state a slightly stronger result that directly follows from \cite{bellantoni1995fph}.
+In what follows we will recall some of the intermediate results and state a slightly stronger result that directly follows from \cite{Bellantoni95}.
 %
 %\medskip 
 %\noindent
@@ -228,7 +228,7 @@
   If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions.
  \begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]
  	\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$.
+ 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 polynomial checking function on $\vec u$.
  \end{lemma}
 
 In particular, we also have the following strengthening of Thm.~\ref{thm:mubc},
