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

\label{sect:soundness}

The main result of this section is the following:

\begin{theorem}

	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.

\end{theorem}