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

We now define \emph{length-bounded $\beta$ function} $\beta(i,l;x,b)$ as:

\[

\forall j \leq l . \bigvee\limits_{b=0,1} ( \beta\bit (i,j;x,b) \cand \bit (j;y,b) )

\]

\end{definition}

Our aim is to construct sequences formed from old sequences and new elements.

Namely we want the following result, which says that, given a number $x$ and a sequence $y$, there is another sequence $z$ formed from prepending $x$ to $y$:

\begin{proposition}

	[In $\arith$]

	$$

	\forall x^\safe, y^\safe. \exists z^\safe . \forall i^\normal\leq k, j^\normal\leq l . 

	\left(

	\begin{array}{rl}

	& \bigwedge\limits_{b=0,1} (\bit(j;x,b) \cimp \beta (0,j;z,b) ) \\

	\cand & i>0 \cimp \bigwedge\limits_{b=0,1} (\beta(i-1, j;y,b) \cimp \beta(i,j;z,b) )

	\end{array}

	\right)

	$$

\end{proposition}

To prove this we will need two lemmata.

The first says we can construct a sequence whose $0$th element is $x$ and every other element is $0$.

\begin{lemma}

[In $\arith$]

$\forall l . \exists z . (\beta (0,|l| ; z , x) \cand \forall i \leq |k| . \beta(i,|l|;z,0) )$.	

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}

The second says we can prepend $0$ to any sequence:

\begin{lemma}

	[In $\arith$]

	$\forall x . \exists z . ( \beta(0,|l|;z,0) \cand \forall i\in (0,|k|] . \exists y . (\beta (i, |l| ; z,y) \cand \beta(i-1,|l|;x,y) )   )$

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}