Révision 171 CSL17/completeness.tex
| completeness.tex (revision 171) | ||
|---|---|---|
| 62 | 62 |
So we have proven $\exists z^\safe . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified. |
| 63 | 63 |
|
| 64 | 64 |
\paragraph*{Predicative recursion on notation}
|
| 65 |
|
|
| 66 |
\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):
|
|
| 67 |
\begin{itemize}
|
|
| 68 |
% \item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$'' |
|
| 69 |
\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$'' |
|
| 70 |
\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.'' |
|
| 71 |
\end{itemize}
|
|
| 72 |
} |
|
| 73 |
|
|
| 65 | 74 |
Now suppose that $f$ is defined by PRN: |
| 66 | 75 |
\[ |
| 67 | 76 |
\begin{array}{rcl}
|
Formats disponibles : Unified diff