Révision 195 CSL17/completeness.tex
| completeness.tex (revision 195) | ||
|---|---|---|
| 71 | 71 |
\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.'' |
| 72 | 72 |
\end{itemize}
|
| 73 | 73 |
} |
| 74 |
|
|
| 74 |
\patrick{I also assume access to the following predicates:
|
|
| 75 |
\begin{itemize}
|
|
| 76 |
\item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)" |
|
| 77 |
\item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" |
|
| 78 |
\end{itemize}}
|
|
| 75 | 79 |
Now suppose that $f$ is defined by PRN: |
| 76 | 80 |
\[ |
| 77 | 81 |
\begin{array}{rcl}
|
| ... | ... | |
| 91 | 95 |
%Seq(z) \cand |
| 92 | 96 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\ |
| 93 | 97 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1}) \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
| 98 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1}) \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
|
| 94 | 99 |
\end{array}
|
| 95 | 100 |
\right) |
| 96 | 101 |
\] |
| 102 |
|
|
| 103 |
where |
|
| 104 |
|
|
| 105 |
\[ |
|
| 106 |
B (u , \vec u ; \vec x , y_k , y_{k+1}) =
|
|
| 107 |
\begin{array}{ll}
|
|
| 108 |
& \\ |
|
| 109 |
\cand & |
|
| 110 |
|
|
| 111 |
\end{array}
|
|
| 112 |
|
|
| 113 |
\] |
|
| 97 | 114 |
which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$. |
| 98 | 115 |
|
| 99 | 116 |
To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$. |
Formats disponibles : Unified diff