Révision 234 CSL17/arithmetic.tex

arithmetic.tex (revision 234)
342 342 
\vlinf{\rigrul{\exists}}{}{\normal(\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x^\safe . A(x)}{ \normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A(t) }
343 343 
\]
344 344 
\[
345 
\vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(t(\vec u)  ) , \Gamma \seqar \Delta  }
345 
\vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(s(\vec u)  ) , \Gamma \seqar \Delta  }
346 346 
\]
347 347 
where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.

Formats disponibles : Unified diff