text_formalization/tame/ssreflect/KCBLRQC-compiled.hl

   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";;
   4
   5 (* Module Kcblrqc*)
   6 module Kcblrqc = struct
   7
   8 open Ssrbool;;
   9 open Ssrnat;;
  10 open Hypermap;;
  11 open Lp_ineqs_proofs;;
  12 open Lp_main_estimate;;
  13 open Tame_lemmas;;
  14 open Tame_defs;;
  15 open Tame_general;;
  16 open Hypermap_and_fan;;
  17 open Hypermap_iso;;
  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))`;;
  26
  27 (* Lemma a_sum_mul *)
  28 let a_sum_mul = Sections.section_proof ["s";"f"]
  29 `FINITE s ==> &(CARD s) * (sum s f / &(CARD s)) = sum s f`
  30 [
  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));
  35 ];;
  36
  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`));;
  41
  42 (* Let h_fan *)
  43 Sections.add_section_lemma "h_fan" (Sections.section_proof []
  44 `lp_fan (V,ESTD V)`
  45 [
  46    ((((use_arg_then2 ("contravening_lp_fan", [contravening_lp_fan]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  47 ]);;
  48
  49 (* Let fanV *)
  50 Sections.add_section_lemma "fanV" (Sections.section_proof []
  51 `FAN (vec 0,V,ESTD V)`
  52 [
  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));
  54 ]);;
  55
  56 (* Let f_surr *)
  57 Sections.add_section_lemma "f_surr" (Sections.section_proof []
  58 `fully_surrounded (V,ESTD V)`
  59 [
  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));
  61 ]);;
  62
  63 (* Let simpleH *)
  64 Sections.add_section_lemma "simpleH" (Sections.section_proof []
  65 `simple_hypermap (hypermap_of_fan (V,ESTD V))`
  66 [
  67    ((((use_arg_then2 ("Jgtdebu.JGTDEBU4", [Jgtdebu.JGTDEBU4]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  68 ]);;
  69
  70 (* Let dartH *)
  71 Sections.add_section_lemma "dartH" (Sections.section_proof []
  72 `dart (hypermap_of_fan (V,ESTD V)) = dart_of_fan (V,ESTD V)`
  73 [
  74    ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  75 ]);;
  76
  77 (* Let finite_sets *)
  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)}`
  83 [
  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));
  85 ]);;
  86
  87 (* Section SumEqs *)
  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`))));;
  90
  91 (* Lemma anglesum *)
  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`
  97 [
  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));
 107 ];;
 108
 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`
 115 [
 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));
 117 ];;
 118
 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`
 125 [
 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));
 127 ];;
 128
 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))`
 136 [
 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));
 158 ];;
 159
 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))`
 167 [
 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));
 182 ];;
 183
 184 (* Section Tgt *)
 185 Sections.begin_section "Tgt";;
 186 (Sections.add_section_hyp "h_main" (`lp_main_estimate`));;
 187
 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`
 193 [
 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));
 206 ];;
 207
 208 (* Finalization of the section Tgt *)
 209 let tausum_upper_bound = Sections.finalize_theorem tausum_upper_bound;;
 210 Sections.end_section "Tgt";;
 211
 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";;
 220
 221 (* Section Ineqs *)
 222 Sections.begin_section "Ineqs";;
 223
 224 (* Let y_bounds *)
 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`
 233 [
 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));
 238 ]);;
 239
 240 (* Let eqs *)
 241 Sections.add_section_lemma "eqs" (Sections.section_proof []
 242 `#2.0 = &2 /\ &2 * h0 = #2.52 /\ #0.0 = &0 /\ #5.04 = &4 * h0`
 243 [
 244    ((((use_arg_then2 ("Sphere.h0", [Sphere.h0]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 245 ]);;
 246
 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`))));;
 250
 251 (* Section Lo *)
 252 Sections.begin_section "Lo";;
 253 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "5735387903")).ineq));;
 254
 255 (* Lemma azimp_lo *)
 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
 259         /\ ~(p = 0)
 260         ==> #0.852 <= a_azim ((=) 3) V d`
 261 [
 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));
 275 ];;
 276
 277 (* Finalization of the section Lo *)
 278 let azimp_lo = Sections.finalize_theorem azimp_lo;;
 279 Sections.end_section "Lo";;
 280
 281 (* Section Hi *)
 282 Sections.begin_section "Hi";;
 283 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "5490182221")).ineq));;
 284
 285 (* Lemma azimp_hi *)
 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`
 289 [
 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));
 305 ];;
 306
 307 (* Finalization of the section Hi *)
 308 let azimp_hi = Sections.finalize_theorem azimp_hi;;
 309 Sections.end_section "Hi";;
 310
 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";;
 315
 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`))));;
 319
 320 (* Section Lo *)
 321 Sections.begin_section "Lo";;
 322 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "2570626711")).ineq));;
 323
 324 (* Lemma azimq_lo *)
 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
 328         /\ ~(q = 0)
 329         ==> #1.15 <= a_azim ((=) 4) V d`
 330 [
 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));
 349 ];;
 350
 351 (* Lemma azimr_lo *)
 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
 355         /\ ~(r = 0)
 356         ==> #1.15 <= a_azim ((<=) 5) V d`
 357 [
 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));
 376 ];;
 377
 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";;
 382
 383 (* Section Hi *)
 384 Sections.begin_section "Hi";;
 385
 386 (* Lemma azimq_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`
 390 [
 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));
 402 ];;
 403
 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`
 408 [
 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));
 410 ];;
 411
 412 (* Lemma azimr_hi *)
 413 let azimr_hi = Sections.section_proof ["d"]
 414 `d IN dart_of_fan (V,ESTD V)
 415         ==> a_azim ((<=) 5) V d <= pi`
 416 [
 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));
 428 ];;
 429
 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";;
 435
 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";;
 443
 444 (* Section A_tau *)
 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`));;
 448
 449 (* Lemma taup_lo *)
 450 let taup_lo = Sections.section_proof ["d"]
 451 `d IN dart_of_fan (V,ESTD V)
 452         ==> &0 <= a_tau ((=) 3) V d`
 453 [
 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));
 462 ];;
 463
 464 (* Lemma tauq_lo *)
 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
 468         /\ ~(q = 0)
 469         ==> #0.206 <= a_tau ((=) 4) V d`
 470 [
 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));
 481 ];;
 482
 483 (* Lemma taur_lo *)
 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
 487         /\ ~(r = 0)
 488         ==> #0.4819 <= a_tau ((<=) 5) V d`
 489 [
 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));
 510 ];;
 511
 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";;
 517
 518 (* Section Case50 *)
 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));;
 523
 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`
 529 [
 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));
 570 ];;
 571
 572 (* Finalization of the section Case50 *)
 573 let case50_ineq = Sections.finalize_theorem case50_ineq;;
 574 Sections.end_section "Case50";;
 575
 576 (* Let aux_ge *)
 577 Sections.add_section_lemma "aux_ge" (Sections.section_proof ["a"]
 578 `a > &0 ==> a >= &0`
 579 [
 580    ((arith_tac) THEN (done_tac));
 581 ]);;
 582
 583 (* Let aux_ineq *)
 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`
 592 [
 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));
 606 ]);;
 607
 608 (* Section P1 *)
 609 Sections.begin_section "P1";;
 610 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "3296257235")).ineq));;
 611
 612 (* Lemma p1_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`
 617 [
 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));
 626 ];;
 627
 628 (* Finalization of the section P1 *)
 629 let p1_ineq = Sections.finalize_theorem p1_ineq;;
 630 Sections.end_section "P1";;
 631
 632 (* Section P2 *)
 633 Sections.begin_section "P2";;
 634 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "8519146937")).ineq));;
 635
 636 (* Lemma p2_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`
 641 [
 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));
 650 ];;
 651
 652 (* Finalization of the section P2 *)
 653 let p2_ineq = Sections.finalize_theorem p2_ineq;;
 654 Sections.end_section "P2";;
 655
 656 (* Section P3 *)
 657 Sections.begin_section "P3";;
 658 (Sections.add_section_hyp "ineq" ((hd (Ineq.getexact "4667071578")).ineq));;
 659
 660 (* Lemma p3_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`
 665 [
 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));
 674 ];;
 675
 676 (* Finalization of the section P3 *)
 677 let p3_ineq = Sections.finalize_theorem p3_ineq;;
 678 Sections.end_section "P3";;
 679
 680 (* Section Q1 *)
 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));;
 685
 686 (* Lemma q1_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`
 691 [
 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));
 697 ];;
 698
 699 (* Finalization of the section Q1 *)
 700 let q1_ineq = Sections.finalize_theorem q1_ineq;;
 701 Sections.end_section "Q1";;
 702
 703 (* Section Q2 *)
 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));;
 708
 709 (* Lemma q2_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`
 714 [
 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));
 720 ];;
 721
 722 (* Finalization of the section Q2 *)
 723 let q2_ineq = Sections.finalize_theorem q2_ineq;;
 724 Sections.end_section "Q2";;
 725
 726 (* Section Q3 *)
 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));;
 731
 732 (* Lemma q3_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`
 737 [
 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));
 743 ];;
 744
 745 (* Finalization of the section Q3 *)
 746 let q3_ineq = Sections.finalize_theorem q3_ineq;;
 747 Sections.end_section "Q3";;
 748
 749 (* Section Q4 *)
 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));;
 757
 758 (* Lemma q4_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`
 763 [
 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));
 769 ];;
 770
 771 (* Finalization of the section Q4 *)
 772 let q4_ineq = Sections.finalize_theorem q4_ineq;;
 773 Sections.end_section "Q4";;
 774
 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";;
 795 let add_ineqs_hyp =
 796   let imp_th = (UNDISCH o MATCH_MP EQ_IMP) kcblrqc_ineq_def in
 797   let ths = CONJUNCTS imp_th in
 798     fun th ->
 799       itlist PROVE_HYP ths th;;
 800 let ineq_table =
 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
 804         [
 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;
 827         ];;
 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
 831         else
 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
 847           else
 848             th3;;
 849 let lp_data = [
 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`];
 898 ];;
 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
 904           CONV_RULE conv sum;;
 905
 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`));;
 910
 911 (* Lemma KCBLRQC *)
 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)`
 917 [
 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));
 949 ];;
 950
 951 (* Finalization of the section KCBLRQC *)
 952 let KCBLRQC = Sections.finalize_theorem KCBLRQC;;
 953 Sections.end_section "KCBLRQC";;
 954
 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`));;
 959
 960 (* Lemma BDJYFFB1 *)
 961 let BDJYFFB1 = Sections.section_proof []
 962 `tame_12o (hypermap_of_fan (V,ESTD V))`
 963 [
 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));
1003 ];;
1004
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))`
1011 [
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));
1016 ];;
1017
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";;
1022
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";;
1052
1053 (* Close the module *)
1054 end;;