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)).$$