Index: CharacterizingPH/LCC17/lcc2017.tex
===================================================================
--- CharacterizingPH/LCC17/lcc2017.tex	(revision 268)
+++ CharacterizingPH/LCC17/lcc2017.tex	(revision 269)
@@ -89,6 +89,9 @@
 In this work we improve the situation by using implicit methods in first-order theories to characterise $\ph$.
 To achieve this we work with a function algebra of Bellantoni from \cite{BellantoniThesis} in which to extract programs, and use the \emph{witness function method} of Buss to extract programs at ground type and preserve quantifier information, necessary to delineate the levels of $\ph$.
 
+
+
+
 %One particular feature of this work that helps make this possible is to break one of the aforementioned correlations: while we use implicit constraints, our witness extraction methods will use only functions of bounded type level. In this way we can naturally appeal to function algebras, which are of ground type in nature, which implicitly characterise $\ph$, namely via \emph{predicative minimisation} \cite{BellantoniThesis}.
 %In order to remain in this class of programs and not get lost with higher types, we appeal to the \emph{witness function method} of extracting programs from proofs, a technique developed by Buss \cite{Buss86book} \cite{Buss:95:wfm-arith}, which is ideal for extracting ground programs directly from classical proofs in weak theories.
 %This extends work presented in \cite{BaillotDas16}. %at \emph{CSL '16}.
@@ -187,8 +190,11 @@
 While he allows arbitrary alternation of unbounded quantifiers, note that his induction is \emph{positive}, and so universal quantifiers cannot vary over certified natural numbers, i.e.\ individuals in $N$. In fact this sort of unbounded quantification is also compatible with our approach of \cite{BaillotDas16}.
 %with an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs %\cite{BaillotDas16}.
 
+The idea of using ramified theories in implicit complexity, inducting on normal variables rather than safe, is largely due to Leivant \cite{Leivant94:intrinsic-theories}, who introduced \emph{intrinsic theories} for an arbitrary free algebra.
+The same idea was also used in \cite{OstrinWainer05} for a theory of arithmetic characterising the elementary functions, somewhat reworking of Leivant's work.
+The main difference in this work, which is why we are able to characterise $\ph$, is that for our model of computation we simply use formulas of the theory rather than equational specifications used in \cite{Leivant94:intrinsic-theories} and \cite{OstrinWainer05}. This indeed has a significant effect on the complexity class characterised, as observed in \cite{BelHof:02}.
+%In this way, we extend rather certain work in Bellantoni's thesis \cite{BellantoniThesis}, where theories for $\ptime$ are presented.
 
-
 \subsection{Extraction at ground type}
 We rely on the \emph{witness function method} for extracting functions at bounded type.
 %This was pioneered by Buss, although independently used by Mints beforehand. 
@@ -197,7 +203,7 @@
 	\item\label{item:de-morgan} Reduce a proof to \emph{De Morgan} normal form, with formulae over the basis $\{ \bot, \top, \vee , \wedge , \exists, \wedge \}$ and negation restricted to atoms.
 	\item\label{item:free-cut} Conduct a \emph{free-cut elimination} on the proof, resulting in a proof whose formulae are restricted to
 	essentially just subformulae of the conclusion, axioms and nonlogical steps.
-	\item\label{item:interp} Extract witnesses inductively from the proof, with appropriate semantic properties of these programs verified by an interpretation into a (classical) quantifier-free theory.
+	\item\label{item:interp} Extract witnesses inductively from the proof into an appropriate function algebra, verifying the necessary semantic properties along the way.
 	\end{enumerate}
 	
 	\ref{item:de-morgan} ensures that our extraction works at ground type, rather than higher types which are typically necessary when negation has larger scope.
Index: CharacterizingPH/LCC17/biblio.bib
===================================================================
--- CharacterizingPH/LCC17/biblio.bib	(revision 268)
+++ CharacterizingPH/LCC17/biblio.bib	(revision 269)
@@ -1,4 +1,15 @@
 
+@article{OstrinWainer05,
+	author    = {Geoffrey E. Ostrin and
+	Stanley S. Wainer},
+	title     = {Elementary arithmetic},
+	journal   = {Ann. Pure Appl. Logic},
+	volume    = {133},
+	number    = {1-3},
+	pages     = {275--292},
+	year      = {2005}
+}
+
 @article{GaboardiMarionRonchi12,
   author    = {Marco Gaboardi and
                Jean{-}Yves Marion and
