needs "../formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl";;
needs "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";;
(* Module List_hypermap_iso*)
module List_hypermap_iso = struct
parse_as_infix ("::", (12, "right"));;
override_interface ("::", `CONS`);;
make_overloadable "++" `:A -> A -> A`;;
overload_interface ("++", `cat`);;
let split_list_hyp = (GEN_ALL o define)
`split_list_hyp [] d = [] /\
split_list_hyp (f :: t) d =
if MEM d (list_pairs f) then
split_list_face (rotr 1 (rot (indexl d (list_pairs f)) f)) ++ t
else
f :: split_list_hyp t d`;;
open Ssrbool;;
open Ssrnat;;
open Seq;;
open Seq2;;
open Hypermap;;
open Hypermap_and_fan;;
open Fan_defs;;
open List_hypermap;;
open Add_triangle;;
open Hypermap_iso;;
(* Section MoreFan *)
Sections.begin_section "MoreFan";;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
(* Lemma fan_imp_finite_set *)
let fan_imp_finite_set = Sections.section_proof ["V";"E"]
`FAN (vec 0,V,E) ==> FINITE V`
[
((((((use_arg_then2 ("FAN", [FAN]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan1", [fan1]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma e_fan_pair_ext_explicit *)
let e_fan_pair_ext_explicit = Sections.section_proof ["v";"w"]
`(v,w) IN dart_of_fan (V,E)
==> e_fan_pair_ext (V,E) (v,w) = (w,v)`
[
((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext", [e_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`v,w IN _`))) (disch_eq_tac "vw_in" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("e_fan_pair", [e_fan_pair]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
((BETA_TAC THEN (case THEN (move ["z"])) THEN (case THEN (move ["_"]))) THEN ((((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) THEN (done_tac));
];;
(* Lemma fan_number_of_nodes *)
let fan_number_of_nodes = Sections.section_proof ["V";"E"]
`FAN (vec 0,V,E)
==> number_of_nodes (hypermap_of_fan (V,E)) = CARD V`
[
((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (move ["fanV"]));
(((fun arg_tac -> (use_arg_then2 ("NODE_SET_AS_IMAGE", [NODE_SET_AS_IMAGE])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["f"])) THEN (case THEN (move ["inj"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
((((((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
];;
(* Finalization of the section MoreFan *)
let fan_imp_finite_set = Sections.finalize_theorem fan_imp_finite_set;;
let e_fan_pair_ext_explicit = Sections.finalize_theorem e_fan_pair_ext_explicit;;
let fan_number_of_nodes = Sections.finalize_theorem fan_number_of_nodes;;
Sections.end_section "MoreFan";;
(* Section SplitListHyp *)
Sections.begin_section "SplitListHyp";;
(Sections.add_section_type (mk_var ("d", (`:A#A`))));;
(* Lemma split_list_hyp_alt *)
let split_list_hyp_alt = Sections.section_proof ["L";"d"]
`MEM d (list_of_darts L)
==> (let f = find_pair_list L d and
n = indexl (find_pair_list L d) L in
split_list_hyp L d = take n L ++
(split_list_face (rotr 1 (rot (indexl d (list_pairs f)) f))) ++ dropl (n + 1) L)`
[
((BETA_TAC THEN (move ["mem_d"])) THEN (CONV_TAC let_CONV) THEN (((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC));
((THENL_FIRST) ((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) (((((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((((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 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))));
(((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 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop1", [drop1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("behead", [behead]))(thm_tac (new_rewrite [] [])))));
(((((use_arg_then2 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(BETA_TAC THEN (move ["mem_dt"]));
((((use_arg_then2 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`indexl _1 (CONS h t)`))) (term_tac (set_tac "m")));
((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`m = SUC n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) (((((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((((use_arg_then2 ("m_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_cons", [index_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> arg_tac (Arg_term (`_ = h`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((use_arg_then2 ("mem_dt", [])) (disch_tac [])) THEN (clear_assumption "mem_dt") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma d_not_in_dart_split_eq *)
let d_not_in_dart_split_eq = Sections.section_proof ["L";"d"]
`~(MEM d (list_of_darts L)) ==> split_list_hyp L d = L`
[
((((use_arg_then2 ("mem_list_of_darts", [mem_list_of_darts]))(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 [] [])))));
(((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 ("split_list_hyp", [split_list_hyp]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["mem_d"])));
((((fun arg_tac -> (use_arg_then2 ("mem_d", [])) (fun fst_arg -> (use_arg_then2 ("h", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL MEM)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (move ["x"])));
((((fun arg_tac -> (use_arg_then2 ("mem_d", [])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL MEM)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))));
((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma list_eq_cat_find_pair_list *)
let list_eq_cat_find_pair_list = Sections.section_proof ["L";"d"]
`MEM d (list_of_darts L)
==> (let f = find_pair_list L d and
n = indexl (find_pair_list L d) L in
L = take n L ++ [f] ++ dropl (n + 1) L)`
[
((BETA_TAC THEN (move ["mem_d"])) THEN (CONV_TAC let_CONV) THEN (((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC));
((THENL_FIRST) ((THENL) (((use_arg_then2 ("L", [])) (disch_tac [])) THEN (clear_assumption "L") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) (((((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((((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 ("find_pair_list", [find_pair_list]))(thm_tac (new_rewrite [] [])))));
(((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 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("add0n", [add0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop1", [drop1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("behead", [behead]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((BETA_TAC THEN (move ["mem_dt"])) THEN ((((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac))));
((fun arg_tac -> arg_tac (Arg_term (`indexl _1 _2`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`indexl _1 (CONS h t)`))) (term_tac (set_tac "m")));
((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`m = SUC n`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) (((((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addSn", [addSn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
((((use_arg_then2 ("m_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_cons", [index_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> arg_tac (Arg_term (`_ = h`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((use_arg_then2 ("mem_dt", [])) (disch_tac [])) THEN (clear_assumption "mem_dt") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma list_eq_cat_list_diag *)
let list_eq_cat_list_diag = Sections.section_proof ["f";"d"]
`MEM d (list_pairs f) /\ 2 <= sizel f
==> (let k = indexl d (list_pairs f) and
y = FST (prev_el (list_pairs f) d) in
rot k f = [FST d] ++ belast (SND d) (dropl 2 (rot k f)) ++ [y])`
[
((BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["f_size"])))) THEN (CONV_TAC let_CONV));
((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k")));
((fun arg_tac -> arg_tac (Arg_term (`FST (_1 _2 d)`))) (term_tac (set_tac "y")));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k < sizel f`))) (term_tac (have_gen_tac [](move ["k_lt"])))) (((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((((fun arg_tac -> (use_arg_then2 ("eq_from_nth", [eq_from_nth])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cat", [size_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size1", [size1]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) ((THENL) (split_tac) [ALL_TAC; (move ["i"])]) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`2 <= sizel f /\ 1 < sizel f /\ 0 < sizel f /\ k <= sizel f /\ 0 < sizel f - 1 /\ 1 <= sizel f`))) (term_tac (have_gen_tac [](move ["size_ineqs"]))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
((THENL) (((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [(move ["_"]); (move ["i"])]);
((((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("addn0", [addn0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MOD_LT", [MOD_LT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (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 BETA_TAC);
((((((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 (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) 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));
(((fun arg_tac -> arg_tac (Arg_term (`sizel f = 2`))) (disch_eq_tac "size_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
(((((use_arg_then2 ("drop_oversize", [drop_oversize]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("leqnn", [leqnn]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (move ["i_lt"]));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`i = 0`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(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)));
((((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))));
(((repeat_tactic 1 9 (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))))) THEN (TRY (((((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("size_ineqs", [])) (disch_tac [])) THEN (clear_assumption "size_ineqs") THEN BETA_TAC) THEN (arith_tac)))));
((((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 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] [])))));
(((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`2 - 1 + k = k + 1`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel f - 2 /\ 2 < sizel f`))) (term_tac (have_gen_tac [](move ["size_ineqs2"])))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((THENL) (((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [(move ["_"]); (move ["i"])]);
((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((use_arg_then2 ("nth0", [nth0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("head_belast", [head_belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (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 BETA_TAC);
(((((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 (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((BETA_TAC THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))));
(((fun arg_tac -> arg_tac (Arg_term (`SUC i < sizel f - 2`))) (disch_eq_tac "i_lt2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (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 [1] []))))) THEN (((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC (SUC i) < 2 <=> F`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((arith_tac) THEN (done_tac)));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC (SUC i) - 2 = i`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((arith_tac) THEN (done_tac)));
((((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_lt2", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
(((((use_arg_then2 ("nth_belast", [nth_belast]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("succnK", [succnK]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("eqS0", [eqS0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`SUC i = sizel f - 2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN ((use_arg_then2 ("i_lt2", [])) (disch_tac [])) THEN (clear_assumption "i_lt2") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((((use_arg_then2 ("nth_cat", [nth_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_belast", [size_belast]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnn", [ltnn]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("subnn", [subnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("prev_el_alt", [prev_el_alt])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`y,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))));
(((repeat_tactic 1 9 (((use_arg_then2 ("nth_rot", [nth_rot]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))))) THEN (TRY (((((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN ((use_arg_then2 ("size_ineqs", [])) (disch_tac [])) THEN (clear_assumption "size_ineqs") THEN BETA_TAC) THEN (arith_tac)))));
((((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 ("FST", [FST]))(thm_tac (new_rewrite [] [])))));
(((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k + SUC (sizel f - 2) = sizel f - 1 + k`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))) THEN (done_tac));
];;
(* Lemma split_list_explicit *)
let split_list_explicit = Sections.section_proof ["L";"d"]
`let f = find_pair_list L d in
(let y = FST (prev_el (list_pairs f) d) and
k = indexl d (list_pairs f) in
3 < sizel f
==> split_list_face (rotr 1 (rot k f))
= [[y; FST d; SND d]; [y; SND d] ++ dropl 3 (rotr 1 (rot k f))]
/\ perm_eq (list_of_darts (split_list_face (rotr 1 (rot k f))))
([list_hyp_diag L d; e_list (list_hyp_diag L d)] ++ list_pairs f))`
[
(repeat_tactic 1 9 ((CONV_TAC let_CONV)));
((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
(BETA_TAC THEN (move ["f_size"]));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y")));
((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k")));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'")));
(((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_list_diag))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
(((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
(((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(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 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] []))))) THEN (move ["rot_eq"]));
((((use_arg_then2 ("rot_eq", [])) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("congr1", [congr1])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rotr 1`))) (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 (((((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr1_rcons", [rotr1_rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("EQ_SYM_EQ", [EQ_SYM_EQ]))(thm_tac (new_rewrite [] []))))) THEN (move ["f'_eq"])));
((fun arg_tac -> arg_tac (Arg_term (`belast (SND d) (dropl 2 (rot k f)) = SND d :: dropl 3 f'`))) (term_tac (have_gen_tac [](move ["eqX"]))));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`1 <= sizel (dropl 2 (rot k f))`))) (term_tac (have_gen_tac []ALL_TAC))) (((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((THENL_FIRST) ((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((THENL) (((fun arg_tac -> arg_tac (Arg_term (`dropl 2 (rot k f)`))) (disch_tac [])) THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))])) ((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
((((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (term_tac (have_gen_tac [](move ["h1"]))));
((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
(congr_tac (`[_1; _2]`));
(((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("take_size_cat", [take_size_cat]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((THENL_FIRST) ((((use_arg_then2 ("f'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_cons", [size_cons]))(fun tmp_arg1 -> (use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))))) ((arith_tac) THEN (done_tac)));
((((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("y", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("catA", [catA]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))));
(((((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("drop_size_cat", [drop_size_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))));
((repeat_tactic 2 0 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`FST d,SND d`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))));
((repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SND d,y`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`list_pairs (rot k f)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
((((use_arg_then2 ("list_pairs_rot", [list_pairs_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eqX", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons_cat", [rcons_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("perm_catC", [perm_catC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cons", [perm_cons]))(thm_tac (new_rewrite [] [])))));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("y", [])) (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)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] [(`SND d :: _1 ++ [y]`)]))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("zip_cat", [zip_cat]))(thm_tac (new_rewrite [] [])))));
(((repeat_tactic 1 9 (((use_arg_then2 ("size_cat", [size_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("addnC", [addnC]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma darts_of_list_split *)
let darts_of_list_split = Sections.section_proof ["L";"d"]
`3 < sizel (find_pair_list L d)
==> perm_eq (list_of_darts (split_list_hyp L d))
([list_hyp_diag L d; e_list (list_hyp_diag L d)] ++ list_of_darts L)`
[
((BETA_TAC THEN (move ["f_size"])) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_d"]))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [3] [])))) THEN ((TRY done_tac)));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_explicit))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["split_eq"]) THEN (move ["darts_perm"])))));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'")));
((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cat", [list_of_darts_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_catCA", [perm_catCA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2r", [perm_cat2r]))(thm_tac (new_rewrite [] [])))));
(((((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_perm", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma darts_of_list_split_same *)
let darts_of_list_split_same = Sections.section_proof ["L";"d"]
`sizel (find_pair_list L d) <= 3
==> perm_eq (list_of_darts (split_list_hyp L d)) (list_of_darts L)`
[
((BETA_TAC THEN (move ["f_size"])) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))));
((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
(((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'")));
((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cat", [list_of_darts_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_cat2l", [perm_cat2l]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_cat2r", [perm_cat2r]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k")));
((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts", [list_of_darts]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL foldr)))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] [])))))));
(((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rot k _`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(fun tmp_arg1 -> (use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(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));
];;
(* Lemma list_of_elements_split *)
let list_of_elements_split = Sections.section_proof ["L";"d"]
`perm_eq (list_of_elements L) (list_of_elements (split_list_hyp L d))`
[
(((use_arg_then2 ("uniq_perm_eq", [uniq_perm_eq])) (thm_tac apply_tac)) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("uniq_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["i"])));
((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n")));
((repeat_tactic 1 9 (((use_arg_then2 ("list_of_elements", [list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("flatten_cat", [flatten_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_undup", [mem_undup]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("orb_id2l", [orb_id2l])) (disch_tac [])) THEN (clear_assumption "orb_id2l") THEN (DISCH_THEN apply_tac) THEN (move ["_"])) THEN (((use_arg_then2 ("orb_id2r", [orb_id2r])) (disch_tac [])) THEN (clear_assumption "orb_id2r") THEN (DISCH_THEN apply_tac) THEN (move ["_"])));
((((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("flatten0", [flatten0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))));
((((fun arg_tac -> arg_tac (Arg_term (`_ <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("flatten_cons", [flatten_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("flatten0", [flatten0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("mem_rotr", [mem_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_rot", [mem_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "s")));
((fun arg_tac -> arg_tac (Arg_term (`?k. s = rot k f`))) (term_tac (have_gen_tac [](case THEN ((move ["k"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))));
((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`sizel f - 1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`indexl d (list_pairs f)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["k"]) THEN (move ["eq"])))));
(((use_arg_then2 ("k", [])) (term_tac exists_tac)) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel f /\ 2 < 3`))) (term_tac (have_gen_tac [](move ["ineqs"])))) ((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("mem_rot", [mem_rot])) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (split_tac));
((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))));
((case THEN (simp_tac) THEN (move ["mem_i"])) THEN (DISJ2_TAC) THEN (DISJ2_TAC));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`rot k f`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("drop_cat", [drop_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
(((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_i", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (((THENL) case [(DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_take", [mem_take])) (thm_tac (match_mp_then snd_th MP_TAC)))); ((THENL) case [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_drop", [mem_drop])) (thm_tac (match_mp_then snd_th MP_TAC))))])]) THEN ((TRY done_tac))));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`0 < sizel (rot k f)`))) (term_tac (have_gen_tac []ALL_TAC))) ((((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineqs", [])) (disch_tac [])) THEN (clear_assumption "ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
(((THENL) (((fun arg_tac -> arg_tac (Arg_term (`rot k f`))) (disch_tac [])) THEN case) [ALL_TAC; ((move ["h"]) THEN (move ["t"]))]) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("size_nil", [size_nil]))(fun tmp_arg1 -> (use_arg_then2 ("ltn0", [ltn0]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL HD)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma mem_list_hyp_diag *)
let mem_list_hyp_diag = Sections.section_proof ["L";"d"]
`MEM d (list_of_darts L) /\
(sizel (find_pair_list L d) = 1 \/ sizel (find_pair_list L d) = 3)
==> MEM (list_hyp_diag L d) (find_face L d)`
[
((BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["size_eq"])))) THEN ((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl d (list_pairs f)`))) (term_tac (set_tac "k")));
((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y")));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs f)`))) (term_tac (have_gen_tac [](move ["mem_d2"])))) (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dart_in_find_pair_list", [dart_in_find_pair_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`k < sizel f`))) (term_tac (have_gen_tac [](move ["k_lt"])))) (((((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
(((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN case THEN (move ["size_eq"]));
((((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size1_eq", [size1_eq]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (move ["f_eq"])));
((((use_arg_then2 ("mem_d2", [])) (disch_tac [])) THEN (clear_assumption "mem_d2") THEN BETA_TAC) THEN (((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_seq1", [mem_seq1]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el", [prev_el]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("Seq.index_head", [Seq.index_head]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`2 <= sizel f`))) (term_tac (have_gen_tac [](move ["size_ineq"])))) ((((use_arg_then2 ("size_eq", [])) (disch_tac [])) THEN (clear_assumption "size_eq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_list_diag))) (fun fst_arg -> (use_arg_then2 ("mem_d2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("size_ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
(((((use_arg_then2 ("k_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_def", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`dropl 2 _`))) (term_tac (set_tac "l")));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`belast (SND d) l = [SND d]`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
(((repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`sizel l = 1`))) (term_tac (have_gen_tac []ALL_TAC))) (((((use_arg_then2 ("l_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac)));
(((((use_arg_then2 ("size1_eq", [size1_eq]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["x"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("belast", [belast]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma good_list_split *)
let good_list_split = Sections.section_proof ["L";"d"]
`good_list L /\
(sizel (find_pair_list L d) <= 3 \/
~(MEM (list_hyp_diag L d) (list_of_darts L))
/\ ~(FST (list_hyp_diag L d) = SND (list_hyp_diag L d)))
==> good_list (split_list_hyp L d)`
[
(BETA_TAC THEN (case THEN ((move ["goodL"]) THEN (move ["hyp"]))));
((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "f'")));
((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((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 ["symL"]) THEN (move ["L_eq"]) THEN (move ["split_eq"])));
(((fun arg_tac -> arg_tac (Arg_term (`sizel (find_pair_list L d) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE darts_of_list_split_same))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"])));
((THENL_ROT (-1)) (((((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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniqL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)));
((BETA_TAC THEN (move ["y"])) 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)))(thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
((((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN BETA_TAC) THEN (((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all_cat", [all_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["f_neq"])) THEN (move ["_"])));
(((((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_eq0", [size_eq0]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("hyp", [])) (disch_tac [])) THEN (clear_assumption "hyp") THEN BETA_TAC) THEN (((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ALL_TAC THEN (case THEN (move ["n_mem"])) THEN (move ["neq"])));
(in_tac ["f_size"] false (((use_arg_then2 ("NOT_LE", [NOT_LE]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE darts_of_list_split))) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"])));
(split_tac);
((THENL_ROT (-1)) (((((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)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL uniq)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("uniqL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (split_tac)));
((((use_arg_then2 ("n_mem", [])) (disch_tac [])) THEN (clear_assumption "n_mem") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN ((((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FST", [FST]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((((use_arg_then2 ("n_mem", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("neq", [])) (disch_tac [])) THEN (clear_assumption "neq") THEN ((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) 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));
(split_tac);
((((use_arg_then2 ("allL", [])) (disch_tac [])) THEN (clear_assumption "allL") THEN BETA_TAC) THEN ((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("split_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all_cat", [all_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`3 < sizel f'`))) (term_tac (have_gen_tac [](move ["f'_size"])))) (((((use_arg_then2 ("f'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
(((((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["_"]));
(((repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f'_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((BETA_TAC THEN (move ["y"])) 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)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))));
((fun arg_tac -> arg_tac (Arg_term (`list_hyp_diag L d`))) (term_tac (set_tac "h")));
((THENL_LAST) case (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("symL", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma hypermap_of_list_perm *)
let hypermap_of_list_perm = Sections.section_proof ["L1";"L2"]
`perm_eq L1 L2 /\ good_list L1
==> hypermap_of_list L1 = hypermap_of_list L2`
[
(BETA_TAC THEN (case THEN ((move ["perm"]) THEN (move ["good1"]))));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("good_list_perm", [good_list_perm])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("good1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["good2"])));
((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"])));
((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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["mem_eq"])));
((repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`hypermap _`)));
((repeat_tactic 1 9 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
((fun arg_tac -> arg_tac (Arg_term (`(!d. MEM d (list_of_darts L1) ==> f1 d = f2 d)
==> res f1 (darts_of_list L1) = res f2 (darts_of_list L2)`))) (term_tac (have_gen_tac ["f1"; "f2"](move ["res_eq"]))));
((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["eq"]) THEN (move ["d"]));
((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((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 [] []))))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))));
((((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 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
((THENL_FIRST) (split_tac) ((repeat_tactic 1 9 (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L1) ==> find_face L2 d = find_face L1 d`))) (term_tac (have_gen_tac ["d"](move ["face_eq"]))));
((BETA_TAC THEN (move ["mem_d"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`list_pairs _`)));
((((use_arg_then2 ("good1", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniq1"])) THEN (move ["_"])));
(((fun arg_tac -> (use_arg_then2 ("find_pair_list_unique", [find_pair_list_unique])) (fun fst_arg -> (use_arg_then2 ("uniq1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
((((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_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
(((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((split_tac) THEN (repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("n_list_ext", [n_list_ext]))(fun tmp_arg1 -> (use_arg_then2 ("f_list_ext", [f_list_ext]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"])));
(((repeat_tactic 1 9 (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
(((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("face_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma find_face_rot *)
let find_face_rot = Sections.section_proof ["L1";"L2";"d"]
`ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2
==> ?n. find_face L2 d = rot n (find_face L1 d)`
[
((((THENL) (((use_arg_then2 ("L2", [])) (disch_tac [])) THEN (clear_assumption "L2") THEN ((use_arg_then2 ("L1", [])) (disch_tac [])) THEN (clear_assumption "L1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["Ih"]))]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]))])) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))));
(((((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 (((use_arg_then2 ("rot_nil", [rot_nil]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["n"])) THEN (move ["h2_eq"]) THEN (move ["all2"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_face_cons", [find_face_cons]))(thm_tac (new_rewrite [] []))))));
(((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_pairs h1)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
(((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((fun arg_tac -> (use_arg_then2 ("Ih", [])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["m"])) THEN (move ["eq"])) THEN ((use_arg_then2 ("m", [])) (term_tac exists_tac)));
(((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_pairs_rot", [list_pairs_rot])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma rot_list_of_darts_perm *)
let rot_list_of_darts_perm = Sections.section_proof ["L1";"L2"]
`ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2
==> perm_eq (list_of_darts L1) (list_of_darts L2)`
[
((((THENL) (((use_arg_then2 ("L2", [])) (disch_tac [])) THEN (clear_assumption "L2") THEN ((use_arg_then2 ("L1", [])) (disch_tac [])) THEN (clear_assumption "L1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["Ih"]))]) THEN ((THENL) case [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]))])) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) 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 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac))));
(BETA_TAC THEN (case THEN ALL_TAC) THEN (case THEN ((move ["n"]) THEN (move ["h2_eq"]))) THEN (move ["all2"]));
((repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_cat", [perm_eq_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
(((((use_arg_then2 ("h2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_pairs_rot", [list_pairs_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma rot_hypermap_of_list_eq *)
let rot_hypermap_of_list_eq = Sections.section_proof ["L1";"L2"]
`ALL2 (\f1 f2. ?n. f2 = rot n f1) L1 L2 /\ uniq (list_of_darts L1)
==> hypermap_of_list L2 = hypermap_of_list L1`
[
(BETA_TAC THEN (case THEN ((move ["all2"]) THEN (move ["uniq1"]))));
((repeat_tactic 1 9 (((use_arg_then2 ("hypermap_of_list", [hypermap_of_list]))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`hypermap _`)));
((fun arg_tac -> (use_arg_then2 ("rot_list_of_darts_perm", [rot_list_of_darts_perm])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["perm_darts"])));
((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))) (fun arg -> thm_tac MP_TAC arg THEN (move ["mem_eq"])));
((fun arg_tac -> (use_arg_then2 ("find_face_rot", [find_face_rot])) (fun fst_arg -> (use_arg_then2 ("all2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["face_eq"])));
((repeat_tactic 1 9 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("perm_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac));
((fun arg_tac -> arg_tac (Arg_term (`(!d. MEM d (list_of_darts L1) ==> f1 d = f2 d)
==> res f2 (darts_of_list L2) = res f1 (darts_of_list L1)`))) (term_tac (have_gen_tac ["f1"; "f2"](move ["res_eq"]))));
((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN (move ["eq"]) THEN (move ["y"]));
((repeat_tactic 1 9 (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((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 [] []))))) THEN (((use_arg_then2 ("mem_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))));
((((fun arg_tac -> arg_tac (Arg_term (`MEM y _`))) (disch_eq_tac "mem_y" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
((THENL_FIRST) (split_tac) ((repeat_tactic 1 9 (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["y"]) THEN (move ["mem_y"])) THEN (repeat_tactic 1 9 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
(split_tac);
((repeat_tactic 1 9 (((use_arg_then2 ("n_list_ext", [n_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"])));
(((fun arg_tac -> (use_arg_then2 ("face_eq", [])) (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 (case THEN (move ["n"])) THEN (move ["f_eq"]));
((repeat_tactic 1 9 (((use_arg_then2 ("n_list", [n_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el_rot_eq", [prev_el_rot_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((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));
((repeat_tactic 1 9 (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("res_eq", [])) (disch_tac [])) THEN (clear_assumption "res_eq") THEN (DISCH_THEN apply_tac) THEN (move ["d"]) THEN (move ["mem_d"])));
(((fun arg_tac -> (use_arg_then2 ("face_eq", [])) (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 (case THEN (move ["n"])) THEN (move ["f_eq"]));
(((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq]))(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));
];;
(* Lemma hypermap_of_split_list_eq3 *)
let hypermap_of_split_list_eq3 = Sections.section_proof ["L";"d"]
`sizel (find_face L d) <= 3 /\ uniq (list_of_darts L)
==> hypermap_of_list (split_list_hyp L d) = hypermap_of_list L`
[
(BETA_TAC THEN (case THEN ((move ["f_size"]) THEN (move ["uniq_darts"]))));
((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`!s:((A)list)list. ALL2 (\f1 f2. ?n. f2 = rot n f1) s s`))) (term_tac (have_gen_tac [](move ["all2_refl"]))));
(((THENL) elim [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["Ih"]))]) THEN ((((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("Ih", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`0`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("rot0", [rot0]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
(((fun arg_tac -> (use_arg_then2 ("rot_hypermap_of_list_eq", [rot_hypermap_of_list_eq])) (fun fst_arg -> (use_arg_then2 ("uniq_darts", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
((((fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("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)))(thm_tac (new_rewrite [1] [])))) THEN ((TRY done_tac)));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`indexl f L`))) (term_tac (set_tac "n")));
(BETA_TAC THEN (move ["f_size"]));
((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((repeat_tactic 1 9 (((use_arg_then2 ("ALL2_cat", [ALL2_cat]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all2_refl", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ALL2", [ALL2]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> arg_tac (Arg_term (`sizel _ - 1`))) (term_tac (set_tac "i"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "j"))));
((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["k"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("k", [])) (term_tac exists_tac)) THEN (done_tac));
];;
(* Lemma f_split_list *)
let f_split_list = Sections.section_proof ["L";"d"]
`let L2 = split_list_hyp L d and g = list_hyp_diag L d and f = find_face L d in
good_list L /\ 3 < sizel f
/\ ~(MEM g (list_of_darts L))
/\ ~(FST g = SND g)
==> f_list L2 d = g
/\ f_list L2 g = prev_el f d
/\ f_list L2 (e_list g) = f_list L d
/\ f_list L2 (prev_el f (prev_el f d)) = e_list g
/\ (!x. MEM x (list_of_darts L2)
/\ ~(x = d \/ x = g \/ x = e_list g \/ x = prev_el f (prev_el f d))
==> f_list L2 x = f_list L x)`
[
(CONV_TAC let_CONV);
(BETA_TAC THEN (case THEN (move ["goodL"])) THEN (case THEN (move ["f_size"])) THEN (case THEN (move ["g_n_mem"])) THEN (move ["g_neq"]));
((fun arg_tac -> arg_tac (Arg_term (`3 < sizel (find_pair_list L d)`))) (term_tac (have_gen_tac [](move ["size_gt3"]))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_d"]))));
((((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("find_pair_list_empty", [find_pair_list_empty]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("size_nil", [size_nil]))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> (use_arg_then2 ("darts_of_list_split", [darts_of_list_split])) (fun fst_arg -> (use_arg_then2 ("size_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_hyp_alt))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE split_list_explicit))) (fun fst_arg -> (use_arg_then2 ("size_gt3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
(((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("good_list_split", [good_list_split])) (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 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN ((THENL) (ANTS_TAC) [((TRY done_tac)); (move ["goodL2"])]));
(repeat_tactic 1 9 (((use_arg_then2 ("find_face_alt", [find_face_alt]))(gsym_then (thm_tac (new_rewrite [] []))))));
((fun arg_tac -> arg_tac (Arg_term (`find_pair_list L d`))) (term_tac (set_tac "s")));
((fun arg_tac -> arg_tac (Arg_term (`indexl s _`))) (term_tac (set_tac "n")));
((fun arg_tac -> arg_tac (Arg_term (`indexl d _`))) (term_tac (set_tac "k")));
((fun arg_tac -> arg_tac (Arg_term (`rotr 1 _`))) (term_tac (set_tac "s'")));
((fun arg_tac -> arg_tac (Arg_term (`split_list_hyp L d`))) (term_tac (set_tac "L2")));
((fun arg_tac -> arg_tac (Arg_term (`list_hyp_diag L d`))) (term_tac (set_tac "g")));
((fun arg_tac -> arg_tac (Arg_term (`find_face L d`))) (term_tac (set_tac "f")));
((fun arg_tac -> arg_tac (Arg_term (`FST _ :: _2`))) (term_tac (set_tac "s1")));
((fun arg_tac -> arg_tac (Arg_term (`cat _1 _2`))) (term_tac (set_tac "s2")));
(BETA_TAC THEN (case THEN ((move ["split_s'_eq"]) THEN (move ["darts_s'"]))) THEN (move ["L2_eq"]) THEN (move ["dartsL2"]));
((((use_arg_then2 ("goodL2", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL2"])) THEN (move ["_"])));
((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"])));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`list_pairs s = f`))) (term_tac (have_gen_tac [](move ["fs_eq"])))) (((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`list_pairs s1 = [prev_el f d; d; g]`))) (term_tac (have_gen_tac [](move ["s1_pairs_eq"]))));
((((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("g_def", []))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`[_; d; g]`)));
((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (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 fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC));
(((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] [])))) 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));
((((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["z"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`uniq f`))) (term_tac (have_gen_tac [](move ["uniq_f"])))) (((((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 (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`MEM s1 L2 /\ MEM s2 L2`))) (term_tac (have_gen_tac [](move ["s12_mem"]))));
(((((use_arg_then2 ("L2_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_s'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`MEM (list_pairs s1) (list_of_faces L2) /\ MEM (list_pairs s2) (list_of_faces L2)`))) (term_tac (have_gen_tac [](move ["s12_pairs_mem"]))));
(((THENL) (((((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 (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] [])))))) THEN (split_tac)) [((use_arg_then2 ("s1", [])) (term_tac exists_tac)); ((use_arg_then2 ("s2", [])) (term_tac exists_tac))]) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`uniq (list_pairs s1) /\ uniq (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["s12_pairs_uniq"]))));
((split_tac) THEN (((fun arg_tac -> (use_arg_then2 ("uniq_face", [uniq_face])) (fun fst_arg -> (use_arg_then2 ("goodL2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`next_el f x = next_el (list_pairs s') x`))) (term_tac (have_gen_tac ["x"](move ["next_el_fs'"]))));
((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("next_el_rotr_eq", [next_el_rotr_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("rot_uniq", [rot_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`prev_el f x = prev_el (list_pairs s') x`))) (term_tac (have_gen_tac ["x"](move ["prev_el_fs'"]))));
((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("prev_el_rotr_eq", [prev_el_rotr_eq]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("rot_uniq", [rot_uniq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("prev_el_rot_eq", [prev_el_rot_eq]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`MEM x f ==> MEM x (list_of_darts L)`))) (term_tac (have_gen_tac ["x"](move ["mem_f_darts"]))));
(((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`MEM d f`))) (term_tac (have_gen_tac [](move ["mem_df"])))) (((((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)));
((fun arg_tac -> arg_tac (Arg_term (`perm_eq (list_pairs s') f`))) (term_tac (have_gen_tac [](move ["p_eq_f_s'"]))));
((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr_list_pairs", [rotr_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rot_list_pairs", [rot_list_pairs]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("rotr", [rotr]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`sizel _ - 1`))) (term_tac (set_tac "r")));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("rot_rot_eq_rot", [rot_rot_eq_rot])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`list_pairs s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("r", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["i"]) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
((((use_arg_then2 ("perm_eq_rot", [perm_eq_rot]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`sizel s' = sizel s`))) (term_tac (have_gen_tac [](move ["size_s'"])))) (((((use_arg_then2 ("s'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_rotr", [size_rotr]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_rot", [size_rot]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`s' = s1 ++ dropl 3 s'`))) (term_tac (have_gen_tac [](move ["s'_eq1"]))));
((((use_arg_then2 ("split_s'_eq", [])) (disch_tac [])) THEN (clear_assumption "split_s'_eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("split_list_face", [split_list_face]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leqNgt", [leqNgt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_gt3", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
((((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`3`))) (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 [4] []))))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (injectivity "list")))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`list_pairs s' = prev_el f d :: d :: dropl 2 (list_pairs s')`))) (term_tac (have_gen_tac [](move ["s'_pairs_eq"]))));
(((((fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (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 [1] []))))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] []))))) THEN ((congr_tac (`_1 ++ _2`)) THEN ((TRY done_tac))));
((((use_arg_then2 ("s'_eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("TWO", [TWO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("take", [take]))(thm_tac (new_rewrite [] []))))));
((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("prev_el_list_pairs_general", [prev_el_list_pairs_general])) (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 fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (ANTS_TAC));
(((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] [])))) 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));
((BETA_TAC THEN (case THEN (move ["z"]))) THEN (((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`list_pairs s2 = e_list g :: dropl 2 (list_pairs s')`))) (term_tac (have_gen_tac [](move ["s2_pairs_eq"]))));
((((use_arg_then2 ("s'_eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_pairs", [list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("zip", [zip]))(thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("TWO", [TWO]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ONE", [ONE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("drop", [drop]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("g_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`0 < sizel (dropl 2 (list_pairs s')) /\ 1 < sizel (dropl 2 (list_pairs s'))
/\ 0 < sizel (list_pairs s') /\ 2 < sizel (list_pairs s')`))) (term_tac (have_gen_tac [](move ["size_uneqs"]))));
(((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`sizel (list_pairs s2) = sizel (list_pairs s') - 1 /\ 0 < sizel (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["size_ineqs_s2"]))));
(((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_cons", [size_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_s'", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_gt3", [])) (disch_tac [])) THEN (clear_assumption "size_gt3") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`last d (list_pairs s') = prev_el f (prev_el f d)`))) (term_tac (have_gen_tac [](move ["last_s'"]))));
(((((use_arg_then2 ("prev_el_hd", [prev_el_hd]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL HD)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("prev_el_fs'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`last d (list_pairs s2) = prev_el f (prev_el f d)`))) (term_tac (have_gen_tac [](move ["last_s2"]))));
(((((use_arg_then2 ("last_s'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last_drop", [last_drop]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN ((use_arg_then2 ("last_eq", [last_eq])) (thm_tac apply_tac)) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`MEM x (list_of_darts L2) <=> x = g \/ x = e_list g \/ MEM x (list_of_darts L)`))) (term_tac (have_gen_tac ["x"](move ["memL2"]))));
(((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("dartsL2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("orbF", [orbF]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orbA", [orbA]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`find_face L2 d = list_pairs s1 /\ find_face L2 g = list_pairs s1
/\ find_face L2 (prev_el f d) = list_pairs s1`))) (term_tac (have_gen_tac [](move ["find_s1"]))));
((repeat_tactic 1 9 (((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("uniqL2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("memL2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("mem_d", []))(fun tmp_arg1 -> (use_arg_then2 ("s12_pairs_mem", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_f_darts", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`find_face L2 (e_list g) = list_pairs s2
/\ find_face L2 (prev_el f (prev_el f d)) = list_pairs s2`))) (term_tac (have_gen_tac [](move ["find_s2"]))));
((repeat_tactic 1 9 (((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("uniqL2", []))(fun tmp_arg1 -> (use_arg_then2 ("memL2", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_f_darts", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("s12_pairs_mem", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("last_s'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("last_drop", [last_drop])) (fun fst_arg -> (use_arg_then2 ("d", [])) (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)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("last_eq", [last_eq])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`e_list g`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("mem_last", [mem_last]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((repeat_tactic 1 9 (((use_arg_then2 ("f_list", [f_list]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_s1", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("find_s2", []))(thm_tac (new_rewrite [] []))))));
(split_tac);
(((((fun arg_tac -> (use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(split_tac);
((((fun arg_tac -> (use_arg_then2 ("next_el_rotr_eq", [next_el_rotr_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))));
(((((use_arg_then2 ("cat1s", [cat1s]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("catA", [catA]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats1", [cats1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rotr1_rcons", [rotr1_rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cat1s", [cat1s]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(split_tac);
((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons", [next_el_hd_cons]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("f_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_fs'", []))(thm_tac (new_rewrite [] [])))));
((((fun arg_tac -> (use_arg_then2 ("next_el_rot_eq", [next_el_rot_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("p_eq_f_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("rot1_cons", [rot1_cons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("rcons", [rcons]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons", [next_el_hd_cons]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_rcons", [size_rcons]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("gtS0", [gtS0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((use_arg_then2 ("headI", [headI]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("head_HD", [head_HD]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(split_tac);
(((((use_arg_then2 ("last_s2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("next_el_last", [next_el_last]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("HD", [HD]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((repeat_tactic 1 9 (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (case THEN (move ["mem_x"])) THEN (move ["x_neq"]));
((((use_arg_then2 ("mem_x", [])) (disch_tac [])) THEN (clear_assumption "mem_x") THEN BETA_TAC) THEN (((((use_arg_then2 ("memL2", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("x_neq", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] [])))))) THEN (move ["mem_x"])));
((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`MEM x f`))) (disch_eq_tac "mem_x_f" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
(congr_tac (`next_el _ x`));
((((use_arg_then2 ("find_face_eq", [find_face_eq]))(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 (((use_arg_then2 ("mem_x", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE list_eq_cat_find_pair_list))) (fun fst_arg -> (use_arg_then2 ("mem_d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
(((((use_arg_then2 ("s_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (move ["L_eq"]));
((((fun arg_tac -> (use_arg_then2 ("mem_find_face", [mem_find_face])) (fun fst_arg -> (use_arg_then2 ("mem_x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("L_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("L2_eq", []))(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", [map_MAP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mapP", [mapP]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))))));
((BETA_TAC THEN (case THEN (move ["l"])) THEN (case THEN (move ["mem_l"])) THEN (move ["eq"])) THEN ((use_arg_then2 ("l", [])) (term_tac exists_tac)));
((((THENL) (((use_arg_then2 ("mem_l", [])) (disch_tac [])) THEN (clear_assumption "mem_l") THEN case) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); ((THENL) case [ALL_TAC; (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))])]) THEN ((TRY done_tac))) THEN ((((use_arg_then2 ("mem_seq1", [mem_seq1]))(thm_tac (new_rewrite [] [])))) THEN (move ["l_eq"])));
((((use_arg_then2 ("mem_x_f", [])) (disch_tac [])) THEN (clear_assumption "mem_x_f") THEN ((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN (((((use_arg_then2 ("l_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fs_eq", []))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(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));
((fun arg_tac -> arg_tac (Arg_term (`find_face L x = f`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
(((((use_arg_then2 ("f_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) 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))));
((((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))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("mem_find_pair_list", [mem_find_pair_list]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
(((fun arg_tac -> arg_tac (Arg_term (`x = prev_el f d`))) (disch_eq_tac "x_eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
(((((use_arg_then2 ("x_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("find_s1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el_hd_cons2", [next_el_hd_cons2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_prev_id", [next_prev_id]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`MEM x (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["mem_x_s2"]))));
((((fun arg_tac -> (use_arg_then2 ("iffRL", [iffRL])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("darts_s'", [])) (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 snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_x_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
((((use_arg_then2 ("split_s'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("list_of_darts_cons", [list_of_darts_cons]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("list_of_darts_nil", [list_of_darts_nil]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("cats0", [cats0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_cat", [mem_cat]))(thm_tac (new_rewrite [] [])))));
((case THEN ((TRY done_tac))) THEN ((((use_arg_then2 ("s1_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`find_face L2 x = list_pairs s2`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))) (((((use_arg_then2 ("find_face_eq", [find_face_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("s12_pairs_mem", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((((use_arg_then2 ("next_el_fs'", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`indexl x _`))) (term_tac (set_tac "i")));
((fun arg_tac -> arg_tac (Arg_term (`1 <= i /\ i < sizel (list_pairs s2) - 1`))) (term_tac (have_gen_tac [](move ["i_ineqs"]))));
((((use_arg_then2 ("mem_x_s2", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("index_mem", [index_mem]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`~(i = 0) /\ ~(i = sizel (list_pairs s2) - 1)`))) (term_tac (have_gen_tac []ALL_TAC)))) ((arith_tac) THEN (done_tac)));
((((fun arg_tac ->(use_arg_then2 ("x_eq", []))(fun tmp_arg1 -> (use_arg_then2 ("x_neq", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2)))))) (disch_tac [])) THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))))));
((case THEN (move ["i_eq"])) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_x_s2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] []))))));
((((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`i = indexl (last d (list_pairs s2)) (list_pairs s2)`))) (term_tac (have_gen_tac [](move ["i_eq2"]))));
(((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_last", [index_last]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("s2_pairs_eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("i_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((((use_arg_then2 ("i_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last_s2", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
(((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("last", [last]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_last", [mem_last]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(i = sizel (list_pairs s2) - 1)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
((((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("next_el", [next_el]))(thm_tac (new_rewrite [] [])))));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`indexl x (list_pairs s') = i + 1`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(i + 1 = sizel (list_pairs s') - 1)`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac)));
(((repeat_tactic 1 9 (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [1] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`nth x (list_pairs s') (i + 1) = x`))) (term_tac (have_gen_tac [](move ["nth_eq"])))));
((((use_arg_then2 ("nth_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_uniq", [index_uniq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_uniq", [perm_eq_uniq])) (fun fst_arg -> (use_arg_then2 ("p_eq_f_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("uniq_f", []))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN BETA_TAC) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("mem_x_s2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("i_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("addn1", [addn1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s'_pairs_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("s2_pairs_eq", []))(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) ((THENL) (((use_arg_then2 ("i_ineqs", [])) (disch_tac [])) THEN (clear_assumption "i_ineqs") THEN ((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN case) [ALL_TAC; ((move ["j"]) THEN (move ["j_ineq"]))]) ((arith_tac) THEN (done_tac)));
((repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [2] []))))));
(((use_arg_then2 ("set_nth_default", [set_nth_default])) (thm_tac apply_tac)) THEN (((use_arg_then2 ("j_ineq", [])) (disch_tac [])) THEN (clear_assumption "j_ineq") THEN BETA_TAC) THEN ((((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_ineqs_s2", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
];;
(* Finalization of the section SplitListHyp *)
let split_list_hyp_alt = Sections.finalize_theorem split_list_hyp_alt;;
let d_not_in_dart_split_eq = Sections.finalize_theorem d_not_in_dart_split_eq;;
let list_eq_cat_find_pair_list = Sections.finalize_theorem list_eq_cat_find_pair_list;;
let list_eq_cat_list_diag = Sections.finalize_theorem list_eq_cat_list_diag;;
let split_list_explicit = Sections.finalize_theorem split_list_explicit;;
let darts_of_list_split = Sections.finalize_theorem darts_of_list_split;;
let darts_of_list_split_same = Sections.finalize_theorem darts_of_list_split_same;;
let list_of_elements_split = Sections.finalize_theorem list_of_elements_split;;
let mem_list_hyp_diag = Sections.finalize_theorem mem_list_hyp_diag;;
let good_list_split = Sections.finalize_theorem good_list_split;;
let hypermap_of_list_perm = Sections.finalize_theorem hypermap_of_list_perm;;
let find_face_rot = Sections.finalize_theorem find_face_rot;;
let rot_list_of_darts_perm = Sections.finalize_theorem rot_list_of_darts_perm;;
let rot_hypermap_of_list_eq = Sections.finalize_theorem rot_hypermap_of_list_eq;;
let hypermap_of_split_list_eq3 = Sections.finalize_theorem hypermap_of_split_list_eq3;;
let f_split_list = Sections.finalize_theorem f_split_list;;
Sections.end_section "SplitListHyp";;
(* Section FanAndList *)
Sections.begin_section "FanAndList";;
(* Lemma set_of_edge_subset *)
let set_of_edge_subset = Sections.section_proof ["V";"E";"E'";"x"]
`E SUBSET E' ==> set_of_edge x V E SUBSET set_of_edge x V E'`
[
((((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("set_of_edge", [set_of_edge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))))) THEN (move ["subE"]) THEN (move ["y"]) THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("subE", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma fan_list_iso_invariant *)
let fan_list_iso_invariant = Sections.section_proof ["F1";"F2";"f"]
`fan_list_iso (fan_list_iso (f, F1), F2) = fan_list_iso (f, F1)`
[
((((use_arg_then2 ("F2", [])) (disch_tac [])) THEN (clear_assumption "F2") THEN ((use_arg_then2 ("F1", [])) (disch_tac [])) THEN (clear_assumption "F1") THEN BETA_TAC THEN (case THEN ((move ["V"]) THEN (move ["E"]))) THEN (case THEN ((move ["V'"]) THEN (move ["E'"])))) THEN ((((use_arg_then2 ("FUN_EQ_THM", [FUN_EQ_THM]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["v"]) THEN (move ["w"])))));
((repeat_tactic 1 9 (((fun arg_tac ->(use_arg_then2 ("fan_list_iso", [fan_list_iso]))(fun tmp_arg1 -> (use_arg_then2 ("fan_list_nodes_iso", [fan_list_nodes_iso]))(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));
];;
(Sections.add_section_var (mk_var ("V", (`:real^3->bool`))));;
(Sections.add_section_var (mk_var ("E", (`:(real^3->bool)->bool`))));;
(Sections.add_section_var (mk_var ("L", (`:((A)list)list`))));;
(Sections.add_section_var (mk_var ("f", (`:real^3#real^3 -> A#A`))));;
(Sections.add_section_hyp "fanV" (`FAN (vec 0,V,E)`));;
(Sections.add_section_hyp "goodL" (`good_list L`));;
(Sections.add_section_hyp "f_iso" (`hyp_iso f (hypermap_of_fan (V,E), hypermap_of_list L)`));;
(* Lemma hyp_iso_eq_fan_list_iso *)
let hyp_iso_eq_fan_list_iso = Sections.section_proof ["y"]
`y IN dart_of_fan (V,E) ==> f y = fan_list_iso (f, (V,E)) y`
[
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["mapsH"])))));
((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 (case THEN ((move ["dartG"]) THEN (move ["mapsG"])))));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G")));
((fun arg_tac -> arg_tac (Arg_term (`d IN dart_of_fan (V,E) ==> f d IN darts_of_list L`))) (term_tac (have_gen_tac ["d"](move ["f_in"]))));
((((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["d_in"])) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
(((use_arg_then2 ("y", [])) (disch_tac [])) THEN (clear_assumption "y") THEN case THEN ((move ["a"]) THEN (move ["b"])) THEN (move ["ab_in"]));
(((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))));
((fun arg_tac -> arg_tac (Arg_term (`fan_list_nodes_iso _`))) (term_tac (set_tac "h")));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?g. !v w. (v,w) IN dart_of_fan (V,E) ==> f(v,w) = (h v:A, g (v,w):A)`))) (term_tac (have_gen_tac [](case THEN ((move ["g"]) THEN (move ["f_eq"])))))));
(((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("IN_DART_OF_FAN", [IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["v"])) THEN (case THEN (move ["w"])) THEN (case THEN (move ["vw_eq"])) THEN (move ["vw_in"]));
((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`a,b`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)));
((((use_arg_then2 ("mapsG", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mapsH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext_explicit", [e_fan_pair_ext_explicit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("e_list_ext", [e_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)));
((((repeat_tactic 1 9 (((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (repeat_tactic 0 1 (((use_arg_then2 ("dart_switch", [dart_switch]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) 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));
((fun arg_tac -> arg_tac (Arg_term (`\d. SND (f d)`))) (term_tac exists_tac));
((BETA_TAC THEN (move ["v"]) THEN (move ["w"]) THEN (move ["vw_in"])) THEN ((((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("h_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fan_list_nodes_iso", [fan_list_nodes_iso]))(thm_tac (new_rewrite [] []))))));
(((fun arg_tac -> arg_tac (Arg_term (`set_of_edge v V E = {}`))) (disch_eq_tac "set_empty" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN (clear_assumption "vw_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) case (((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((((use_arg_then2 ("set_empty", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((BETA_TAC THEN (case THEN (move ["u"])) THEN (case THEN (move ["_"])) THEN (case THEN ((move ["eq1"]) THEN (move ["eq2"])))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"]))));
((((use_arg_then2 ("vw_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))));
(case THEN ((TRY done_tac)) THEN (case THEN (move ["u"])) THEN (case THEN (move ["empty"])) THEN (move ["eq"]));
((((use_arg_then2 ("empty", [])) (disch_tac [])) THEN (clear_assumption "empty") THEN BETA_TAC) THEN ((((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_empty", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`CHOICE _`))) (term_tac (set_tac "w'")));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f (v,w') IN node G (f (v,w))`))) (term_tac (have_gen_tac []ALL_TAC))));
((((use_arg_then2 ("Hypermap.node", [Hypermap.node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Hypermap.orbit_map", [Hypermap.orbit_map]))(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 ("mapsG", []))(thm_tac (new_rewrite [] [])))));
(BETA_TAC THEN (case THEN (move ["n"])) THEN (case THEN (move ["_"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("pair_expand", [pair_expand]))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("fst_n_list_ext_power", [fst_n_list_ext_power]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
(((((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("dartG", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((fun arg_tac -> (use_arg_then2 ("iso_components", [iso_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dartH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("FUN_IN_IMAGE", [FUN_IN_IMAGE]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("NODE_HYPERMAP_OF_FAN_ALT", [NODE_HYPERMAP_OF_FAN_ALT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
(((use_arg_then2 ("w'", [])) (term_tac exists_tac)) THEN ((split_tac) THEN ((TRY done_tac))) THEN (((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("CHOICE_DEF", [CHOICE_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ssrbool.implybF", [Ssrbool.implybF]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["eq"])));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART1_OF_FAN", [PAIR_IN_DART1_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
(((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IN_EMPTY", [NOT_IN_EMPTY]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma fan_list_nodes_iso_surj *)
let fan_list_nodes_iso_surj = Sections.section_proof []
`SURJ (fan_list_nodes_iso (f,(V,E))) V (elements_of_list L)`
[
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"])));
((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"])));
((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso_eq"])));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G")));
((((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 (repeat_tactic 1 9 (((use_arg_then2 ("mem_list_of_elements", [mem_list_of_elements]))(thm_tac (new_rewrite [] []))))));
((THENL) (split_tac) [(move ["v"]); ((move ["a"]) THEN (case THEN (move ["b"])))]);
((DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("DART_EXISTS", [DART_EXISTS])) (fun fst_arg -> (use_arg_then2 ("E", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["w"])) THEN (move ["vw_in"]));
((fun arg_tac -> arg_tac (Arg_term (`fan_list_nodes_iso (f,V,E) w`))) (term_tac exists_tac));
((((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(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 ("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 ("iso_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((((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"]));
((fun arg_tac -> arg_tac (Arg_term (`res_inv f (dart H) (a,b)`))) (term_tac (set_tac "d")));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_inv", [hyp_iso_inv])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ab_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
(((((use_arg_then2 ("d_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (move ["d_in"]));
(((fun arg_tac -> arg_tac (Arg_term (`FST d`))) (term_tac exists_tac)) THEN (split_tac));
(((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (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)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`f d = a,b`))) (term_tac (have_gen_tac []ALL_TAC))));
((((((use_arg_then2 ("iso_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [1] [])))) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] [])))) 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));
(((((use_arg_then2 ("d_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("surj_res_inv_right", [surj_res_inv_right])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_SURJ", [hyp_iso_SURJ])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma fan_list_nodes_to *)
let fan_list_nodes_to = Sections.section_proof ["v"]
`v IN V ==> fan_list_nodes_iso (f,(V,E)) v IN elements_of_list L`
[
((((use_arg_then2 ("fan_list_nodes_iso_surj", [fan_list_nodes_iso_surj])) (disch_tac [])) THEN (clear_assumption "fan_list_nodes_iso_surj") THEN BETA_TAC) THEN ((((use_arg_then2 ("SURJ", [SURJ]))(thm_tac (new_rewrite [] [])))) THEN (move ["surj"]) THEN (move ["vV"])) THEN (((use_arg_then2 ("surj", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
];;
(* Lemma fan_list_diag_eq *)
let fan_list_diag_eq = Sections.section_proof ["v";"w"]
`(v,w) IN dart1_of_fan (V,E)
==> fan_list_iso (f,(V,E)) (w, sigma_fan (vec 0) V E v w) = list_hyp_diag L (f (v,w))`
[
((((use_arg_then2 ("list_hyp_diag", [list_hyp_diag]))(thm_tac (new_rewrite [] [])))) THEN (move ["vw_in1"]));
((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"])));
((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in"]))));
(((((use_arg_then2 ("dart_of_fan_eq", [dart_of_fan_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["fan_hyp"])));
((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 ["list_hyp"])));
((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (fun arg -> thm_tac MP_TAC arg THEN (move ["f_eq"])));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G")));
((fun arg_tac -> arg_tac (Arg_term (`FST _`))) (term_tac (set_tac "y")));
((fun arg_tac -> arg_tac (Arg_term (`y = FST (inverse (face_map G) (f (v,w)))`))) (term_tac (have_gen_tac [](move ["y_eq"]))));
(((((use_arg_then2 ("list_hyp", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("list_hyp", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_hyp", []))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SND", [SND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("y_eq", []))(thm_tac (new_rewrite [] [])))));
((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("fan_hyp", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
((((use_arg_then2 ("Hypermap_and_fan.INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [Hypermap_and_fan.INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
(((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("dart_switch", [dart_switch]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("in_dart1_in_dart", [in_dart1_in_dart]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sigma_in_dart1", [sigma_in_dart1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(Sections.add_section_hyp "good_nodes" (`good_list_nodes L`));;
(* Lemma fan_list_nodes_iso_BIJ *)
let fan_list_nodes_iso_BIJ = Sections.section_proof []
`BIJ (fan_list_nodes_iso (f,(V,E))) V (elements_of_list L)`
[
((((use_arg_then2 ("finite_surj_eq_bij", [finite_surj_eq_bij]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fan_list_nodes_iso_surj", [fan_list_nodes_iso_surj]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("elements_of_list", [elements_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_SET_OF_LIST", [FINITE_SET_OF_LIST]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((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_list_of_elements", [uniq_list_of_elements]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((fun arg_tac -> (use_arg_then2 ("iffLR", [iffLR])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition])) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (use_arg_then2 ("NODE_SET_AS_IMAGE", [NODE_SET_AS_IMAGE])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["f"]) THEN (case THEN (move ["inj"])) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
(((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ])) (thm_tac apply_tac)) THEN (((((fun arg_tac -> (use_arg_then2 ("fan_imp_finite_set", [fan_imp_finite_set])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("inj", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
];;
(* Lemma fan_list_nodes_iso_inj *)
let fan_list_nodes_iso_inj = Sections.section_proof ["x";"y"]
`x IN V /\ y IN V
/\ fan_list_nodes_iso (f,(V,E)) x = fan_list_nodes_iso (f,(V,E)) y
==> x = y`
[
(BETA_TAC THEN (case THEN (move ["x_in"])) THEN (case THEN (move ["y_in"])) THEN (move ["eq"]));
((((use_arg_then2 ("fan_list_nodes_iso_BIJ", [fan_list_nodes_iso_BIJ])) (disch_tac [])) THEN (clear_assumption "fan_list_nodes_iso_BIJ") THEN BETA_TAC) THEN (((((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ALL_TAC) THEN (case THEN (move ["_"])) THEN (move ["inj"]) THEN (move ["_"])));
(((use_arg_then2 ("inj", [])) (disch_tac [])) THEN (clear_assumption "inj") THEN (exact_tac));
];;
(Sections.add_section_hyp "f_surr" (`fully_surrounded (V,E)`));;
(* Lemma iso_imp_good_conditions *)
let iso_imp_good_conditions = Sections.section_proof ["d"]
`MEM d (list_of_darts L) /\ 3 < sizel (find_face L d)
==> ~MEM (list_hyp_diag L d) (list_of_darts L) /\
~(FST (list_hyp_diag L d) = SND (list_hyp_diag L d))`
[
(BETA_TAC THEN (case THEN ((move ["mem_d"]) THEN (move ["f_size"]))));
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"])));
((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"])));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G")));
((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN BETA_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 (move ["d_in"])));
((fun arg_tac -> arg_tac (Arg_term (`?x. f x = d /\ x IN dart_of_fan (V,E)`))) (term_tac (have_gen_tac [](case THEN ((case THEN ((move ["v"]) THEN (move ["w"]))) THEN (case THEN ((move ["d_eq"]) THEN (move ["vw_in"]))))))));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["x"]) THEN (case THEN ((move ["x_in"]) THEN (move ["f_eq"])))))));
(((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E) /\ v,w IN dart H`))) (term_tac (have_gen_tac [](move ["vw_in1"]))));
(((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`3 < CARD (face H (v,w))`))) (term_tac (have_gen_tac [](move ["card_f"]))));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_card_components", [hyp_iso_card_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("G_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("card_face_of_list", [card_face_of_list]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_ROT (-1)) (((((use_arg_then2 ("d_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("fan_list_diag_eq", [fan_list_diag_eq]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (split_tac)));
(((repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("implybF", [implybF]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))));
((((use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)));
((((use_arg_then2 ("sigma_fan_not_fixed", [sigma_fan_not_fixed]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((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 [] []))))));
(((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_diag_not_in_dart", [fully_surrounded_diag_not_in_dart])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
(((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (((use_arg_then2 ("contra", [contra])) (disch_tac [])) THEN (clear_assumption "contra") THEN (DISCH_THEN apply_tac) THEN (move ["ww'_in"])));
((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E v w`))) (term_tac (set_tac "w'")));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ww'_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN (case THEN ((move ["a"]) THEN (move ["b"]))))));
((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["ab_in"])));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a IN V /\ b IN V`))) (term_tac (have_gen_tac [](move ["ab_inV"])))) ((repeat_tactic 1 9 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("a", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("b", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`w IN V /\ w' IN V`))) (term_tac (have_gen_tac [](move ["ww'_inV"]))));
(((((use_arg_then2 ("w'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sigma_fan_inV", [sigma_fan_inV]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("v", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("w", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] [])))));
(BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (move ["eq1"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["eq2"]));
(((((use_arg_then2 ("eq1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("eq2", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;
(* Lemma iso_imp_good_list_split *)
let iso_imp_good_list_split = Sections.section_proof ["d"]
`good_list (split_list_hyp L d)`
[
((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
(((fun arg_tac -> (use_arg_then2 ("good_list_split", [good_list_split])) (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));
(((fun arg_tac -> arg_tac (Arg_term (`sizel (find_pair_list L d) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
(((use_arg_then2 ("iso_imp_good_conditions", [iso_imp_good_conditions])) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_d", []))(thm_tac (new_rewrite [] []))))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
];;
(* Lemma split_list_hyp_iso *)
let split_list_hyp_iso = Sections.section_proof ["d"]
`d IN dart_of_fan (V,E) ==>
hyp_iso (fan_list_iso (f,(V,E)))
(hypermap_of_fan (split_fan_face (V,E) d), hypermap_of_list (split_list_hyp L (f d)))`
[
(((use_arg_then2 ("d", [])) (disch_tac [])) THEN (clear_assumption "d") THEN BETA_TAC THEN (case THEN ((move ["v"]) THEN (move ["w"]))) THEN (move ["vw_in"]));
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["hypV"])));
((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"])));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan (V,E)`))) (term_tac (set_tac "H")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list L`))) (term_tac (set_tac "G")));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["d1_eq"])));
((fun arg_tac -> arg_tac (Arg_term (`MEM (f (v,w)) (list_of_darts L)`))) (term_tac (have_gen_tac [](move ["mem_fd"]))));
(((((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 (((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`CARD (face H (v,w)) = sizel (find_face L (f (v,w)))`))) (term_tac (have_gen_tac [](move ["card_f"]))));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_card_components", [hyp_iso_card_components])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(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));
((((use_arg_then2 ("goodL", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("good_list", [good_list]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["uniqL"])) THEN (move ["_"])));
(((fun arg_tac -> arg_tac (Arg_term (`sizel (find_face L (f (v,w))) <= 3`))) (disch_eq_tac "f_size" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((fun arg_tac -> (use_arg_then2 ("hypermap_of_split_list_eq3", [hypermap_of_split_list_eq3])) (fun fst_arg -> (use_arg_then2 ("f_size", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("G_def", []))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("split_fan_face_eq", [split_fan_face_eq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("fanV", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("vw_in", []))(thm_tac (new_rewrite [] []))))));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("FULLY_SURROUNDED_IMP_CARD_FACE_GE_3", [FULLY_SURROUNDED_IMP_CARD_FACE_GE_3])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (arith_tac) THEN (done_tac));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_ext", [hyp_iso_ext])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN (move ["x"]) THEN (move ["x_in"]));
((((use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`3 < CARD (face (hypermap_of_fan (V,E)) (v,w))`))) (term_tac (have_gen_tac [](move ["card_f3"]))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["fan_split"]) THEN (case THEN (move ["dart_splitV_eq"])) THEN (move ["f_split_surr"])))));
((fun arg_tac -> arg_tac (Arg_term (`split_fan_face (V,E) (v,w)`))) (term_tac (set_tac "F1")));
(in_tac ["f_split_surr"; "fan_split"] false (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (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 ("fully_surrounded_dart_of_fan_eq", [fully_surrounded_dart_of_fan_eq])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_split_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac))) THEN (move ["split1_eq"]));
((fun arg_tac -> (use_arg_then2 ("iso_imp_good_list_split", [iso_imp_good_list_split])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["good_split"])));
((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`v,w IN dart1_of_fan (V,E)`))) (term_tac (have_gen_tac [](move ["vw_in1"])))) ((((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> (use_arg_then2 ("fan_list_diag_eq", [fan_list_diag_eq])) (fun fst_arg -> (use_arg_then2 ("vw_in1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["diag_eq"])));
((fun arg_tac -> arg_tac (Arg_term (`sigma_fan (vec 0) V E v w`))) (term_tac (set_tac "w'")));
((fun arg_tac -> arg_tac (Arg_term (`fan_list_iso _`))) (term_tac (set_tac "R")));
((fun arg_tac -> arg_tac (Arg_term (`dart (hypermap_of_list (split_list_hyp L (f (v,w))))
= darts_of_list L UNION {R (w',w), R (w, w')}`))) (term_tac (have_gen_tac [](move ["dart_splitL_eq"]))));
((((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("good_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`3 < sizel (find_pair_list L (f (v,w)))`))) (term_tac (have_gen_tac [](move ["gt3"]))));
((((use_arg_then2 ("f_size", [])) (disch_tac [])) THEN (clear_assumption "f_size") THEN BETA_TAC) THEN ((((use_arg_then2 ("find_face_alt", [find_face_alt]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_list_pairs", [size_list_pairs]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
(((fun arg_tac -> (use_arg_then2 ("perm_eq_set_of_list_eq", [perm_eq_set_of_list_eq])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("darts_of_list_split", [darts_of_list_split])) (fun fst_arg -> (use_arg_then2 ("gt3", [])) (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 [] []))));
((((use_arg_then2 ("APPEND_cat", [APPEND_cat]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("SET_OF_LIST_APPEND", [SET_OF_LIST_APPEND]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("UNION_COMM", [UNION_COMM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("darts_of_list", [darts_of_list]))(thm_tac (new_rewrite [] [])))));
((congr_tac (`_1 UNION _2`)) THEN ((TRY done_tac)));
((repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL set_of_list)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("diag_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [2] []))))) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_def", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL Collect_geom.PER_SET2)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (simp_tac)));
((fun arg_tac -> (use_arg_then2 ("components_hypermap_of_list", [components_hypermap_of_list])) (fun fst_arg -> (use_arg_then2 ("good_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H1")));
((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_list _`))) (term_tac (set_tac "G1")));
(BETA_TAC THEN (move ["hypL1"]) THEN (move ["hypV1"]));
((fun arg_tac -> arg_tac (Arg_term (`dart G1 = IMAGE R (dart H1)`))) (term_tac (have_gen_tac [](move ["dartG1_eq"]))));
((((use_arg_then2 ("dart_splitL_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_splitV_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((use_arg_then2 ("IMAGE_UNION", [IMAGE_UNION]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL IMAGE_CLAUSES)))(thm_tac (new_rewrite [] [])))))) THEN ((congr_tac (`_1 UNION _2`)) THEN ((TRY done_tac))));
(((((fun arg_tac -> (use_arg_then2 ("iso_dart", [iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("image_ext_eq", [image_ext_eq])) (thm_tac apply_tac)) THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("hyp_iso_edge_face", [hyp_iso_edge_face]))(thm_tac (new_rewrite [] [])))) THEN (split_tac));
((((use_arg_then2 ("dartG1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("BIJ", [BIJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Misc_defs_and_lemmas.IMAGE_SURJ", [Misc_defs_and_lemmas.IMAGE_SURJ]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INJ", [INJ]))(thm_tac (new_rewrite [] [])))));
((THENL_FIRST) (split_tac) ((BETA_TAC THEN (move ["x"]) THEN (move ["x_in"])) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN ((use_arg_then2 ("x", [])) (term_tac exists_tac)) THEN (done_tac)));
(BETA_TAC THEN (case THEN ((move ["v1"]) THEN (move ["w1"]))) THEN (case THEN ((move ["v2"]) THEN (move ["w2"]))) THEN (case THEN (move ["vw1_in"])) THEN (case THEN (move ["vw2_in"])) THEN (move ["eq"]));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`v1 IN V /\ v2 IN V /\ w1 IN V /\ w2 IN V`))) (term_tac (have_gen_tac [](move ["inV"])))));
((((use_arg_then2 ("eq", [])) (disch_tac [])) THEN (clear_assumption "eq") THEN BETA_TAC) THEN ((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))));
((BETA_TAC THEN (case THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("vw2_in", [])) (disch_tac [])) THEN (clear_assumption "vw2_in") THEN ((use_arg_then2 ("vw1_in", [])) (disch_tac [])) THEN (clear_assumption "vw1_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))));
(BETA_TAC THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["vw1_in"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fan_split", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))));
((((use_arg_then2 ("vw1_in", [])) (disch_tac [])) THEN (clear_assumption "vw1_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("F1_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
(case THEN (move ["a"]) THEN (move ["b"]) THEN (move ["ab_in"]));
((fun arg_tac -> arg_tac (Arg_term (`R (a,b) IN dart G1`))) (term_tac (have_gen_tac [](move ["Rab_in"]))));
(((((use_arg_then2 ("dartG1_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`a,b`))) (term_tac exists_tac)) THEN (done_tac));
(split_tac);
((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL1", []))(thm_tac (new_rewrite [] [])))) 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 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("e_fan_pair_ext_explicit", [e_fan_pair_ext_explicit]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("pair_expand", [pair_expand]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_split_fan_face))) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("card_f3", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC));
((((use_arg_then2 ("F1_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`sigma_fan _ V E w' v`))) (term_tac (set_tac "u")));
(BETA_TAC THEN (move ["f_fan_eq"]));
(((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE f_split_list))) (fun fst_arg -> (use_arg_then2 ("goodL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN (ANTS_TAC));
(((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_size", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("iso_imp_good_conditions", [iso_imp_good_conditions])) (thm_tac apply_tac)));
((((use_arg_then2 ("ltnNge", [ltnNge]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`split_list_hyp L _`))) (term_tac (set_tac "L2")));
((((use_arg_then2 ("diag_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (BETA_TAC THEN (move ["f_list_eq"])));
((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("pair_expand", [pair_expand])) (fun fst_arg -> (use_arg_then2 ("F1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("split1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((((use_arg_then2 ("hypL1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((fun arg_tac -> arg_tac (Arg_term (`x IN dart_of_fan (V,E) ==> R x = f x`))) (term_tac (have_gen_tac ["x"](move ["R_eq_f"]))));
(((DISCH_THEN (fun snd_th -> (use_arg_then2 ("hyp_iso_eq_fan_list_iso", [hyp_iso_eq_fan_list_iso])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN ((((use_arg_then2 ("R_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`a,b = v,w`))) (disch_eq_tac "eq1" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) (((((use_arg_then2 ("eq1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`w',v = inverse (face_map H) (v,w)`))) (term_tac (have_gen_tac [](move ["w'v_eq"]))));
(((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("w'_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`w',v IN dart H`))) (term_tac (have_gen_tac [](move ["w'v_in"]))));
(((((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`u,w' = inverse (face_map H) (w',v)`))) (term_tac (have_gen_tac [](move ["uw'_eq"]))));
((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("INVERSE_F_FAN_PAIR_EXT_EXPLICIT", [INVERSE_F_FAN_PAIR_EXT_EXPLICIT]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))));
(((((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("w'v_in", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("u_def", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((fun arg_tac -> arg_tac (Arg_term (`a,b = w,w'`))) (disch_eq_tac "eq2" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))));
(((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(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 (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`R (w',w) = e_list (R (w,w'))`))) (term_tac (have_gen_tac [](move ["Rw'w_eq"]))));
(((((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("e_list", [e_list]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((fun arg_tac -> arg_tac (Arg_term (`a,b = w',w`))) (disch_eq_tac "eq3" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
((((use_arg_then2 ("eq3", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Rw'w_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair (V,E) (v,w) = face_map H (v,w)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
(((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("vw_in1", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(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 (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`find_face L (f (v,w))`))) (term_tac (set_tac "ff")));
((fun arg_tac -> arg_tac (Arg_term (`R (u,w') = prev_el ff (prev_el ff (f (v,w)))`))) (term_tac (have_gen_tac [](move ["Ruw'_eq"]))));
((((use_arg_then2 ("uw'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("w'v_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("hyp_iso_inverse_comm", [hyp_iso_inverse_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [2] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(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 ("mem_fd", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("ff_def", []))(thm_tac (new_rewrite [] [])))));
(((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`prev_el ff (f (v,w)) IN darts_of_list L`))) (term_tac (have_gen_tac [](move ["mem_ff"])))));
((((use_arg_then2 ("f_list_ext_inverse", [f_list_ext_inverse]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_ff", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`find_face L (prev_el ff (f (v,w))) = ff`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
((((fun arg_tac -> (use_arg_then2 ("find_face_eq", [find_face_eq])) (fun fst_arg -> (use_arg_then2 ("uniqL", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("darts_of_list", [darts_of_list]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
((repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("dart_in_face", [dart_in_face]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("mem_find_face", [mem_find_face]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
(((((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 ("mem_find_face_imp_mem_darts", [mem_find_face_imp_mem_darts])) (thm_tac apply_tac)));
(((fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("ff_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("mem_prev_el", [mem_prev_el]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ff_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));
(((fun arg_tac -> arg_tac (Arg_term (`a,b = u,w'`))) (disch_eq_tac "eq4" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
(((((use_arg_then2 ("eq4", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Ruw'_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Rw'w_eq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_FIRST) (((use_arg_then2 ("f_fan_eq", []))(thm_tac (new_rewrite [] [])))) (((((use_arg_then2 ("hypV1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negb_or", [negb_or]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`a,b IN dart H`))) (term_tac (have_gen_tac [](move ["ab_in0"]))));
((((use_arg_then2 ("ab_in", [])) (disch_tac [])) THEN (clear_assumption "ab_in") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("dart_splitV_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_UNION", [IN_UNION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))));
(((((use_arg_then2 ("IN_INSERT", [IN_INSERT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_SING", [IN_SING]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("eq3", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((THENL_ROT (-1)) (((use_arg_then2 ("f_list_eq", []))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> arg_tac (Arg_term (`f_fan_pair (V,E) (a,b) = face_map H (a,b)`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
(((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_fan_pair_ext", [f_fan_pair_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d1_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ab_in0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
((((use_arg_then2 ("eq_sym", [eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("lemma_dart_invariant", [lemma_dart_invariant]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((fun arg_tac -> (use_arg_then2 ("hyp_iso_comm", [hyp_iso_comm])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypL", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("f_list_ext", [f_list_ext]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("res", [res]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("hypL", []))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((fun arg_tac -> (use_arg_then2 ("hyp_iso_dart", [hyp_iso_dart])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("R_eq_f", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("hypV", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
((((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 ("hypL1", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rab_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("Ruw'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("Rw'w_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_eq_f", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((fun arg_tac -> arg_tac (Arg_term (`a IN V /\ b IN V /\ u IN V /\ v IN V /\ w' IN V /\ w IN V`))) (term_tac (have_gen_tac [](move ["in_all"]))));
((((use_arg_then2 ("ab_in0", [])) (disch_tac [])) THEN (clear_assumption "ab_in0") THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (simp_tac)));
((((use_arg_then2 ("w'v_in", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] [])))) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (case THEN ((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))) THEN (simp_tac)));
(((fun arg_tac -> (use_arg_then2 ("lemma_dart_inveriant_under_inverse_maps", [lemma_dart_inveriant_under_inverse_maps])) (fun fst_arg -> (use_arg_then2 ("w'v_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
(((((use_arg_then2 ("uw'_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("hypV", []))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PAIR_IN_DART_OF_FAN", [PAIR_IN_DART_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
(((fun arg_tac ->(use_arg_then2 ("eq1", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("eq2", []))(fun tmp_arg1 -> (fun arg_tac ->(use_arg_then2 ("eq3", []))(fun tmp_arg1 -> (use_arg_then2 ("eq4", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2)))))) (disch_tac [])) THEN ((use_arg_then2 ("contraL", [contraL])) (disch_tac [])) THEN (clear_assumption "contraL") THEN (DISCH_THEN apply_tac));
((repeat_tactic 1 9 (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("R_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("fan_list_iso", [fan_list_iso]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("PAIR_EQ", [PAIR_EQ]))(thm_tac (new_rewrite [] []))))));
((repeat_tactic 1 9 (case)) THEN ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (move ["h1"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("fan_list_nodes_iso_inj", [fan_list_nodes_iso_inj])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["h2"])) THEN ((((use_arg_then2 ("h1", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("h2", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
(* Lemma iso_imp_good_list_nodes_split *)
let iso_imp_good_list_nodes_split = Sections.section_proof ["d"]
`good_list_nodes (split_list_hyp L d)`
[
((THENL_LAST) (((fun arg_tac -> arg_tac (Arg_term (`MEM d (list_of_darts L)`))) (disch_eq_tac "mem_d" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("d_not_in_dart_split_eq", [d_not_in_dart_split_eq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
((((use_arg_then2 ("mem_d", [])) (disch_tac [])) THEN (clear_assumption "mem_d") THEN BETA_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 (((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)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["d_in"])));
((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("hyp_iso_surj", [hyp_iso_surj])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((case THEN ((move ["v"]) THEN (move ["w"]))) THEN (case THEN ((move ["vw_in"]) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))))))));
(in_tac ["vw_in"] false (((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (use_arg_then2 ("split_list_hyp_iso", [split_list_hyp_iso])) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["iso_th"])));
((((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("iso_imp_good_list_split", [iso_imp_good_list_split]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
((((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("iso_th", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
(((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_of_elements_split", [list_of_elements_split])) (fun fst_arg -> (use_arg_then2 ("L", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`f (v,w)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))));
((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fan_split_fan_face", [fan_split_fan_face])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("vw_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["fan_split"]) THEN (move ["_"])))));
(in_tac ["fan_split"] true (((use_arg_then2 ("split_fan_face", [split_fan_face]))(thm_tac (new_rewrite [] [])))));
((((use_arg_then2 ("fan_number_of_nodes", [fan_number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (use_arg_then2 ("fan_number_of_nodes", [fan_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))));
(((((fun arg_tac -> (use_arg_then2 ("iso_number_of_nodes", [iso_number_of_nodes])) (fun fst_arg -> (use_arg_then2 ("f_iso", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("number_of_nodes", [number_of_nodes]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("good_list_nodes_condition", [good_list_nodes_condition]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
];;
(* Finalization of the section FanAndList *)
let set_of_edge_subset = Sections.finalize_theorem set_of_edge_subset;;
let fan_list_iso_invariant = Sections.finalize_theorem fan_list_iso_invariant;;
let hyp_iso_eq_fan_list_iso = Sections.finalize_theorem hyp_iso_eq_fan_list_iso;;
let fan_list_nodes_iso_surj = Sections.finalize_theorem fan_list_nodes_iso_surj;;
let fan_list_nodes_to = Sections.finalize_theorem fan_list_nodes_to;;
let fan_list_diag_eq = Sections.finalize_theorem fan_list_diag_eq;;
let fan_list_nodes_iso_BIJ = Sections.finalize_theorem fan_list_nodes_iso_BIJ;;
let fan_list_nodes_iso_inj = Sections.finalize_theorem fan_list_nodes_iso_inj;;
let iso_imp_good_conditions = Sections.finalize_theorem iso_imp_good_conditions;;
let iso_imp_good_list_split = Sections.finalize_theorem iso_imp_good_list_split;;
let split_list_hyp_iso = Sections.finalize_theorem split_list_hyp_iso;;
let iso_imp_good_list_nodes_split = Sections.finalize_theorem iso_imp_good_list_nodes_split;;
Sections.end_section "FanAndList";;
(* Close the module *)
end;;