(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Sgtrnaf = struct
open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;

open Uxckfpe;;



let UXCKFPE2=
prove_by_refinement( ` !s vv. is_scs_v39 s /\ vv IN BBs_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime2_v39 s = {})`,
(* {{{ proof *) [ REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC UXCKFPE[`s:scs_v39`;`vv:num->real^3`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;] THEN STRIP_TAC THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s vv1=n)` ASSUME_TAC; EXISTS_TAC`BBindex_v39 s vv1` THEN EXISTS_TAC`vv1:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[MINIMAL] THEN STRIP_TAC THEN EXISTS_TAC`vv1':num->real^3` THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th)) THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`] THEN STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;] THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN EQ_TAC; STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC; EXISTS_TAC`vv1':num->real^3` THEN ASM_REWRITE_TAC[]; STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`) THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==> BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`) THEN RESA_TAC THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th` BBindex_v39 s x`) THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC; EXISTS_TAC`x:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; EXISTS_TAC`vv1':num->real^3` THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1' \/ BBindex_v39 s vv1' <= BBindex_v39 s x`) THEN RESA_TAC; REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th` BBindex_v39 s x`) THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC; EXISTS_TAC`x:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let SGTRNAF =
prove( `!s vv. is_scs_v39 s/\ unadorned_v39 s /\ vv IN BBs_v39 s /\ taustar_v39 s vv < &0 ==> ~(MMs_v39 s = {})`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC unadorned_MMs THEN RESA_TAC THEN MATCH_MP_TAC UXCKFPE2 THEN EXISTS_TAC`vv:num->real^3` THEN ASM_REWRITE_TAC[]);;
end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)