1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
7 (* Date: Feb 14, 2010 *)
8 (* ========================================================================== *)
14 module type Idbezal_type = sig
15 val IDBEZAL_concl : term
20 module Idbezal : Idbezal_type = struct
22 let IDBEZAL_concl = `!V ul k F. saturated V /\ packing V /\ vor_list V k ul /\ (k < 3) ==>
23 (F facet_of voronoi_list V ul <=>
24 (?vl. (F = voronoi_list V vl) /\ vor_list V (k+1) vl /\ (truncate_simplex k vl = ul)))`;;