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