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

\end{proof}

\subsection{Summary}

Assume the existence of a simple pairing function for elements of fixed size: $\pair{k,l}{x}{y}$ denotes the pair $(x \mode k , y \mode l )$.

An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary.

We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.

We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.

\begin{lemma}

	[Creating sequences]

	\label{lem:sequence-creation}

	Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)$ such that:

	\[

	F(l,u,\vec u ; \vec x)

	\quad = \quad

	\langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l , \dots , f(|u|, \vec u ; \vec x) \mode l \rangle

	\]

\end{lemma}

\begin{proof}

	We simply define $F$ by safe recursion from $f$:

	\[

	\begin{array}{rcl}

	F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\

	F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{O(|u| l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}

	\end{array}

	\]

	where the constants for $O(|u|l)$ are sufficiently large.

\end{proof}

\begin{lemma}

[Decoding sequences]

We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.	

\end{lemma}

\begin{proof}

First define $\beta (j,i;x)$ as $j$th bit of $i$th element of $x$, then use similar idea to above, by a recursion on $j$.

\end{proof}

Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.

We define