Révision 237
| CSL17/arithmetic.tex (revision 237) | ||
|---|---|---|
| 153 | 153 |
$$ |
| 154 | 154 |
\item The following predicates will also be needed in proofs: |
| 155 | 155 |
|
| 156 |
$\zerobit(x,k)$ (resp. $\onebit(x,k)$) holds iff the $k$th bit of $x$ is 0 (resp. 1). The predicate $\zerobit(x,k)$ can be |
|
| 156 |
$\zerobit(x,k)$ (resp. $\onebit(x,k)$) holds iff the $k$th bit of $x$ is 0 (resp. 1). The predicate $\zerobit(x,k)$ for instance can be
|
|
| 157 | 157 |
defined by: |
| 158 |
$$ \exists^{\safe} y.(\pref(k,x,y) \cand C(y,0,1,0)).$$
|
|
| 158 |
$$ \exists^{\safe} y.(\pref(k,x,y) \cand \exists^{\safe} z. y=\succ{0}z).$$
|
|
| 159 |
%$$ \exists^{\safe} y.(\pref(k,x,y) \cand C(y,0,1,0)).$$
|
|
| 159 | 160 |
\end{itemize}
|
| 160 | 161 |
|
| 161 |
|
|
| 162 |
|
|
| 163 |
|
|
| 164 | 162 |
\subsection{A sequent calculus presentation}
|
| 165 | 163 |
\begin{figure}
|
| 166 | 164 |
\[ |
Formats disponibles : Unified diff