Révision 171 CSL17/soundness.tex

soundness.tex (revision 171)
7 7 
	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
8 8 
\end{theorem}
9 9 

  		





  
  10
  
    
For this we will use length-bounded witnessing.


  		





  
  11
  
    

  		












Formats disponibles :
  Unified diff