1 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
2 needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
3 needs "tame/CDTETAT.hl";;
6 module Kcblrqc = struct
11 open Lp_ineqs_proofs;;
12 open Lp_main_estimate;;
16 open Hypermap_and_fan;;
18 let a_azim = new_definition `a_azim f_test V d =
19 (let H = hypermap_of_fan (V,ESTD V) in
20 let s = {y | y IN node H d /\ f_test (CARD (face H y))} in
21 sum s (azim_dart (V,ESTD V)) / &(CARD s))`;;
22 let a_tau = new_definition `a_tau f_test V d =
23 (let H = hypermap_of_fan (V,ESTD V) in
24 let s = {y | y IN node H d /\ f_test (CARD (face H y))} in
25 sum s (\y. tauVEF (V, ESTD V, face H y)) / &(CARD s))`;;
28 let a_sum_mul = Sections.section_proof ["s";"f"]
29 `FINITE s ==> &(CARD s) * (sum s f / &(CARD s)) = sum s f`
31 ((BETA_TAC THEN (move ["fin_s"])) THEN (((fun arg_tac -> arg_tac (Arg_term (`CARD s = 0`))) (disch_eq_tac "card0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
32 ((((use_arg_then2 ("card0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] [])))));
33 ((((use_arg_then2 ("card0", [])) (disch_tac [])) THEN (clear_assumption "card0") THEN BETA_TAC) THEN (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
34 (((((use_arg_then2 ("REAL_DIV_LMUL", [REAL_DIV_LMUL]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_OF_NUM_EQ", [REAL_OF_NUM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
37 (* Section Contravening *)
38 Sections.begin_section "Contravening";;
39 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
40 (Sections.add_section_hyp "contrV" (`contravening V`));;
43 Sections.add_section_lemma "h_fan" (Sections.section_proof []
46 ((((use_arg_then2 ("contravening_lp_fan", [contravening_lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
50 Sections.add_section_lemma "fanV" (Sections.section_proof []
51 `FAN (vec 0,V,ESTD V)`
53 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
57 Sections.add_section_lemma "f_surr" (Sections.section_proof []
58 `fully_surrounded (V,ESTD V)`
60 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
64 Sections.add_section_lemma "simpleH" (Sections.section_proof []
65 `simple_hypermap (hypermap_of_fan (V,ESTD V))`
67 ((((use_arg_then2 ("Jgtdebu.JGTDEBU4", [Jgtdebu.JGTDEBU4]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
71 Sections.add_section_lemma "dartH" (Sections.section_proof []
72 `dart (hypermap_of_fan (V,ESTD V)) = dart_of_fan (V,ESTD V)`
74 ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
78 Sections.add_section_lemma "finite_sets" (Sections.section_proof ["n";"d"]
79 `FINITE {y | y IN node (hypermap_of_fan (V,ESTD V)) d
80 /\ CARD (face (hypermap_of_fan (V,ESTD V)) y) = n}
81 /\ FINITE {y | y IN node (hypermap_of_fan (V,ESTD V)) d
82 /\ n <= CARD (face (hypermap_of_fan (V,ESTD V)) y)}`
84 ((split_tac) THEN ((use_arg_then2 ("FINITE_SUBSET", [FINITE_SUBSET])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node (hypermap_of_fan (V,ESTD V)) d`))) (term_tac exists_tac)) THEN (((((use_arg_then2 ("NODE_FINITE", [NODE_FINITE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
88 Sections.begin_section "SumEqs";;
89 (Sections.add_section_var (mk_var ("p", (`:num`))); Sections.add_section_var (mk_var ("q", (`:num`))); Sections.add_section_var (mk_var ("r", (`:num`))));;
92 let anglesum = Sections.section_proof ["d"]
93 `d IN dart_of_fan (V,ESTD V)
94 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
95 ==> (&p) * a_azim ((=) 3) V d + (&q) * a_azim ((=) 4) V d
96 + (&r) * a_azim ((<=) 5) V d = &2 * pi`
98 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN (move ["eqs"])));
99 ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
100 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
101 ((repeat_tactic 1 9 (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
102 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE SUM_AZIM_DART_FULLY_SURROUNDED))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
103 ((((use_arg_then2 ("REAL_EQ_ADD_LCANCEL", [REAL_EQ_ADD_LCANCEL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_UNION", [SUM_UNION]))(gsym_then (thm_tac (new_rewrite [] []))))));
104 (((repeat_tactic 1 9 (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
105 ((congr_tac (`sum _1 _2`)) THEN ((TRY done_tac)));
106 (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andb_orr", [andb_orr]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (ARITH_RULE `!a. a >= 4 <=> a = 4 \/ 5 <= a`)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
109 (* Lemma anglesum_lo_approx *)
110 let anglesum_lo_approx = Sections.section_proof ["d"]
111 `d IN dart_of_fan (V,ESTD V)
112 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
113 ==> #6.28318 <= (&p) * a_azim ((=) 3) V d + (&q) * a_azim ((=) 4) V d
114 + (&r) * a_azim ((<=) 5) V d`
116 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("anglesum", [anglesum])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PI_APPROX_32", [PI_APPROX_32])) (disch_tac [])) THEN (clear_assumption "PI_APPROX_32") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
119 (* Lemma anglesum_hi_approx *)
120 let anglesum_hi_approx = Sections.section_proof ["d"]
121 `d IN dart_of_fan (V,ESTD V)
122 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
123 ==> (&p) * a_azim ((=) 3) V d + (&q) * a_azim ((=) 4) V d
124 + (&r) * a_azim ((<=) 5) V d <= #6.28319`
126 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("anglesum", [anglesum])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PI_APPROX_32", [PI_APPROX_32])) (disch_tac [])) THEN (clear_assumption "PI_APPROX_32") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
129 (* Lemma tausum_eq *)
130 let tausum_eq = Sections.section_proof ["d"]
131 `let H = hypermap_of_fan (V,ESTD V) in
132 d IN dart_of_fan (V,ESTD V)
133 /\ (p,q,r) = type_of_node H d
134 ==> (&p) * a_tau ((=) 3) V d + (&q) * a_tau ((=) 4) V d + (&r) * a_tau ((<=) 5) V d
135 = sum (set_of_face_meeting_node H d) (\f. tauVEF (V,ESTD V,f))`
137 (((CONV_TAC let_CONV) THEN ALL_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN (move ["eqs"])));
138 ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("set_of_face_meeting_node", [set_of_face_meeting_node]))(thm_tac (new_rewrite [] [])))));
139 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
140 (repeat_tactic 1 9 (((use_arg_then2 ("SUM_UNION", [SUM_UNION]))(gsym_then (thm_tac (new_rewrite [] []))))));
141 (((repeat_tactic 1 9 (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
142 ((((use_arg_then2 ("FINITE_UNION", [FINITE_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("DISJOINT", [DISJOINT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] [])))));
143 (((((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
144 ((fun arg_tac -> arg_tac (Arg_term (`(\y. tauVEF (V, ESTD V, face H y)) = (\f. tauVEF (V,ESTD V,f)) o face H`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
145 (((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
146 (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(gsym_then (thm_tac (new_rewrite [] [])))));
147 (((repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andb_orr", [andb_orr]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in_n"])) THEN (move ["card_y"]) THEN (move ["face_eq"]));
148 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("SIMPLE_HYPERMAP_IMP_FACE_INJ", [SIMPLE_HYPERMAP_IMP_FACE_INJ])) (fun fst_arg -> (use_arg_then2 ("face_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("simpleH", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (done_tac));
149 ((congr_tac (`sum _1 _2`)) THEN ((TRY done_tac)));
150 (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andb_orr", [andb_orr]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (move ["f"]));
151 ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"])); ((case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
152 (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
153 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
154 (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
155 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FULLY_SURROUNDED_IMP_CARD_FACE_GE_3", [FULLY_SURROUNDED_IMP_CARD_FACE_GE_3])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
156 ((THENL_LAST) (ANTS_TAC) ((arith_tac) THEN (done_tac)));
157 ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
160 (* Lemma tausum_triangles *)
161 let tausum_triangles = Sections.section_proof ["d"]
162 `let H = hypermap_of_fan (V,ESTD V) in
163 d IN dart_of_fan (V,ESTD V)
164 /\ p,q,r = type_of_node H d
165 ==> (&p) * a_tau ((=) 3) V d
166 = sum {f | f IN set_of_face_meeting_node H d /\ CARD(f)=3 } (\f. tauVEF (V, ESTD V,f))`
168 (((CONV_TAC let_CONV) THEN ALL_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN (move ["eqs"])));
169 ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
170 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
171 ((fun arg_tac -> arg_tac (Arg_term (`(\y. tauVEF (V, ESTD V, face H y)) = (\f. tauVEF (V,ESTD V,f)) o face H`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
172 (((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
173 (((use_arg_then2 ("SUM_IMAGE", [SUM_IMAGE]))(gsym_then (thm_tac (new_rewrite [] [])))));
174 ((repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in_n"])) THEN (move ["card_y"]) THEN (move ["face_eq"]));
175 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("SIMPLE_HYPERMAP_IMP_FACE_INJ", [SIMPLE_HYPERMAP_IMP_FACE_INJ])) (fun fst_arg -> (use_arg_then2 ("face_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("y_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("simpleH", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (done_tac));
176 ((congr_tac (`sum _1 _2`)) THEN ((TRY done_tac)));
177 (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_face_meeting_node", [set_of_face_meeting_node]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"]));
178 ((THENL) (split_tac) [((case THEN (move ["x"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"])); ((case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["card_y"]))]);
179 (((((use_arg_then2 ("card_x", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
180 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
181 (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("y_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("card_y", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
185 Sections.begin_section "Tgt";;
186 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
188 (* Lemma tausum_upper_bound *)
189 let tausum_upper_bound = Sections.section_proof ["d"]
190 `let H = hypermap_of_fan (V,ESTD V) in
191 d IN dart_of_fan (V,ESTD V)
192 ==> sum (set_of_face_meeting_node H d) (\f. tauVEF (V,ESTD V,f)) <= #1.541`
194 ((CONV_TAC let_CONV) THEN (move ["d_in"]));
195 ((THENL_ROT (-1)) ((((use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`&4 * pi - &20 * sol0`))) (term_tac exists_tac)) THEN (split_tac)));
196 ((((use_arg_then2 ("Flyspeck_constants.bounds", [Flyspeck_constants.bounds])) (disch_tac [])) THEN (clear_assumption "Flyspeck_constants.bounds") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
197 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sum_tauVEF_upper_bound", [sum_tauVEF_upper_bound])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC));
198 ((((use_arg_then2 ("contrV", [])) (disch_tac [])) THEN (clear_assumption "contrV") THEN BETA_TAC) THEN (((use_arg_then2 ("contravening", [contravening]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
199 ((fun arg_tac -> arg_tac (Arg_term (`sum _1 _2`))) (term_tac (set_tac "s")));
200 ((BETA_TAC THEN (move ["ineq"])) THEN (((use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((use_arg_then2 ("s", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))));
201 (((((use_arg_then2 ("SUM_SUBSET_SIMPLE", [SUM_SUBSET_SIMPLE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (split_tac));
202 (((((use_arg_then2 ("set_of_face_meeting_node", [set_of_face_meeting_node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"]) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
203 ((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
204 (((((use_arg_then2 ("IN_DIFF", [IN_DIFF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"]) THEN (case THEN (move ["f_in"])) THEN (move ["_"]));
205 ((((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN ((use_arg_then2 ("f", [])) (disch_tac [])) THEN (clear_assumption "f") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_tau", [lp_tau]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("contravening_lp_tau", [contravening_lp_tau]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
208 (* Finalization of the section Tgt *)
209 let tausum_upper_bound = Sections.finalize_theorem tausum_upper_bound;;
210 Sections.end_section "Tgt";;
212 (* Finalization of the section SumEqs *)
213 let anglesum = Sections.finalize_theorem anglesum;;
214 let anglesum_lo_approx = Sections.finalize_theorem anglesum_lo_approx;;
215 let anglesum_hi_approx = Sections.finalize_theorem anglesum_hi_approx;;
216 let tausum_eq = Sections.finalize_theorem tausum_eq;;
217 let tausum_triangles = Sections.finalize_theorem tausum_triangles;;
218 let tausum_upper_bound = Sections.finalize_theorem tausum_upper_bound;;
219 Sections.end_section "SumEqs";;
222 Sections.begin_section "Ineqs";;
225 Sections.add_section_lemma "y_bounds" (Sections.section_proof ["d"]
226 `d IN dart_of_fan (V,ESTD V)
227 ==> &2 <= y1_fan d /\ &2 <= y2_fan d /\ &2 <= y3_fan (V,ESTD V) d
228 /\ &2 <= y4_fan (V,ESTD V) d /\ &2 <= y5_fan (V,ESTD V) d /\ &2 <= y6_fan d
229 /\ &2 <= y8_fan (V,ESTD V) d /\ &2 <= y9_fan (V,ESTD V) d
230 /\ y1_fan d <= #2.52 /\ y2_fan d <= #2.52 /\ y3_fan (V,ESTD V) d <= #2.52
231 /\ y4_fan (V,ESTD V) d <= #2.52 /\ y5_fan (V,ESTD V) d <= #2.52 /\ y6_fan d <= #2.52
232 /\ y8_fan (V,ESTD V) d <= #2.52 /\ y9_fan (V,ESTD V) d <= #2.52`
234 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"]) THEN (move ["d_in"])));
235 ((((fun arg_tac -> (use_arg_then2 ("y1_lo", [y1_lo])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y2_lo", [y2_lo])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y3_lo", [y3_lo]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4_lo", [y4_lo]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y5_lo", [y5_lo]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y6_lo", [y6_lo])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y8_lo", [y8_lo]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y9_lo", [y9_lo]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
236 ((((fun arg_tac -> (use_arg_then2 ("y1_hi", [y1_hi])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y2_hi", [y2_hi])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y3_hi", [y3_hi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4_hi_std2", [y4_hi_std2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y5_hi_std2", [y5_hi_std2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
237 (((((fun arg_tac -> (use_arg_then2 ("y6_hi_std2", [y6_hi_std2])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y8_hi_std", [y8_hi_std]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y9_hi_std", [y9_hi_std]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
241 Sections.add_section_lemma "eqs" (Sections.section_proof []
242 `#2.0 = &2 /\ &2 * h0 = #2.52 /\ #0.0 = &0 /\ #5.04 = &4 * h0`
244 ((((use_arg_then2 ("Sphere.h0", [Sphere.h0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
247 (* Section A_azim3 *)
248 Sections.begin_section "A_azim3";;
249 (Sections.add_section_var (mk_var ("p", (`:num`))); Sections.add_section_var (mk_var ("q", (`:num`))); Sections.add_section_var (mk_var ("r", (`:num`))));;
252 Sections.begin_section "Lo";;
253 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "5735387903")).ineq));;
256 let azimp_lo = Sections.section_proof ["d"]
257 `d IN dart_of_fan (V,ESTD V)
258 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
260 ==> #0.852 <= a_azim ((=) 3) V d`
262 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["neq"])));
263 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
264 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
265 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_RMUL", [SUM_RMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
266 (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"]));
267 ((((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
268 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"])));
269 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
270 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
271 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(gsym_then (thm_tac (new_rewrite [] []))))));
272 (in_tac ["ineq"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ineq.dart_std3", [Ineq.dart_std3]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] [])))))));
273 ((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
274 (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
277 (* Finalization of the section Lo *)
278 let azimp_lo = Sections.finalize_theorem azimp_lo;;
279 Sections.end_section "Lo";;
282 Sections.begin_section "Hi";;
283 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "5490182221")).ineq));;
286 let azimp_hi = Sections.section_proof ["d"]
287 `d IN dart_of_fan (V,ESTD V)
288 ==> a_azim ((=) 3) V d <= #1.9`
290 ((BETA_TAC THEN (move ["d_in"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
291 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
292 (((fun arg_tac -> arg_tac (Arg_term (`CARD s = 0`))) (disch_eq_tac "card0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
293 (((((use_arg_then2 ("card0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_INV_0", [REAL_INV_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
294 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < &(CARD s)`))) (term_tac (have_gen_tac [](move ["gt0"])))) (((((use_arg_then2 ("REAL_LT_LE", [REAL_LT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_OF_NUM_EQ", [REAL_OF_NUM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
295 ((((fun arg_tac -> (use_arg_then2 ("REAL_LE_LMUL_EQ", [REAL_LE_LMUL_EQ])) (fun fst_arg -> (use_arg_then2 ("gt0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))));
296 (((((use_arg_then2 ("SUM_BOUND", [SUM_BOUND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]));
297 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
298 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
299 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"])));
300 ((THENL_LAST) (((use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`#1.893`))) (term_tac exists_tac)) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
301 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))));
302 (in_tac ["ineq"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ineq.dart_std3", [Ineq.dart_std3]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] [])))))));
303 ((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
304 (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
307 (* Finalization of the section Hi *)
308 let azimp_hi = Sections.finalize_theorem azimp_hi;;
309 Sections.end_section "Hi";;
311 (* Finalization of the section A_azim3 *)
312 let azimp_lo = Sections.finalize_theorem azimp_lo;;
313 let azimp_hi = Sections.finalize_theorem azimp_hi;;
314 Sections.end_section "A_azim3";;
316 (* Section A_azim4_excep *)
317 Sections.begin_section "A_azim4_excep";;
318 (Sections.add_section_var (mk_var ("p", (`:num`))); Sections.add_section_var (mk_var ("q", (`:num`))); Sections.add_section_var (mk_var ("r", (`:num`))));;
321 Sections.begin_section "Lo";;
322 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "2570626711")).ineq));;
325 let azimq_lo = Sections.section_proof ["d"]
326 `d IN dart_of_fan (V,ESTD V)
327 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
329 ==> #1.15 <= a_azim ((=) 4) V d`
331 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["neq"])));
332 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
333 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
334 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_RMUL", [SUM_RMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
335 (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"]) THEN (simp_tac));
336 ((((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
337 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan2"])));
338 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
339 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
340 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(gsym_then (thm_tac (new_rewrite [] []))))));
341 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Tame_inequalities.DIH_Y_INEQ))) (fun fst_arg -> (use_arg_then2 ("ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y1_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y2_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y3_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y4'_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y5_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y6_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
342 (((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (ANTS_TAC));
343 ((repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_hi", [y4'_hi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y4'_lo_2h0", [y4'_lo_2h0])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`CARD (face H x)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
344 (((((use_arg_then2 ("h_fan", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_x", [])) (disch_tac [])) THEN (clear_assumption "card_x") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
345 (case THEN ((TRY done_tac)));
346 (((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN ((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
347 ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ys_eq", [ys_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
348 ((((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("REAL_NOT_LE", [REAL_NOT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Tame_lemmas.fully_surrounded_delta_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
352 let azimr_lo = Sections.section_proof ["d"]
353 `d IN dart_of_fan (V,ESTD V)
354 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
356 ==> #1.15 <= a_azim ((<=) 5) V d`
358 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["neq"])));
359 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] []))));
360 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
361 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_RMUL", [SUM_RMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
362 (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"]) THEN (simp_tac));
363 ((((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
364 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan2"])));
365 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
366 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
367 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(gsym_then (thm_tac (new_rewrite [] []))))));
368 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Tame_inequalities.DIH_Y_INEQ))) (fun fst_arg -> (use_arg_then2 ("ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y1_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y2_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y3_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y4'_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y5_fan (V,ESTD V) x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y6_fan x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
369 (((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (ANTS_TAC));
370 ((repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_hi", [y4'_hi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y4'_lo_2h0", [y4'_lo_2h0])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`CARD (face H x)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
371 (((((use_arg_then2 ("h_fan", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_in", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_x", [])) (disch_tac [])) THEN (clear_assumption "card_x") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
372 (case THEN ((TRY done_tac)));
373 (((use_arg_then2 ("x_in", [])) (disch_tac [])) THEN (clear_assumption "x_in") THEN ((use_arg_then2 ("x", [])) (disch_tac [])) THEN (clear_assumption "x") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
374 ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ys_eq", [ys_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
375 ((((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("REAL_NOT_LE", [REAL_NOT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE Tame_lemmas.fully_surrounded_delta_pos)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
378 (* Finalization of the section Lo *)
379 let azimq_lo = Sections.finalize_theorem azimq_lo;;
380 let azimr_lo = Sections.finalize_theorem azimr_lo;;
381 Sections.end_section "Lo";;
384 Sections.begin_section "Hi";;
387 let azimq_hi = Sections.section_proof ["d"]
388 `d IN dart_of_fan (V,ESTD V)
389 ==> a_azim ((=) 4) V d <= pi`
391 ((BETA_TAC THEN (move ["d_in"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
392 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
393 (((fun arg_tac -> arg_tac (Arg_term (`CARD s = 0`))) (disch_eq_tac "card0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
394 (((((use_arg_then2 ("card0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_INV_0", [REAL_INV_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PI_POS", [PI_POS])) (disch_tac [])) THEN (clear_assumption "PI_POS") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
395 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < &(CARD s)`))) (term_tac (have_gen_tac [](move ["gt0"])))) (((((use_arg_then2 ("REAL_LT_LE", [REAL_LT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_OF_NUM_EQ", [REAL_OF_NUM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
396 ((((fun arg_tac -> (use_arg_then2 ("REAL_LE_LMUL_EQ", [REAL_LE_LMUL_EQ])) (fun fst_arg -> (use_arg_then2 ("gt0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))));
397 (((((use_arg_then2 ("SUM_BOUND", [SUM_BOUND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]));
398 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
399 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
400 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"])));
401 ((((use_arg_then2 ("azim_hi", [azim_hi]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
404 (* Lemma azimq_hi_approx *)
405 let azimq_hi_approx = Sections.section_proof ["d"]
406 `d IN dart_of_fan (V,ESTD V)
407 ==> a_azim ((=) 4) V d <= #3.141593`
409 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("azimq_hi", [azimq_hi])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((use_arg_then2 ("PI_APPROX_32", [PI_APPROX_32])) (disch_tac [])) THEN (clear_assumption "PI_APPROX_32") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
413 let azimr_hi = Sections.section_proof ["d"]
414 `d IN dart_of_fan (V,ESTD V)
415 ==> a_azim ((<=) 5) V d <= pi`
417 ((BETA_TAC THEN (move ["d_in"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))));
418 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
419 (((fun arg_tac -> arg_tac (Arg_term (`CARD s = 0`))) (disch_eq_tac "card0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
420 (((((use_arg_then2 ("card0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_INV_0", [REAL_INV_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PI_POS", [PI_POS])) (disch_tac [])) THEN (clear_assumption "PI_POS") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
421 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < &(CARD s)`))) (term_tac (have_gen_tac [](move ["gt0"])))) (((((use_arg_then2 ("REAL_LT_LE", [REAL_LT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_OF_NUM_EQ", [REAL_OF_NUM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
422 ((((fun arg_tac -> (use_arg_then2 ("REAL_LE_LMUL_EQ", [REAL_LE_LMUL_EQ])) (fun fst_arg -> (use_arg_then2 ("gt0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))));
423 (((((use_arg_then2 ("SUM_BOUND", [SUM_BOUND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]));
424 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["x_in"]))));
425 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
426 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"])));
427 ((((use_arg_then2 ("azim_hi", [azim_hi]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
430 (* Finalization of the section Hi *)
431 let azimq_hi = Sections.finalize_theorem azimq_hi;;
432 let azimq_hi_approx = Sections.finalize_theorem azimq_hi_approx;;
433 let azimr_hi = Sections.finalize_theorem azimr_hi;;
434 Sections.end_section "Hi";;
436 (* Finalization of the section A_azim4_excep *)
437 let azimq_lo = Sections.finalize_theorem azimq_lo;;
438 let azimr_lo = Sections.finalize_theorem azimr_lo;;
439 let azimq_hi = Sections.finalize_theorem azimq_hi;;
440 let azimq_hi_approx = Sections.finalize_theorem azimq_hi_approx;;
441 let azimr_hi = Sections.finalize_theorem azimr_hi;;
442 Sections.end_section "A_azim4_excep";;
445 Sections.begin_section "A_tau";;
446 (Sections.add_section_var (mk_var ("p", (`:num`))); Sections.add_section_var (mk_var ("q", (`:num`))); Sections.add_section_var (mk_var ("r", (`:num`))));;
447 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
450 let taup_lo = Sections.section_proof ["d"]
451 `d IN dart_of_fan (V,ESTD V)
452 ==> &0 <= a_tau ((=) 3) V d`
454 ((BETA_TAC THEN (move ["d_in"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
455 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
456 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_MUL", [REAL_LE_MUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
457 (((((use_arg_then2 ("SUM_POS_LE", [SUM_POS_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_f"]) THEN (simp_tac));
458 (((((fun arg_tac -> (use_arg_then2 ("ineq_tau3_tauVEF_std", [ineq_tau3_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
459 ((BETA_TAC THEN (move ["v1"]) THEN (move ["v2"]) THEN (move ["v3"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
460 ((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
461 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
465 let tauq_lo = Sections.section_proof ["d"]
466 `d IN dart_of_fan (V,ESTD V)
467 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
469 ==> #0.206 <= a_tau ((=) 4) V d`
471 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["neq"])));
472 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`4`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
473 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
474 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_RMUL", [SUM_RMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
475 (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in"])) THEN (move ["card_x"]) THEN (simp_tac));
476 ((((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
477 (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau4_tauVEF_std", [ineq_tau4_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
478 ((BETA_TAC THEN (move ["v1"]) THEN (move ["v2"]) THEN (move ["v3"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
479 ((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_x", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
480 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
484 let taur_lo = Sections.section_proof ["d"]
485 `d IN dart_of_fan (V,ESTD V)
486 /\ (p,q,r) = type_of_node (hypermap_of_fan (V,ESTD V)) d
488 ==> #0.4819 <= a_tau ((<=) 5) V d`
490 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("GE", [GE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["neq"])));
491 (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] []))));
492 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
493 ((((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_RMUL", [SUM_RMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("finite_sets", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
494 (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]) THEN (simp_tac));
495 ((((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_RMUL", [REAL_LE_RMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_INV", [REAL_LE_INV]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
496 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart H`))) (term_tac (have_gen_tac [](move ["x_in"]))));
497 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
498 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Crttxat_tame.CRTTXAT", [Crttxat_tame.CRTTXAT])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_perimeter_bound", [fully_surrounded_perimeter_bound])) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("Jgtdebu.JGTDEBU4", [Jgtdebu.JGTDEBU4])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
499 (((((use_arg_then2 ("tame_9a", [tame_9a]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))) THEN (move ["card_f_ineq"]));
500 ((fun arg_tac -> arg_tac (Arg_term (`CARD (face H x) = 5 \/ CARD (face H x) = 6`))) (term_tac (have_gen_tac []ALL_TAC)));
501 ((((use_arg_then2 ("card_x", [])) (disch_tac [])) THEN (clear_assumption "card_x") THEN ((fun arg_tac -> (use_arg_then2 ("card_f_ineq", [])) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
502 (case THEN (move ["card_eq"]));
503 (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau5_tauVEF_std", [ineq_tau5_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
504 ((BETA_TAC THEN (move ["v1"]) THEN (move ["v2"]) THEN (move ["v3"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
505 (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
506 ((THENL_FIRST) ((((use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`#0.712`))) (term_tac exists_tac)) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
507 (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau6_tauVEF_std", [ineq_tau6_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
508 ((BETA_TAC THEN (move ["v1"]) THEN (move ["v2"]) THEN (move ["v3"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
509 (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
512 (* Finalization of the section A_tau *)
513 let taup_lo = Sections.finalize_theorem taup_lo;;
514 let tauq_lo = Sections.finalize_theorem tauq_lo;;
515 let taur_lo = Sections.finalize_theorem taur_lo;;
516 Sections.end_section "A_tau";;
519 Sections.begin_section "Case50";;
520 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
521 (Sections.add_section_hyp "ineq1" ((hd (Ineq.getexact "4652969746 1")).ineq));;
522 (Sections.add_section_hyp "ineq2" ((hd (Ineq.getexact "4652969746 2")).ineq));;
524 (* Lemma case50_ineq *)
525 let case50_ineq = Sections.section_proof ["d"]
526 `d IN dart_of_fan (V,ESTD V)
527 /\ type_of_node (hypermap_of_fan (V,ESTD V)) d = (5,0,0)
528 ==> #0.04 <= &5 * a_tau ((=) 3) V d`
530 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN ((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))));
531 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
532 ((fun arg_tac -> arg_tac (Arg_term (`CARD (GSPEC _)`))) (term_tac (set_tac "q")));
533 ((fun arg_tac -> arg_tac (Arg_term (`CARD (GSPEC _)`))) (term_tac (set_tac "r")));
534 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`FINITE s`))) (term_tac (have_gen_tac [](move ["fin_s"])))) ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
535 ((BETA_TAC THEN (move ["eqs"])) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqs", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
536 ((fun arg_tac -> arg_tac (Arg_term (`y IN s ==> y IN darts_k 3 (hypermap_of_fan (V,ESTD V))`))) (term_tac (have_gen_tac ["y"](move ["in_s3"]))));
537 (((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["y_in_n"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
538 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
539 ((fun arg_tac -> arg_tac (Arg_term (`y IN s ==> y IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac ["y"](move ["in_s"]))));
540 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("in_s3", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
541 ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`!y. y IN s ==> y4_fan (V,ESTD V) y <= #2.1771`))) (disch_eq_tac "y4_ge" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
542 ((((use_arg_then2 ("y4_ge", [])) (disch_tac [])) THEN (clear_assumption "y4_ge") THEN BETA_TAC) THEN (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IMP", [NOT_IMP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NOT_LE", [REAL_NOT_LE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in_s"])) THEN (move ["x_ineq"])));
543 ((((fun arg_tac -> (use_arg_then2 ("INSERT_DELETE", [INSERT_DELETE])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_CLAUSES", [SUM_CLAUSES]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_DELETE", [FINITE_DELETE]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
544 ((THENL_ROT (-1)) (((((use_arg_then2 ("IN_DELETE", [IN_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_LE_ADD2", [REAL_LE_ADD2]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)));
545 (((((use_arg_then2 ("SUM_POS_LE", [SUM_POS_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_DELETE", [FINITE_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_DELETE", [IN_DELETE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (case THEN (move ["y_in_s"])) THEN (move ["_"]) THEN (simp_tac));
546 ((((fun arg_tac -> (use_arg_then2 ("ineq_tau3_tauVEF_std", [ineq_tau3_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("in_s3", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
547 ((BETA_TAC THEN (move ["v1"]) THEN (move ["v2"]) THEN (move ["v3"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
548 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan2"])));
549 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("dart3_tauVEF_eq_taum", [dart3_tauVEF_eq_taum])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_s3", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
550 (in_tac ["ineq1"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(thm_tac (new_rewrite [] []))))));
551 ((fun arg_tac -> (use_arg_then2 ("in_s", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["x_in"])));
552 (((((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineq1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
553 (((use_arg_then2 ("REAL_SUB_RZERO", [REAL_SUB_RZERO]))(gsym_then (thm_tac (new_rewrite [] [(`sum s _`)])))));
554 ((fun arg_tac -> arg_tac (Arg_term (`&0 = #0.312 * sum s (\y. azim_dart (V,ESTD V) y - &2 * pi / &5)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
555 (((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ENTIRE", [REAL_ENTIRE]))(thm_tac (new_rewrite [] []))))) THEN (DISJ2_TAC));
556 ((((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("SUM_CONST", [SUM_CONST])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&2 * pi / &5`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_SUB_0", [REAL_SUB_0]))(thm_tac (new_rewrite [] [])))));
557 ((THENL_FIRST) (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("anglesum", [anglesum])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`CARD s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("q", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("r", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)) ((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
558 ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_MUL_LZERO", [REAL_MUL_LZERO]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("REAL_ADD_RID", [REAL_ADD_RID]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqs", []))(gsym_then (thm_tac (new_rewrite [1] []))))));
559 ((((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("ETA_AX", [ETA_AX])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`azim_dart _`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
560 ((((use_arg_then2 ("SUM_LMUL", [SUM_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_SUB", [SUM_SUB]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
561 ((((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_NEG", [SUM_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_BOUND_GEN", [SUM_BOUND_GEN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fin_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
562 ((THENL_FIRST) (((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
563 (BETA_TAC THEN (move ["x"]) THEN (move ["x_in_s"]) THEN (simp_tac));
564 ((((use_arg_then2 ("REAL_LE_NEG", [REAL_LE_NEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_NEG_NEG", [REAL_NEG_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_LMUL", [REAL_NEG_LMUL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_NEG", [REAL_NEG_NEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_div", [real_div]))(gsym_then (thm_tac (new_rewrite [] []))))));
565 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan2"])));
566 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("dart3_tauVEF_eq_taum", [dart3_tauVEF_eq_taum])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_s3", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))));
567 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_s", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_s3", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
568 (in_tac ["ineq2"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(thm_tac (new_rewrite [] []))))));
569 (((((use_arg_then2 ("ineq2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 11 0 (((fun arg_tac -> (use_arg_then2 ("y_bounds", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_s", [])) (fun fst_arg -> (use_arg_then2 ("x_in_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y4_ge", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
572 (* Finalization of the section Case50 *)
573 let case50_ineq = Sections.finalize_theorem case50_ineq;;
574 Sections.end_section "Case50";;
577 Sections.add_section_lemma "aux_ge" (Sections.section_proof ["a"]
580 ((arith_tac) THEN (done_tac));
584 Sections.add_section_lemma "aux_ineq" (Sections.section_proof ["n";"a";"b";"d"]
585 `(!x. x IN darts_k n (hypermap_of_fan (V,ESTD V))
586 ==> tauVEF (V,ESTD V,face (hypermap_of_fan (V,ESTD V)) x)
587 + a * azim_dart (V,ESTD V) x + b >= &0)
588 /\ d IN dart_of_fan (V,ESTD V) /\
589 ~(CARD {y | y IN node (hypermap_of_fan (V,ESTD V)) d
590 /\ CARD (face (hypermap_of_fan (V,ESTD V)) y) = n} = 0)
591 ==> &0 <= a_tau ((=) n) V d + a * a_azim ((=) n) V d + b`
593 (BETA_TAC THEN (case THEN (move ["ineq"])) THEN (case THEN (move ["d_in"])) THEN (move ["card_n0"]));
594 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_tau)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (let_RULE a_azim)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("eq_sym", [eq_sym])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
595 ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H")));
596 ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s")));
597 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`FINITE s`))) (term_tac (have_gen_tac [](move ["fin_s"])))) ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
598 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`&0 < &(CARD s)`))) (term_tac (have_gen_tac [](move ["gt0"])))) (((((use_arg_then2 ("REAL_LT_LE", [REAL_LT_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_POS", [REAL_POS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_OF_NUM_EQ", [REAL_OF_NUM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
599 ((((fun arg_tac -> (use_arg_then2 ("REAL_LE_LMUL_EQ", [REAL_LE_LMUL_EQ])) (fun fst_arg -> (use_arg_then2 ("gt0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_MUL_RZERO", [REAL_MUL_RZERO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_LDISTRIB", [REAL_ADD_LDISTRIB]))(thm_tac (new_rewrite [] [])))));
600 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x * (a * z + b) = a * (x * z) + x * b:real`))) (term_tac (have_gen_tac ["x"; "z"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
601 ((repeat_tactic 1 9 (((use_arg_then2 ("a_sum_mul", [a_sum_mul]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUM_CONST", [SUM_CONST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUM_LMUL", [SUM_LMUL]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SUM_ADD", [SUM_ADD]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUM_ADD", [SUM_ADD]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
602 (((((fun arg_tac -> (use_arg_then2 ("SUM_POS_LE", [SUM_POS_LE])) (fun fst_arg -> (use_arg_then2 ("fin_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_in_n"])) THEN (move ["card_x"]));
603 ((((use_arg_then2 ("real_ge", [real_ge]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))));
604 ((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_x", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
605 ((((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_subset", [lemma_node_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN apply_tac) THEN (done_tac));
609 Sections.begin_section "P1";;
610 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "3296257235")).ineq));;
613 let p1_ineq = Sections.section_proof ["d"]
614 `d IN dart_of_fan (V,ESTD V)
615 /\ ~(FST (type_of_node (hypermap_of_fan (V,ESTD V)) d) = 0)
616 ==> #0.77 <= a_tau ((=) 3) V d + #0.626 * a_azim ((=) 3) V d`
618 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] []))))));
619 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (move ["neq0"])));
620 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in3"])) THEN ((((use_arg_then2 ("aux_ge", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))));
621 ((((use_arg_then2 ("x_in3", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
622 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (move ["h_fan"])));
623 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart3_tauVEF_eq_taum", [dart3_tauVEF_eq_taum]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
624 (in_tac ["ineq"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ineq.dart_std3", [Ineq.dart_std3]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] [])))))));
625 (((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
628 (* Finalization of the section P1 *)
629 let p1_ineq = Sections.finalize_theorem p1_ineq;;
630 Sections.end_section "P1";;
633 Sections.begin_section "P2";;
634 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "8519146937")).ineq));;
637 let p2_ineq = Sections.section_proof ["d"]
638 `d IN dart_of_fan (V,ESTD V)
639 /\ ~(FST (type_of_node (hypermap_of_fan (V,ESTD V)) d) = 0)
640 ==> -- #0.32 <= a_tau ((=) 3) V d - #0.259 * a_azim ((=) 3) V d`
642 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_NEG", [REAL_NEG_NEG]))(thm_tac (new_rewrite [] [])))));
643 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["neq0"])));
644 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in3"])) THEN (((use_arg_then2 ("aux_ge", []))(thm_tac (new_rewrite [] [])))));
645 ((((use_arg_then2 ("x_in3", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
646 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN (((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["h_fan"])));
647 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart3_tauVEF_eq_taum", [dart3_tauVEF_eq_taum]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
648 (in_tac ["ineq"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ineq.dart_std3", [Ineq.dart_std3]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] [])))))));
649 (((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
652 (* Finalization of the section P2 *)
653 let p2_ineq = Sections.finalize_theorem p2_ineq;;
654 Sections.end_section "P2";;
657 Sections.begin_section "P3";;
658 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "4667071578")).ineq));;
661 let p3_ineq = Sections.section_proof ["d"]
662 `d IN dart_of_fan (V,ESTD V)
663 /\ ~(FST (type_of_node (hypermap_of_fan (V,ESTD V)) d) = 0)
664 ==> -- #0.724 <= a_tau ((=) 3) V d - #0.507 * a_azim ((=) 3) V d`
666 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_NEG", [REAL_NEG_NEG]))(thm_tac (new_rewrite [] [])))));
667 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["neq0"])));
668 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in3"])) THEN (((use_arg_then2 ("aux_ge", []))(thm_tac (new_rewrite [] [])))));
669 ((((use_arg_then2 ("x_in3", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
670 ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN (clear_assumption "h_fan") THEN BETA_TAC) THEN (((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["h_fan"])));
671 ((((use_arg_then2 ("azim_fan_eq_dih_y", [azim_fan_eq_dih_y]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart3_tauVEF_eq_taum", [dart3_tauVEF_eq_taum]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y4'_eq_y4", [y4'_eq_y4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
672 (in_tac ["ineq"] false ((((use_arg_then2 ("INEQ_ALT", [INEQ_ALT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ineq.dart_std3", [Ineq.dart_std3]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL ALL)))(thm_tac (new_rewrite [] [])))))));
673 (((((use_arg_then2 ("ineq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
676 (* Finalization of the section P3 *)
677 let p3_ineq = Sections.finalize_theorem p3_ineq;;
678 Sections.end_section "P3";;
681 Sections.begin_section "Q1";;
682 (Sections.add_section_hyp "ineq1" ((hd (Ineq.getexact "7043724150 a")).ineq));;
683 (Sections.add_section_hyp "ineq2" ((hd (Ineq.getexact "7043724150 a reduced v2")).ineq));;
684 (Sections.add_section_hyp "ineq3" ((hd (Ineq.getexact "3287695934")).ineq));;
687 let q1_ineq = Sections.section_proof ["d"]
688 `d IN dart_of_fan (V,ESTD V)
689 /\ ~(FST (SND (type_of_node (hypermap_of_fan (V,ESTD V)) d)) = 0)
690 ==> #6.248 <= a_tau ((=) 4) V d + #4.72 * a_azim ((=) 4) V d`
692 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] []))))));
693 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (move ["neq0"])));
694 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in4"]));
695 ((((use_arg_then2 ("x_in4", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
696 (((((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ineq122_tauVEF", [ineq122_tauVEF])) (fun fst_arg -> (use_arg_then2 ("ineq1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
699 (* Finalization of the section Q1 *)
700 let q1_ineq = Sections.finalize_theorem q1_ineq;;
701 Sections.end_section "Q1";;
704 Sections.begin_section "Q2";;
705 (Sections.add_section_hyp "ineq1" ((hd (Ineq.getexact "6944699408 a")).ineq));;
706 (Sections.add_section_hyp "ineq2" ((hd (Ineq.getexact "6944699408 a reduced")).ineq));;
707 (Sections.add_section_hyp "ineq3" ((hd (Ineq.getexact "3287695934")).ineq));;
710 let q2_ineq = Sections.section_proof ["d"]
711 `d IN dart_of_fan (V,ESTD V)
712 /\ ~(FST (SND (type_of_node (hypermap_of_fan (V,ESTD V)) d)) = 0)
713 ==> #1.707 <= a_tau ((=) 4) V d + #0.972 * a_azim ((=) 4) V d`
715 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] []))))));
716 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (move ["neq0"])));
717 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in4"]));
718 ((((use_arg_then2 ("x_in4", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
719 (((((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ineq121_tauVEF", [ineq121_tauVEF])) (fun fst_arg -> (use_arg_then2 ("ineq1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
722 (* Finalization of the section Q2 *)
723 let q2_ineq = Sections.finalize_theorem q2_ineq;;
724 Sections.end_section "Q2";;
727 Sections.begin_section "Q3";;
728 (Sections.add_section_hyp "ineq1" ((hd (Ineq.getexact "4240815464 a")).ineq));;
729 (Sections.add_section_hyp "ineq2" ((hd (Ineq.getexact "4240815464 a reduced")).ineq));;
730 (Sections.add_section_hyp "ineq3" ((hd (Ineq.getexact "3287695934")).ineq));;
733 let q3_ineq = Sections.section_proof ["d"]
734 `d IN dart_of_fan (V,ESTD V)
735 /\ ~(FST (SND (type_of_node (hypermap_of_fan (V,ESTD V)) d)) = 0)
736 ==> #1.433 <= a_tau ((=) 4) V d + #0.7573 * a_azim ((=) 4) V d`
738 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] []))))));
739 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (move ["neq0"])));
740 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in4"]));
741 ((((use_arg_then2 ("x_in4", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
742 (((((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ineq120_tauVEF", [ineq120_tauVEF])) (fun fst_arg -> (use_arg_then2 ("ineq1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineq3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
745 (* Finalization of the section Q3 *)
746 let q3_ineq = Sections.finalize_theorem q3_ineq;;
747 Sections.end_section "Q3";;
750 Sections.begin_section "Q4";;
751 (Sections.add_section_hyp "h_main" ((hd (Ineq.getexact "3862621143 revised")).ineq));;
752 (Sections.add_section_hyp "h_reduced" ((hd (Ineq.getexact "3862621143 side")).ineq));;
753 (Sections.add_section_hyp "h_front" ((hd (Ineq.getexact "3862621143 front")).ineq));;
754 (Sections.add_section_hyp "h_back" ((hd (Ineq.getexact "3862621143 back")).ineq));;
755 (Sections.add_section_hyp "h_back2" ((hd (Ineq.getexact "6988401556")).ineq));;
756 (Sections.add_section_hyp "h_y4" ((hd (Ineq.getexact "3287695934")).ineq));;
759 let q4_ineq = Sections.section_proof ["d"]
760 `d IN dart_of_fan (V,ESTD V)
761 /\ ~(FST (SND (type_of_node (hypermap_of_fan (V,ESTD V)) d)) = 0)
762 ==> -- #0.777 <= a_tau ((=) 4) V d - #0.453 * a_azim ((=) 4) V d`
764 ((((use_arg_then2 ("REAL_SUB_LE", [REAL_SUB_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NEG_NEG", [REAL_NEG_NEG]))(thm_tac (new_rewrite [] [])))));
765 ((BETA_TAC THEN (case THEN (move ["d_in"]))) THEN (((((use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["neq0"])));
766 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("aux_ineq", [])) (fun fst_arg -> (use_arg_then2 ("neq0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac) THEN (move ["x"]) THEN (move ["x_in4"])) THEN ((((use_arg_then2 ("REAL_ADD_ASSOC", [REAL_ADD_ASSOC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_MUL_LNEG", [REAL_MUL_LNEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_sub", [real_sub]))(gsym_then (thm_tac (new_rewrite [] [])))))));
767 ((((use_arg_then2 ("x_in4", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["_"])));
768 (((((use_arg_then2 ("ineq119_tauVEF", [ineq119_tauVEF]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("y_bounds", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
771 (* Finalization of the section Q4 *)
772 let q4_ineq = Sections.finalize_theorem q4_ineq;;
773 Sections.end_section "Q4";;
775 (* Finalization of the section Ineqs *)
776 let azimp_lo = Sections.finalize_theorem azimp_lo;;
777 let azimp_hi = Sections.finalize_theorem azimp_hi;;
778 let azimq_lo = Sections.finalize_theorem azimq_lo;;
779 let azimr_lo = Sections.finalize_theorem azimr_lo;;
780 let azimq_hi = Sections.finalize_theorem azimq_hi;;
781 let azimq_hi_approx = Sections.finalize_theorem azimq_hi_approx;;
782 let azimr_hi = Sections.finalize_theorem azimr_hi;;
783 let taup_lo = Sections.finalize_theorem taup_lo;;
784 let tauq_lo = Sections.finalize_theorem tauq_lo;;
785 let taur_lo = Sections.finalize_theorem taur_lo;;
786 let case50_ineq = Sections.finalize_theorem case50_ineq;;
787 let p1_ineq = Sections.finalize_theorem p1_ineq;;
788 let p2_ineq = Sections.finalize_theorem p2_ineq;;
789 let p3_ineq = Sections.finalize_theorem p3_ineq;;
790 let q1_ineq = Sections.finalize_theorem q1_ineq;;
791 let q2_ineq = Sections.finalize_theorem q2_ineq;;
792 let q3_ineq = Sections.finalize_theorem q3_ineq;;
793 let q4_ineq = Sections.finalize_theorem q4_ineq;;
794 Sections.end_section "Ineqs";;
796 let imp_th = (UNDISCH o MATCH_MP EQ_IMP) kcblrqc_ineq_def in
797 let ths = CONJUNCTS imp_th in
799 itlist PROVE_HYP ths th;;
801 let r = add_ineqs_hyp o UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP] o let_RULE in
802 let neg = ONCE_REWRITE_RULE[GSYM REAL_LE_NEG] in
803 let move_l = ONCE_REWRITE_RULE[GSYM REAL_SUB_0] in
805 "anglesum_lo", r anglesum_lo_approx;
806 "anglesum_hi", (neg o r) anglesum_hi_approx;
807 "tausum", (SYM o move_l o r) tausum_eq;
808 "azimp_lo", (r o r) azimp_lo;
809 "azimp_hi", (neg o r o r) azimp_hi;
810 "azimq_lo", (r o r) azimq_lo;
811 "azimq_hi", (neg o r o r) azimq_hi_approx;
812 "azimr_lo", (r o r) azimr_lo;
813 "azimr_hi", (neg o r o r) azimr_hi;
814 "taup_lo", (r o r) taup_lo;
815 "tauq_lo", (r o r) tauq_lo;
816 "taur_lo", (r o r) taur_lo;
817 "case50", (r o r) case50_ineq;
818 "p1", (r o r) p1_ineq;
819 "p2", (r o r) p2_ineq;
820 "p3", (r o r) p3_ineq;
821 "q1", (r o r) q1_ineq;
822 "q2", (r o r) q2_ineq;
823 "q3", (r o r) q3_ineq;
824 "q4", (r o r) q4_ineq;
825 "tausum_tri", (SYM o move_l o r) tausum_triangles;
826 "tausum_hi", (neg o r o r) tausum_upper_bound;
828 let mul_ineq c_tm ineq_th =
829 if (is_eq (concl ineq_th)) then
830 AP_TERM (mk_comb (`( * ):real->real->real`, c_tm)) ineq_th
832 let pos_ineq = REAL_ARITH (mk_binary "real_le" (`&0`, c_tm)) in
833 MATCH_MP REAL_LE_LMUL (CONJ pos_ineq ineq_th);;
834 let add_ineqs th1 th2 = MATCH_MP REAL_LE_ADD2 (CONJ th1 th2);;
835 let get_ineq (p,q,r) (name, c_tm) =
836 let p_tm = mk_small_numeral p and
837 q_tm = mk_small_numeral q and
838 r_tm = mk_small_numeral r in
839 let th0 = assoc name ineq_table in
840 let type_tm = mk_pair (p_tm, mk_pair (q_tm, r_tm)) in
841 let type_th = ASSUME (mk_eq (`type_of_node (hypermap_of_fan (V,ESTD V)) d`, type_tm)) in
842 let th1 = (DISCH_ALL o INST[p_tm, `p:num`; q_tm, `q:num`; r_tm, `r:num`]) th0 in
843 let th2 = (UNDISCH_ALL o REWRITE_RULE[type_th; ARITH]) th1 in
844 let th3 = mul_ineq c_tm th2 in
845 if (is_eq (concl th3)) then
846 MATCH_MP REAL_EQ_IMP_LE th3
850 (4,0,0), ["anglesum_lo", `#0.259`; "p2", `#4.0`];
851 (5,0,0), ["case50", `&1`];
852 (6,0,0), ["anglesum_hi", `#0.626`; "p1", `#6.0`];
853 (7,0,0), ["anglesum_hi", `#0.626`; "p1", `#7.0`];
854 (2,1,0), ["anglesum_lo", `#0.453`; "p2", `#0.435`;
855 "p3", `#1.565`; "q4", `#1.0`; "azimp_lo", `#0.00012`];
856 (3,1,0), ["anglesum_lo", `#0.259`; "p2", `#3.0`;
857 "q4", `#0.572`; "tauq_lo", `#0.428`; "azimq_lo", `#0.000116`];
858 (4,1,0), ["anglesum_hi", `#0.626`; "p1", `#4.0`;
859 "q3", `#0.8266`; "tauq_lo", `#0.1734`; "azimq_lo", `#0.00001582`];
860 (5,1,0), ["anglesum_hi", `#0.626`; "p1", `#5.0`;
861 "q3", `#0.8266`; "tauq_lo", `#0.1734`; "azimq_lo", `#0.00001582`];
862 (1,2,0), ["anglesum_lo", `#0.453`; "p2", `#0.218`;
863 "p3", `#0.782`; "q4", `#2.0`; "azimp_hi", `#0.000064`];
864 (2,2,0), ["taup_lo", `#2.0`; "tauq_lo", `#2.0`];
865 (3,2,0), ["anglesum_hi", `#0.626`; "p1", `#3.0`;
866 "q3", `#1.6532`; "tauq_lo", `#0.3468`; "azimq_lo", `#0.00003164`];
867 (0,3,0), ["tauq_lo", `#3.0`];
868 (1,3,0), ["taup_lo", `#1.0`; "tauq_lo", `#3.0`];
869 (2,3,0), ["anglesum_hi", `#0.7573`; "p1", `#2.0`;
870 "q3", `#3.0`; "azimp_lo", `#0.2626`];
871 (0,4,0), ["anglesum_hi", `#0.7573`; "q3", `#4.0`];
872 (0,5,0), ["anglesum_hi", `#0.972`; "q2", `#5.0`];
873 (1,4,0), ["anglesum_hi", `#0.7573`; "p1", `#1.0`;
874 "q3", `#4.0`; "azimp_lo", `#0.1313`];
875 (3,3,0), ["anglesum_hi", `#0.972`; "p1", `#3.0`;
876 "q2", `#3.0`; "azimp_lo", `#1.038`];
877 (4,2,0), ["anglesum_hi", `#0.7573`; "p1", `#4.0`;
878 "q3", `#2.0`; "azimp_lo", `#0.5252`];
879 (6,1,0), ["anglesum_hi", `#4.72`; "p1", `#6.0`;
880 "q1", `#1.0`; "azimp_lo", `#24.564`];
881 (3,0,3), ["anglesum_hi", `#0.626`; "p1", `#3.0`; "azimr_lo", `#1.878`;
882 "taur_lo", `#3.0`; "tausum_hi", `&1`];
883 (3,1,2), ["anglesum_hi", `#0.7573`; "p1", `#3.0`;
884 "q3", `#1.0`; "azimp_lo", `#0.3939`; "azimr_lo", `#1.5146`;
885 "taur_lo", `#2.0`; "tausum_hi", `&1`];
886 (3,2,1), ["anglesum_hi", `#0.7573`; "p1", `#3.0`;
887 "q3", `#2.0`; "azimp_lo", `#0.3939`; "azimr_lo", `#0.7573`;
888 "taur_lo", `#1.0`; "tausum_hi", `&1`];
889 (4,0,2), ["anglesum_hi", `#0.626`; "p1", `#4.0`; "azimr_lo", `#1.252`;
890 "taur_lo", `#2.0`; "tausum_hi", `&1`];
891 (4,1,1), ["anglesum_hi", `#0.626`; "p1", `#4.0`; "q3", `#0.827`;
892 "azimr_lo", `#0.626`; "tauq_lo", `#0.173`; "azimq_hi", `#0.0002871`;
893 "taur_lo", `#1.0`; "tausum_hi", `&1`];
894 (6,0,1), ["anglesum_hi", `#0.626`; "p1", `#6.0`; "azimr_lo", `#0.626`;
895 "taur_lo", `#1.0`; "tausum_hi", `&1`];
896 (5,0,1), ["anglesum_hi", `#0.626`; "p1", `#5.0`; "azimr_lo", `#0.626`;
897 "tausum", `&1`; "tausum_tri", `-- &1`];
899 let get_b_tame_ineq node_type =
900 let data = assoc node_type lp_data @ ["tausum", `-- &1`] in
901 let ths = map (get_ineq node_type) data in
902 let sum = end_itlist add_ineqs ths in
903 let conv = BINOP_CONV (NUM_REDUCE_CONV THENC REWRITE_CONV[DECIMAL] THENC REAL_POLY_CONV) in
906 (* Section KCBLRQC *)
907 Sections.begin_section "KCBLRQC";;
908 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
909 (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;
912 let KCBLRQC = Sections.section_proof ["d"]
913 `d IN dart_of_fan (V,ESTD V)
914 ==> let H = hypermap_of_fan (V,ESTD V) in
915 let (p,q,r) = type_of_node H d in
916 (r > 0) \/ (sum (set_of_face_meeting_node H d) (\f. tauVEF (V,ESTD V,f)) >= b_tame p q)`
918 ((BETA_TAC THEN (move ["d_in"])) THEN (CONV_TAC let_CONV));
919 ((THENL_FIRST) (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma])) (fun fst_arg -> (use_arg_then2 ("simpleH", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)) ((ALL_TAC) THEN (done_tac)));
920 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "p")));
921 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "q")));
922 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "r")));
923 ((BETA_TAC THEN (move ["type_eq"])) THEN (((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (CONV_TAC let_CONV));
924 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Cdtetat_tame.CDTETAT", [Cdtetat_tame.CDTETAT])) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
925 (((((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_DEF", [LET_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_END_DEF", [LET_END_DEF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["pq_in"]));
926 (((fun arg_tac -> arg_tac (Arg_term (`r > 0`))) (disch_eq_tac "r_gt0" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
927 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`r = 0`))) (term_tac (have_gen_tac [](move ["r0"])))) ((((use_arg_then2 ("r_gt0", [])) (disch_tac [])) THEN (clear_assumption "r_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
928 ((((use_arg_then2 ("type_eq", [])) (disch_tac [])) THEN (clear_assumption "type_eq") THEN ((use_arg_then2 ("pq_in", [])) (disch_tac [])) THEN (clear_assumption "pq_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("r0", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 20 0 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 20 0 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))));
929 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (0,3,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH]) THEN (arith_tac) THEN (done_tac)));
930 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (0,4,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH]) THEN (arith_tac) THEN (done_tac)));
931 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (0,5,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
932 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (1,2,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
933 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (1,3,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
934 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (1,4,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
935 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (2,1,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
936 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (2,2,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
937 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (2,3,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
938 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,1,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
939 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,2,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
940 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,3,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
941 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (4,0,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
942 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (4,1,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
943 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (4,2,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
944 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (5,0,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
945 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (5,1,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
946 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (6,0,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
947 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (6,1,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac)));
948 ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (7,0,0)))) (disch_tac [])) THEN BETA_TAC) THEN (REWRITE_TAC[b_tame; PAIR_EQ; ARITH; tgt]) THEN (arith_tac) THEN (done_tac));
951 (* Finalization of the section KCBLRQC *)
952 let KCBLRQC = Sections.finalize_theorem KCBLRQC;;
953 Sections.end_section "KCBLRQC";;
955 (* Section BDJYFFB *)
956 Sections.begin_section "BDJYFFB";;
957 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
958 (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));;
961 let BDJYFFB1 = Sections.section_proof []
962 `tame_12o (hypermap_of_fan (V,ESTD V))`
964 (((((use_arg_then2 ("tame_12o", [tame_12o]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_type_exceptional_face", [node_type_exceptional_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_exceptional_face", [node_exceptional_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("exceptional_face", [exceptional_face]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"]));
965 (((fun arg_tac -> arg_tac (Arg_term (`CARD _ >= 5`))) (disch_eq_tac "card_f" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
966 ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (V,ESTD V)`))) (term_tac (have_gen_tac [](move ["d_in"]))));
967 ((((fun arg_tac -> (use_arg_then2 ("Add_triangle.fully_surrounded_dart_of_fan_eq", [Add_triangle.fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
968 ((((fun arg_tac -> (use_arg_then2 ("CARD_FACE_GT_1", [CARD_FACE_GT_1])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", [])) (disch_tac [])) THEN (clear_assumption "card_f") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
969 ((THENL_FIRST) (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("NODE_TYPE_lemma", [NODE_TYPE_lemma])) (fun fst_arg -> (use_arg_then2 ("simpleH", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC)) ((ALL_TAC) THEN (done_tac)));
970 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "p")));
971 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "q")));
972 ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "r")));
973 (BETA_TAC THEN (move ["type_eq"]));
974 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE", [FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("simpleH", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
975 (((((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_DEF", [LET_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_END_DEF", [LET_END_DEF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["card_node_eq"]));
976 ((fun arg_tac -> arg_tac (Arg_term (`FINITE {x | x IN node (hypermap_of_fan (V,ESTD V)) d
977 /\ CARD (face (hypermap_of_fan (V,ESTD V)) x) >= 5}`))) (term_tac (have_gen_tac [](move ["fin_s"]))));
978 (((use_arg_then2 ("FINITE_SUBSET", [FINITE_SUBSET])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node (hypermap_of_fan (V,ESTD V)) d`))) (term_tac exists_tac)));
979 ((((((use_arg_then2 ("NODE_FINITE", [NODE_FINITE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["y"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
980 ((fun arg_tac -> arg_tac (Arg_term (`1 <= r`))) (term_tac (have_gen_tac [](move ["r_ge1"]))));
981 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(r = 0)`))) (term_tac (have_gen_tac []ALL_TAC)))) ((arith_tac) THEN (done_tac)));
982 ((((use_arg_then2 ("r_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
983 (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
984 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Cdtetat_tame.CDTETAT", [Cdtetat_tame.CDTETAT])) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
985 (((((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_DEF", [LET_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_END_DEF", [LET_END_DEF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["pqr_in"]));
986 ((THENL_ROT (-1)) (split_tac));
987 ((((use_arg_then2 ("r_ge1", [])) (disch_tac [])) THEN (clear_assumption "r_ge1") THEN ((use_arg_then2 ("pqr_in", [])) (disch_tac [])) THEN (clear_assumption "pqr_in") THEN BETA_TAC) THEN ((repeat_tactic 20 0 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 20 0 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))));
988 ((repeat_tactic 0 20 (case)) THEN (TRY ((arith_tac))));
989 ((BETA_TAC THEN (move ["p_eq"]) THEN (move ["qr_eq"]) THEN (move ["r_ge1"])) THEN (((use_arg_then2 ("type_eq", [])) (disch_tac [])) THEN (clear_assumption "type_eq") THEN BETA_TAC) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))));
990 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`q = 0 /\ r = 1`))) (term_tac (have_gen_tac [](case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))))) ((((use_arg_then2 ("r_ge1", [])) (disch_tac [])) THEN (clear_assumption "r_ge1") THEN ((use_arg_then2 ("qr_eq", [])) (disch_tac [])) THEN (clear_assumption "qr_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
991 ((BETA_TAC THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (6,0,1)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
992 ((((use_arg_then2 ("r_ge1", [])) (disch_tac [])) THEN (clear_assumption "r_ge1") THEN ((use_arg_then2 ("pqr_in", [])) (disch_tac [])) THEN (clear_assumption "pqr_in") THEN BETA_TAC) THEN ((repeat_tactic 20 0 (((fun arg_tac ->(use_arg_then2 ("IN_SING", [IN_SING]))(fun tmp_arg1 -> (use_arg_then2 ("IN_INSERT", [IN_INSERT]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 30 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))));
993 ((repeat_tactic 0 20 (case)) THEN (TRY ((arith_tac))));
994 ((BETA_TAC THEN (move ["p_eq"]) THEN (move ["qr_eq"]) THEN (move ["r_ge1"]) THEN (move ["_"])) THEN (((use_arg_then2 ("type_eq", [])) (disch_tac [])) THEN (clear_assumption "type_eq") THEN BETA_TAC) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))));
995 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`q = 0 /\ r = 3 \/ q = 1 /\ r = 2 \/ q = 2 /\ r = 1`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("qr_eq", [])) (disch_tac [])) THEN (clear_assumption "qr_eq") THEN ((use_arg_then2 ("r_ge1", [])) (disch_tac [])) THEN (clear_assumption "r_ge1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
996 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,0,3)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
997 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,1,2)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
998 ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (3,2,1)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
999 ((BETA_TAC THEN (move ["p_eq"]) THEN (move ["qr_eq"]) THEN (move ["r_ge1"]) THEN (move ["_"])) THEN (((use_arg_then2 ("type_eq", [])) (disch_tac [])) THEN (clear_assumption "type_eq") THEN BETA_TAC) THEN (((use_arg_then2 ("p_eq", []))(thm_tac (new_rewrite [] [])))));
1000 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`q = 0 /\ r = 2 \/ q = 1 /\ r = 1`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("qr_eq", [])) (disch_tac [])) THEN (clear_assumption "qr_eq") THEN ((use_arg_then2 ("r_ge1", [])) (disch_tac [])) THEN (clear_assumption "r_ge1") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
1001 ((THENL_FIRST) case ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (4,0,2)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
1002 ((BETA_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (move ["type_eq"])) THEN (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (4,1,1)))) (disch_tac [])) THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1005 (* Lemma BDJYFFB2 *)
1006 let BDJYFFB2 = Sections.section_proof ["d"]
1007 `let H = hypermap_of_fan (V,ESTD V) in
1008 d IN dart_of_fan (V,ESTD V) /\ type_of_node H d = (5,0,1)
1009 ==> #0.63 < sum {f | f IN set_of_face_meeting_node H d /\ CARD f = 3}
1010 (\f. tauVEF (V, ESTD V,f))`
1012 ((CONV_TAC let_CONV) THEN ALL_TAC THEN (case THEN (move ["d_in"])) THEN (move ["type_eq"]));
1013 (((fun arg_tac -> arg_tac (Arg_theorem (get_b_tame_ineq (5,0,1)))) (disch_tac [])) THEN BETA_TAC);
1014 ((fun arg_tac -> arg_tac (Arg_term (`sum _1 _2`))) (term_tac (set_tac "s")));
1015 ((arith_tac) THEN (done_tac));
1018 (* Finalization of the section BDJYFFB *)
1019 let BDJYFFB1 = Sections.finalize_theorem BDJYFFB1;;
1020 let BDJYFFB2 = Sections.finalize_theorem BDJYFFB2;;
1021 Sections.end_section "BDJYFFB";;
1023 (* Finalization of the section Contravening *)
1024 let anglesum = Sections.finalize_theorem anglesum;;
1025 let anglesum_lo_approx = Sections.finalize_theorem anglesum_lo_approx;;
1026 let anglesum_hi_approx = Sections.finalize_theorem anglesum_hi_approx;;
1027 let tausum_eq = Sections.finalize_theorem tausum_eq;;
1028 let tausum_triangles = Sections.finalize_theorem tausum_triangles;;
1029 let tausum_upper_bound = Sections.finalize_theorem tausum_upper_bound;;
1030 let azimp_lo = Sections.finalize_theorem azimp_lo;;
1031 let azimp_hi = Sections.finalize_theorem azimp_hi;;
1032 let azimq_lo = Sections.finalize_theorem azimq_lo;;
1033 let azimr_lo = Sections.finalize_theorem azimr_lo;;
1034 let azimq_hi = Sections.finalize_theorem azimq_hi;;
1035 let azimq_hi_approx = Sections.finalize_theorem azimq_hi_approx;;
1036 let azimr_hi = Sections.finalize_theorem azimr_hi;;
1037 let taup_lo = Sections.finalize_theorem taup_lo;;
1038 let tauq_lo = Sections.finalize_theorem tauq_lo;;
1039 let taur_lo = Sections.finalize_theorem taur_lo;;
1040 let case50_ineq = Sections.finalize_theorem case50_ineq;;
1041 let p1_ineq = Sections.finalize_theorem p1_ineq;;
1042 let p2_ineq = Sections.finalize_theorem p2_ineq;;
1043 let p3_ineq = Sections.finalize_theorem p3_ineq;;
1044 let q1_ineq = Sections.finalize_theorem q1_ineq;;
1045 let q2_ineq = Sections.finalize_theorem q2_ineq;;
1046 let q3_ineq = Sections.finalize_theorem q3_ineq;;
1047 let q4_ineq = Sections.finalize_theorem q4_ineq;;
1048 let KCBLRQC = Sections.finalize_theorem KCBLRQC;;
1049 let BDJYFFB1 = Sections.finalize_theorem BDJYFFB1;;
1050 let BDJYFFB2 = Sections.finalize_theorem BDJYFFB2;;
1051 Sections.end_section "Contravening";;
1053 (* Close the module *)