Révision 145 CharacterizingPH/soundness.tex

soundness.tex (revision 145)
119 119 
	\end{cases}
120 120 
	\end{array}
121 121 
	\]
122 
	\item Induction. NB: Can assume no side-formulae on the right!!
123 
	\[
124 
	\dfrac{\Box N(a), \Gamma, A(a) \seqar A(s_i a)}{\Box N(s), \Gamma , A(0) \seqar A(s)}
125 
	\]
126 
	We need to keep track of all the terms in the witness predicate.
127 
	\[
128 
%	\begin{array}{rl}
129 
%	&\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
130 
%	\\
131 
%	\implies &
132 
%	\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^A (u , \vec u ; \vec x , \vec y)  )
133 
%	\vee
134 
%	\wit{a , t(a), t(s_i a), \vec t}{\bigvee \Delta} (; \vec f^\Delta (u , \vec u ; \vec x , \vec y)  )
135 
%	\end{array}
136 
\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
137 
\implies
138 
\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^i (u , \vec u ; \vec x , \vec y)  )
139 
	\]
140 
	Define $\vec g$ by safe recursion as follows:
141 
	\[
142 
	\begin{array}{rcl}
143 
	\vec g (0 , \vec u ; \vec x , \vec y) & \dfn & \vec y \\
144 
	\vec g (s_i u, \vec u ; \vec x , \vec y) & \dfn & \vec f^i ( u, \vec u; \vec x, \vec g (u, \vec u ; \vec x , \vec y) )
145 
	\end{array}
146 
	\]
122 147 
	\end{itemize}
123 148 
	\subsection{Proof of correctness}
124 149

Formats disponibles : Unified diff