(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Conclusions *)
(* Chapter: Fan *)
(* Author: Thomas C. Hales *)
(* Date: 2010-05-14 *)
(* ========================================================================== *)
flyspeck_needs "fan/fan_defs.hl";;
module Fan_concl = struct
open Fan_defs;
(* move to fan_misc.hl *)
let CTVTAQA_concl = `!V E E'. fan (V,E) /\ (E' SUBSET E) ==> fan (V,E')`;;
let XOLHLED_concl = `!V E v. fan (V,E) /\ (v IN V) ==> cyclic_set(set_of_edge v V E) (vec 0) v`;; (* introduction.hl:XOHLED *)
let AAUHTVE_concl = `!V E. fan(V,E) ==>
(hypermap_of_fan (V,E))
(!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fan_pair (V,E) d) = d)) /\
(!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fa
let PIIJBJK_concl= `!x V E . FAN (x,V,E) /\ fan81 (x,V,E) ==> conforming_fan (x,V,E)`;;
end;;