root / CSL17 / soundness.tex @ 168
Historique | Voir | Annoter | Télécharger (364 octet)
| 1 |
\section{Soundness}
|
|---|---|
| 2 |
\label{sect:soundness}
|
| 3 |
|
| 4 |
The main result of this section is the following: |
| 5 |
|
| 6 |
\begin{theorem}
|
| 7 |
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))$.
|
| 8 |
\end{theorem}
|
| 9 |
|