Révision 249
| CSL17/soundness.tex (revision 249) | ||
|---|---|---|
| 126 | 126 |
\end{proposition}
|
| 127 | 127 |
|
| 128 | 128 |
|
| 129 |
In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$:
|
|
| 129 |
In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$.
|
|
| 130 | 130 |
|
| 131 | 131 |
|
| 132 | 132 |
\begin{lemma}
|
Formats disponibles : Unified diff