Révision 260 CSL17/tech-report/completeness.tex

completeness.tex (revision 260)
53 53 
	\right) \\
54 54 
	\cor & \left(
55 55 
	\begin{array}{ll}
56 
	z\neq 0
56 
	%z\neq 0
57 
	z=\succ{1} p z
57 58 
	& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
58 59 
	& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1)
59 60 
	\end{array}
......
111 112 
	Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.
112 113 
	We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$.
113 114 
	%\todo{verify $z\neq 0$ disjunct.}
114 
	Then $z \neq 0$ holds. Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
115 
	%Then $z \neq 0$ holds.
116 
	Then $z=\succ{1} p z$ holds.
117 
	Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
115 118 
	$\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that
116 119 
	$\exists y^\safe .  (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce
117 120 
	$\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction

Formats disponibles : Unified diff