Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\item Prefix:

  This is a predicate that we will need for technical reasons, in the completeness proof. The predicate $\pref(k,x,y)$ holds if the prefix of string $x$

  of length $k$ is $y$. It is defined as:

  $$\begin{array}{ll}

\exists^{\safe} z, \exists^{\normal} l\leq |x|. & (k+l= |x|\\

                                                                                                   & \cand \; |z|=l\\

                                                                                                   & \cand \; x=y\smsh(2,l)+z)

                                                                                                   \end{array}

$$

\item The following predicates will also be needed in proofs:

$\zerobit(x,k)$ (resp. $\onebit(x,k)$) holds iff the $k$th bit of $x$ is 0 (resp. 1). The predicate $\zerobit(x,k)$  can be

defined by:

$$ \exists^{\safe} y.(\pref(k,x,y) \cand C(y,0,1,0)).$$

%   \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$" 

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:

\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^{\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}) )