Révision 176 CSL17/soundness.tex

soundness.tex (revision 176)
30 30 
%	If $A$ is a $\Pi_{i}$ formula then:
31 31 
	\[
32 32 
	\begin{array}{rcl}
33 
	\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(;s,t) \\
33 
	\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(l;s,t) \\
34 34 
	\smallskip
35 
	\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(;s,t) \\
35 
	\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(l;s,t) \\
36 36 
	\smallskip
37 37 
	\charfn{}{\neg A} (l, \vec u ; \vec x, w) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
38 38 
	\smallskip
......
45 45 
	0 & \text{otherwise}
46 46 
	\end{cases} \\
47 47 
	\smallskip
48 
	\charfn{\vec u; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
48 
	\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
49 49 
	\begin{cases}
50 50 
	0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
51 51 
	1 & \text{otherwise}
......
55 55 
\end{definition}
56 56 

  		





  57
  57
  
    

  		





  
  58
  
    
\begin{proposition}


  		





  
  59
  
    
	$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.


  		





  
  60
  
    
\end{proposition}


  		





  
  61
  
    

  		





  58
  62
  
    
\begin{definition}


  		





  59
  63
  
    
	[Length bounded witness function]


  		





  60
  64
  
    
	We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.


  		












Formats disponibles :
  Unified diff