legacy/oldpacking/IDBEZAL.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: IDBEZAL                                                             *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13
  14 module type Idbezal_type = sig
  15   val IDBEZAL_concl : term
  16 end;;
  17
  18
  19
  20 module Idbezal : Idbezal_type = struct
  21
  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)))`;;
  25
  26 end;;
  27