Révision 174 CSL17/completeness.tex

completeness.tex (revision 174)
40 40 
[Minimisation]
41 41 
$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.
42 42 
\end{lemma}
43 
% see Thm 20 p. 58 in Buss' book.
43 44 
\begin{proof}
44 45 
\todo{}
45 46 
\end{proof}
......
89 90 
&
90 91 
%Seq(z) \cand
91 92 
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
92 
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_i) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
93 
\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}) )
93 94 
\end{array}
94 95 
\right)
95 96 
\]

Formats disponibles : Unified diff