formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl

   1 needs "tame/ssreflect/seq2-compiled.hl";;
   2 needs "hypermap/hypermap.hl";;
   3 needs "fan/HypermapAndFan.hl";;
   4 needs "fan/hypermap_iso-compiled.hl";;
   5
   6 (* Module List_hypermap*)
   7 module List_hypermap = struct
   8
   9 open Ssrbool;;
  10 open Ssrnat;;
  11 open Seq;;
  12 open Seq2;;
  13 open Hypermap;;
  14 open Hypermap_and_fan;;
  15 parse_as_infix ("::", (12, "right"));;
  16 override_interface ("::", `CONS`);;
  17 make_overloadable "++" `:A -> A -> A`;;
  18 overload_interface ("++", `cat`);;
  19 let darts_k = new_definition `darts_k k H = {d:A | d IN dart H /\ CARD (face H d) = k}`;;
  20 let face_set_k =
  21         new_definition `face_set_k k (H:(A)hypermap) = {f | f IN face_set H /\ CARD f = k}`;;
  22 let list_pairs = new_definition `list_pairs list = zip list (rot 1 list)`;;
  23 let list_of_darts = new_definition
  24         `list_of_darts L = foldr (\list all. (list_pairs list) ++ all) [] L`;;
  25 let darts_of_list = new_definition `darts_of_list L = set_of_list (list_of_darts L)`;;
  26 let list_of_faces = new_definition `list_of_faces L = MAP list_pairs L`;;
  27 let faces_of_list = new_definition `faces_of_list L = MAP set_of_list (list_of_faces L)`;;
  28 let list_of_elements = new_definition `list_of_elements L = undup (flatten L)`;;
  29 let elements_of_list = new_definition `elements_of_list L = set_of_list (list_of_elements L)`;;
  30 let list_of_nodes = new_definition
  31   `list_of_nodes L = MAP (\x. filter (\d. FST d = x) (list_of_darts L)) (list_of_elements L)`;;
  32 let nodes_of_list = new_definition `nodes_of_list L = MAP set_of_list (list_of_nodes L)`;;
  33 let list_of_faces3 = new_definition `list_of_faces3 (L:((A)list)list) =
  34   filter (\f. LENGTH f = 3) (list_of_faces L)`;;
  35 let list_of_faces4 = new_definition `list_of_faces4 (L:((A)list)list) =
  36   filter (\f. LENGTH f = 4) (list_of_faces L)`;;
  37 let list_of_faces5 = new_definition `list_of_faces5 (L:((A)list)list) =
  38   filter (\f. LENGTH f = 5) (list_of_faces L)`;;
  39 let list_of_faces6 = new_definition `list_of_faces6 (L:((A)list)list) =
  40   filter (\f. LENGTH f = 6) (list_of_faces L)`;;
  41 let list_of_darts3 = new_definition `list_of_darts3 (L:((A)list)list) =
  42   flatten (list_of_faces3 L)`;;
  43 let list_of_darts4 = new_definition `list_of_darts4 (L:((A)list)list) =
  44   flatten (list_of_faces4 L)`;;
  45 let list_of_darts5 = new_definition `list_of_darts5 (L:((A)list)list) =
  46   flatten (list_of_faces5 L)`;;
  47 let list_of_darts6 = new_definition `list_of_darts6 (L:((A)list)list) =
  48   flatten (list_of_faces6 L)`;;
  49 let find_list = (GEN_ALL o define) `find_list [] x = []
  50         /\ find_list (CONS h t) x = if (MEM x h) then h else find_list t x`;;
  51 let find_pair_list = (GEN_ALL o define) `find_pair_list [] d = []
  52    /\ find_pair_list (CONS h t) d = if (MEM d (list_pairs h)) then h else find_pair_list t d`;;
  53 let find_face = new_definition `find_face L d = find_list (list_of_faces L) d`;;
  54 let f_list = new_definition `f_list L d = next_el (find_face L d) d`;;
  55 let e_list = new_definition `e_list d = (SND d, FST d)`;;
  56 let n_list = new_definition `n_list L d = e_list (prev_el (find_face L d) d)`;;
  57 let f_list_ext = new_definition `f_list_ext L = res (f_list L) (darts_of_list L)`;;
  58 let e_list_ext = new_definition `e_list_ext L = res (e_list) (darts_of_list L)`;;
  59 let n_list_ext = new_definition `n_list_ext L = res (n_list L) (darts_of_list L)`;;
  60 let hypermap_of_list = new_definition
  61         `hypermap_of_list (L:((A)list)list) =
  62                 hypermap (darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L)`;;
  63 let good_list = new_definition `good_list L <=>
  64         uniq (list_of_darts L) /\
  65          all (\l. ~(l = [])) L /\
  66          (!d. MEM d (list_of_darts L) ==> MEM (SND d, FST d) (list_of_darts L))`;;
  67 let good_list_nodes = new_definition `good_list_nodes L <=>
  68         node_set (hypermap_of_list L) = set_of_list (nodes_of_list L)`;;
  69
  70 (* Lemma list_pairs_empty *)
  71 let list_pairs_empty = Sections.section_proof ["s"]
  72 `list_pairs s = [] <=> s = []`
  73 [
  74    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  75 ];;
  76
  77 (* Lemma list_of_darts_alt *)
  78 let list_of_darts_alt = Sections.section_proof ["L"]
  79 `list_of_darts L = flatten (list_of_faces L)`
  80 [
  81    ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))));
  82    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
  83 ];;
  84
  85 (* Lemma find_face_alt *)
  86 let find_face_alt = Sections.section_proof ["L";"d"]
  87 `find_face L d = list_pairs (find_pair_list L d)`
  88 [
  89    ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))));
  90    ((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]);
  91    (((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
  92    ((((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))));
  93    ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
  94 ];;
  95
  96 (* Lemma mem_find_list *)
  97 let mem_find_list = Sections.section_proof ["x";"L"]
  98 `MEM x (flatten L) ==> MEM (find_list L x) L`
  99 [
 100    ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])));
 101    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))));
 102    ((THENL_FIRST) (BETA_TAC THEN (case THEN (((THENL) case [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); (move ["lt"])]) THEN (move ["xl"])))) (((((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 103    ((((fun arg_tac -> arg_tac (Arg_term (`MEM x h`))) (disch_eq_tac "xh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 104 ];;
 105
 106 (* Lemma mem_find_face *)
 107 let mem_find_face = Sections.section_proof ["d";"L"]
 108 `MEM d (list_of_darts L)
 109         ==> MEM (find_face L d) (list_of_faces L)`
 110 [
 111    ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"]));
 112    (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list", [mem_find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 113 ];;
 114
 115 (* Lemma find_list_empty *)
 116 let find_list_empty = Sections.section_proof ["d";"L"]
 117 `find_list L d = [] <=> ~(MEM d (flatten L))`
 118 [
 119    ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))));
 120    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
 121    (((fun arg_tac -> arg_tac (Arg_term (`MEM d h`))) (disch_eq_tac "dh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 122    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(h = [])`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("dh", [])) (disch_tac [])) THEN (clear_assumption "dh") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 123    (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
 124    ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((split_tac) THEN (move ["h1"]) THEN (move ["x"])));
 125    ((((fun arg_tac -> arg_tac (Arg_term (`x = h`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((fun arg_tac ->(use_arg_then2 ("eq", []))(fun tmp_arg1 -> (use_arg_then2 ("h1", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 126    ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
 127 ];;
 128
 129 (* Lemma mem_find_list_nonempty *)
 130 let mem_find_list_nonempty = Sections.section_proof ["x";"L"]
 131 `all (\l. ~(l = [])) L
 132         ==> (MEM x (flatten L) <=> MEM (find_list L x) L)`
 133 [
 134    (((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["h1"]));
 135    ((THENL_FIRST) ((THENL) (split_tac) [ALL_TAC; (move ["h2"])]) (((use_arg_then2 ("mem_find_list", [mem_find_list])) (thm_tac apply_tac)) THEN (done_tac)));
 136    ((((fun arg_tac -> (use_arg_then2 ("h1", [])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 137 ];;
 138
 139 (* Lemma mem_find_face_nonempty *)
 140 let mem_find_face_nonempty = Sections.section_proof ["d";"L"]
 141 `all (\l. ~(l = [])) L
 142         ==> (MEM d (list_of_darts L) <=> MEM (find_face L d) (list_of_faces L))`
 143 [
 144    (BETA_TAC THEN (move ["h1"]));
 145    ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_list_nonempty", [mem_find_list_nonempty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 146    ((in_tac ["h1"] true ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac))) THEN ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["s"])));
 147    ((((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["l_L"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 148    (((((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 149 ];;
 150
 151 (* Lemma e_list_ext_involution *)
 152 let e_list_ext_involution = Sections.section_proof ["L"]
 153 `good_list L ==> e_list_ext L o e_list_ext L = I`
 154 [
 155    (((((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 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["h_uniq"])) THEN (case THEN (move ["all_n"])) THEN (move ["mem_snd"]) THEN (case THEN ((move ["x"]) THEN (move ["y"]))));
 156    ((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
 157    (((fun arg_tac -> arg_tac (Arg_term (`MEM (x,y) _`))) (disch_eq_tac "xy_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 158    ((((fun arg_tac -> (use_arg_then2 ("mem_snd", [])) (fun fst_arg -> (use_arg_then2 ("xy_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (simp_tac)) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 159    ((((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 160 ];;
 161 let INVERSE_EXISTS_IMP_BIJECTIVE = prove(`!(f:A->B) g. f o g = I /\ g o f = I ==> (!y. ?!x. f x = y)`,
 162    REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
 163      REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
 164      EXISTS_TAC `(g:B->A) y` THEN
 165      ASM_REWRITE_TAC[] THEN
 166      REPEAT STRIP_TAC THEN
 167      POP_ASSUM (MP_TAC o AP_TERM `g:B->A`) THEN
 168      ASM_REWRITE_TAC[]);;
 169
 170 (* Lemma e_list_ext_permutes_darts *)
 171 let e_list_ext_permutes_darts = Sections.section_proof ["L"]
 172 `good_list L
 173         ==> (e_list_ext L) permutes (darts_of_list L)`
 174 [
 175    (((((use_arg_then2 ("permutes", [permutes]))(thm_tac (new_rewrite [] [])))) THEN (move ["good_l"])) THEN (split_tac));
 176    ((BETA_TAC THEN (move ["x"]) THEN (move ["x_n"])) THEN ((((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_n", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 177    ((use_arg_then2 ("INVERSE_EXISTS_IMP_BIJECTIVE", [INVERSE_EXISTS_IMP_BIJECTIVE])) (thm_tac apply_tac));
 178    (((fun arg_tac -> arg_tac (Arg_term (`e_list_ext L`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("ETA_AX", [ETA_AX]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 179 ];;
 180
 181 (* Lemma dart_in_darts *)
 182 let dart_in_darts = Sections.section_proof ["d";"l";"L"]
 183 `MEM d (list_pairs l) /\ MEM l L
 184         ==> MEM d (list_of_darts L)`
 185 [
 186    (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]));
 187    (((fun arg_tac -> arg_tac (Arg_term (`list_pairs l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 188 ];;
 189
 190 (* Lemma mem_find_pair_list *)
 191 let mem_find_pair_list = Sections.section_proof ["d";"L"]
 192 `MEM d (list_of_darts L) ==> MEM (find_pair_list L d) L`
 193 [
 194    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 195    (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 196    ((((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 197 ];;
 198
 199 (* Lemma dart_in_find_pair_list *)
 200 let dart_in_find_pair_list = Sections.section_proof ["d";"L"]
 201 `MEM d (list_of_darts L) <=> MEM d (list_pairs (find_pair_list L d))`
 202 [
 203    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] []))))));
 204    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 205    ((((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] []))))));
 206    (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 207 ];;
 208
 209 (* Lemma dart_in_face *)
 210 let dart_in_face = Sections.section_proof ["d";"L"]
 211 `MEM d (list_of_darts L) <=> MEM d (find_face L d)`
 212 [
 213    (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 214 ];;
 215
 216 (* Lemma uniq_imp_unique_list *)
 217 let uniq_imp_unique_list = Sections.section_proof ["l1";"l2";"d";"L"]
 218 `uniq (list_of_darts L) /\ MEM l1 L /\ MEM l2 L
 219         /\ MEM d (list_pairs l1) /\ MEM d (list_pairs l2)
 220         ==> l1 = l2`
 221 [
 222    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
 223    ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))));
 224    ((((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))));
 225    (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_mem"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h1"])) THEN (case THEN (move ["h2"])) THEN (case THEN (move ["d_l1"])) THEN (move ["d_l2"]));
 226    ((THENL_LAST) (((use_arg_then2 ("h2", [])) (disch_tac [])) THEN (clear_assumption "h2") THEN ((use_arg_then2 ("h1", [])) (disch_tac [])) THEN (clear_assumption "h1") THEN case THEN (move ["h1"]) THEN (case THEN ALL_TAC) THEN (move ["h2"]) THEN ((TRY done_tac))) (((use_arg_then2 ("Ih", [])) (disch_tac [])) THEN (clear_assumption "Ih") THEN (exact_tac)));
 227    ((((fun arg_tac -> (use_arg_then2 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 228    ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 229    ((((fun arg_tac -> (use_arg_then2 ("not_mem", [])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("h2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_l2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
 230    ((((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("d_l1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 231 ];;
 232
 233 (* Lemma find_pair_list_unique *)
 234 let find_pair_list_unique = Sections.section_proof ["l";"d";"L"]
 235 `uniq (list_of_darts L) /\ MEM l L /\ MEM d (list_pairs l)
 236         ==> l = find_pair_list L d`
 237 [
 238    (BETA_TAC THEN (case THEN (move ["uniq_darts"])) THEN (case THEN (move ["l_L"])) THEN (move ["mem_d"]));
 239    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_imp_unique_list", [uniq_imp_unique_list])) (fun fst_arg -> (use_arg_then2 ("uniq_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 240    (((((use_arg_then2 ("l_L", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("dart_in_darts", [dart_in_darts])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 241 ];;
 242
 243 (* Lemma uniq_find_face *)
 244 let uniq_find_face = Sections.section_proof ["d";"L"]
 245 `uniq (list_of_darts L) ==> uniq (find_face L d)`
 246 [
 247    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
 248    (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["_"])) THEN (move ["uniq_t"]));
 249    ((((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_tac [])) THEN case THEN ((simp_tac THEN TRY done_tac))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 250 ];;
 251
 252 (* Lemma size_list_pairs *)
 253 let size_list_pairs = Sections.section_proof ["l"]
 254 `sizel (list_pairs l) = sizel l`
 255 [
 256    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size1_zip", [size1_zip]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 257 ];;
 258
 259 (* Lemma mem_list_pairs *)
 260 let mem_list_pairs = Sections.section_proof ["x";"y";"l"]
 261 `MEM (x,y) (list_pairs l) ==> MEM x l /\ MEM y l`
 262 [
 263    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_zip", [mem_zip])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("mem_rot", [mem_rot]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 264 ];;
 265
 266 (* Lemma mem_f_list *)
 267 let mem_f_list = Sections.section_proof ["d";"L"]
 268 `MEM d (list_of_darts L) ==> MEM (f_list L d) (find_face L d)`
 269 [
 270    ((BETA_TAC THEN (move ["mem_d"])) THEN ((((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 271 ];;
 272
 273 (* Lemma nth_list_pairs *)
 274 let nth_list_pairs = Sections.section_proof ["x0";"i";"s"]
 275 `i < sizel s
 276         ==> nth (x0, x0) (list_pairs s) i
 277                 = (nth x0 s i, nth x0 s (if i = sizel s - 1 then 0 else i + 1))`
 278 [
 279    ((BETA_TAC THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
 280    (((((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("fun_if", [fun_if]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 281 ];;
 282
 283 (* Lemma uniq_list_pairs *)
 284 let uniq_list_pairs = Sections.section_proof ["s"]
 285 `uniq s ==> uniq (list_pairs s)`
 286 [
 287    ((fun arg_tac -> arg_tac (Arg_term (`HD s`))) (term_tac (set_tac "x0")));
 288    (((((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("uniq_nthP", [uniq_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x0, x0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]) THEN (move ["i"]) THEN (move ["j"]) THEN (case THEN (move ["i_lt_j"])) THEN (move ["j_lt"]));
 289    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i_lt_j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac));
 290    ((repeat_tactic 1 9 (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 291    ((((use_arg_then2 ("j_lt", [])) (disch_tac [])) THEN (clear_assumption "j_lt") THEN ((use_arg_then2 ("i_lt_j", [])) (disch_tac [])) THEN (clear_assumption "i_lt_j") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 292 ];;
 293
 294 (* Lemma mem_list_pairs_explicit *)
 295 let mem_list_pairs_explicit = Sections.section_proof ["x";"y";"s"]
 296 `uniq s /\ MEM (x,y) (list_pairs s)
 297         ==> y = next_el s x`
 298 [
 299    (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i"])));
 300    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(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 (move ["i_lt"])) THEN (case THEN (move ["x_eq"])) THEN (move ["y_eq"]));
 301    ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (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 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac)));
 302    (((((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_eq", []))(gsym_then (thm_tac (new_rewrite [3] []))))) THEN (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 303 ];;
 304
 305 (* Lemma index_fst_snd *)
 306 let index_fst_snd = Sections.section_proof ["x0";"i";"x";"y";"s"]
 307 `uniq s /\ i < sizel s /\ nth (x0,x0) (list_pairs s) i = (x,y)
 308         ==> indexl x s = i /\ indexl y s = if (i = sizel s - 1) then 0 else i + 1`
 309 [
 310    (BETA_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["i_lt"])) THEN (simp_tac));
 311    (((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))))));
 312    (((repeat_tactic 1 9 (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_s", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 313 ];;
 314
 315 (* Lemma next_el_list_pairs *)
 316 let next_el_list_pairs = Sections.section_proof ["x";"y";"s"]
 317 `uniq s /\ MEM (x,y) (list_pairs s)
 318         ==> next_el (list_pairs s) (x,y) = (y, next_el s y)`
 319 [
 320    (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
 321    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM y s`))) (term_tac (have_gen_tac [](move ["ys"])))) ((((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 322    ((((fun arg_tac -> (use_arg_then2 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (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 ("next_el_alt", [next_el_alt])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 323    ((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "i")));
 324    ((fun arg_tac -> arg_tac (Arg_term (`nth (x,x) (list_pairs s) i = x,y`))) (term_tac (have_gen_tac [](move ["nth_i"]))));
 325    (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 326    ((fun arg_tac -> arg_tac (Arg_term (`i < sizel s`))) (term_tac (have_gen_tac [](move ["i_lt"]))));
 327    (((((use_arg_then2 ("i_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 328    ((repeat_tactic 1 9 (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 329    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 ((TRY done_tac)));
 330    (((fun arg_tac -> arg_tac (Arg_term (`i = sizel s - 1`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 331    ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 332    ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac));
 333    (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (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))) (fun fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 (done_tac));
 334    ((((fun arg_tac -> arg_tac (Arg_term (`0 = sizel s - 1`))) (disch_eq_tac "eq2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 335    ((THENL_FIRST) (((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 336    ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (split_tac));
 337    (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (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))) (fun fst_arg -> (use_arg_then2 ("s", [])) (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 -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_fst_snd", [index_fst_snd])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_lt", [])) (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 ("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 (done_tac));
 338    ((((fun arg_tac -> arg_tac (Arg_term (`i + 1 = _`))) (disch_eq_tac "eq2" [])) THEN case THEN (process_fst_eq_tac)) THEN (done_tac));
 339 ];;
 340
 341 (* Lemma prev_el_list_pairs *)
 342 let prev_el_list_pairs = Sections.section_proof ["x";"y";"s"]
 343 `uniq s /\ MEM (x,y) (list_pairs s)
 344         ==> prev_el (list_pairs s) (x,y) = (prev_el s x, x)`
 345 [
 346    (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
 347    ((fun arg_tac -> arg_tac (Arg_term (`prev_el _1 _2`))) (term_tac (set_tac "t")));
 348    ((fun arg_tac -> arg_tac (Arg_term (`MEM t (list_pairs s)`))) (term_tac (have_gen_tac [](move ["mem_t"]))));
 349    (((((use_arg_then2 ("t_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 350    (((use_arg_then2 ("t_def", [])) (disch_tac [])) THEN (clear_assumption "t_def") THEN ((use_arg_then2 ("mem_t", [])) (disch_tac [])) THEN (clear_assumption "mem_t") THEN ((use_arg_then2 ("t", [])) (disch_tac [])) THEN (clear_assumption "t") THEN case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["mem_t"]) THEN (move ["t_def"]));
 351    ((fun arg_tac -> arg_tac (Arg_term (`b = next_el s a`))) (term_tac (have_gen_tac []ALL_TAC)));
 352    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_list_pairs_explicit", [mem_list_pairs_explicit])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 353    ((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`prev_el s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC);
 354    (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (fun fst_arg -> (use_arg_then2 ("mem_t", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
 355    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`b = x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)))))));
 356    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`next_el (list_pairs s)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("t_def", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 357    ((((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_pairs", [uniq_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("next_el_list_pairs", [next_el_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 358 ];;
 359
 360 (* Lemma f_list_inverse *)
 361 let f_list_inverse = Sections.section_proof ["d";"L"]
 362 `uniq (list_of_darts L) /\ MEM d (list_of_darts L)
 363         ==> f_list L (prev_el (find_face L d) d) = d
 364         /\ prev_el (find_face L (f_list L d)) (f_list L d) = d`
 365 [
 366    ((BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (split_tac));
 367    ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
 368    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 369    (((((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 370    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
 371    (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 372    ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 373    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 374    ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
 375    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (next_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 376    (((((use_arg_then2 ("prev_next_id", [prev_next_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 377    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
 378    (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 379    ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_next_el", [mem_next_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 380    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 381 ];;
 382
 383 (* Lemma find_face_f_list *)
 384 let find_face_f_list = Sections.section_proof ["d";"L"]
 385 `uniq (list_of_darts L) /\ MEM d (list_of_darts L)
 386         ==> find_face L (f_list L d) = find_face L d`
 387 [
 388    (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d"]))));
 389    (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
 390    (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 391    (((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 392 ];;
 393
 394 (* Lemma f_list_ext_permutes_darts *)
 395 let f_list_ext_permutes_darts = Sections.section_proof ["L"]
 396 `uniq (list_of_darts L)
 397         ==> (f_list_ext L) permutes (darts_of_list L)`
 398 [
 399    (BETA_TAC THEN (move ["uniq_s"]));
 400    ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Hypermap_and_fan.RES_PERMUTES", [Hypermap_and_fan.RES_PERMUTES]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
 401    ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ALL_TAC]);
 402    (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_f_list", [find_face_f_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_f_list", [mem_f_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 403    ((THENL_ROT (-1)) ((THENL) (split_tac) [((move ["d"]) THEN (move ["mem_d"])); ((move ["d1"]) THEN (move ["d2"]) THEN (case THEN (move ["mem_d1"])) THEN (case THEN (move ["mem_d2"])) THEN (move ["eq"]))]));
 404    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["_"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))));
 405    (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("f_list_inverse", [f_list_inverse])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_d2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 406    ((fun arg_tac -> arg_tac (Arg_term (`prev_el (find_face L d) d`))) (term_tac exists_tac));
 407    ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))));
 408    ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
 409    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el f d) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 410    (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 411    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
 412    (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 413    ((((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 414    (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 415 ];;
 416
 417 (* Lemma find_face_empty *)
 418 let find_face_empty = Sections.section_proof ["d";"L"]
 419 `find_face L d = [] <=> ~MEM d (list_of_darts L)`
 420 [
 421    (((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list_empty", [find_list_empty]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 422 ];;
 423
 424 (* Lemma mem_find_face_imp_faces_eq *)
 425 let mem_find_face_imp_faces_eq = Sections.section_proof ["d1";"d2";"L"]
 426 `uniq (list_of_darts L) /\ MEM d1 (find_face L d2)
 427         ==> find_face L d1 = find_face L d2`
 428 [
 429    (BETA_TAC THEN (case THEN ((move ["uniq_s"]) THEN (move ["mem_d1"]))));
 430    (((repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))));
 431    (((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 432    ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 433    (((use_arg_then2 ("mem_d1", [])) (disch_tac [])) THEN (clear_assumption "mem_d1") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac));
 434    (((((use_arg_then2 ("find_face_empty", [find_face_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 435 ];;
 436
 437 (* Lemma mem_find_face_imp_mem_darts *)
 438 let mem_find_face_imp_mem_darts = Sections.section_proof ["d";"y";"L"]
 439 `MEM d (find_face L y) ==> MEM d (list_of_darts L)`
 440 [
 441    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
 442    ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))));
 443    (((fun arg_tac -> arg_tac (Arg_term (`MEM y _`))) (disch_eq_tac "mem_y" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 444    ((((((use_arg_then2 ("list_of_faces", [list_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face", [find_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("Ih", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 445 ];;
 446
 447 (* Lemma f_list_ext_inverse *)
 448 let f_list_ext_inverse = Sections.section_proof ["L"]
 449 `uniq (list_of_darts L)
 450         ==> inverse (f_list_ext L) = res (\d. prev_el (find_face L d) d) (darts_of_list L)`
 451 [
 452    ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["uniq_s"]) THEN (move ["d"]));
 453    (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSE_EQ", [PERMUTES_INVERSE_EQ])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_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 [] []))));
 454    ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
 455    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 456    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("f_list_inverse", [f_list_inverse]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 457    (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
 458    (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 459 ];;
 460
 461 (* Lemma f_list_ext_inverse_works *)
 462 let f_list_ext_inverse_works = Sections.section_proof ["L"]
 463 `uniq (list_of_darts L)
 464         ==> f_list_ext L o inverse (f_list_ext L) = I
 465         /\ inverse (f_list_ext L) o f_list_ext L = I`
 466 [
 467    (BETA_TAC THEN (move ["uniq_s"]));
 468    (((fun arg_tac -> (use_arg_then2 ("PERMUTES_INVERSES_o", [PERMUTES_INVERSES_o])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_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))) (disch_tac [])) THEN (exact_tac));
 469 ];;
 470
 471 (* Lemma n_eq_e_fi *)
 472 let n_eq_e_fi = Sections.section_proof ["L"]
 473 `uniq (list_of_darts L)
 474         ==> n_list_ext L = e_list_ext L o inverse (f_list_ext L)`
 475 [
 476    (BETA_TAC THEN (move ["uniq_s"]));
 477    (((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq_ext", [eq_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"]));
 478    ((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
 479    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 480    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM _1 _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))))) ((((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 481    (((use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
 482    (((((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 483 ];;
 484
 485 (* Lemma n_list_ext_permutes_darts *)
 486 let n_list_ext_permutes_darts = Sections.section_proof ["L"]
 487 `good_list L
 488         ==> (n_list_ext L) permutes (darts_of_list L)`
 489 [
 490    ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
 491    ((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_COMPOSE", [PERMUTES_COMPOSE]))(thm_tac (new_rewrite [] [])))));
 492    ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_INVERSE", [PERMUTES_INVERSE]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 493    (((fun arg_tac -> (use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
 494 ];;
 495
 496 (* Lemma e_n_f_id *)
 497 let e_n_f_id = Sections.section_proof ["L"]
 498 `good_list L
 499         ==> e_list_ext L o n_list_ext L o f_list_ext L = I`
 500 [
 501    ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
 502    (((((use_arg_then2 ("n_eq_e_fi", [n_eq_e_fi]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_ASSOC", [o_ASSOC]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("I_O_ID", [I_O_ID]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext_inverse_works", [f_list_ext_inverse_works]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 503 ];;
 504
 505 (* Lemma tuple_hypermap_of_list *)
 506 let tuple_hypermap_of_list = Sections.section_proof ["L"]
 507 `good_list L
 508         ==> tuple_hypermap (hypermap_of_list L) =
 509         darts_of_list L, e_list_ext L, n_list_ext L, f_list_ext L`
 510 [
 511    ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
 512    ((((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (CONJUNCT2 hypermap_tybij)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 513    ((((use_arg_then2 ("e_list_ext_permutes_darts", [e_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_list_ext_permutes_darts", [n_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 514    (((((use_arg_then2 ("e_n_f_id", [e_n_f_id]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 515 ];;
 516
 517 (* Lemma f_list_ext_orbit *)
 518 let f_list_ext_orbit = Sections.section_proof ["L";"x"]
 519 `MEM x (list_of_darts L) /\ uniq (list_of_darts L)
 520         ==> orbit_map (f_list_ext L) x = set_of_list (find_face L x)`
 521 [
 522    (BETA_TAC THEN (case THEN ((move ["mem_x"]) THEN (move ["uniq_l"]))));
 523    ((((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ORBIT_MAP_RES", [ORBIT_MAP_RES]))(thm_tac (new_rewrite [] [])))));
 524    (((((use_arg_then2 ("f_list_ext", [f_list_ext]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_list_ext_permutes_darts", [f_list_ext_permutes_darts]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 525    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM x (find_face L x)`))) (term_tac (have_gen_tac [](move ["x_in_face"])))) ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 526    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`orbit_map (f_list L) x = orbit_map (next_el (find_face L x)) x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 527    (((((use_arg_then2 ("next_el_orbit", [next_el_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 528    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`(f_list L POWER n) x = (next_el (find_face L x) POWER n) x`))) (term_tac (have_gen_tac ["n"](move ["eq"])))));
 529    (((repeat_tactic 1 9 (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 530    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))]) ((repeat_tactic 1 9 (((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 531    ((repeat_tactic 1 9 (((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] [])))));
 532    ((congr_tac (`next_el _1 _2`)) THEN ((TRY done_tac)));
 533    (((fun arg_tac -> (use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (fun fst_arg -> (use_arg_then2 ("uniq_l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 534    ((((fun arg_tac -> (use_arg_then2 ("next_el_power", [next_el_power])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 535    ((((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("DIVISION", [DIVISION]))(gsym_then (thm_tac (new_rewrite [] []))))));
 536    ((((use_arg_then2 ("x_in_face", [])) (disch_tac [])) THEN (clear_assumption "x_in_face") THEN BETA_TAC) THEN (((use_arg_then2 ("index_mem", [index_mem]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
 537 ];;
 538
 539 (* Lemma uniq_flatten *)
 540 let uniq_flatten = Sections.section_proof ["L"]
 541 `uniq (flatten L) /\ all (\l. ~(l = [])) L ==> uniq L`
 542 [
 543    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("uniq", [uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] [])))))));
 544    (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["h_n0"])) THEN (move ["all_t"]));
 545    ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
 546    ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["ht"])));
 547    ((((use_arg_then2 ("h_n0", [])) (disch_tac [])) THEN (clear_assumption "h_n0") THEN BETA_TAC) THEN (((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("lt0n", [lt0n]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("has_predT", [has_predT]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["xh"])) THEN (move ["_"])));
 548    (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("xh", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
 549    ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
 550 ];;
 551
 552 (* Lemma flatten_filter_empty *)
 553 let flatten_filter_empty = Sections.section_proof ["L"]
 554 `flatten (filter (\l. ~(l = [])) L) = flatten L`
 555 [
 556    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("filter", [filter]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
 557    (((fun arg_tac -> arg_tac (Arg_term (`h = []`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 558    (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 559    (((((use_arg_then2 ("flatten", [flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten", [flatten]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 560 ];;
 561
 562 (* Lemma uniq_sublist_unique *)
 563 let uniq_sublist_unique = Sections.section_proof ["l1";"l2";"L";"x"]
 564 `uniq (flatten L) /\ MEM l1 L /\ MEM l2 L
 565         /\ MEM x l1 /\ MEM x l2
 566         ==> l1 = l2`
 567 [
 568    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] []))))));
 569    (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_h"])) THEN (case THEN (move ["not_has"])) THEN (move ["uniq_t"]) THEN (case THEN (move ["c1"])) THEN (case THEN (move ["c2"])) THEN (case THEN (move ["x_l1"])) THEN (move ["x_l2"]));
 570    ((THENL_LAST) (((THENL) (((use_arg_then2 ("c2", [])) (disch_tac [])) THEN (clear_assumption "c2") THEN ((use_arg_then2 ("c1", [])) (disch_tac [])) THEN (clear_assumption "c1") THEN case) [(move ["eq1"]); (move ["l1t"])]) THEN ((THENL) case [(move ["eq2"]); (move ["l2t"])]) THEN ((TRY done_tac))) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 571    ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
 572    (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac));
 573    ((((use_arg_then2 ("not_has", [])) (disch_tac [])) THEN (clear_assumption "not_has") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN ((((use_arg_then2 ("hasP", [hasP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
 574    (((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("x_l2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l1", [])) (term_tac exists_tac)) THEN (done_tac));
 575 ];;
 576
 577 (* Lemma uniq_face_unique *)
 578 let uniq_face_unique = Sections.section_proof ["f1";"f2";"d";"L"]
 579 `uniq (list_of_darts L)
 580         /\ MEM f1 (list_of_faces L) /\ MEM f2 (list_of_faces L) /\ MEM d f1 /\ MEM d f2
 581         ==> f1 = f2`
 582 [
 583    (BETA_TAC THEN (case THEN (move ["uniq_l"])) THEN (case THEN (move ["mem_f1"])) THEN (case THEN (move ["mem_f2"])) THEN (case THEN (move ["mem_d1"])) THEN (move ["mem_d2"]));
 584    ((use_arg_then2 ("uniq_sublist_unique", [uniq_sublist_unique])) (thm_tac apply_tac));
 585    (((fun arg_tac -> arg_tac (Arg_term (`list_of_faces L`))) (term_tac exists_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)));
 586    ((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 587 ];;
 588
 589 (* Lemma mem_face_lemma *)
 590 let mem_face_lemma = Sections.section_proof ["f";"L"]
 591 `good_list L /\ MEM f (list_of_faces L)
 592         ==> ?d. MEM d (list_of_darts L) /\ f = find_face L d`
 593 [
 594    ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"]) THEN (move ["mem_f"]));
 595    ((fun arg_tac -> arg_tac (Arg_term (`HD f`))) (term_tac exists_tac));
 596    ((fun arg_tac -> arg_tac (Arg_term (`~(f = [])`))) (term_tac (have_gen_tac [](move ["f_n0"]))));
 597    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`all (\l. ~(l = [])) (list_of_faces L)`))) (term_tac (have_gen_tac []ALL_TAC))));
 598    ((((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("allPn", [allPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["f_eq"])) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 599    (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all_map", [all_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("preim", [preim]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_L"]) THEN (simp_tac));
 600    (((use_arg_then2 ("list_pairs_empty", [list_pairs_empty]))(thm_tac (new_rewrite [] []))));
 601    ((((use_arg_then2 ("all_n0", [])) (disch_tac [])) THEN (clear_assumption "all_n0") THEN BETA_TAC) THEN ((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (use_arg_then2 ("x_L", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (done_tac));
 602    ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) f`))) (term_tac (have_gen_tac [](move ["mem_hd"]))));
 603    ((((use_arg_then2 ("f_n0", [])) (disch_tac [])) THEN (clear_assumption "f_n0") THEN ((use_arg_then2 ("f", [])) (disch_tac [])) THEN (clear_assumption "f") THEN case THEN ((TRY done_tac)) THEN (move ["h"]) THEN (move ["t"])) THEN ((((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 604    (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] []))));
 605    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (HD f) = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
 606    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("uniq_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`HD f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 607    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`MEM (HD f) (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_hd2"])))));
 608    (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 609    (((((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("f", [])) (term_tac exists_tac)) THEN (done_tac));
 610 ];;
 611
 612 (* Lemma face_set_eq_list *)
 613 let face_set_eq_list = Sections.section_proof ["L"]
 614 `good_list L
 615         ==> face_set (hypermap_of_list L) = set_of_list (faces_of_list L)`
 616 [
 617    ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (case THEN (move ["all_n0"])) THEN (move ["_"])));
 618    ((((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
 619    (((((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["f"]));
 620    ((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
 621    ((THENL) (split_tac) [((case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ALL_TAC]);
 622    ((((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))));
 623    (((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 624    (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["ff"])) THEN (case THEN (move ["mem_ff"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 625    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_ff", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 626    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("f_list_ext_orbit", [f_list_ext_orbit]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 627 ];;
 628
 629 (* Lemma components_hypermap_of_list *)
 630 let components_hypermap_of_list = Sections.section_proof ["L"]
 631 `good_list L
 632         ==> dart (hypermap_of_list L) = darts_of_list L
 633         /\ edge_map (hypermap_of_list L) = e_list_ext L
 634         /\ node_map (hypermap_of_list L) = n_list_ext L
 635         /\ face_map (hypermap_of_list L) = f_list_ext L`
 636 [
 637    (BETA_TAC THEN (move ["good_s"]));
 638    ((((use_arg_then2 ("dart", [dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_map", [edge_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_map", [node_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_map", [face_map]))(thm_tac (new_rewrite [] [])))));
 639    ((((use_arg_then2 ("tuple_hypermap_of_list", [tuple_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 640 ];;
 641
 642 (* Lemma node_of_list_lemma *)
 643 let node_of_list_lemma = Sections.section_proof ["x";"L"]
 644 `set_of_list (filter (\d. FST d = x) (list_of_darts L))
 645         = {(x, y) | y | (x, y) IN darts_of_list L}`
 646 [
 647    (((((use_arg_then2 ("set_of_list_filter", [set_of_list_filter]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["d"]));
 648    ((THENL) (split_tac) [((case THEN (move ["y"])) THEN (move ["h"])); ((case THEN (move ["y"])) THEN (move ["h"]))]);
 649    (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 650    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac));
 651 ];;
 652
 653 (* Lemma image_lemma *)
 654 let image_lemma = Sections.section_proof ["f";"s"]
 655 `{f x | x IN s} = IMAGE f s`
 656 [
 657    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("andbC", [andbC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 658 ];;
 659
 660 (* Lemma set_nodes_of_list *)
 661 let set_nodes_of_list = Sections.section_proof ["L"]
 662 `set_of_list (nodes_of_list L)
 663         = {{(x, y) | y | (x, y) IN darts_of_list L} | x | x IN elements_of_list L}`
 664 [
 665    ((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SET_OF_LIST_MAP", [SET_OF_LIST_MAP]))(thm_tac (new_rewrite [] []))))));
 666    ((repeat_tactic 1 9 (((use_arg_then2 ("image_lemma", [image_lemma]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))));
 667    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["y"]));
 668    ((THENL) (split_tac) [((case THEN (move ["n"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["i"])) THEN (move ["h"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["i"])) THEN (move ["h"]))]);
 669    (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 670    ((fun arg_tac -> arg_tac (Arg_term (`filter (\d. FST d = i) (list_of_darts L)`))) (term_tac exists_tac));
 671    ((((use_arg_then2 ("node_of_list_lemma", [node_of_list_lemma]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac));
 672    (((use_arg_then2 ("i", [])) (term_tac exists_tac)) THEN (done_tac));
 673 ];;
 674
 675 (* Lemma good_list_node *)
 676 let good_list_node = Sections.section_proof ["L";"d"]
 677 `good_list L /\ good_list_nodes L /\ d IN darts_of_list L
 678         ==> node (hypermap_of_list L) d = {(FST d, y) | y | (FST d, y) IN darts_of_list L}`
 679 [
 680    ((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node_set", [node_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("node", [node]))(gsym_then (thm_tac (new_rewrite [] []))))));
 681    (((((use_arg_then2 ("set_nodes_of_list", [set_nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["good_s"])) THEN (case THEN (move ["eq"])) THEN (move ["d_in"]));
 682    (((fun arg_tac -> (use_arg_then2 ("eq", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`node (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 683    ((fun arg_tac -> arg_tac (Arg_term (`?x. _ x`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)))));
 684    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 685    ((BETA_TAC THEN (case THEN (move ["x"])) THEN (case THEN (move ["x_in"])) THEN (move ["eq"])) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))));
 686    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`x = FST d`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
 687    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("node_refl", [node_refl])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (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));
 688    ((((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["y"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 689 ];;
 690
 691 (* Lemma prev_el_list_pairs_general *)
 692 let prev_el_list_pairs_general = Sections.section_proof ["x";"y";"s"]
 693 `MEM (x,y) (list_pairs s)
 694         ==> ?z. prev_el (list_pairs s) (x,y) = (z,x) /\ MEM (z,x) (list_pairs s)`
 695 [
 696    (BETA_TAC THEN (move ["mem_xy"]));
 697    ((fun arg_tac -> arg_tac (Arg_term (`FST (prev_el (list_pairs s) (x,y))`))) (term_tac (set_tac "z")));
 698    ((use_arg_then2 ("z", [])) (term_tac exists_tac));
 699    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["eq"]))))) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 700    ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`SND (prev_el (list_pairs s) (x,y)) = x`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [2] []))))))))) (((((use_arg_then2 ("z_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 701    ((((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 702    ((fun arg_tac -> arg_tac (Arg_term (`indexl (x,y) _`))) (term_tac (set_tac "k")));
 703    ((fun arg_tac -> arg_tac (Arg_term (`sizel s`))) (term_tac (set_tac "n")));
 704    ((fun arg_tac -> arg_tac (Arg_term (`k < n:num`))) (term_tac (have_gen_tac [](move ["k_lt"]))));
 705    (((((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 706    ((fun arg_tac -> arg_tac (Arg_term (`nth x s k = x`))) (term_tac (have_gen_tac [](move ["nth_s"]))));
 707    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 708    ((((((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 709    ((((use_arg_then2 ("nth_shift_right", [nth_shift_right]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))));
 710    (((fun arg_tac -> arg_tac (Arg_term (`k = 0`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
 711    ((THENL_LAST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 712    ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 713    ((THENL_FIRST) ((((use_arg_then2 ("nth_zip", [nth_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_shift_left", [nth_shift_left]))(thm_tac (new_rewrite [] []))))) ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 714    ((THENL_FIRST) (((use_arg_then2 ("subnK", [subnK]))(thm_tac (new_rewrite [] [])))) ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 715    (((((use_arg_then2 ("nth_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 716 ];;
 717
 718 (* Lemma n_list_ext_fst *)
 719 let n_list_ext_fst = Sections.section_proof ["x";"y";"L"]
 720 `good_list L /\ (x,y) IN darts_of_list L
 721         ==> ?z. n_list_ext L (x,y) = (x,z) /\ (x,z) IN darts_of_list L`
 722 [
 723    (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"]))));
 724    ((((use_arg_then2 ("xy_in", [])) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (move ["mem_xy"])));
 725    ((fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (fun fst_arg -> (use_arg_then2 ("mem_xy", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["z"]) THEN (case THEN ((move ["eq"]) THEN (move ["mem_zx"])))))));
 726    ((use_arg_then2 ("z", [])) (term_tac exists_tac));
 727    ((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["n_eq"]))));
 728    (((((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("xy_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 729    ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
 730    (((((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 731 ];;
 732
 733 (* Lemma list_ext_power_in_darts *)
 734 let list_ext_power_in_darts = Sections.section_proof ["d";"L";"n"]
 735 `good_list L /\ d IN darts_of_list L
 736         ==> (e_list_ext L POWER n) d IN darts_of_list L /\
 737             (n_list_ext L POWER n) d IN darts_of_list L /\
 738             (f_list_ext L POWER n) d IN darts_of_list L`
 739 [
 740    ((BETA_TAC THEN (case THEN (move ["good_s"]))) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac))) THEN (move ["d_in"])));
 741    ((((use_arg_then2 ("lemma_dart_invariant_power_node", [lemma_dart_invariant_power_node]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 742    ((((use_arg_then2 ("lemma_dart_invariant_power_face", [lemma_dart_invariant_power_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
 743    (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`edge (hypermap_of_list L) d`))) (term_tac exists_tac)));
 744    (((((use_arg_then2 ("lemma_edge_subset", [lemma_edge_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("lemma_in_edge2", [lemma_in_edge2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 745 ];;
 746
 747 (* Lemma fst_n_list_ext_power *)
 748 let fst_n_list_ext_power = Sections.section_proof ["x";"y";"L";"n"]
 749 `good_list L /\ x,y IN darts_of_list L
 750         ==> FST ((n_list_ext L POWER n) (x,y)) = x`
 751 [
 752    (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["xy_in"]))));
 753    ((THENL_FIRST) ((THENL) (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN elim) [ALL_TAC; ((move ["n"]) THEN (move ["Ih"]))]) (((((use_arg_then2 ("POWER_0", [POWER_0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 754    ((fun arg_tac -> arg_tac (Arg_term (`(n_list_ext L POWER n) (x,y)`))) (term_tac (set_tac "d")));
 755    ((((use_arg_then2 ("COM_POWER", [COM_POWER]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_def", []))(thm_tac (new_rewrite [] [])))));
 756    ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("n_list_ext_fst", [n_list_ext_fst])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`FST d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
 757    ((((use_arg_then2 ("PAIR", [PAIR]))(thm_tac (new_rewrite [] [])))) THEN (ANTS_TAC));
 758    (((((use_arg_then2 ("d_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_ext_power_in_darts", [list_ext_power_in_darts]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 759    ((BETA_TAC THEN (case THEN (move ["z"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 760 ];;
 761
 762 (* Lemma mem_list_pairs_exists *)
 763 let mem_list_pairs_exists = Sections.section_proof ["x";"l"]
 764 `MEM x l <=> ?y. MEM (x,y) (list_pairs l)`
 765 [
 766    ((THENL) (split_tac) [(move ["mem_x"]); ((case THEN (move ["y"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_list_pairs", [mem_list_pairs])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (simp_tac))]);
 767    ((fun arg_tac -> arg_tac (Arg_term (`next_el l x`))) (term_tac exists_tac));
 768    (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nthP", [nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,next_el l x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x,x`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
 769    ((fun arg_tac -> arg_tac (Arg_term (`indexl x l`))) (term_tac exists_tac));
 770    ((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
 771    ((((use_arg_then2 ("nth_list_pairs", [nth_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 772    ((((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth0", [nth0]))(gsym_then (thm_tac (new_rewrite [] []))))));
 773    ((((fun arg_tac -> arg_tac (Arg_term (`indexl x l = _`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN (done_tac));
 774 ];;
 775
 776 (* Lemma mem_list_of_darts *)
 777 let mem_list_of_darts = Sections.section_proof ["d";"L"]
 778 `MEM d (list_of_darts L)
 779         <=> ?l. MEM l L /\ MEM d (list_pairs l)`
 780 [
 781    ((THENL_LAST) ((THENL) (split_tac) [ALL_TAC; ((case THEN (move ["l"])) THEN (case THEN ((move ["mem_l"]) THEN (move ["mem_d"]))))]) (((use_arg_then2 ("dart_in_darts", [dart_in_darts])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac)));
 782    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("foldr", [foldr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
 783    ((((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))));
 784    ((THENL_FIRST) (case THEN (move ["mem_d"])) (((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac)));
 785    (((fun arg_tac -> (use_arg_then2 ("Ih", [])) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (move ["mem_d2"]));
 786    (((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
 787 ];;
 788
 789 (* Lemma mem_list_of_elements *)
 790 let mem_list_of_elements = Sections.section_proof ["x";"L"]
 791 `MEM x (list_of_elements L)
 792         <=> ?y. MEM (x,y) (list_of_darts L)`
 793 [
 794    ((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))));
 795    ((((use_arg_then2 ("SWAP_EXISTS_THM", [SWAP_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("RIGHT_EXISTS_AND_THM", [RIGHT_EXISTS_AND_THM]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))));
 796    ((((use_arg_then2 ("mem_list_pairs_exists", [mem_list_pairs_exists]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
 797 ];;
 798
 799 (* Lemma uniq_node *)
 800 let uniq_node = Sections.section_proof ["L";"n"]
 801 `good_list L /\ MEM n (list_of_nodes L) ==> uniq n`
 802 [
 803    (((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["uniq_s"])) THEN (move ["_"]) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
 804    ((((use_arg_then2 ("filter_uniq", [filter_uniq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 805 ];;
 806
 807 (* Lemma uniq_face *)
 808 let uniq_face = Sections.section_proof ["L";"f"]
 809 `good_list L /\ MEM f (list_of_faces L) ==> uniq f`
 810 [
 811    ((BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_f"])))) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["h"])));
 812    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
 813    ((((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 814 ];;
 815
 816 (* Lemma list_of_darts_nil *)
 817 let list_of_darts_nil = Sections.section_proof []
 818 `list_of_darts [] = []`
 819 [
 820    (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 821 ];;
 822
 823 (* Lemma list_of_darts_cons *)
 824 let list_of_darts_cons = Sections.section_proof ["h";"t"]
 825 `list_of_darts (h :: t) = list_pairs h ++ list_of_darts t`
 826 [
 827    (((((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts", [list_of_darts]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 828 ];;
 829
 830 (* Lemma list_of_darts_cat *)
 831 let list_of_darts_cat = Sections.section_proof ["s1";"s2"]
 832 `list_of_darts (s1 ++ s2) = list_of_darts s1 ++ list_of_darts s2`
 833 [
 834    (((THENL) (((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(fun tmp_arg1 -> (use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(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 10 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
 835    (((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 836 ];;
 837
 838 (* Lemma good_list_uniq *)
 839 let good_list_uniq = Sections.section_proof ["L"]
 840 `good_list L ==> uniq L`
 841 [
 842    ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (case THEN (move ["allL"])) THEN (move ["_"]));
 843    (((THENL) (((use_arg_then2 ("uniqL", [])) (disch_tac [])) THEN (clear_assumption "uniqL") THEN ((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN ((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL uniq)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
 844    (((((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat_uniq", [cat_uniq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hasPn", [hasPn]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["h_neq"])) THEN (move ["all_t"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["mem_h"])) THEN (move ["uniq_t"]));
 845    ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
 846    ((fun arg_tac -> arg_tac (Arg_term (`?d. MEM d (list_pairs h)`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["mem_d"]))))));
 847    ((THENL_LAST) (((THENL) (((fun arg_tac -> arg_tac (Arg_term (`list_pairs h`))) (disch_eq_tac "eq" [])) THEN case) [ALL_TAC; ((move ["h'"]) THEN (move ["t'"]))]) THEN (process_fst_eq_tac)) (((use_arg_then2 ("h'", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
 848    ((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h_neq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 849    ((((use_arg_then2 ("mem_h", [])) (disch_tac [])) THEN (clear_assumption "mem_h") THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_imply", [negb_imply]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (move ["mem_h"])));
 850    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
 851    ((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
 852 ];;
 853
 854 (* Lemma list_pairs_inj *)
 855 let list_pairs_inj = Sections.section_proof ["s1";"s2"]
 856 `list_pairs s1 = list_pairs s2 ==> s1 = s2`
 857 [
 858    ((repeat_tactic 1 9 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`unzip1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))));
 859    (((repeat_tactic 1 9 (((use_arg_then2 ("unzip1_zip", [unzip1_zip]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 860 ];;
 861
 862 (* Lemma uniq_list_of_faces *)
 863 let uniq_list_of_faces = Sections.section_proof ["L"]
 864 `good_list L ==> uniq (list_of_faces L)`
 865 [
 866    ((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"]));
 867    ((((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_uniq", [map_inj_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("good_list_uniq", [good_list_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["y"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("list_pairs_inj", [list_pairs_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
 868 ];;
 869
 870 (* Lemma uniq_faces_of_list *)
 871 let uniq_faces_of_list = Sections.section_proof ["L"]
 872 `good_list L ==> uniq (faces_of_list L)`
 873 [
 874    ((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"]));
 875    (((((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_faces", [uniq_list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["f1"]) THEN (move ["f2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"]));
 876    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN (move ["d"]))));
 877    ((((use_arg_then2 ("dart_in_face", [dart_in_face]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["mem_d"])) THEN (move ["f1_eq"]));
 878    (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("uniq_face_unique", [uniq_face_unique])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (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))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
 879    ((THENL_FIRST) (((((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac)) ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
 880    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f1_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 881 ];;
 882
 883 (* Lemma card_faces_of_list *)
 884 let card_faces_of_list = Sections.section_proof ["L"]
 885 `good_list L
 886         ==> CARD (face_set (hypermap_of_list L)) = sizel (list_of_faces L)`
 887 [
 888    ((BETA_TAC THEN (move ["goodL"])) THEN ((((use_arg_then2 ("face_set_eq_list", [face_set_eq_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
 889    ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_faces_of_list", [uniq_faces_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 890    (((((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 891 ];;
 892
 893 (* Lemma card_darts_of_list *)
 894 let card_darts_of_list = Sections.section_proof ["L"]
 895 `good_list L
 896         ==> CARD (dart (hypermap_of_list L)) = sizel (list_of_darts L)`
 897 [
 898    (BETA_TAC THEN (move ["goodL"]));
 899    ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 900    ((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN (clear_assumption "goodL") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 901 ];;
 902
 903 (* Lemma uniq_list_of_elements *)
 904 let uniq_list_of_elements = Sections.section_proof ["L"]
 905 `uniq (list_of_elements L)`
 906 [
 907    (((((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("undup_uniq", [undup_uniq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 908 ];;
 909
 910 (* Lemma uniq_list_of_nodes *)
 911 let uniq_list_of_nodes = Sections.section_proof ["L"]
 912 `uniq (list_of_nodes L)`
 913 [
 914    (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))) THEN (move ["a"]) THEN (move ["b"]));
 915    ((repeat_tactic 1 9 (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["c"]) THEN (move ["mem_a"]))) THEN (case THEN ((move ["d"]) THEN (move ["mem_b"]))));
 916    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`MEM (a,c)`))) (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 (DISCH_THEN (fun snd_th -> (use_arg_then2 ("EQ_IMP", [EQ_IMP])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_a", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 917 ];;
 918
 919 (* Lemma mem_not_nil *)
 920 let mem_not_nil = Sections.section_proof ["s"]
 921 `~(s = []) <=> (?x. MEM x s)`
 922 [
 923    (((THENL) (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("NOT_CONS_NIL", [NOT_CONS_NIL]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("h", [])) (term_tac exists_tac)) THEN (done_tac));
 924 ];;
 925
 926 (* Lemma node_of_list_not_nil *)
 927 let node_of_list_not_nil = Sections.section_proof ["L";"n"]
 928 `MEM n (list_of_nodes L) ==> ~(n = [])`
 929 [
 930    (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["a"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["b"])) THEN (move ["mem_ab"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 931    (((((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)));
 932    (((((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_ab", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 933 ];;
 934
 935 (* Lemma nodes_of_list_eq *)
 936 let nodes_of_list_eq = Sections.section_proof ["L";"n1";"n2";"a"]
 937 `MEM n1 (list_of_nodes L) /\ MEM n2 (list_of_nodes L) /\
 938         MEM a n1 /\ MEM a n2 ==> n1 = n2`
 939 [
 940    ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
 941    (BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["x"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (move ["mem_xy"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (case THEN ALL_TAC) THEN (case THEN (move ["u"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["v"])) THEN (move ["mem_uv"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 942    ((((repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 943 ];;
 944
 945 (* Lemma uniq_nodes_of_list *)
 946 let uniq_nodes_of_list = Sections.section_proof ["L"]
 947 `uniq (nodes_of_list L)`
 948 [
 949    (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("map_inj_in_uniq", [map_inj_in_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_nodes", [uniq_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["n1"]) THEN (move ["n2"]) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["mem1"]) THEN (move ["mem2"]))) THEN (move ["eq"]));
 950    ((fun arg_tac -> arg_tac (Arg_term (`?d. d IN set_of_list n1`))) (term_tac (have_gen_tac [](case THEN ((move ["d"]) THEN (move ["d_in"]))))));
 951    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("node_of_list_not_nil", [node_of_list_not_nil])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 952    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nodes_of_list_eq", [nodes_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("mem1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
 953 ];;
 954
 955 (* Lemma size_list_of_nodes *)
 956 let size_list_of_nodes = Sections.section_proof ["L"]
 957 `sizel (list_of_nodes L) = sizel (list_of_elements L)`
 958 [
 959    (((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 960 ];;
 961
 962 (* Lemma card_nodes_of_list *)
 963 let card_nodes_of_list = Sections.section_proof ["L"]
 964 `CARD (set_of_list (nodes_of_list L)) = sizel (list_of_elements L)`
 965 [
 966    ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_nodes_of_list", [uniq_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
 967    (((((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_map", [size_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_of_nodes", [size_list_of_nodes]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 968 ];;
 969
 970 (* Lemma surj_delete *)
 971 let surj_delete = Sections.section_proof ["f";"s";"t";"a";"b"]
 972 `SURJ f s t /\ f a = f b /\ a IN s /\ b IN s /\ ~(a = b)
 973         ==> SURJ f (s DELETE a) t`
 974 [
 975    ((((repeat_tactic 1 9 (((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_DELETE", [IN_DELETE]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["f_in"]) THEN (move ["f_surj"]))) THEN (case THEN (move ["eq"])) THEN (case THEN (move ["a_in"])) THEN (case THEN (move ["b_in"])) THEN (move ["neq"])) THEN (split_tac));
 976    ((BETA_TAC THEN (move ["x"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_in", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 977    (BETA_TAC THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("f_surj", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (move ["f_eq"]));
 978    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`y = a`))) (disch_eq_tac "y_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)));
 979    (((use_arg_then2 ("b", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("b_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("y_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 980 ];;
 981
 982 (* Lemma fst_node_hypermap_of_list *)
 983 let fst_node_hypermap_of_list = Sections.section_proof ["L";"d"]
 984 `good_list L
 985         ==> (!x. x IN node (hypermap_of_list L) d ==> FST x = FST d)`
 986 [
 987    (((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN BETA_TAC THEN (case THEN ((move ["a"]) THEN (move ["b"]))) THEN (move ["goodL"]) THEN (move ["x"]));
 988    ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
 989    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
 990    ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`a,b IN darts_of_list L`))) (disch_eq_tac "ab_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
 991    ((((((use_arg_then2 ("lemma_node_exception", [lemma_node_exception]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) 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));
 992    (((((use_arg_then2 ("node", [node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbit_map", [orbit_map]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["k"])) THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
 993    (((((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_n_list_ext_power", [fst_n_list_ext_power]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 994 ];;
 995
 996 (* Lemma fst_choice_node_hypermap_of_list *)
 997 let fst_choice_node_hypermap_of_list = Sections.section_proof ["L";"d"]
 998 `good_list L
 999         ==> FST (CHOICE (node (hypermap_of_list L) d)) = FST d`
1000 [
1001    ((BETA_TAC THEN (move ["goodL"])) THEN (((fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)));
1002    ((((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEMBER_NOT_EMPTY", [MEMBER_NOT_EMPTY]))(gsym_then (thm_tac (new_rewrite [] []))))));
1003    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("node_refl", [node_refl]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1004 ];;
1005
1006 (* Lemma surj_fst_nodes_hypermap_of_list *)
1007 let surj_fst_nodes_hypermap_of_list = Sections.section_proof ["L"]
1008 `good_list L
1009         ==> SURJ (\n. FST (CHOICE n)) (node_set (hypermap_of_list L)) (elements_of_list L)`
1010 [
1011    (((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))))) THEN (move ["goodL"]));
1012    ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
1013    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
1014    (((THENL) (split_tac) [((move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_in"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); (move ["a"])]) THEN (simp_tac));
1015    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
1016    (((fun arg_tac -> arg_tac (Arg_term (`SND d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1017    ((((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["b"])));
1018    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["ab_in"]));
1019    ((fun arg_tac -> arg_tac (Arg_term (`node H (a,b)`))) (term_tac exists_tac));
1020    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
1021    ((((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
1022 ];;
1023
1024 (* Lemma good_list_nodes_condition *)
1025 let good_list_nodes_condition = Sections.section_proof ["L"]
1026 `good_list L
1027    ==> (good_list_nodes L <=> CARD (node_set (hypermap_of_list L)) = sizel (list_of_elements L))`
1028 [
1029    ((THENL_FIRST) (((((use_arg_then2 ("good_list_nodes", [good_list_nodes]))(thm_tac (new_rewrite [] [])))) THEN (move ["goodL"])) THEN ((split_tac) THEN (move ["eq"]))) (((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
1030    (((((use_arg_then2 ("SUBSET_CARD_EQ", [SUBSET_CARD_EQ]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("card_nodes_of_list", [card_nodes_of_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(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 (move ["n"]));
1031    ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"])));
1032    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
1033    ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("lemma_node_representation", [lemma_node_representation])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["r"])) THEN (case THEN (move ["r_in"])) THEN (move ["n_eq"]));
1034    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM r (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_r"])))) (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
1035    ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nodes_of_list", [nodes_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))));
1036    (((fun arg_tac -> arg_tac (Arg_term (`filter (\y. FST y = FST r) (list_of_darts L)`))) (term_tac exists_tac)) THEN (split_tac));
1037    ((((use_arg_then2 ("list_of_nodes", [list_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))));
1038    ((((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
1039    (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
1040    ((fun arg_tac -> arg_tac (Arg_term (`set_of_list _`))) (term_tac (set_tac "s")));
1041    (((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (move ["neq"]));
1042    ((fun arg_tac -> arg_tac (Arg_term (`n PSUBSET s`))) (term_tac (have_gen_tac []ALL_TAC)));
1043    (((((use_arg_then2 ("PSUBSET", [PSUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (move ["x_in"]));
1044    ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))));
1045    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fst_node_hypermap_of_list", [fst_node_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1046    (((use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (thm_tac apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`node H r`))) (term_tac exists_tac)));
1047    (((((use_arg_then2 ("lemma_node_subset", [lemma_node_subset]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1048    ((((use_arg_then2 ("PSUBSET_ALT", [PSUBSET_ALT]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["a"])) THEN (case THEN (move ["a_in"])) THEN (move ["a_n_in"]));
1049    ((fun arg_tac -> arg_tac (Arg_term (`~(sizel (list_of_elements L) = 0)`))) (term_tac (have_gen_tac [](move ["size_gt0"]))));
1050    ((((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_not_nil", [mem_not_nil]))(thm_tac (new_rewrite [] [])))));
1051    (((fun arg_tac -> arg_tac (Arg_term (`FST r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] [])))));
1052    (((fun arg_tac -> arg_tac (Arg_term (`SND r`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
1053    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`sizel (list_of_elements L) <= CARD (node_set H DELETE n) `))) (term_tac (have_gen_tac []ALL_TAC))));
1054    ((((use_arg_then2 ("CARD_DELETE", [CARD_DELETE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_HYPERMAP_ORBITS", [FINITE_HYPERMAP_ORBITS]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1055    ((((use_arg_then2 ("size_gt0", [])) (disch_tac [])) THEN (clear_assumption "size_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
1056    ((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))));
1057    ((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.surj_imp_card_le", [Hypermap_iso.surj_imp_card_le])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`\x. FST (CHOICE x)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac));
1058    ((((use_arg_then2 ("FINITE_DELETE", [FINITE_DELETE]))(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 [] [])))));
1059    (((use_arg_then2 ("surj_delete", [surj_delete])) (thm_tac apply_tac)) THEN (((fun arg_tac -> arg_tac (Arg_term (`node H a`))) (term_tac exists_tac)) THEN (simp_tac)));
1060    ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1; 2] []))))) THEN (((use_arg_then2 ("surj_fst_nodes_hypermap_of_list", [surj_fst_nodes_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1061    ((fun arg_tac -> arg_tac (Arg_term (`a IN dart H`))) (term_tac (have_gen_tac [](move ["a_in2"]))));
1062    ((((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
1063    ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN (((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1064    ((((use_arg_then2 ("n_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("lemma_in_node_set", [lemma_in_node_set]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("a_in2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("r_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("fst_choice_node_hypermap_of_list", [fst_choice_node_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1065    ((((use_arg_then2 ("lemma_different_nodes", [lemma_different_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("n_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((simp_tac THEN TRY done_tac)));
1066    ((((use_arg_then2 ("a_in", [])) (disch_tac [])) THEN (clear_assumption "a_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
1067 ];;
1068
1069 (* Lemma plain_hypermap_of_list *)
1070 let plain_hypermap_of_list = Sections.section_proof ["L"]
1071 `good_list L ==> plain_hypermap (hypermap_of_list L)`
1072 [
1073    ((BETA_TAC THEN (move ["goodL"])) THEN ((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypL"]))));
1074    (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list_ext_involution", [e_list_ext_involution]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1075 ];;
1076
1077 (* Lemma edge_CARD_dart *)
1078 let edge_CARD_dart = Sections.section_proof ["H"]
1079 `plain_hypermap H /\ is_edge_nondegenerate H
1080         ==> CARD (dart H) = 2 * number_of_edges H`
1081 [
1082    (((((use_arg_then2 ("plain_hypermap", [plain_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("is_edge_nondegenerate", [is_edge_nondegenerate]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["plain"]) THEN (move ["edge_nd"]))));
1083    ((((use_arg_then2 ("number_of_edges", [number_of_edges]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("edge_set", [edge_set]))(thm_tac (new_rewrite [] [])))));
1084    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("lemma_card_eq", [lemma_card_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("number_of_orbits", [number_of_orbits]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
1085    (((repeat_tactic 1 9 (((use_arg_then2 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["x_in"]));
1086    ((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL lemma_orbit_of_size_2))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`dart H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("edge_map_and_darts", [edge_map_and_darts]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
1087    (((((use_arg_then2 ("edge_nd", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("o_THM", [o_THM])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`edge_map H`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("plain", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1088 ];;
1089
1090 (* Lemma good_list_nodes_size_condition *)
1091 let good_list_nodes_size_condition = Sections.section_proof ["L"]
1092 `good_list L /\ planar_hypermap (hypermap_of_list L)
1093      /\ connected_hypermap (hypermap_of_list L) /\ is_edge_nondegenerate (hypermap_of_list L)
1094         ==> (good_list_nodes L <=>
1095                 2 * (sizel (list_of_elements L) + sizel (list_of_faces L)) =
1096                         sizel (list_of_darts L) + 4)`
1097 [
1098    (BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["planarL"])) THEN (case THEN (move ["connL"])) THEN (move ["nondL"]));
1099    ((((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
1100    ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "H")));
1101    ((THENL_FIRST) ((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
1102    ((((use_arg_then2 ("planarL", [])) (disch_tac [])) THEN (clear_assumption "planarL") THEN ((use_arg_then2 ("connL", [])) (disch_tac [])) THEN (clear_assumption "connL") THEN BETA_TAC) THEN (((((use_arg_then2 ("planar_hypermap", [planar_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("connected_hypermap", [connected_hypermap]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
1103    ((THENL_FIRST) (((fun arg_tac -> (use_arg_then2 ("eqn_pmul2l", [eqn_pmul2l])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`2`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) ((arith_tac) THEN (done_tac)));
1104    ((repeat_tactic 1 9 (((use_arg_then2 ("muln_addr", [muln_addr]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("edge_CARD_dart", [edge_CARD_dart]))(gsym_then (thm_tac (new_rewrite [] []))))));
1105    (((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("plain_hypermap_of_list", [plain_hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1106    ((((use_arg_then2 ("card_faces_of_list", [card_faces_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("number_of_faces", [number_of_faces]))(gsym_then (thm_tac (new_rewrite [] []))))));
1107    ((((use_arg_then2 ("card_darts_of_list", [card_darts_of_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))));
1108    ((arith_tac) THEN (done_tac));
1109 ];;
1110
1111 (* Lemma face_of_list *)
1112 let face_of_list = Sections.section_proof ["L";"d"]
1113 `good_list L /\ MEM d (list_of_darts L)
1114         ==> face (hypermap_of_list L) d = set_of_list (find_face L d)`
1115 [
1116    (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"]))));
1117    ((fun arg_tac -> (use_arg_then2 ("face_set_eq_list", [face_set_eq_list])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
1118    ((((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] []))))));
1119    ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
1120    ((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN ((fun arg_tac ->  (conv_thm_tac DISCH_THEN)  (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`face (hypermap_of_list L) d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)));
1121    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`face _1 d IN _2`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) (((((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (done_tac)));
1122    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("faces_of_list", [faces_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["f"])) THEN (case THEN (move ["mem_f"])) THEN (move ["face_eq"]));
1123    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d2"]) THEN (case THEN (move ["mem_d2"])) THEN (move ["f_eq"])))));
1124    (((((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 _2`)) THEN ((TRY done_tac))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))));
1125    ((use_arg_then2 ("mem_find_face_imp_faces_eq", [mem_find_face_imp_faces_eq])) (thm_tac apply_tac));
1126    ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
1127    (((((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1128 ];;
1129
1130 (* Lemma card_face_of_list *)
1131 let card_face_of_list = Sections.section_proof ["L";"d"]
1132 `good_list L /\ MEM d (list_of_darts L)
1133         ==> CARD (face (hypermap_of_list L) d) = sizel (find_face L d)`
1134 [
1135    (BETA_TAC THEN (case THEN ((move ["good_s"]) THEN (move ["mem_d"]))));
1136    ((((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] [])))));
1137    ((((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN (clear_assumption "good_s") THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1138 ];;
1139
1140 (* Lemma list_of_faces_k *)
1141 let list_of_faces_k = Sections.section_proof ["L";"k"]
1142 `good_list L
1143         ==> face_set_k k (hypermap_of_list L) =
1144                 set_of_list (MAP set_of_list (filter (\f. sizel f = k) (list_of_faces L)))`
1145 [
1146    ((BETA_TAC THEN (move ["good_s"])) THEN (((use_arg_then2 ("good_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq_s"])) THEN (move ["_"])));
1147    ((((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set", [face_set]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_orbits", [set_of_orbits]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face", [face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
1148    ((((use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))));
1149    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("MEM_MAP", [MEM_MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (move ["f"]) THEN (simp_tac));
1150    ((THENL) (split_tac) [((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN ALL_TAC) THEN (case THEN (move ["d"])) THEN (case THEN (move ["mem_d"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (move ["card_eq"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))); ((case THEN (move ["g"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["size_g"])) THEN (move ["mem_g"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
1151    ((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac exists_tac));
1152    (((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("card_face_of_list", [card_face_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1153    ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_face_lemma", [mem_face_lemma])) (fun fst_arg -> (use_arg_then2 ("good_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_g", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["d"]) THEN (case THEN (move ["mem_d"])) THEN (move ["g_eq"])))));
1154    ((((fun arg_tac -> arg_tac (Arg_term (`set_of_list g`))) (term_tac exists_tac)) THEN (simp_tac)) THEN (split_tac));
1155    (((use_arg_then2 ("d", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("face_of_list", [face_of_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
1156    (((((use_arg_then2 ("card_set_of_list_uniq", [card_set_of_list_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("g_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_find_face", [uniq_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1157 ];;
1158
1159 (* Lemma darts_k_union_face_set_k *)
1160 let darts_k_union_face_set_k = Sections.section_proof ["H";"k"]
1161 `darts_k k H = UNIONS (face_set_k k H)`
1162 [
1163    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_k", [darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("face_set_k", [face_set_k]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("Hypermap_iso.inE", [Hypermap_iso.inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["d"]));
1164    ((THENL) (split_tac) [(move ["h"]); ((case THEN (move ["t"])) THEN (case THEN ALL_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 ["card_eq"]) THEN (move ["d_in"]))]);
1165    (((fun arg_tac -> arg_tac (Arg_term (`face H d`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("lemma_in_face_set", [lemma_in_face_set]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_refl", [face_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1166    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`face H x = face H d`))) (term_tac (have_gen_tac [](move ["eq"])))));
1167    (((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((fun arg_tac -> (use_arg_then2 ("Hypermap_iso.IN_TRANS", [Hypermap_iso.IN_TRANS])) (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 (((use_arg_then2 ("lemma_face_subset", [lemma_face_subset]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1168    (((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))) (disch_tac [])) THEN (exact_tac));
1169 ];;
1170
1171 (* Lemma set_of_list_flatten_map *)
1172 let set_of_list_flatten_map = Sections.section_proof ["s"]
1173 `set_of_list (flatten s)
1174         = UNIONS (set_of_list (map set_of_list s))`
1175 [
1176    (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNIONS", [IN_UNIONS]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_flatten", [mem_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]));
1177    ((THENL) (split_tac) [((case THEN (move ["l"])) THEN (move ["h"])); ((case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["l2"])) THEN (case THEN (move ["mem_l2"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))]);
1178    (((fun arg_tac -> arg_tac (Arg_term (`set_of_list l`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)) THEN (done_tac));
1179    (((((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (move ["mem_x"])) THEN ((use_arg_then2 ("l2", [])) (term_tac exists_tac)) THEN (done_tac));
1180 ];;
1181
1182 (* Lemma list_of_darts_k *)
1183 let list_of_darts_k = Sections.section_proof ["L";"k"]
1184 `good_list L
1185         ==> darts_k k (hypermap_of_list L)
1186                 = set_of_list (flatten (filter (\f. sizel f = k) (list_of_faces L)))`
1187 [
1188    ((BETA_TAC THEN (move ["goodL"])) THEN (((use_arg_then2 ("darts_k_union_face_set_k", [darts_k_union_face_set_k]))(thm_tac (new_rewrite [] [])))));
1189    (((((use_arg_then2 ("list_of_faces_k", [list_of_faces_k]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_list_flatten_map", [set_of_list_flatten_map]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1190 ];;
1191
1192 (* Lemma darts3_eq_list_of_darts3 *)
1193 let darts3_eq_list_of_darts3 = Sections.section_proof ["L"]
1194 `good_list L
1195         ==> darts_k 3 (hypermap_of_list L) = set_of_list (list_of_darts3 L)`
1196 [
1197    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (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 (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("list_of_darts3", [list_of_darts3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces3", [list_of_faces3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1198 ];;
1199
1200 (* Lemma darts4_eq_list_of_darts4 *)
1201 let darts4_eq_list_of_darts4 = Sections.section_proof ["L"]
1202 `good_list L
1203         ==> darts_k 4 (hypermap_of_list L) = set_of_list (list_of_darts4 L)`
1204 [
1205    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (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 (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((((use_arg_then2 ("list_of_darts4", [list_of_darts4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces4", [list_of_faces4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1206 ];;
1207
1208 (* Lemma darts5_eq_list_of_darts5 *)
1209 let darts5_eq_list_of_darts5 = Sections.section_proof ["L"]
1210 `good_list L
1211         ==> darts_k 5 (hypermap_of_list L) = set_of_list (list_of_darts5 L)`
1212 [
1213    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`5`))) (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 ((((use_arg_then2 ("list_of_darts5", [list_of_darts5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces5", [list_of_faces5]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1214 ];;
1215
1216 (* Lemma darts6_eq_list_of_darts6 *)
1217 let darts6_eq_list_of_darts6 = Sections.section_proof ["L"]
1218 `good_list L
1219         ==> darts_k 6 (hypermap_of_list L) = set_of_list (list_of_darts6 L)`
1220 [
1221    (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("list_of_darts_k", [list_of_darts_k])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`6`))) (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 ((((use_arg_then2 ("list_of_darts6", [list_of_darts6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_faces6", [list_of_faces6]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Seq.size", [Seq.size]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1222 ];;
1223
1224 (* Lemma rot_list_pairs *)
1225 let rot_list_pairs = Sections.section_proof ["s";"n"]
1226 `rot n (list_pairs s) = list_pairs (rot n s)`
1227 [
1228    (((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_zip", [rot_zip]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("rot_rot", [rot_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1229 ];;
1230
1231 (* Lemma rotr_list_pairs *)
1232 let rotr_list_pairs = Sections.section_proof ["s";"n"]
1233 `rotr n (list_pairs s) = list_pairs (rotr n s)`
1234 [
1235    (((((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1236 ];;
1237
1238 (* Lemma list_pairs_rot *)
1239 let list_pairs_rot = Sections.section_proof ["s";"n"]
1240 `perm_eq (list_pairs (rot n s)) (list_pairs s)`
1241 [
1242    (((((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1243 ];;
1244
1245 (* Lemma find_pair_list_empty *)
1246 let find_pair_list_empty = Sections.section_proof ["L";"d"]
1247 `find_pair_list L d = [] <=> ~(MEM d (list_of_darts L))`
1248 [
1249    (((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
1250    ((((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))));
1251    ((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d _`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
1252    ((((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["h_eq"]));
1253    ((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC) THEN ((((use_arg_then2 ("h_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1254 ];;
1255
1256 (* Lemma list_of_darts_perm *)
1257 let list_of_darts_perm = Sections.section_proof ["L1";"L2"]
1258 `perm_eq L1 L2 ==> perm_eq (list_of_darts L1) (list_of_darts L2)`
1259 [
1260    ((BETA_TAC THEN (move ["perm"])) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_alt", [list_of_darts_alt]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))))));
1261    (((((use_arg_then2 ("perm_eq_flatten", [perm_eq_flatten]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_map", [perm_eq_map]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1262 ];;
1263
1264 (* Lemma good_list_perm *)
1265 let good_list_perm = Sections.section_proof ["L1";"L2"]
1266 `perm_eq L1 L2 /\ good_list L1 ==> good_list L2`
1267 [
1268    ((repeat_tactic 1 9 (((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["perm"])) THEN (case THEN (move ["uniq1"])) THEN (case THEN (move ["all1"])) THEN (move ["sym1"]));
1269    ((fun arg_tac -> (use_arg_then2 ("list_of_darts_perm", [list_of_darts_perm])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"])));
1270    ((((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniq1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("all_perm_eq", [all_perm_eq])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all1", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
1271    ((BETA_TAC THEN (move ["d"])) THEN ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("sym1", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
1272 ];;
1273
1274 (* Lemma find_face_cons *)
1275 let find_face_cons = Sections.section_proof ["h";"t";"d"]
1276 `find_face (h :: t) d = if MEM d (list_pairs h) then (list_pairs h) else find_face t d`
1277 [
1278    (((repeat_tactic 1 9 (((use_arg_then2 ("find_face", [find_face]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MAP", [MAP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_list", [find_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1279 ];;
1280
1281 (* Lemma find_face_eq *)
1282 let find_face_eq = Sections.section_proof ["L";"d";"f"]
1283 `uniq (list_of_darts L) /\ MEM d (list_of_darts L)
1284         ==> (find_face L d = f <=> MEM f (list_of_faces L) /\ MEM d f)`
1285 [
1286    ((BETA_TAC THEN (case THEN ((move ["uniqL"]) THEN (move ["mem_d"])))) THEN ((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); ALL_TAC]));
1287    (((((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
1288    (((((use_arg_then2 ("list_of_faces", [list_of_faces]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("map_MAP", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["s"])) THEN (case THEN (move ["mem_s"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq"]));
1289    (((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
1290 ];;
1291
1292 (* Close the module *)
1293 end;;