Révision 248 CSL17/soundness.tex
| soundness.tex (revision 248) | ||
|---|---|---|
| 133 | 133 |
[Proof interpretation] |
| 134 | 134 |
\label{lem:proof-interp}
|
| 135 | 135 |
From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma \seqar \Delta$ |
| 136 |
there are $\bc (\charfn{}{i})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
|
|
| 136 |
there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
|
|
| 137 | 137 |
% such that, for any $l, \vec u ; \vec x , w$, we have: |
| 138 | 138 |
\[ |
| 139 | 139 |
% \vec a^\nu = \vec u , |
Formats disponibles : Unified diff