1 needs "tame/ssreflect/tame_lemmas-compiled.hl";;
4 module Rnsyjxm = struct
10 open Hypermap_and_fan;;
16 open Wrgcvdr_cizmrrh;;
18 (* Lemma localization_set_of_edge_subset *)
19 let localization_set_of_edge_subset = Sections.section_proof ["V";"E";"f";"v"]
20 `set_of_edge v (v_prime V f) (e_prime E f) SUBSET set_of_edge v V E`
22 ((((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [] [])))) THEN (((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));
23 ((BETA_TAC THEN (move ["u"]) THEN (case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["h"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
26 (* Lemma in_face_imp_in_dart *)
27 let in_face_imp_in_dart = Sections.section_proof ["x";"H";"d"]
28 `x IN dart H /\ d IN face H x ==> d IN dart H`
30 (BETA_TAC THEN (case THEN ((move ["x_in"]) THEN (move ["d_in"]))));
31 (((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (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 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
34 (* Lemma in_face_imp_in_dart_alt *)
35 let in_face_imp_in_dart_alt = Sections.section_proof ["H";"f";"d"]
36 `f IN face_set H /\ d IN f ==> d IN dart H`
38 (BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["d_in"]));
39 ((((fun arg_tac -> (use_arg_then2 ("in_face_imp_in_dart", [in_face_imp_in_dart])) (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 (done_tac));
42 (* Lemma face_face_map_eq *)
43 let face_face_map_eq = Sections.section_proof ["H";"d"]
44 `face H (face_map H d) = face H d`
46 ((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("face", [face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("in_orbit_map1", [in_orbit_map1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
50 Sections.begin_section "Fan";;
51 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
52 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
53 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
56 Sections.add_section_lemma "dartH" (Sections.section_proof []
57 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
59 ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
63 Sections.add_section_lemma "in_dart_inV" (Sections.section_proof ["d"]
64 `d IN dart_of_fan (V,E) ==> FST d IN V /\ SND d IN V`
66 (((((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
69 (* Lemma card_set_of_edge_gt1_imp_in_dart1 *)
70 let card_set_of_edge_gt1_imp_in_dart1 = Sections.section_proof ["v";"w"]
71 `v,w IN dart_of_fan (V,E)
72 /\ CARD (set_of_edge v V E) > 1 ==> v,w IN dart1_of_fan (V,E)`
74 (BETA_TAC THEN (case THEN ((move ["vw_in"]) THEN (move ["card_gt1"]))));
75 ((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (case THEN ((TRY done_tac))));
76 (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["z"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["z_in"])) THEN (move ["eq1"]) THEN (move ["eq2"]));
77 ((((use_arg_then2 ("card_gt1", [])) (disch_tac [])) THEN (clear_assumption "card_gt1") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("CARD_CLAUSES", [CARD_CLAUSES]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
80 (* Lemma azim_in_fan_eq_azim_dart *)
81 let azim_in_fan_eq_azim_dart = Sections.section_proof ["d"]
82 `d IN dart_of_fan (V,E)
83 ==> azim_in_fan d E = azim_dart (V,E) d`
85 (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
86 ((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE azim_in_fan)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("azim_dart_eq_azim_fan", [azim_dart_eq_azim_fan]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("azim_fan", [azim_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
87 (((fun arg_tac -> arg_tac (Arg_term (`_ > 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
88 ((((fun arg_tac -> (use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
89 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("card_set_of_edge_gt1_imp_in_dart1", [card_set_of_edge_gt1_imp_in_dart1])) (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 ("ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
92 (* Lemma wedge_in_fan_gt_eq_w_dart_fan *)
93 let wedge_in_fan_gt_eq_w_dart_fan = Sections.section_proof ["d"]
94 `d IN dart1_of_fan (V,E)
95 ==> wedge_in_fan_gt d E = w_dart_fan (vec 0) V E (ext_dart (V,E) d)`
97 (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"]));
98 ((((use_arg_then2 ("wedge_in_fan_gt", [wedge_in_fan_gt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w_dart_fan", [w_dart_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
99 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (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 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["w_inE"])) THEN (move ["_"])))));
100 (((fun arg_tac -> arg_tac (Arg_term (`CARD _ > 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
101 ((((fun arg_tac -> (use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
102 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`set_of_edge v V E = {w}`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))));
103 (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_DIFF", [IN_DIFF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIV", [IN_UNIV]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
104 ((((use_arg_then2 ("ineq", [])) (disch_tac [])) THEN (clear_assumption "ineq") THEN BETA_TAC) THEN ((((use_arg_then2 ("gtE", [gtE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_LT", [NOT_LT]))(thm_tac (new_rewrite [] []))))));
105 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("finite_set_of_edge", [finite_set_of_edge])) (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 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["finE"])));
106 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x <= 1 <=> x = 0 \/ x = 1`))) (term_tac (have_gen_tac ["x"](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
107 ((THENL_FIRST) case ((((((use_arg_then2 ("CARD_EQ_0", [CARD_EQ_0]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["eq"])) THEN (((use_arg_then2 ("w_inE", [])) (disch_tac [])) THEN (clear_assumption "w_inE") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
108 ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("Rogers.CARD_1_IMP_SING", [Rogers.CARD_1_IMP_SING])) (fun fst_arg -> (use_arg_then2 ("finE", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"])) THEN (move ["eq"]));
109 ((((use_arg_then2 ("w_inE", [])) (disch_tac [])) THEN (clear_assumption "w_inE") THEN BETA_TAC) THEN (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
112 (* Lemma localization_dart_eq_dart1 *)
113 let localization_dart_eq_dart1 = Sections.section_proof ["f"]
114 `f IN face_set (hypermap_of_fan (V,E))
116 ==> dart_of_fan (v_prime V f, e_prime E f) = dart1_of_fan (v_prime V f, e_prime E f)`
118 (BETA_TAC THEN (case THEN ((move ["f_in"]) THEN (move ["card_f"]))));
119 ((((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (move ["d"])) THEN ((THENL) (split_tac) [((case THEN ALL_TAC) THEN ((TRY done_tac))); ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))]));
120 (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])));
121 (((((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))))) THEN (move ["v"]));
122 ((((fun arg_tac -> arg_tac (Arg_term (`v IN _`))) (disch_eq_tac "v_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (DISJ1_TAC));
123 ((((use_arg_then2 ("v_in", [])) (disch_tac [])) THEN (clear_assumption "v_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["v_in"])) THEN (case THEN (move ["w"])) THEN (move ["vw_in_f"])));
124 ((((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac)));
125 ((((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (clear_assumption "f_in") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"]))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["f_eq"])));
126 ((fun arg_tac -> arg_tac (Arg_term (`x IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["x_in1"]))));
127 (((use_arg_then2 ("card_f", [])) (disch_tac [])) THEN (clear_assumption "card_f") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["x_not_in"]));
128 (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("CARD_SINGLETON", [CARD_SINGLETON]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
129 ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"]))));
130 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART1_OF_FAN", [FACE_SUBSET_DART1_OF_FAN])) (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 ("x_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
131 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
132 (((((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac));
133 ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN (((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
134 ((((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
135 ((fun arg_tac -> arg_tac (Arg_term (`SND (f_fan_pair (V,E) (v,w))`))) (term_tac exists_tac));
136 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`w, SND (f_fan_pair (V,E) (v,w)) = face_map (hypermap_of_fan (V,E)) (v,w)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
137 (in_tac ["vw_in_f"] false (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))));
138 (((((use_arg_then2 ("POWER_1", [POWER_1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (use_arg_then2 ("vw_in_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_in_face", [lemma_in_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
139 (((((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (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 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
142 (* Lemma localization_dart1_subset *)
143 let localization_dart1_subset = Sections.section_proof ["f";"d"]
144 `d IN dart1_of_fan (v_prime V f, e_prime E f) ==> d IN dart1_of_fan (V,E)`
146 (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]));
147 ((repeat_tactic 1 9 (((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> arg_tac (Arg_term (`{v,w}`))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(gsym_then (thm_tac (new_rewrite [] []))))));
148 ((use_arg_then2 ("Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E", [Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E])) (thm_tac apply_tac));
151 (* Lemma localization_node_subset *)
152 let localization_node_subset = Sections.section_proof ["f";"d"]
153 `f IN face_set (hypermap_of_fan (V,E))
154 ==> node (hypermap_of_fan (v_prime V f, e_prime E f)) d
155 SUBSET node (hypermap_of_fan (V,E)) d`
157 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["x"]))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x_in"])) THEN (move ["f_eq"])));
158 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Wrgcvdr_cizmrrh.IMP_FAN_V_PRIME_E_PRIME))) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
159 ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
160 (BETA_TAC THEN (move ["fan'"]));
161 ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`d IN dart1_of_fan (V,E)`))) (disch_eq_tac "d_in1" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
162 ((repeat_tactic 1 9 (((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("SUBSET_REFL", [SUBSET_REFL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fan'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
163 ((((use_arg_then2 ("d_in1", [])) (disch_tac [])) THEN (clear_assumption "d_in1") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
164 (((use_arg_then2 ("d_in1", [])) (disch_tac [])) THEN (clear_assumption "d_in1") THEN ((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in1"]));
165 ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (v_prime V f, e_prime E f)`))) (disch_eq_tac "vw_in1'" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
166 (((((use_arg_then2 ("E_N_F_DEGENERATE_CASE", [E_N_F_DEGENERATE_CASE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SING_SUBSET", [SING_SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
167 (((repeat_tactic 1 9 (((use_arg_then2 ("NODE_HYPERMAP_OF_FAN_ALT", [NODE_HYPERMAP_OF_FAN_ALT]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))));
168 (((repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["u_in"])) THEN (move ["eqs"]));
169 (((use_arg_then2 ("u", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("eqs", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
170 ((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("u_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("localization_set_of_edge_subset", [localization_set_of_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
173 (* Lemma f_fan_pair_ext_in_dart1 *)
174 let f_fan_pair_ext_in_dart1 = Sections.section_proof ["d"]
175 `d IN dart1_of_fan (V,E) ==>
176 f_fan_pair_ext (V,E) d IN dart1_of_fan (V,E)`
178 ((BETA_TAC THEN (move ["d_in"])) THEN ((((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("E_N_F_IN_DART1_OF_FAN", [E_N_F_IN_DART1_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
181 (* Lemma localization_simple_hypermap *)
182 let localization_simple_hypermap = Sections.section_proof ["f"]
183 `f IN face_set (hypermap_of_fan (V,E))
185 /\ simple_hypermap (hypermap_of_fan (V,E))
186 ==> simple_hypermap (hypermap_of_fan (v_prime V f, e_prime E f))`
188 (((repeat_tactic 1 9 (((use_arg_then2 ("simple_hypermap", [simple_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f_in"])) THEN (case THEN (move ["card_f"])) THEN (move ["simpleH"]));
189 ((((use_arg_then2 ("f_in", [])) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_representation", [lemma_face_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (case THEN ((move ["v"]) THEN (move ["w"]))))) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["vw_in"])) THEN (move ["f_eq"])));
190 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Lvducxu.LVDUCXU))) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
191 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
192 ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
193 (BETA_TAC THEN (move ["fan'"]));
194 ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH'"]) THEN (move ["_"])))));
195 (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_hyp_elim", [darts_of_hyp_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)));
196 ((THENL_FIRST) (ANTS_TAC) ((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
197 (BETA_TAC THEN (case THEN (move ["ff_eq"])) THEN (move ["_"]));
198 ((((use_arg_then2 ("dartH'", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["ab_in"]));
199 ((((use_arg_then2 ("ab_in", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["ab_in1"])));
200 ((THENL_ROT (-1)) ((((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["x"]) THEN (move ["y"])))) THEN (split_tac)));
201 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
202 (BETA_TAC THEN (case THEN (move ["xy_in_n"])) THEN (move ["xy_in_f"]));
203 ((fun arg_tac -> arg_tac (Arg_term (`d IN f ==> d IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac ["d"](move ["in_f_in_dart"]))));
204 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (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 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
205 ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (v_prime V f, e_prime E f) ==> d IN f \/ SND d, FST d IN f`))) (term_tac (have_gen_tac ["d"](move ["dart_or"]))));
206 (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["u"]) THEN (move ["z"])));
207 ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
208 ((BETA_TAC THEN (case THEN (move ["x'"])) THEN (case THEN (move ["y'"])) THEN (case THEN (move ["xy'_in"]))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Geomdetail.PAIR_EQ_EXPAND)))(thm_tac (new_rewrite [] [])))));
209 ((case THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac));
210 (((fun arg_tac -> (use_arg_then2 ("dart_or", [])) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac));
211 (((fun arg_tac -> arg_tac (Arg_term (`a,b IN f`))) (disch_eq_tac "ab_in_f" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
212 (((fun arg_tac -> (use_arg_then2 ("simpleH", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("in_f_in_dart", [])) (fun fst_arg -> (use_arg_then2 ("ab_in_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
213 (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_INTER", [IN_INTER]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
214 ((((fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ff_eq", []))(thm_tac (new_rewrite [] [])))));
215 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("xy_in_f", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
216 ((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("localization_node_subset", [localization_node_subset])) (fun fst_arg -> (use_arg_then2 ("f_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (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 (done_tac));
217 (BETA_TAC THEN (move ["ba_in_f"]));
218 ((fun arg_tac -> arg_tac (Arg_term (`x = a`))) (term_tac (have_gen_tac [](move ["x_eq_a"]))));
219 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_fan", [fst_node_hypermap_of_fan])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("xy_in_n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (done_tac));
220 ((in_tac ["xy_in_f"] true ((((use_arg_then2 ("x_eq_a", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("x_eq_a", [])) (disch_tac [])) THEN (clear_assumption "x_eq_a") THEN ((use_arg_then2 ("xy_in_n", [])) (disch_tac [])) THEN (clear_assumption "xy_in_n") THEN BETA_TAC THEN (move ["_"]) THEN (move ["_"]) THEN (simp_tac)));
221 ((fun arg_tac -> arg_tac (Arg_term (`a,y IN dart_of_fan (v_prime V f,e_prime E f)`))) (term_tac (have_gen_tac [](move ["ay_in'"]))));
222 (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (use_arg_then2 ("xy_in_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
223 ((fun arg_tac -> arg_tac (Arg_term (`y,a IN f`))) (term_tac (have_gen_tac [](move ["ya_in_f"]))));
224 (((use_arg_then2 ("ay_in'", [])) (disch_tac [])) THEN (clear_assumption "ay_in'") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("dart_or", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN case THEN (simp_tac) THEN (move ["ay_in_f2"]));
225 (((use_arg_then2 ("xy_in_f", [])) (disch_tac [])) THEN (clear_assumption "xy_in_f") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
226 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["eq1"]));
227 ((((use_arg_then2 ("ab_in_f", [])) (disch_tac [])) THEN (clear_assumption "ab_in_f") THEN BETA_TAC) THEN ((((use_arg_then2 ("ff_eq", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_different_faces", [lemma_different_faces])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
228 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair_ext (V,E) (y,a) = f_fan_pair_ext (V,E) (b,a)`))) (term_tac (have_gen_tac []ALL_TAC))));
229 (((((fun arg_tac -> (use_arg_then2 ("PERMUTES_INJECTIVE", [PERMUTES_INJECTIVE])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN", [F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN])) (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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
230 ((fun arg_tac -> arg_tac (Arg_term (`_1 _2 (y,a)`))) (term_tac (set_tac "d1")));
231 ((fun arg_tac -> arg_tac (Arg_term (`_1 _2 (b,a)`))) (term_tac (set_tac "d2")));
232 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`{d1} = {d2}`))) (term_tac (have_gen_tac []ALL_TAC)))) ((((use_arg_then2 ("SING_EQ", [SING_EQ]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
233 ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (move ["fH"])))));
234 ((fun arg_tac -> arg_tac (Arg_term (`y,a IN dart1_of_fan (V,E) /\ b,a IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["ya_in1"]) THEN (move ["ba_in1"]))))));
235 ((split_tac) THEN (((use_arg_then2 ("dart1_switch", [dart1_switch]))(thm_tac (new_rewrite [] [])))));
236 ((((use_arg_then2 ("ay_in'", [])) (disch_tac [])) THEN (clear_assumption "ay_in'") THEN BETA_TAC) THEN (((((use_arg_then2 ("localization_dart_eq_dart1", [localization_dart_eq_dart1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
237 ((((use_arg_then2 ("ab_in1", [])) (disch_tac [])) THEN (clear_assumption "ab_in1") THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("localization_dart1_subset", [localization_dart1_subset])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
238 ((fun arg_tac -> arg_tac (Arg_term (`d1 IN dart1_of_fan (V,E) /\ d2 IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["d1_in1"]) THEN (move ["d2_in1"]))))));
239 (((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair_ext_in_dart1", [f_fan_pair_ext_in_dart1]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
240 ((fun arg_tac -> arg_tac (Arg_term (`d1 IN dart_of_fan (V,E) /\ d2 IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((move ["d1_in"]) THEN (move ["d2_in"]))))));
241 (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d1_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d2_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
242 (((((fun arg_tac -> (use_arg_then2 ("simpleH", [])) (fun fst_arg -> (use_arg_then2 ("d1_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("simpleH", [])) (fun fst_arg -> (use_arg_then2 ("d2_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (congr_tac (`_1 INTER _2`)));
243 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("HYPERMAP_OF_FAN_NODE_EQ", [HYPERMAP_OF_FAN_NODE_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 ("d1_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d2_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
244 (((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ya_in1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ba_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_fan_pair", [f_fan_pair]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
245 ((((use_arg_then2 ("d1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("face_face_map_eq", [face_face_map_eq]))(thm_tac (new_rewrite [] []))))));
246 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,a`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
247 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_face_identity", [lemma_face_identity])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`b,a`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
250 (* Finalization of the section Fan *)
251 let card_set_of_edge_gt1_imp_in_dart1 = Sections.finalize_theorem card_set_of_edge_gt1_imp_in_dart1;;
252 let azim_in_fan_eq_azim_dart = Sections.finalize_theorem azim_in_fan_eq_azim_dart;;
253 let wedge_in_fan_gt_eq_w_dart_fan = Sections.finalize_theorem wedge_in_fan_gt_eq_w_dart_fan;;
254 let localization_dart_eq_dart1 = Sections.finalize_theorem localization_dart_eq_dart1;;
255 let localization_dart1_subset = Sections.finalize_theorem localization_dart1_subset;;
256 let localization_node_subset = Sections.finalize_theorem localization_node_subset;;
257 let f_fan_pair_ext_in_dart1 = Sections.finalize_theorem f_fan_pair_ext_in_dart1;;
258 let localization_simple_hypermap = Sections.finalize_theorem localization_simple_hypermap;;
259 Sections.end_section "Fan";;
261 (* Section FullySurrounded *)
262 Sections.begin_section "FullySurrounded";;
263 (Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
264 (Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
265 (Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
266 (Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
269 Sections.add_section_lemma "dartH" (Sections.section_proof []
270 `dart (hypermap_of_fan (V,E)) = dart_of_fan (V,E)`
272 ((((use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
276 Sections.add_section_lemma "dart1_eq" (Sections.section_proof []
277 `dart1_of_fan (V,E) = dart_of_fan (V,E)`
279 ((((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
282 (* Lemma fully_surrounded_simple_hypermap *)
283 let fully_surrounded_simple_hypermap = Sections.section_proof []
284 `simple_hypermap (hypermap_of_fan (V,E))`
286 ((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.fan_hypermaps_iso", [Hypermap_iso.fan_hypermaps_iso])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso"])));
287 ((((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.iso_simple", [Hypermap_iso.iso_simple])) (fun fst_arg -> (use_arg_then2 ("iso", [iso])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Conforming.SRPRNPL", [Conforming.SRPRNPL]))(thm_tac (new_rewrite [] [])))));
288 ((((use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
291 (* Lemma f_surr_localization *)
292 let f_surr_localization = Sections.section_proof ["d"]
293 `d IN dart_of_fan (V,E)
294 ==> let f = face (hypermap_of_fan (V,E)) d in
295 local_fan (v_prime V f,e_prime E f,f)
296 /\ face (hypermap_of_fan (v_prime V f, e_prime E f)) d = f
297 /\ (!x. x IN f ==> azim_dart (V,E) x = azim_dart (v_prime V f, e_prime E f) x)
298 /\ (!x. x IN f ==> wedge_in_fan_gt x E = wedge_in_fan_gt x (e_prime E f))
299 /\ (!x. x IN f ==> wedge_in_fan_ge x E = wedge_in_fan_ge x (e_prime E f))`
301 ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
302 ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f")));
303 ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Lvducxu.LVDUCXU))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
304 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
305 ((((use_arg_then2 ("darts_of_hyp_elim", [darts_of_hyp_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))));
306 ((THENL_FIRST) (ANTS_TAC) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
307 ((BETA_TAC THEN (move ["fan'"]) THEN ((fun arg_tac -> (fun arg_tac -> (conv_thm_tac DISCH_THEN) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))));
308 (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((ANTS_TAC) THEN ((TRY done_tac)) THEN (case THEN (move ["f_eq"])) THEN (case THEN (move ["in_f_eq"]))));
309 ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH'"]) THEN (move ["_"])))));
311 ((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 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["card_ge3"])));
312 ((THENL_FIRST) (split_tac) ((((use_arg_then2 ("card_ge3", [])) (disch_tac [])) THEN (clear_assumption "card_ge3") THEN BETA_TAC) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
313 ((((use_arg_then2 ("localization_simple_hypermap", [localization_simple_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fanV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fully_surrounded_simple_hypermap", [fully_surrounded_simple_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
314 (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_ge3", [])) (disch_tac [])) THEN (clear_assumption "card_ge3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
315 ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
316 ((repeat_tactic 1 9 ((split_tac))) THEN (BETA_TAC THEN (move ["d"]) THEN (move ["d_in_f"])) THEN ((repeat_tactic 0 10 (((use_arg_then2 ("in_f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
317 ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["d_in"]))));
318 (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("in_face_imp_in_dart", [in_face_imp_in_dart])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`v,w`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
319 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["d_in'"])))));
320 (((((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("in_f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
321 (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (DISJ1_TAC));
322 (((use_arg_then2 ("d_in", [])) (disch_tac [])) THEN (clear_assumption "d_in") THEN ((use_arg_then2 ("d_in_f", [])) (disch_tac [])) THEN (clear_assumption "d_in_f") THEN ((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["ab_in_f"]) THEN (move ["ab_in"]));
323 ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
324 ((((use_arg_then2 ("a", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("b", [])) (term_tac exists_tac))) THEN ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("E", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
327 (* Lemma f_surr_localization_convex_local *)
328 let f_surr_localization_convex_local = Sections.section_proof ["d"]
329 `d IN dart_of_fan (V,E)
330 ==> let f = face (hypermap_of_fan (V,E)) d in
331 convex_local_fan (v_prime V f,e_prime E f,f)`
333 ((((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN case THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN (CONV_TAC let_CONV));
334 ((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_surr_localization))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["local"]) THEN (case THEN (move ["f_eq"])) THEN (case THEN (move ["azim_eq"])) THEN (move ["wedge_eq"])))));
335 ((((use_arg_then2 ("convex_local_fan", [convex_local_fan]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_surr_localization))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
336 ((fun arg_tac -> arg_tac (Arg_term (`face _1 _2`))) (term_tac (set_tac "f")));
337 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMP_FAN_V_PRIME_E_PRIME))) (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", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
338 ((THENL_FIRST) (((((use_arg_then2 ("hypermap_HYP_elim", [hypermap_HYP_elim]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (ANTS_TAC)) (((fun arg_tac -> arg_tac (Arg_term (`v,w`))) (term_tac exists_tac)) THEN (done_tac)));
339 (BETA_TAC THEN (move ["fan'"]) THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["ab_in_f"]));
340 ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["ab_in"]))));
341 (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (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 snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
342 ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["vw_in'"]))));
343 (((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] []))))) THEN (DISJ1_TAC));
344 ((((use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_prime", [e_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
345 ((((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN ((use_arg_then2 ("w", [])) (term_tac exists_tac))) THEN ((((fun arg_tac -> (use_arg_then2 ("inE_eq_in_dart1", [inE_eq_in_dart1])) (fun fst_arg -> (use_arg_then2 ("V", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
346 (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
347 ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart_of_fan (v_prime V f, e_prime E f)`))) (term_tac (have_gen_tac [](move ["ab_in'"]))));
348 (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (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 snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
349 ((((fun arg_tac -> (use_arg_then2 ("azim_in_fan_eq_azim_dart", [azim_in_fan_eq_azim_dart])) (fun fst_arg -> (use_arg_then2 ("fan'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("azim_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
350 ((THENL_FIRST) (split_tac) ((((use_arg_then2 ("f_surr", [])) (disch_tac [])) THEN (clear_assumption "f_surr") THEN BETA_TAC) THEN ((((use_arg_then2 ("fully_surrounded", [fully_surrounded]))(thm_tac (new_rewrite [] [])))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac)));
351 (((((use_arg_then2 ("wedge_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("v_prime", [v_prime]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["x_inV"])) THEN (case THEN (move ["y"])) THEN (move ["xy_in_f"]));
352 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["ab_in1"])))) ((((use_arg_then2 ("dart1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
353 (((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`closure (wedge_in_fan_gt (a,b) E)`))) (term_tac exists_tac)) THEN (split_tac));
354 ((((use_arg_then2 ("wedge_in_fan_gt", [wedge_in_fan_gt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("wedge_in_fan_ge", [wedge_in_fan_ge]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EE_elim", [EE_elim])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
355 ((((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)));
356 ((((use_arg_then2 ("CLOSURE_MINIMAL_EQ", [CLOSURE_MINIMAL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("Leaf_cell.WEDGE_SUBSET_WEDGE_GE", [Leaf_cell.WEDGE_SUBSET_WEDGE_GE]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
357 ((((use_arg_then2 ("AZIM_CYCLE_EQ_SIGMA_FAN_ALT", [AZIM_CYCLE_EQ_SIGMA_FAN_ALT]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("ab_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
358 (((((use_arg_then2 ("Leaf_cell.CLOSED_WEDGE", [Leaf_cell.CLOSED_WEDGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("DART1_NOT_COLLINEAR_2", [DART1_NOT_COLLINEAR_2])) (fun fst_arg -> (use_arg_then2 ("ab_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
359 ((((fun arg_tac -> (use_arg_then2 ("wedge_in_fan_gt_eq_w_dart_fan", [wedge_in_fan_gt_eq_w_dart_fan])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
360 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_imp_conforming", [fully_surrounded_imp_conforming])) (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 arg -> thm_tac MP_TAC arg THEN (move ["confV"])));
361 (((fun arg_tac -> (use_arg_then2 ("fan_hypermaps_iso_explicit2", [fan_hypermaps_iso_explicit2])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN ((fun arg_tac -> arg_tac (Arg_term (`ext_dart _`))) (term_tac (set_tac "h"))));
362 (BETA_TAC THEN (move ["h_iso"]));
363 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Conforming.DARTSET_LEADS_INTO_SUBSET_WDART_FAN", [Conforming.DARTSET_LEADS_INTO_SUBSET_WDART_FAN])) (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 ("confV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`IMAGE h f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`h (a,b)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
365 ((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
366 ((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
367 (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)) THEN (done_tac));
368 ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("SUBSET_CLOSURE", [SUBSET_CLOSURE])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
369 ((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E x y`))) (term_tac (set_tac "y'")));
370 ((fun arg_tac -> arg_tac (Arg_term (`x,y IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["xy_in"]))));
371 (((((fun arg_tac -> (use_arg_then2 ("IN_TRANS", [IN_TRANS])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FACE_SUBSET_DART_OF_FAN", [FACE_SUBSET_DART_OF_FAN])) (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 snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
372 (((use_arg_then2 ("IN_TRANS", [IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`closure (aff_gt {vec 0} {x,y})`))) (term_tac exists_tac)));
373 ((((use_arg_then2 ("Planarity.POINT_IN_CLOSURE_AFF_GT_1_2", [Planarity.POINT_IN_CLOSURE_AFF_GT_1_2]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
374 ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (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 arg -> thm_tac MP_TAC arg THEN (move ["xyV"])));
375 ((((use_arg_then2 ("fanV", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan2", [fan2]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (case THEN (move ["n0V"])) THEN (move ["_"])));
376 ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ", [PAIR_IN_DART1_OF_FAN_IMP_NOT_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 ("x", [])) (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)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
377 ((split_tac) THEN (((use_arg_then2 ("n0V", [])) (disch_tac [])) THEN (clear_assumption "n0V") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
378 ((((use_arg_then2 ("CLOSURE_MINIMAL_EQ", [CLOSURE_MINIMAL_EQ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("CLOSED_CLOSURE", [CLOSED_CLOSURE]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
379 ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Cfyxfty.AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN))) (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 -> arg_tac (Arg_term (`h (x,y)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`IMAGE h f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
380 ((THENL_ROT (-1)) (ANTS_TAC));
381 (((((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ext_dart", [ext_dart]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Fan.pr2", [Fan.pr2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Fan.pr3", [Fan.pr3]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
382 ((((use_arg_then2 ("fully_surrounded_imp_fan80", [fully_surrounded_imp_fan80]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
383 ((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))));
384 (((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac));
385 ((BETA_TAC THEN (move ["z"]) THEN (move ["zV"])) THEN (((use_arg_then2 ("fully_surrounded_card_set_of_edge1", [fully_surrounded_card_set_of_edge1]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
386 (((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("h_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`x,y`))) (term_tac exists_tac)) THEN (done_tac));
389 (* Finalization of the section FullySurrounded *)
390 let fully_surrounded_simple_hypermap = Sections.finalize_theorem fully_surrounded_simple_hypermap;;
391 let f_surr_localization = Sections.finalize_theorem f_surr_localization;;
392 let f_surr_localization_convex_local = Sections.finalize_theorem f_surr_localization_convex_local;;
393 Sections.end_section "FullySurrounded";;
394 let RNSYJXM = REWRITE_RULE[IMP_IMP] f_surr_localization_convex_local;;
396 (* Close the module *)