Révision 192 CSL17/DICE2017_TALK/unboundedArithmetic.tex

unboundedArithmetic.tex (revision 192)
186 186 
\end{itemize}
187 187 
$$ \begin{array}{l}
188 188 
 \exists^{|s_1|\leq k } s_1, \forall^{|s_2|\leq k+1 } s_2,\\
189 
  (|s_1|=k \cand \mbox{CLIQUE}(s_1,x) \cand (|s_2|\geq k+1 \rightarrow \neg  \mbox{CLIQUE}(s_2,x))   )
189 
  (|s_1|=k \cand \mbox{CLIQUE}(s_1,x) \cand (s_1\subsetneq s_2 \rightarrow \neg  \mbox{CLIQUE}(s_2,x))   )
190 190 
\end{array}
191 191 
$$
192 192 
\begin{itemize}
......
417 417 
 \end{claim}
418 418
419 419 
  \begin{claim}[Completeness]
420 
  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
420 
  If $f$ $f$ belongs to $\fphi{i}$ then $f$ is provably total in \RCi\ .
421 421 
 \end{claim}
422 422 

  		





  423
  423
  
    
\end{frame}


  		












Formats disponibles :
  Unified diff