\section{Completeness}

The main result of this section is the following:

\begin{theorem}
	\label{thm:completeness}
	For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall \vec u \in \normal . \forall \vec x \in \safe. \exists ! y \in \safe . A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x))$.
\end{theorem}

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.

\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_{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_{i-1}$, since $A_g$ is $\Sigma_{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_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}
\todo{}
\end{proof}

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$" 
\end{itemize}}
Now suppose that $f$ is defined by PRN:
\[
\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 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 k < |u| . \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)
\]

where 

\[
B (u , \vec u ; \vec x , y_k , y_{k+1}) =
\begin{array}{ll}
&  \\
\cand & 

\end{array}

\]
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 , y)
\]

\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}

\paragraph*{Other cases}
\todo{}
























