(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma:                                                          *)
(*      Chaper    : Packing (Cells cluster)                                  *)
(*                                                                           *)
(* ------------------ The lemma about sum of beta_bump --------------------- *)
(* ========================================================================= *)

(* ========================================================================= *)
(*    Checkpointed files                                                     *)
(* ========================================================================= *)
(*

loads "/home/vu/flyspeck/working/marchal_cells_3.hl";;
flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;
open Upfzbzm_support_lemmas;;
flyspeck_needs "packing/LEPJBDJ.hl";;
open Lepjbdj;;

*)

(* ========================================================================== *)
(*   Begin the proof                                                          *)
(* ========================================================================== *)

module Sum_beta_bump = struct

open Rogers;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2_new;;
open Lepjbdj;;
open Upfzbzm_support_lemmas;;

let SUM_BETA_BUMP_LEMMA = 
prove_by_refinement (
 `!V X. saturated V /\ packing V /\ mcell_set V X ==> 
         sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`,


[(REPEAT STRIP_TAC THEN UP_ASM_TAC);
 (ASM_CASES_TAC `~(X:real^3->bool = {})`);
 (REWRITE_TAC[mcell_set; IN_ELIM_THM]);
 (STRIP_TAC);
 (NEW_GOAL `barV V 3 ul`);
 (ASM_SET_TAC[IN]);

 (ASM_CASES_TAC `i < 4`);  (* consider case i < 4 va i >= 4 *)
 (NEW_GOAL `~(i = 4)`);
 (ASM_ARITH_TAC);
 (NEW_GOAL `i <= 4`);
 (ASM_ARITH_TAC);
 (ASM_REWRITE_TAC[beta_bump]);
 (REPEAT LET_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (STRIP_TAC);
 (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ 
                              mcell i V ul = mcell k V ul')`);
 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SELECT_AX);
 (EXISTS_TAC `(i:num,ul:(real^3)list)`);
 (EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM]);
 (ASM_REWRITE_TAC[IN]);
 (UP_ASM_TAC THEN EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 (NEW_GOAL `barV V 3 ul'`);
 (ASM_SET_TAC[]);

 (NEW_GOAL `i = k:num`);
 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);

 (ASM_CASES_TAC `i = 0`);
 (NEW_GOAL `V INTER mcell i V ul  = {} `);
 (REWRITE_TAC[ASSUME `i = 0`]);
 (MATCH_MP_TAC LEPJBDJ_0);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 0`);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `V INTER mcell k V ul' 
           = set_of_list (truncate_simplex (k - 1) ul')`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `k = 1`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 2`);
 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 3`);
 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 (ASM_SET_TAC[]);
 (ASM_CASES_TAC `k = 4`);
 (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);
 (ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);  (* Finish the case i = 0 *)

 (NEW_GOAL `V INTER mcell i V ul
           = set_of_list (truncate_simplex (i - 1) ul)`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `k = 0`);
 (NEW_GOAL `V INTER mcell k V ul' = {}`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC LEPJBDJ_0);
 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 (NEW_GOAL `F`);
 (NEW_GOAL 
  `~(set_of_list (truncate_simplex (i - 1) (ul:(real^3)list)) = {})`);
 (ASM_CASES_TAC `i = 1`);
 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
 (SET_TAC[]);
 (ASM_CASES_TAC `i = 2`);
 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (SET_TAC[]);
 (ASM_CASES_TAC `i = 3`);
 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 (SET_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `V INTER mcell k V ul'
           = set_of_list (truncate_simplex (k - 1) ul')`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `CARD (set_of_list (truncate_simplex (i - 1) (ul:(real^3)list))) 
            = i:num`);
 (REWRITE_WITH 
  `LENGTH (truncate_simplex (i - 1) (ul:(real^3)list)) = (i - 1) + 1 /\ 
   CARD (set_of_list (truncate_simplex (i - 1) ul)) = (i - 1) + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (ASM_ARITH_TAC);

 (NEW_GOAL `CARD (set_of_list (truncate_simplex (k - 1) (ul':(real^3)list))) 
            = k:num`);
 (REWRITE_WITH 
  `LENGTH (truncate_simplex (k - 1) (ul':(real^3)list)) = (k - 1) + 1 /\ 
   CARD (set_of_list (truncate_simplex (k - 1) ul')) = (k - 1) + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 (EXISTS_TAC `3`);
 (STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_ARITH_TAC);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!e. sum
      {e',e'',p,vl | k = 4 /\  critical_edgeX V (mcell k V ul') = {e', e''} /\
                     e = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\
                     e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}}
      (\(e',e'',p,vl). 
           (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4) 
            = &0`);
 GEN_TAC;
 (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\
                    critical_edgeX V (mcell k V ul') = {e', e''} /\
                    e = e' /\ p permutes 0..3 /\
                    vl = left_action_list p ul' /\
                    e' = {EL 0 vl, EL 1 vl} /\
                    e'' = {EL 2 vl, EL 3 vl}}`);
 (NEW_GOAL 
  `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`);
 (EXPAND_TAC "SET1");
 (NEW_GOAL `~(k = 4)`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[SUM_CLAUSES]);

 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUM_0]);

(* Finish the case where i < 4 *)
(* ========================================================================= *)
(* begin with the case i >= 4  *)

 (ASM_REWRITE_TAC[beta_bump]);
 (REPEAT LET_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (STRIP_TAC);
 (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\ 
                              mcell i V ul = mcell k V ul')`);
 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
 (ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC SELECT_AX);
 (EXISTS_TAC `(4,ul:(real^3)list)`);
 (EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM]);
 (ASM_REWRITE_TAC[IN; ARITH_RULE `4 <= 4`]);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; mcell4]);
 (UP_ASM_TAC THEN EXPAND_TAC "P");
 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 (NEW_GOAL `barV V 3 ul'`);
 (ASM_SET_TAC[]);
 (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);

 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);
 (MATCH_MP_TAC BARV_3_EXPLICIT);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
 (NEW_GOAL `mcell i V ul = mcell 4 V ul`);
 (UNDISCH_TAC `mcell i V ul = mcell k V ul'` THEN DISCH_TAC THEN DEL_TAC);
 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`; 
   ARITH_RULE `4 >= 4`; mcell4]);

 (NEW_GOAL `k = 4:num`);

 (NEW_GOAL `V INTER mcell 4 V ul  = 
             set_of_list (truncate_simplex 3 ul)`);
 (REWRITE_TAC[ARITH_RULE `3 = 4 - 1`]);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `k = 0`);
 (NEW_GOAL `V INTER mcell k V ul'  = {}`);
 (REWRITE_TAC[ASSUME `k = 0`]);
 (MATCH_MP_TAC LEPJBDJ_0);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `V INTER mcell 4 V ul = set_of_list (truncate_simplex 3 ul)`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[]);

(* ============================= *)

 (NEW_GOAL `V INTER mcell k V ul'  = 
             set_of_list (truncate_simplex (k - 1) ul')`);
 (MATCH_MP_TAC LEPJBDJ);
 (ASM_REWRITE_TAC[]);
 (STRIP_TAC);
 (ASM_ARITH_TAC);
 (ASM_SET_TAC[]);

 (NEW_GOAL `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = 
             set_of_list (truncate_simplex (k - 1) ul')`);
 (ASM_SET_TAC[]);
 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);
 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
 (ASM_REWRITE_TAC[set_of_list]);
 (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (ARITH_TAC);

 (ASM_CASES_TAC `k = 1`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = 
                set_of_list (truncate_simplex (k - 1) ul')`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `1 - 1 = 0`;   
                   TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
 (STRIP_TAC);
 (NEW_GOAL `CARD {v0:real^3} = 4`);
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[Geomdetail.CARD_SING]);
 (ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `k = 2`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = 
                set_of_list (truncate_simplex (k - 1) ul')`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `2 - 1 = 1`;   
                   TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
 (STRIP_TAC);
 (NEW_GOAL `CARD {v0, v1:real^3} = 4`);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `CARD {v0, v1:real^3} <= 2`);
 (MESON_TAC[Geomdetail.CARD2]);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_CASES_TAC `k = 3`);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) = 
                set_of_list (truncate_simplex (k - 1) ul')`);
 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `3 - 1 = 2`;   
                   TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
 (STRIP_TAC);
 (NEW_GOAL `CARD {v0, v1, v2:real^3} = 4`);
 (ASM_MESON_TAC[]);
 (NEW_GOAL `CARD {v0, v1, v2:real^3} <= 3`);
 (MESON_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (ASM_ARITH_TAC);  (* concluded that k = 4 now *)

(* ======================================================================== *)


 (REWRITE_TAC[ASSUME `mcell i V ul = mcell k V ul'`; ASSUME `k = 4`]);
 (ASM_CASES_TAC `~(CARD (critical_edgeX V (mcell 4 V ul'))  = 2)`);
 (MATCH_MP_TAC SUM_EQ_0);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `y = {v0,v1,v2,v3:real^3} DIFF x`);
 (ASM_CASES_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);
 (REWRITE_WITH 
 `{e',e'',p,vl | critical_edgeX V (mcell 4 V ul') = {e', e''} /\
                x = e' /\
                p permutes 0..3 /\
                vl = left_action_list p ul' /\
                e' = {EL 0 vl, EL 1 vl} /\
                e'' = {EL 2 vl, EL 3 vl}} = {}`);
 (REWRITE_TAC[SET_RULE `a = {} <=> (!t. t IN a ==> F)`]);
 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (NEW_GOAL `y = e'':real^3->bool`);
 (ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "y");
 (REWRITE_TAC[ASSUME `x = e':real^3->bool`; 
               ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
 (REWRITE_WITH `{v0, v1, v2, v3:real^3} = set_of_list (ul')`);
 (ASM_REWRITE_TAC[set_of_list]);
 (REWRITE_WITH `set_of_list (ul':(real^3)list) = set_of_list vl`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REWRITE_TAC[ASSUME 
  `vl:(real^3)list = left_action_list p ul'`]);
 (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);
 (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);

 (NEW_GOAL `vl:(real^3)list = [EL 0 vl; EL 1 vl; EL 2 vl; EL 3 vl]`);
 (ASM_REWRITE_TAC[TABLE_4; left_action_list; LENGTH; EL; HD; TL;
   ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4 /\ 1 = SUC 0 /\ 2 = SUC 1/\ 3 = SUC 2`]);
 (ABBREV_TAC `w0:real^3 = EL 0 vl`);
 (ABBREV_TAC `w1:real^3 = EL 1 vl`);
 (ABBREV_TAC `w2:real^3 = EL 2 vl`);
 (ABBREV_TAC `w3:real^3 = EL 3 vl`);
 (REWRITE_TAC[ASSUME `vl = [w0;w1;w2;w3:real^3]`; set_of_list]);
 (REWRITE_WITH `{w0,w1,w2,w3} = {w0,w1} UNION {w2,w3:real^3}`);
 (SET_TAC[]);
 (MATCH_MP_TAC (SET_RULE `DISJOINT a b ==> ((a UNION b) DIFF a = b)`));

 (REWRITE_TAC[DISJOINT; INTER]);
 (NEW_GOAL `CARD {w0, w1, w2 , w3:real^3} = 4`);
 (REWRITE_WITH `{w0, w1, w2 , w3:real^3} = set_of_list vl`);
 (REWRITE_TAC[ASSUME `vl = [w0; w1; w2; w3:real^3]`; set_of_list]);
 (ONCE_ASM_REWRITE_TAC[]);
 (REWRITE_WITH `set_of_list (left_action_list p ul') 
               = set_of_list (ul':(real^3)list)`);
 (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);
 (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
 (REWRITE_WITH `LENGTH (ul':(real^3)list) = 3 + 1 /\ 
                 CARD (set_of_list ul') = 3 + 1`);
 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 (ARITH_TAC);
 (REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);
 (REWRITE_TAC[SET_RULE `x = {} <=> (!z. z IN x ==> F)`]);
 (REWRITE_TAC[IN;IN_ELIM_THM] THEN STRIP_TAC);
 (REPEAT STRIP_TAC);

 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);
 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);
 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 (REWRITE_TAC[Geomdetail.CARD3]);
 (ASM_ARITH_TAC);

 (UNDISCH_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);
 (REWRITE_TAC[ASSUME `x = e':real^3->bool`; ASSUME `y = e'':real^3->bool`]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[SUM_CLAUSES]);
 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);
 (NEW_GOAL `F`);
 (UNDISCH_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`);
 (REWRITE_TAC[ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);
 (REWRITE_TAC[Geomdetail.CARD_SET2]);
 (EXPAND_TAC "y");
 (STRIP_TAC);
 (NEW_GOAL `{v0, v1,v2,v3:real^3} = {}`);
 (MATCH_MP_TAC (SET_RULE `!s:real^3->bool. x = s DIFF x ==> s = {}`));
 (ASM_MESON_TAC[]);
 (UP_ASM_TAC THEN SET_TAC[]);
 (ASM_MESON_TAC[]);

 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);
 (NEW_GOAL `?x y. critical_edgeX V (mcell 4 V ul') = {x, y} /\ ~(x = y)`);
 (MATCH_MP_TAC Rogers.CARD_2_IMP_DOUBLE);
 (ASM_REWRITE_TAC[FINITE_critical_edgeX]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_TAC[SET_RULE `{x | x IN s} = s`; 
               ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);
 (ASM_SIMP_TAC[Collect_geom.SUM_DIS2]);


 (REWRITE_WITH 
 `{e',e'',p,vl | {x, y} = {e', e''} /\
                x = e' /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3:real^3] /\
                e' = {EL 0 vl, EL 1 vl} /\
                e'' = {EL 2 vl, EL 3 vl}} =
 {e',e'',p,vl | e' = x /\ e'' = y /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3] /\
                x = {EL 0 vl, EL 1 vl} /\
                y = {EL 2 vl, EL 3 vl}}`);
 (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
 (STRIP_TAC);

 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `e':real^3->bool = x`; 
   ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`]);
 (REWRITE_TAC[ASSUME `e'':real^3->bool = y`; 
   ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
 (NEW_GOAL `y = e'':(real^3->bool)`);
 (ASM_SET_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `x:real^3->bool = e'`; 
   ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
 (REWRITE_TAC[ASSUME `y:real^3->bool = e''`; 
   ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);
 (ASM_REWRITE_TAC[]);


 (REWRITE_WITH 
 `{e',e'',p,vl | {x, y} = {e', e''} /\
                y = e' /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3:real^3] /\
                e' = {EL 0 vl, EL 1 vl} /\
                e'' = {EL 2 vl, EL 3 vl}} =
 {e',e'',p,vl | e' = y /\ e'' = x /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3] /\
                y = {EL 0 vl, EL 1 vl} /\
                x = {EL 2 vl, EL 3 vl}}`);
 (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
 (STRIP_TAC);

 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
 (REPEAT STRIP_TAC);

 (REWRITE_TAC[ASSUME `e' = y:real^3->bool`; ASSUME `e'' = x:real^3->bool`]);
 (SET_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `e':real^3->bool = y`; 
   ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`]);
 (REWRITE_TAC[ASSUME `e'':real^3->bool = x`; 
   ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`]);
 (ASM_REWRITE_TAC[]);

 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
 (NEW_GOAL `x = e'':(real^3->bool)`);
 (ASM_SET_TAC[]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[ASSUME `y:real^3->bool = e'`; 
   ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
 (REWRITE_TAC[ASSUME `x:real^3->bool = e''`; 
   ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);
 (ASM_REWRITE_TAC[]);

 (ABBREV_TAC `S1 = {e',e'',p,vl | e' = x /\
                e'' = y /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3:real^3] /\
                x = {EL 0 vl, EL 1 vl} /\
                y = {EL 2 vl, EL 3 vl}}`);
 (ABBREV_TAC `S2 =  {e',e'',p,vl | e' = y /\
                e'' = x /\
                p permutes 0..3 /\
                vl = left_action_list p [v0; v1; v2; v3:real^3] /\
                y = {EL 0 vl, EL 1 vl} /\
                x = {EL 2 vl, EL 3 vl}}`);
 (REWRITE_WITH
  `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool)   
          (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
                   bump (hl [EL 2 vl; EL 3 vl])) / &4) =  
   sum S2 (\(e',e'',p,vl). -- ((bump (hl [EL 2 vl; EL 3 vl]) -
                   bump (hl [EL 0 vl; EL 1 vl])) / &4))`);
 (ONCE_REWRITE_TAC[REAL_ARITH `(bump (hl [EL 0 vl; EL 1 vl]) -
                   bump (hl [EL 2 vl; EL 3 vl])) /
                  &4 = -- ((bump (hl [EL 2 vl; EL 3 vl]) -
                      bump (hl [EL 0 vl; EL 1 vl])) /
                     &4)`]);
 (ASM_REWRITE_TAC[]);
 (ONCE_REWRITE_TAC[SUM_NEG]);
 (ABBREV_TAC `f =  (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). 
 ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4))`);
 (REWRITE_WITH 
`(\(e',e'',p,vl). 
   --((bump (hl [EL 2 vl; EL 3 vl]) -bump (hl [EL 0 vl; EL 1 vl])) / &4)) 
  = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). 
   -- f (e',e'',p,vl))`);
 (EXPAND_TAC "f");
 (REWRITE_TAC[BETA_THM]);

 (REWRITE_WITH 
`sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool) (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).
 -- f (e',e'',p,vl)) =
sum S2 (\x. -- f x)`);
 (AP_TERM_TAC);
 (REWRITE_TAC[FUN_EQ_THM]);
 (EXPAND_TAC "f");
 (REWRITE_TAC[BETA_THM]);
 (REPEAT STRIP_TAC);

 (ABBREV_TAC `e' = FST (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);
 (ABBREV_TAC `e'' = FST (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);
 (ABBREV_TAC `p = FST (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
 (ABBREV_TAC `vl = SND (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);

 (REWRITE_WITH `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = 
  (e',e'',p, vl)`);
 (EXPAND_TAC "e'" THEN EXPAND_TAC "e''" THEN EXPAND_TAC "p" THEN EXPAND_TAC "vl");
 (REWRITE_TAC[PAIR]);
 (REWRITE_TAC[SUM_NEG]);
 (REWRITE_TAC[REAL_ARITH `a + -- b = &0 <=> a = b`]);

(* --------------------------------------------------------------------------- *)
(* Begin new part *)

 (EXPAND_TAC "f");
 (ABBREV_TAC 
`g = (\x. let (e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list) = x 
          in 
           (e'', e', (\i. 
                          if p i = 0 then 2 else
                          if p i = 1 then 3 else
                          if p i = 2 then 0 else
                          if p i = 3 then 1 else i), 
           [EL 2 vl;EL 3 vl;EL 0 vl;EL 1 vl]))`);
 (REWRITE_WITH 
`S1 = IMAGE    
 (g:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->(real^3->bool)#
   (real^3->bool)#(num->num)#(real^3)list) S2 /\  
 (\(e',e'',p,vl). (bump (hl [EL 2 vl; EL 3 vl]) -
                   bump (hl [EL 0 vl; EL 1 vl])) / &4) =  
 (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
                   bump (hl [EL 2 vl; EL 3 vl])) / &4) o g `);

(* ======================================================================= *)

 (REPEAT STRIP_TAC);
  (* New goal 1: to prove S1 = IMAGE g S2 *)
 
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");
 (REWRITE_TAC[IMAGE]);
 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN] THEN  
   REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 (EXISTS_TAC 
   `(e'':real^3->bool,
     e':real^3->bool,
     (\i. if p i = 0
             then 2
             else if p i = 1
                  then 3
                  else if p i = 2 then 0 else if p i = 3 then 1 else i),
     [EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl])`);
 (REPEAT STRIP_TAC);
 (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);
 (ABBREV_TAC `p' =  (\i. if p i = 0
             then 2
             else if p i = 1
                  then 3
                  else if p i = 2 then 0 else if p i = 3 then 1 else i)`);
 (EXISTS_TAC `p':num->num`);
 (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);
 (REWRITE_WITH 
`EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 2 (vl:(real^3)list) /\ 
 EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 3 vl /\
 EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 0 vl /\
 EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 1 vl`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_TAC[ASSUME `e'' = y:real^3->bool`; ASSUME `e' = x:real^3->bool`;
   ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`; 
   ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`;left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);

 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s = (p:num->num) u`);
 (NEW_GOAL `(p:num->num) s = s`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `s = x'':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u = x'':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);



 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
(* begin to prove that p' permutes 0..3 *)


 (NEW_GOAL `p' permutes 0..3`);
 (REWRITE_TAC[permutes]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `x'' > 3`);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (EXPAND_TAC "p'");
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);
 (NEW_GOAL `(p:num->num) x'' = x''`);
 (ASM_SIMP_TAC[]);
 (COND_CASES_TAC);
 (ASM_ARITH_TAC);
 (COND_CASES_TAC);
 (ASM_ARITH_TAC);
 (COND_CASES_TAC);
 (ASM_ARITH_TAC);
 (COND_CASES_TAC);
 (ASM_ARITH_TAC);
 (REFL_TAC);

 (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);

 (ASM_CASES_TAC `y' = 0`);
 (NEW_GOAL `?z. (p:num->num) z = 2`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 2`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 1`);
 (NEW_GOAL `?z. (p:num->num) z = 3`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 3`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 2`);
 (NEW_GOAL `?z. (p:num->num) z = 0`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 0`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 3`);
 (NEW_GOAL `?z. (p:num->num) z = 1`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 1`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);



 (NEW_GOAL `y' > 3`);
 (ASM_ARITH_TAC);
 (NEW_GOAL `?z. (p:num->num) z = y'`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `(p:num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (NEW_GOAL `(p':num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (ASM_ARITH_TAC);

 (NEW_GOAL `(p:num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (NEW_GOAL `(p':num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `(p:num->num) y'' > 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `(p:num->num) y'' = y''`);
 (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p':num->num) y'' = y''`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_MESON_TAC[]);


(* finish proving that p' permutes 0..3 *)

 (REWRITE_TAC[ASSUME `p' permutes 0..3`]);

(* --------------------------------------------------------------------- *)

 (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 2
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);
 (ABBREV_TAC `j = inverse (p:num->num) 2`);
 (NEW_GOAL `(p:num->num) j = 2`);
 (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);



 (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 3
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);
 (ABBREV_TAC `j = inverse (p:num->num) 3`);
 (NEW_GOAL `(p:num->num) j = 3`);
 (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");


 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 0
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);
 (ABBREV_TAC `j = inverse (p:num->num) 0`);
 (NEW_GOAL `(p:num->num) j = 0`);
 (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 1
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);
 (ABBREV_TAC `j = inverse (p:num->num) 1`);
 (NEW_GOAL `(p:num->num) j = 1`);
 (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);


(* ======================================================================= *)

 (EXPAND_TAC "g");
 (LET_TAC);
 (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; 
   ASSUME `x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list =
   e',e'',p,vl`]);
 (REPEAT STRIP_TAC);
 (REWRITE_TAC[ASSUME `e':real^3->bool = e''''`]);
 (REWRITE_TAC[ASSUME `e'':real^3->bool = e'''`]);
 (REWRITE_TAC[FUN_EQ_THM]);

 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s = (p:num->num) u`);
 (NEW_GOAL `(p:num->num) s = s`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `s = x'':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u = x'':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (GEN_TAC);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) x'' > 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);

(* ------------------------------------------------------------------------- *)

 (EXPAND_TAC "vl'");
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  
 (REWRITE_TAC[ASSUME `vl = left_action_list p [v0; v1; v2; v3:real^3]`;                        left_action_list; TABLE_4; LENGTH;EL; HD;TL;
               ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
(* ======================================================================= *)

 (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);
 (ABBREV_TAC `p' =  (\i. if p i = 0
             then 2
             else if p i = 1
                  then 3
                  else if p i = 2 then 0 else if p i = 3 then 1 else i)`);
 (EXISTS_TAC `p':num->num`);
 (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);
 (REWRITE_WITH 
  `{EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], 
    EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} 
   = {EL 0 vl, EL 1 (vl:(real^3)list)}`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  
 (REWRITE_WITH 
  `{EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl], 
    EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]} 
   = {EL 2 vl, EL 3 (vl:(real^3)list)}`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);  
 (REWRITE_TAC[ASSUME `e'' = x:real^3->bool`; ASSUME `e' = y:real^3->bool`;
   ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`; 
   ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`;left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);

 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s = (p:num->num) u`);
 (NEW_GOAL `(p:num->num) s = s`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `s = x''':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u = x''':num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u > 3`);
 (NEW_GOAL `(p':num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p:num->num) u = 0`);
 (NEW_GOAL `(p':num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 1`);
 (NEW_GOAL `(p':num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 2`);
 (NEW_GOAL `(p':num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p:num->num) u = 3`);
 (NEW_GOAL `(p':num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

(* ------------------------------------------------------------------------- *)
(* begin to prove that p' permutes 0..3 *)

 (NEW_GOAL `p' permutes 0..3`);
 (REWRITE_TAC[permutes]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `x''' > 3`);
 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (EXPAND_TAC "p'");
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);

 (NEW_GOAL `(p:num->num) x''' = x'''`);
 (ASM_SIMP_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);

 (ASM_CASES_TAC `y' = 0`);
 (NEW_GOAL `?z. (p:num->num) z = 2`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 2`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 1`);
 (NEW_GOAL `?z. (p:num->num) z = 3`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 3`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 2`);
 (NEW_GOAL `?z. (p:num->num) z = 0`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 0`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `y' = 3`);
 (NEW_GOAL `?z. (p:num->num) z = 1`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p:num->num) y'' = 1`);
 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `y' > 3`);
 (ASM_ARITH_TAC);
 (NEW_GOAL `?z. (p:num->num) z = y'`);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (EXISTS_TAC `z:num`);
 (ASM_REWRITE_TAC[]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `(p:num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (NEW_GOAL `(p':num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (ASM_ARITH_TAC);

 (NEW_GOAL `(p:num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (NEW_GOAL `(p':num->num) z = z`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_ARITH_TAC);
 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (NEW_GOAL `(p:num->num) y'' > 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `(p:num->num) y'' = y''`);
 (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p':num->num) y'' = y''`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (REWRITE_WITH `y'' = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `z = s:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_MESON_TAC[]);


(* finish proving that p' permutes 0..3 *)

 (REWRITE_TAC[ASSUME `p' permutes 0..3`]);

(* --------------------------------------------------------------------- *)

 (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 2
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);
 (ABBREV_TAC `j = inverse (p:num->num) 2`);
 (NEW_GOAL `(p:num->num) j = 2`);
 (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);


 (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 3
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);
 (ABBREV_TAC `j = inverse (p:num->num) 3`);
 (NEW_GOAL `(p:num->num) j = 3`);
 (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_MESON_TAC[]);
 (ASM_MESON_TAC[]);

 (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 0
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);
 (ABBREV_TAC `j = inverse (p:num->num) 0`);
 (NEW_GOAL `(p:num->num) j = 0`);
 (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);


 (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);
 (ASM_REWRITE_TAC[left_action_list; 
   LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
 (REWRITE_WITH  `EL 1
 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3]; 
  EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]] 
 = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);
 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);
 (ABBREV_TAC `j = inverse (p:num->num) 1`);
 (NEW_GOAL `(p:num->num) j = 1`);
 (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);
 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);
 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
 (EXPAND_TAC "p'");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);


(* ======================================================================= *)

 (ONCE_REWRITE_TAC[ASSUME  
   `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list 
 = g (x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`]);
 (REWRITE_TAC[ASSUME
  `x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = e',e'',p,vl`]  
   THEN EXPAND_TAC "g");
 (LET_TAC);
 (REWRITE_TAC[PAIR_EQ]);
 (EXPAND_TAC "p'" THEN REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

(*  --------------------------------------------------- *)
(* It is left to prove only 3 subgoals *)

 (EXPAND_TAC "g");
 (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
 (REWRITE_TAC[FUN_EQ_THM]);
 (GEN_TAC);
 (NEW_GOAL `?e1 e2 p1 vl1. 
   x' = (e1:real^3->bool,e2:real^3->bool,p1:num->num, vl1:(real^3)list)`);
 (EXISTS_TAC `FST  
  (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);
 (EXISTS_TAC `FST (SND
  (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);
 (EXISTS_TAC `FST (SND (SND  
  (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
 (EXISTS_TAC `SND (SND (SND  
  (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
 (REWRITE_TAC[PAIR]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (REWRITE_WITH 
 `(\x. let e',e'',p,vl = x in
       e'', e', (\i. if p i = 0 then 2
                else if p i = 1 then 3
                else if p i = 2 then 0 
                else if p i = 3 then 1 else i),
       [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])
  = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list). 
      e'', e', (\i. if p i = 0 then 2
                else if p i = 1 then 3
                else if p i = 2 then 0 
                else if p i = 3 then 1 else i),
       [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])`);
 (REWRITE_TAC[FUN_EQ_THM]);
 (GEN_TAC);
 (LET_TAC);
 (REWRITE_TAC[BETA_THM]);
 (REWRITE_TAC[o_THM]);
 (REWRITE_WITH 
 `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 2 (vl1:(real^3)list) /\
  EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 3 (vl1:(real^3)list) /\
  EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 0 (vl1:(real^3)list) /\
  EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 1 (vl1:(real^3)list)`);
 (REWRITE_TAC[EL;HD;TL; LENGTH; ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);

 (MATCH_MP_TAC SUM_IMAGE);
 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");
 (ONCE_REWRITE_TAC[IN]);
 (REWRITE_TAC[IN_ELIM_THM]);
 (EXPAND_TAC "g");
 (REPEAT STRIP_TAC);

 (NEW_GOAL `(let e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1 = x' in
       e2,
       e1,
       (\i. if p1 i = 0
            then 2
            else if p1 i = 1
                 then 3
                 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i),
       [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1]) =
      (let f1,f2,p2,vl2 = y' in
       f2,
       f1,
       (\i. if p2 i = 0
            then 2
            else if p2 i = 1
                 then 3
                 else if p2 i = 2 then 0 else if p2 i = 3 then 1 else i),
       [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)])`);
 (ASM_REWRITE_TAC[ETA_AX]);
 (UP_ASM_TAC THEN DEL_TAC THEN REPEAT LET_TAC THEN REWRITE_TAC[PAIR_EQ] THEN 
   REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC);
 (ABBREV_TAC 
  `q = (\i. if p1 i = 0
           then 2
           else if p1 i = 1
                then 3
                else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i)`);

 (NEW_GOAL `!u:num. p1 u = 0 ==> q u = 2`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p1 u = 1 ==> q u = 3`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p1 u = 2 ==> q u = 0`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p1 u = 3 ==> q u = 1`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `!u:num. p1 u > 3 ==> q u = u`);
 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p1 u > 3 ==> p1 u = u`);
 (NEW_GOAL `p1 permutes 0..3`);
 (REWRITE_WITH `p1:num->num = p`);
 (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list = e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);
 (MESON_TAC[]);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p1 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s = (p1:num->num) u`);
 (NEW_GOAL `(p1:num->num) s = s`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (NEW_GOAL `?z. (p1:num->num) z = s /\ (!y'. p1 y' = s ==> y' = z)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `s = z:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u = z:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!u:num. q u = 0 ==> p1 u = 2`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p1:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p1:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 1 ==> p1 u = 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p1:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p1:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 2 ==> p1 u = 0`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p1:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p1:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 3 ==> p1 u = 1`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p1:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p1:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u > 3 ==> p1 u > 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p1:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p1:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);


 (NEW_GOAL `!u:num. p2 u = 0 ==> q u = 2`);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (NEW_GOAL `!u:num. p2 u = 1 ==> q u = 3`);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p2 u = 2 ==> q u = 0`);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p2 u = 3 ==> q u = 1`);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p2 u > 3 ==> q u = u`);
 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (COND_CASES_TAC);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (REFL_TAC);

 (NEW_GOAL `!u:num. p2 u > 3 ==> p2 u = u`);
 (NEW_GOAL `p2 permutes 0..3`);
 (REWRITE_WITH `p2:num->num = p'`);
 (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list = e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);
 (MESON_TAC[]);
 (ASM_REWRITE_TAC[]);
 (UNDISCH_TAC `p2 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
 (REPEAT STRIP_TAC);
 (ABBREV_TAC `s = (p2:num->num) u`);
 (NEW_GOAL `(p2:num->num) s = s`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
 (NEW_GOAL `?z. (p2:num->num) z = s /\ (!y'. p2 y' = s ==> y' = z)`);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN STRIP_TAC);
 (NEW_GOAL `s = z:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `u = z:num`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `!u:num. q u = 0 ==> p2 u = 2`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p2:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p2:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 1 ==> p2 u = 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p2:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p2:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 2 ==> p2 u = 0`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p2:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p2:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u = 3 ==> p2 u = 1`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p2:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u > 3`);
 (NEW_GOAL `(q:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `(p2:num->num) u = u`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (NEW_GOAL `!u:num. q u > 3 ==> p2 u > 3`);
 (REPEAT STRIP_TAC);
 (ASM_CASES_TAC `(p2:num->num) u = 0`);
 (NEW_GOAL `(q:num->num) u = 2`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 1`);
 (NEW_GOAL `(q:num->num) u = 3`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 2`);
 (NEW_GOAL `(q:num->num) u = 0`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_CASES_TAC `(p2:num->num) u = 3`);
 (NEW_GOAL `(q:num->num) u = 1`);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);
 (ASM_ARITH_TAC);

 (ASM_CASES_TAC `(q:num->num) x'' = 0`);
 (NEW_GOAL `(p1:num->num) x'' = 2`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `(p2:num->num) x'' = 2`);
 (ASM_SIMP_TAC[]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `(q:num->num) x'' = 1`);
 (NEW_GOAL `(p1:num->num) x'' = 3`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `(p2:num->num) x'' = 3`);
 (ASM_SIMP_TAC[]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `(q:num->num) x'' = 2`);
 (NEW_GOAL `(p1:num->num) x'' = 0`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `(p2:num->num) x'' = 0`);
 (ASM_SIMP_TAC[]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `(q:num->num) x'' = 3`);
 (NEW_GOAL `(p1:num->num) x'' = 1`);
 (ASM_SIMP_TAC[]);
 (NEW_GOAL `(p2:num->num) x'' = 1`);
 (ASM_SIMP_TAC[]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `(q:num->num) x'' > 3`);
 (ASM_ARITH_TAC);
 (NEW_GOAL `(p1:num->num) x'' > 3`);
 (ASM_SIMP_TAC[]);
 (ASM_SIMP_TAC[]);

 (REWRITE_TAC[Packing3.LIST_EL_EQ]);

(* ------------------------------------------------------------------------- *)

 (REWRITE_WITH `LENGTH (vl1:(real^3)list) = 4`);
 (REWRITE_WITH `(vl1:(real^3)list) = vl`);
 (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list 
   =  e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);
 (MESON_TAC[]);
 (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
 (REWRITE_WITH `LENGTH (vl2:(real^3)list) = 4`);
 (REWRITE_WITH `(vl2:(real^3)list) = vl'`);
 (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list 
   =  e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);
 (MESON_TAC[]);
 (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
 (REPEAT STRIP_TAC);

 (ASM_CASES_TAC `j = 0`);
 (NEW_GOAL `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
             EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
 (AP_TERM_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH 
  `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 0 vl1 /\
   EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 0 vl2`);
 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `j = 1`);
 (NEW_GOAL `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
             EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
 (AP_TERM_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH 
  `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 1 vl1 /\
   EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 1 vl2`);
 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `j = 2`);
 (NEW_GOAL `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
             EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
 (AP_TERM_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH 
  `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 2 vl1 /\
   EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 2 vl2`);
 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (ASM_REWRITE_TAC[]);

 (ASM_CASES_TAC `j = 3`);
 (NEW_GOAL `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
             EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
 (AP_TERM_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_WITH 
  `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 3 vl1 /\
   EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 3 vl2`);
 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `F`);
 (ASM_ARITH_TAC);
 (ASM_MESON_TAC[]);

 (NEW_GOAL `X:real^3->bool = {}`);
 (ASM_MESON_TAC[]);
 (REPEAT STRIP_TAC);
 (REWRITE_WITH `{e | e IN critical_edgeX V X} = {}`);
 (REWRITE_TAC[SET_RULE `{x| x IN s} = s`]);
 (ASM_REWRITE_TAC[critical_edgeX; edgeX]);
 (REWRITE_WITH `VX V {} = {}`);
 (REWRITE_TAC [VX]);
 (COND_CASES_TAC);
 (REFL_TAC);
 (NEW_GOAL `F`);
 (UP_ASM_TAC THEN REWRITE_TAC[NEGLIGIBLE_EMPTY]);
 (ASM_MESON_TAC[]);
 (REWRITE_WITH `{{u:real^3, v:real^3} | {} u /\ {} v /\ ~(u = v)} = 
                 {{u, v} | u IN {} /\ v IN {} /\ ~(u = v)}`);
 (REWRITE_TAC[IN]);
 (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);
 (REWRITE_WITH `{{u:real^3, v:real^3} | F} = {}`);
 (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);
 (GEN_TAC);
 (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);
 (REWRITE_TAC[IN]);
 (SET_TAC[]);
 (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);
 (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);
 (GEN_TAC);
 (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);
 (REWRITE_TAC[IN]);
 (SET_TAC[]);
 (REWRITE_TAC[SUM_CLAUSES])]);;




end;;