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

%\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }

 \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]\label{thm:mubc}

 The following property follows from \cite{BellantoniThesis, Bellantoni95}]

 \begin{proposition}

  If $\Phi$ is a class of polymax bounded polynomial checking functions, then  $\mubc(\Phi)$ satisfies the properties of Thm \ref{thm:mubc}.

 \end{proposition}

  Consider the addition function $+$ with two safe arguments, so denoted as $+(;x,y)$. It is clear that if $+(;x,y)=z$, then we have $|z| \leq \max(|x|,|y|)+1$, so $+$ is a polymax bounded function. Moreover for any $n$, the $n$th least significant bits of $z$ only depend on the $n$th least significant bits  of $x$ and $y$, so $+(;x,y)$ is a polynomial checking function (on no normal argument), with threshold $q(x,y)=0$.

  In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as  as $\succ{} (;x)=+(;x,\succ 1 0)$.