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

 We define the function $\mode$ by $u\mode x:= u \mod 2^{\size{x}}$.

 \begin{definition}

 A function $f(\vec u; \vec x)$ is a \textit{polynomial checking function} on $\vec u$ if there exists a polynomial $q$

 such that, for any $\vec u$, $\vec x$, $y$ and $z$ such that $\size{y} \geq q(\size{\vec u})+ \size{z}$ we have:

 $$ f(\vec u; \vec x) \mode z = f(\vec u; \vec x \mode y)\mode z.$$

 A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.

 \end{definition}

 One then has:

 \begin{lemma}[Bounded Minimization, \cite{BellantoniThesis}]

If  $f(\vec u; \vec x,y)$ is a polynomial checking function on $\vec u$ and $q$ is a threshold, then for any $\vec u$ and $\vec x$ we have:

$$ (\exists y.   f(\vec u; \vec x,y)\mbox{ mod } 2=0) \Rightarrow (\exists y.  (\size{y}\leq q(\size{\vec{x}})+2) \mbox{ and } f(\vec u; \vec x,y) \mbox{ mod } 2=0) .$$

 \end{lemma}

 Finally we can state an important lemma about $\mubc$:

 \begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]

 Let $\Phi$ be a class of polymax bounded functions. If $f(\vec u; \vec x)$ is in $\mubc(\Phi)$, then $f$ is  a polymax bounded function and a polynomial checking function on $\vec u$.

 \end{lemma}

\newcommand{\size}[1]{|#1|}                        %% length of a word

\newcommand{\mode}{\; \underline{\mbox{mod}}\;}   %% mod 2^{|x|}