Révision 219 CSL17/arithmetic.tex

arithmetic.tex (revision 219)
110 110 

  		





  111
  111
  
    
\begin{lemma}


  		





  112
  112
  
    
[Sharply bounded lemma]


  		





  
  113
  
    
\label{lem:sharply-bounded-recursion}


  		





  113
  114
  
    
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.


  		





  114
  115
  
    
Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.


  		





  115
  116
  
    
\end{lemma}


  		












Formats disponibles :
  Unified diff