From 6eb14da614c11bcb30277cfd15fa0b391c03379c Mon Sep 17 00:00:00 2001 From: rriegel Date: Fri, 8 Jun 2007 23:53:44 +0000 Subject: [PATCH] refreshing proofs --- fastlib/u/rriegel/nips07/gnp_nips07.tex | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/fastlib/u/rriegel/nips07/gnp_nips07.tex b/fastlib/u/rriegel/nips07/gnp_nips07.tex index 1d7fe78607..6e2610babb 100644 --- a/fastlib/u/rriegel/nips07/gnp_nips07.tex +++ b/fastlib/u/rriegel/nips07/gnp_nips07.tex @@ -827,7 +827,7 @@ Refinement need not be performed in any particular pattern. Depth-first is often a good choice due to its low overhead, though pruning in some problems strongly favors other expansion patterns. -\begin{lemma}[Correctness of the GNA] +\begin{lemma}[Correctness] The GNA terminates with $\GNP[\Sigma](\kdroot{Y},\kdroot{X}) = \{\GNP(\kdroot{Y},\kdroot{X})\}$. \end{lemma} @@ -839,8 +839,7 @@ pruning in some problems strongly favors other expansion patterns. that values introduced by $\prunes$ ultimately yeild the exact result. Otherwise, by induction and by the definition of composed summary results, all nodes must represent singleton summary sets - containing values equivalent to what exhaustive recursion would have - found. + containing values equivalent to exhaustive recursion. \end{proof} \killspace % \subsection{Intrinsic Pruning}