Révision 196
| CSL17/completeness.tex (revision 196) | ||
|---|---|---|
| 94 | 94 |
& |
| 95 | 95 |
%Seq(z) \cand |
| 96 | 96 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\ |
| 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}) )
|
|
| 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 | 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}) )
|
| 99 | 99 |
\end{array}
|
| 100 | 100 |
\right) |
| 101 | 101 |
\] |
| 102 | 102 |
|
| 103 |
where |
|
| 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 |
%\] |
|
| 114 |
%which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$. |
|
| 104 | 115 |
|
| 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 |
\] |
|
| 114 |
which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$. |
|
| 115 |
|
|
| 116 | 116 |
To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$. |
| 117 | 117 |
The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show: |
| 118 | 118 |
\[ |
Formats disponibles : Unified diff