Révision 265 CSL17/tech-report/soundness.tex

soundness.tex (revision 265)
166 166 
		[Proof interpretation]
167 167 
		\label{lem:proof-interp}
168 168 
	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$
169 
	there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
169 
	there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , \vec w)$ for $B\in\Delta$ such that
170 170 
	% such that, for any $l, \vec u ; \vec x  , w$, we have:
171 171 
	\[
172 172 
%	\vec a^\nu = \vec u ,
......
195 195
196 196
197 197 
	\paragraph*{Negation}
198 
	Can assume only on atomic formulae, so no effect.
198 
Suppose $\pi$ ends with a right negation step:
199 
\[
200 
\vlinf{\rigrul{\cnot}}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \cnot A , \Delta }{\normal (\vec u) , \safe (\vec x) , \Gamma , A\seqar  \Delta}
201 
\]
202 
Notice that, since $\pi$ is in De Morgan form, we have that $A$ is atomic ($s\leq t$) and so, in particular, $\Pi^\safe_{i-1}$.
203 
So we can simply set the witness for both $A$ and $\cnot A$ to $0$.
204 
Namely, if $\vec f (\vec u ; \vec x , \vec w , w )$ is obtained by the inductive hypothesis, then we may set $f^\pi_B ( \vec u ; \vec x , \vec w) \dfn f_B (\vec u ;\vec x , \vec w , 0)$ for $B\in \Delta$, and $f^\pi_A (\vec u ; \vec x , \vec w) \dfn 0$.
205 
The bounding polynomial remains the same.
199 206
200 207 
	\paragraph*{Logical rules}
201 208 
	Pairing, depairing. Need length-boundedness.

Formats disponibles : Unified diff