(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Lemma: IDBEZAL *) (* Chapter: Packing *) (* Author: Thomas C. Hales *) (* Date: Feb 14, 2010 *) (* ========================================================================== *) module type Idbezal_type = sig val IDBEZAL_concl : term end;; module Idbezal : Idbezal_type = struct let IDBEZAL_concl = `!V ul k F. saturated V /\ packing V /\ vor_list V k ul /\ (k < 3) ==> (F facet_of voronoi_list V ul <=> (?vl. (F = voronoi_list V vl) /\ vor_list V (k+1) vl /\ (truncate_simplex k vl = ul)))`;; end;;