Révision 225 CSL17/arithmetic.tex
| arithmetic.tex (revision 225) | ||
|---|---|---|
| 229 | 229 |
The sequent calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with the $\basic$, $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.
|
| 230 | 230 |
|
| 231 | 231 |
\todo{Present typed variable free-cut free form.}
|
| 232 |
\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}
|
|
| 232 |
\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}
|
|
| 233 |
|
|
| 234 |
\begin{theorem}
|
|
| 235 |
[Typed variable normal form] |
|
| 236 |
\label{thm:normal-form}
|
|
| 237 |
\end{theorem}
|
|
Formats disponibles : Unified diff