Index: appendix-completeness.tex
===================================================================
--- appendix-completeness.tex	(revision 222)
+++ appendix-completeness.tex	(revision 223)
@@ -1 +1,173 @@
-\section{Proof of completeness}
\ No newline at end of file
+\section{Proof of completeness}
+
+The rest of this section is devoted to a proof of this theorem.
+We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.
+
+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$. 
+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)
+\]
+Let us define $A_f(\vec u ; \vec x , z)$ as:
+\[
+\begin{array}{rl}
+&\left(
+z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
+\right) \\
+\cor & \left(
+\begin{array}{ll}
+z\neq 0 
+& \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}
+\right)
+\end{array}
+\]
+Notice that $A_f$ is $\Pi^{\safe}_{i-1}$, since $A_g$ is $\Sigma^{\safe}_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.
+In particular this means $A_f$ is $\Sigma^{\safe}_i$.
+
+Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:
+
+\begin{lemma}
+	[Minimisation]
+	$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	
+	\end{lemma}
+	% see Thm 20 p. 58 in Buss' book.
+	%\begin{proof}
+	%\end{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).
+	
+	\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:
+	\[
+	\exists !z^\safe  . A_f(\vec u ; \vec x , z)
+	\]
+	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
+	$\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
+	$A_f(\vec u ; \vec x , z)$ is proven.  
+	
+	Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$, so we can set $z=0$ and the first member of the disjunction $A_f(\vec u ; \vec x , z)$ is proven.  
+	
+	So we have proven $\exists z^\safe  . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified.
+	
+	\paragraph*{Predicative recursion on notation}
+	
+	\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):
+		\begin{itemize}
+			%	\item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$''
+			\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$''
+			\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.''
+			\end{itemize}
+			}
+			\patrick{I also assume access to the following predicates:
+				\begin{itemize}
+					%   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
+					%   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" 
+					\item $\addtosequence(w,y,w')$. "$w'$ represents the sequence obtained by adding $y$ at the end of the sequence represented by $w$". Here we are referring to sequences which can be decoded with predicate $\beta$.
+					\end{itemize}}
+					In the following we will use the predicates $\zerobit (u,k)$, $\onebit(u,k)$, $\pref(k,x,y)$ which have been defined in Sect. \ref{sect:graphsbasicfunctions}.
+					
+					Suppose that $f$ is defined by predicative recursion on notation:
+					\[
+					\begin{array}{rcl}
+					f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\
+					f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x))
+					\end{array}
+					\]
+					
+					\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}
+					
+					Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.
+					We define $A_f (u ,\vec u ; \vec x , y)$ as,
+					\[
+					\exists w^\safe . \left(
+					\begin{array}{ll}
+					& 
+					%Seq(z) \cand 
+					\exists^{\safe} 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_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )\\
+					\cand & \forall^{\normal}  k < |u| . \exists^{\safe} y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
+					\end{array}
+					\right)
+					\]
+					where 
+					\[
+					B (u , \vec u ; \vec x , y_k , y_{k+1}) = \left(
+					\begin{array}{ll}
+					& \zerobit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_0}(v,\vec u ; \vec x, y_k, y_{k+1}) )\\
+					\cand &  \onebit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_1}(v,\vec u ; \vec x, y_k, y_{k+1}) )
+					\end{array}
+					\right)
+					\]
+					
+					%which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.
+					
+					To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.
+					The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show:
+					\[
+					\exists y^\safe . A_f (u , \vec u ; \vec x , y) 
+					\quad \seqar \quad
+					\exists z^\safe . A_f (s_i u, \vec u ; \vec x , z)
+					\]
+					
+					So let us assume $\exists y^\safe . A_f (u , \vec u ; \vec x , y) $. Then there exists $w$ such that $\safe(w)$ and 
+					$A_f (u , \vec u ; \vec x , w) $.
+					
+					We know that there exists a $z$ such that $A_{h_i}(u,\vec u ; \vec x, y, z)$. Let then $w'$ be such that
+					$\addtosequence(w,z,w')$. Observe also that we have $\pref(|u|,s_i u,u)$
+					
+					So we have, for $k=|u|$:
+					
+					$$  \beta (k, w', y) \cand \beta (k+1 ,w', z)  \cand B (u , \vec u ; \vec x , y , z).$$
+					
+					and we can conclude that
+					\[
+					\exists w'^\safe . \left(
+					\begin{array}{ll}
+					& 
+					%Seq(z) \cand 
+					\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w' , y_0) ) \cand \beta(|u|+1, w',z ) \\
+					\cand & \forall k < |u|+1 . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
+					\end{array}
+					\right)
+					\]
+					So $\exists z^{\safe} . A_f (s_i u, \vec u ; \vec x , z)$ has been proven. So by induction we have proven $\forall^{\normal} u,  
+					\forall^{\normal} \vec u, \exists^{\safe} y. A_f (u ,\vec u ; \vec x , y)$. Moreover one can also check the unicity of $y$, and so we have proved the required formula. 
+					
+					\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
+					
+					\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
+					
+					\paragraph*{Safe composition}
+					Now suppose that $f$ is defined by safe composition:
+					\[
+					f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) )
+					\]
+					
+					By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.
+					In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.
+					
+					We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows:
+					\[
+					\exists \vec v^\normal . \exists \vec y^\safe .  
+					\left(  
+					\bigwedge\limits_i A_{h_i} (\vec u , v_i)
+					\wedge
+					\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)
+					\wedge
+					A_g ( \vec v , \vec y , z ) 
+					\right)
+					\]
+					The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations.
+					
+					\todo{elaborate}
+					
+					The proof of Thm \ref{thm:completeness} is thus completed.
