(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Appendix, Main Estimate, check_completeness                       *)
(* Chapter: Local Fan                                                         *)
(* Lemma: JEJTVGB                                                             *)
(* Author: Hoang Le Truong and Thomas Hales                                   *)
(* Date: 2013-08-15                                                           *)
(* ========================================================================== *)

module Jejtvgb = struct

  open Hales_tactic;;

let SCS_ARROW_TRANS_SING = 
prove_by_refinement(
  `!a S. scs_arrow_v39 {a} S /\ (!x. x IN S ==> scs_arrow_v39 {x} {}) ==> scs_arrow_v39 {a} {}`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Appendix.scs_arrow_v39;NOT_IN_EMPTY;IN_SING];
  BY(MESON_TAC[])
  ]);;
  (* }}} *)

let JEJTVGB_case_breakdown = prove_by_refinement(
  (* main_work4 ==> *) ` main_nonlinear_terminal_v11 ==> (
  scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 } /\ // OEHDBEN
    scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 } /\ // OTMTOTJ1
scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 } /\ // 

scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 , 
						    scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 } /\ //  OTMTOTJ3

scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 ,  scs_stab_diag_v39 scs_5M1 0 3, 
    scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 } /\ // OTMTOTJ4 
scs_arrow_v39 { scs_5M2 }  {scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39  scs_5M1 0  2, 
    scs_stab_diag_v39   scs_5M1  0   3, scs_stab_diag_v39  scs_5M1  2  4, 
     scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4} /\ // HIJQAHA
//{ scs_3T1,scs_3T4,scs_4M6',scs_4M7,scs_4M8,
//						   scs_5T1, scs_stab_diag_v39 scs_5I2 0 2 , 
//						   scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4 } /\ // HIJQAHA

scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 0 2 }
    {scs_3M1, scs_4M2  } /\ //  CNICGSF1 ..

scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 0 2 }
    {scs_3T1, scs_4M3'  } /\ //  CNICGSF2

scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 2 }
    {scs_3T4, scs_4M2  } /\ //  CNICGSF3

scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 3 }
    {scs_4M4', scs_3M1 } /\ //  CNICGSF4

scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 2 4 }
    {scs_3M1, scs_4M5'  } /\ //  CNICGSF5 ..

  scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 } /\ // FYSSVEV


  scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 } /\ // ARDBZYE


  scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 0 2 } { scs_3M1 } /\ // AUEAHEH

  // scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 } /\ // ZNLLLDL (internal)

  scs_arrow_v39 { scs_4I3 } {scs_4M6', scs_4T4} /\  // VQFYMZY ..

//  scs_arrow_v39 { scs_4M1 } { scs_4M2, scs_4M6' } /\ // unused.

  scs_arrow_v39 { scs_4M2 } {scs_4M6', scs_3M1, scs_3T4}  /\ //  BNAWVNH

  scs_arrow_v39 { scs_4M3' } {scs_4M6', scs_3T1, scs_3T6'}  /\ // RAWZDIB

  scs_arrow_v39 { scs_4M4' } {scs_4M7, scs_3T3, scs_3M1, scs_3T4} /\ //  MFKLVDK

  scs_arrow_v39 { scs_4M5' } {scs_4M8, scs_3T4} /\ // RYPDIXT

scs_arrow_v39 {scs_4M6'} {scs_4T3,scs_4T5} /\ // NWDGKXH

scs_arrow_v39 {scs_4M7} {scs_4M6', scs_3T3, scs_3M1, scs_3T4} /\ // YOBIMPP

scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7,scs_3T4} /\ // MIQMCSN

    scs_arrow_v39 {scs_3M1} {scs_3T1,scs_3T5} // BKOSSGE

==> 
JEJTVGB_assume_v39)
`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH Ocbicby.OCBICBY) [];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `scs_arrow_v39 {scs_3M1} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3T1, scs_3T5}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M6'} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4T3,scs_4T5}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M7} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M6', scs_3T3, scs_3M1, scs_3T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M8} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M6', scs_3T7, scs_3T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M5'} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M8, scs_3T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M4'} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M7, scs_3T3, scs_3M1, scs_3T4}` EXISTS_TAC; (* revised *)
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M3'} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M6', scs_3T1, scs_3T6'}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4M2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M6', scs_3M1, scs_3T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4I3} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M6', scs_4T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3M1}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4I2}  {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4T1, scs_4T2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_4I1}  {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4I2, scs_stab_diag_v39 scs_4I1 0 2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 2 4}   {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3M1, scs_4M5'}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 0 3}   {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_4M4', scs_3M1}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3T4, scs_4M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5I2 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3T1, scs_4M3'}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_stab_diag_v39 scs_5I1 0 2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_3M1, scs_4M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_5M2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39                                                       scs_5M1                                                      0                                                      2, scs_stab_diag_v39                                                         scs_5M1                                                         0                                                         3, scs_stab_diag_v39                                                            scs_5M1                                                            2                                                            4, scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_5M1} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,       scs_stab_diag_v39 scs_5M1 2      4, scs_5M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_5I3} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,       scs_stab_diag_v39 scs_5M1 2      4, scs_5M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_5I2} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_stab_diag_v39 scs_5I2 0 2, scs_5M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_5I1} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY ` {scs_stab_diag_v39 scs_5I1 0 2, scs_5M2}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  TYPIFY `scs_arrow_v39 {scs_6I1} {}` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SCS_ARROW_TRANS_SING;
    TYPIFY `{scs_6T1, scs_5M1, scs_4M2, scs_3M1}` EXISTS_TAC;
    ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
    BY(REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
  COMMENT "final kill";
  MATCH_MP_TAC Ayqjtmd.EAPGLE;
  REWRITE_TAC[GSYM Ocbicby.scs_arrow_sing_empty];
  REWRITE_TAC[Jotswix.s_init_list_alt;MEM];
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
  BY(REWRITE_TAC[UNDISCH2 Jotswix.LFLACKU])
  ]);;
  (* }}} *)

let JEJTVGB = 
prove_by_refinement(
 `main_nonlinear_terminal_v11 ==> JEJTVGB_assume_v39`,

  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC (UNDISCH JEJTVGB_case_breakdown);
  REWRITE_TAC (map UNDISCH2 [Hexagons.OEHDBEN;Otmtotj.OTMTOTJ1;Otmtotj.OTMTOTJ2;Otmtotj.OTMTOTJ3;Otmtotj.OTMTOTJ4]);
  REWRITE_TAC (map UNDISCH2 [Hijqaha.HIJQAHA;Cnicgsf.CNICGSF1;Cnicgsf.CNICGSF2;Cnicgsf.CNICGSF3;Cnicgsf.CNICGSF4;Cnicgsf.CNICGSF5]);
  REWRITE_TAC (map UNDISCH2 [Ardbzye.FYSSVEV;Ardbzye.ARDBZYE;Aueaheh.AUEAHEH;Aueaheh.VQFYMZY]);
  REWRITE_TAC (map UNDISCH2 [Aueaheh.BNAWVNH;Aueaheh.RAWZDIB;Aueaheh.MFKLVDK;Aueaheh.RYPDIXT]);
  BY(REWRITE_TAC (map UNDISCH2 [Miqmcsn.NWDGKXH;Miqmcsn.YOBIMPP;Miqmcsn.MIQMCSN;Bkossge.BKOSSGE]))
  ]);;
  (* }}} *)


end;;