(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Uaghhbm = struct



open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;





let PERIODIC_PSORT=
prove(`~(k=0)==>psort (k) (i + k,j) = psort (k) (i,j)/\
psort (k) (i,j+k) = psort (k) (i,j) `,

REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]);;

let CASE_PSORT=
prove(`psort (k) (i,j) = psort (k) (i',j')
==> (i MOD k=i' MOD k/\ j MOD k= j' MOD k)\/(i MOD k=j' MOD k/\ j MOD k= i' MOD k)`,

REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`i' MOD k <= j' MOD k \/ ~(i' MOD k <= j' MOD k)`)
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SET_TAC[]);;
let C_LE_2_IS_SCS=
prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
/\ scs_a_v39 s i j <= c 
==> &2<= c`,

REWRITE_TAC[is_scs_v39;periodic2]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC);;


let C_LT_2_IS_SCS=
prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
/\ scs_a_v39 s i j < c 
==> &2< c`,

REWRITE_TAC[is_scs_v39;periodic2]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC);;


let A_LE_A_OVERRIDE=
prove_by_refinement(
`is_scs_v39 s/\
    scs_a_v39 s i j <= c 
==> scs_a_v39 s i' j' <= override (scs_a_v39 s) (scs_k_v39 s) (i,j) c i' j' `,

[

ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

REAL_ARITH_TAC;

REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;






let B_OVERRIDE_LE_B=
prove_by_refinement(
`is_scs_v39 s/\
  c <= scs_b_v39 s i j 
==> override (scs_b_v39 s) (scs_k_v39 s) (i,j) c i' j' <= scs_b_v39 s i' j'`,

[
ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

REAL_ARITH_TAC;

REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;


let BB_EQ_UNION_BB_SUBDIVISION=
prove_by_refinement(`
    is_scs_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j 
==> 
BBs_v39 s = BBs_v39 (restriction_cs1_v39 s i j c) UNION BBs_v39 (restriction_cs2_v39 s i j c)`,

[
REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;restriction_cs1_v39;restriction_cs2_v39]
THEN EQ_TAC;

RESA_TAC;

ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
THEN MP_TAC(SET_RULE`(!i' j'.
      dist ((x:num->real^3) i',x j') <=
      (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/ 
~(!i' j'.
      dist (x i',x j') <=
      (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM]
THEN RESA_TAC;



POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;



REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j'') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j''))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC
;


MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;





ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
THEN MP_TAC(SET_RULE`(!i' j'.
      dist ((x:num->real^3) i',x j') <=
      (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/ 
~(!i' j'.
      dist (x i',x j') <=
      (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM]
THEN RESA_TAC;



POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j'') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j''))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC
;


MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

RESA_TAC;

REPEAT GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
THEN MP_TAC B_OVERRIDE_LE_B
THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN RESA_TAC)
THEN REAL_ARITH_TAC;

REPEAT GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
THEN MP_TAC B_OVERRIDE_LE_B
THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN RESA_TAC)
THEN REAL_ARITH_TAC;

REPEAT GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
THEN REMOVE_ASSUM_TAC
THEN MP_TAC A_LE_A_OVERRIDE
THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN RESA_TAC)
THEN REAL_ARITH_TAC
;
REPEAT GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
THEN REMOVE_ASSUM_TAC
THEN MP_TAC A_LE_A_OVERRIDE
THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN RESA_TAC)
THEN REAL_ARITH_TAC;
]);;

let SUBDIVISION_IS_NOT_EAR=
prove(`3< scs_k_v39 s 
==>
~(is_ear_v39 s)/\ ~(is_ear_v39 (restriction_cs1_v39 s i j c)) /\ ~(is_ear_v39 (restriction_cs2_v39 s i j c))`,

REWRITE_TAC[is_scs_v39;is_ear_v39;restriction_cs1_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;unadorned_v39;restriction_cs2_v39]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s =3)`)
THEN RESA_TAC);;


let SUBDIVISION_CS1_DSV_EQ=
prove(`
   3< scs_k_v39 s
==> 
dsv_v39 (restriction_cs1_v39 s i j c) ww =dsv_v39 s ww
/\ dsv_v39 (restriction_cs2_v39 s i j c) ww =dsv_v39 s ww`,

STRIP_TAC
THEN MP_TAC SUBDIVISION_IS_NOT_EAR
THEN RESA_TAC
THEN ASM_REWRITE_TAC[dsv_v39]
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;dsv_v39;restriction_cs1_v39;restriction_cs2_v39]);;

let SUBDIVISION_CS1_TAUSTAR_EQ=
prove(`
   3< scs_k_v39 s
==> 
taustar_v39 (restriction_cs1_v39 s i j c) ww =taustar_v39 s ww /\
taustar_v39 (restriction_cs2_v39 s i j c) ww =taustar_v39 s ww`,

STRIP_TAC
THEN MP_TAC SUBDIVISION_CS1_DSV_EQ
THEN RESA_TAC
THEN ASM_REWRITE_TAC[taustar_v39]
THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s <=3)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;taustar_v39;restriction_cs1_v39;restriction_cs2_v39]);;


let BBPRIME_SUBSET_SUBDIVISION_UNION=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww
==> 
 ww IN BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> STRIP_TAC
THEN MRESAL1_TAC th`ww:num->real^3`[IN]
THEN ASSUME_TAC(th));

MATCH_MP_TAC(SET_RULE`A==> A\/B`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESAL1_TAC th`ww':num->real^3`[IN])
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[];

MATCH_MP_TAC(SET_RULE`A==> B\/A`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN GEN_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESAL1_TAC th`ww':num->real^3`[IN])
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]]);;


let BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION = 
prove(
`is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j 
 ==>   BBprime_v39 s SUBSET BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,

REWRITE_TAC[SUBSET]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC  BBPRIME_SUBSET_SUBDIVISION_UNION
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]);;

(**********c< norm(ww i- ww j)*********)

let BBINDEX_EQ_SUBDIVISION=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBs_v39 s ww /\ c< norm(ww i- ww j)
==> 
BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\i:num. i)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;

STRIP_TAC;

REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;

REPEAT RESA_TAC;

REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (35-28)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;]);;

let BB_INTER_BBPRIME_SUBDIVISION2= 
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j 
==> 
(BBprime_v39 s) INTER (BBs_v39 (restriction_cs2_v39 s i j c)) SUBSET
(BBprime_v39 (restriction_cs2_v39 s i j c))`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM;SUBSET]
THEN GEN_TAC;

REWRITE_TAC[SUBSET;UNION;IN_ELIM_THM;]
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;BBprime_v39;IN]
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC;

REPLICATE_TAC (11-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (13-5)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[];

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`];

REPLICATE_TAC (10-6)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (14-7)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[];

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;



let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION= 
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
BBs_v39 (restriction_cs2_v39 s i j c) ww`,

[
REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC]);;
let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
(BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s)  `,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;IN]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww:num->real^3`)
THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww:num->real^3`)
THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;


let IN_BBPRIME_SUBDIVISION=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
BBprime_v39 (restriction_cs2_v39 s i j c) ww`,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[BBprime_v39]
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`);

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC]);;


let MIN_NUM_SUBSET=
prove(
`X SUBSET Y/\ a IN X==> min_num Y<= min_num X`,

REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`X:num->bool`;`a:num`]
THEN MP_TAC(SET_RULE`X (min_num X) /\ X SUBSET Y==> Y (min_num X)`)
THEN RESA_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`Y:num->bool`;`min_num X`]);;

let BBINDEX_MIN_S_LE_SUBDIVISION2=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
BBindex_min_v39 s <= min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,

[
STRIP_TAC
THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
THEN RESA_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
THEN EXISTS_TAC`BBindex_v39 s ww`
THEN STRIP_TAC;

MATCH_MP_TAC IMAGE_SUBSET
THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME
THEN RESA_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`ww:num->real^3`
THEN REWRITE_TAC[IN]
THEN MP_TAC IN_BBPRIME_SUBDIVISION
THEN RESA_TAC]);;

let BBINDEX_BBPRIME_LE_SUBDIVISION2=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ c< norm(ww i- ww j)/\
   BBprime_v39 (restriction_cs2_v39 s i j c) vv
==> 
 BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,

[

STRIP_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;



MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (40-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;




MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;






MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;




MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;







MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;




MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;



MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;




MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;




]);;

let MIN_NUM_LE_IMAGE=
prove_by_refinement(`
(a:A) IN s/\ (!x. x IN s==> f x <= g x) ==> min_num (IMAGE f s)<= min_num (IMAGE g s)`,

[
STRIP_TAC
THEN SUBGOAL_THEN `g (a:A) IN ((IMAGE g s):num->bool)`ASSUME_TAC;

ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`a:A`
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE g (s:A->bool)):num->bool`;`(g (a:A)):num`]
THEN SUBGOAL_THEN`(min_num (IMAGE g s)) IN IMAGE g (s:A->bool)`ASSUME_TAC;

ASM_REWRITE_TAC[IN];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN STRIP_TAC
THEN REPLICATE_TAC (6-1)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`x:A`)
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN `f (x:A) IN ((IMAGE f s):num->bool)`ASSUME_TAC;

ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`x:A`
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE f (s:A->bool)):num->bool`;`(f:A->num) (x:A)`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IMAGE;IN]
THEN ARITH_TAC]);;

let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2=
prove(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs2_v39 s i j c)))
<= min_num
 (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
THEN EXISTS_TAC`ww:num->real^3`
THEN MP_TAC IN_BBPRIME_SUBDIVISION
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2
THEN ASM_REWRITE_TAC[]);;

let BBindex_min_LE_SUBDIVISION2=
prove(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ c< norm(ww i- ww j)
==> 
BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,

STRIP_TAC
THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2
THEN RESA_TAC
THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2
THEN RESA_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REWRITE_TAC[BBindex_min_v39]
THEN ARITH_TAC);;

let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    MMs_v39 s ww /\ c< norm(ww i- ww j)
==> 
 ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC;

REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
THEN MP_TAC IN_BBPRIME_SUBDIVISION
THEN RESA_TAC
THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;

ASM_TAC
THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;

MP_TAC BBINDEX_EQ_SUBDIVISION
THEN RESA_TAC
THEN MP_TAC BBindex_min_LE_SUBDIVISION2
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
      (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[IN];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC]);;


let MM_IS_NOT_2EMPTY_SUBDIVISION=
prove_by_refinement(`
   is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
scs_am_v39 s i j < c/\
    MMs_v39 s ww /\ c< norm(ww i- ww j)
==> 
 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[override]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];


ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;


REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;


REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;


REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC;

REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN REWRITE_TAC[dist]
THEN REAL_ARITH_TAC]);;


let MM_IS_NOT_1EMPTY_SUBDIVISION=
prove_by_refinement(
`
   is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
c<= scs_am_v39 s i j /\
    MMs_v39 s ww /\ c< norm(ww i- ww j)
==> 
 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,

[STRIP_TAC
THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[override]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`c<= scs_am_v39 s i j==> ~(scs_am_v39 s i j<c)`)
THEN RESA_TAC]);;


(********************************)



let BBINDEX_EQ_SUBDIVISION1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBs_v39 s ww /\ dist(ww i,ww j) <= c
==> 
BBindex_v39 s ww = BBindex_v39 (restriction_cs1_v39 s i j c) ww`,

[STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC]);;

let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1= 
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
BBs_v39 (restriction_cs1_v39 s i j c) ww`,

[
REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs1_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC]);;



let IN_BBPRIME_SUBDIVISION1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
BBprime_v39 (restriction_cs1_v39 s i j c) ww`,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[BBprime_v39]
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`);

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC]);;




let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
(BBprime_v39 (restriction_cs1_v39 s i j c)) SUBSET (BBprime_v39 s)  `,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;IN]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;


MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (36-30)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`);


MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww:num->real^3`)
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;




let BBINDEX_MIN_S_LE_SUBDIVISION1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
BBindex_min_v39 s <= min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs1_v39 s i j c)))`,

[
STRIP_TAC
THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
THEN RESA_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
THEN EXISTS_TAC`BBindex_v39 s ww`
THEN STRIP_TAC;

MATCH_MP_TAC IMAGE_SUBSET
THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1
THEN RESA_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`ww:num->real^3`
THEN REWRITE_TAC[IN]
THEN MP_TAC IN_BBPRIME_SUBDIVISION1
THEN RESA_TAC;]);;





let BBINDEX_BBPRIME_LE_SUBDIVISION1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) <= c/\
   BBprime_v39 (restriction_cs1_v39 s i j c) vv
==> 
 BBindex_v39 s vv= BBindex_v39 (restriction_cs1_v39 s i j c) vv`,

[STRIP_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39;IN;BBs_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC]);;



let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1=
prove(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs1_v39 s i j c)))
<= min_num
 (IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
 (BBprime_v39 (restriction_cs1_v39 s i j c)))`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
THEN EXISTS_TAC`ww:num->real^3`
THEN MP_TAC IN_BBPRIME_SUBDIVISION1
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL BBINDEX_BBPRIME_LE_SUBDIVISION1)[`ww:num->real^3`;`s:scs_v39`;`i:num`;`j:num`;`c:real`;`x:num->real^3`]
THEN ARITH_TAC);;


let BBindex_min_LE_SUBDIVISION1=
prove(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) <= c
==> 
BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs1_v39 s i j c)`,

STRIP_TAC
THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1
THEN RESA_TAC
THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION1
THEN RESA_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REWRITE_TAC[BBindex_min_v39]
THEN ARITH_TAC);;


let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    MMs_v39 s ww /\ dist(ww i,ww j) <= c
==> 
 ww IN BBprime2_v39 (restriction_cs1_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC;

REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
THEN MP_TAC IN_BBPRIME_SUBDIVISION1
THEN RESA_TAC
THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;

ASM_TAC
THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;

MP_TAC BBINDEX_EQ_SUBDIVISION1
THEN RESA_TAC
THEN MP_TAC BBindex_min_LE_SUBDIVISION1
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs1_v39 s i j c) ww)
IN IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
      (BBprime_v39 (restriction_cs1_v39 s i j c))`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[IN];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c)) (BBprime_v39 (restriction_cs1_v39 s i j c))`;`BBindex_v39 (restriction_cs1_v39 s i j c) ww`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC]);;



let MM_IS_NOT_2EMPTY_SUBDIVISION1=
prove_by_refinement(
`
   is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
c < scs_bm_v39 s i j/\
    MMs_v39 s ww /\ dist(ww i,ww j) <= c
==> 
 ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,

[STRIP_TAC
THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[override]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];


ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;


REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;



REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;


REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;

REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;

REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;
]);;

let MM_IS_NOT_1EMPTY_SUBDIVISION1=
prove_by_refinement(
`
   is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 scs_bm_v39 s i j <=c /\
    MMs_v39 s ww /\ dist(ww i,ww j) <= c
==> 
 ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,

[STRIP_TAC
THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[override]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c==> ~(c< scs_bm_v39 s i j)`)
THEN RESA_TAC]);;



let BBINDEX_EQ_SUBDIVISION_C_EQ_AM=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
    BBs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c
==> 
BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;

MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\i:num. i)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;

STRIP_TAC;

REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`i:num`;`k:num`][];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`j:num`;`k:num`][];

REPEAT RESA_TAC;

REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`][];

ASM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`][]]);;


let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM= 
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
==> 
BBs_v39 (restriction_cs2_v39 s i j c) ww`,

[
REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN REPEAT RESA_TAC;

REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
THEN REAL_ARITH_TAC;

MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]);;



let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
==> 
(BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s)  `,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;IN]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww:num->real^3`)
THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww:num->real^3`)
THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;



let IN_BBPRIME_SUBDIVISION_C_EQ_AM=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
BBprime_v39 s ww  /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
==> 
BBprime_v39 (restriction_cs2_v39 s i j c) ww`,

[
STRIP_TAC
THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[BBprime_v39]
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th -> STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`)
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`ww':num->real^3`);

MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
THEN REPEAT RESA_TAC]);;



let BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
==> 
BBindex_min_v39 s <= min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,

[
STRIP_TAC
THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
THEN RESA_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
THEN EXISTS_TAC`BBindex_v39 s ww`
THEN STRIP_TAC;

MATCH_MP_TAC IMAGE_SUBSET
THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM
THEN RESA_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`ww:num->real^3`
THEN REWRITE_TAC[IN]
THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
THEN RESA_TAC]);;




let BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=
prove_by_refinement(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
   BBprime_v39 (restriction_cs2_v39 s i j c) vv
==> 
 BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,

[

STRIP_TAC
THEN REWRITE_TAC[BBindex_v39]
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC;




MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;



MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (42-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;





MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;







MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;



MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;





MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;








MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;



MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;





MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;




MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC;



MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`x:num`;`SUC x`])
THEN REMOVE_ASSUM_TAC
THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
THEN REAL_ARITH_TAC;





MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;
]);;





let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=
prove(
`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) 
==> 
min_num
 (IMAGE (BBindex_v39 s)
 (BBprime_v39 (restriction_cs2_v39 s i j c)))
<= min_num
 (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
THEN EXISTS_TAC`ww:num->real^3`
THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
THEN ASM_REWRITE_TAC[]);;


let BBindex_min_LE_SUBDIVISION2_C_EQ_AM=
prove(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) 
==> 
BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,

STRIP_TAC
THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
THEN RESA_TAC
THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM
THEN RESA_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REWRITE_TAC[BBindex_min_v39]
THEN ARITH_TAC);;



let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=
prove_by_refinement(`
    is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) 
==> 
 ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
THEN RESA_TAC
THEN ASM_TAC
THEN 
REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN ASM_TAC
THEN REPEAT RESA_TAC;

REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;

ASM_TAC
THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC;

MP_TAC BBINDEX_EQ_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN MP_TAC BBindex_min_LE_SUBDIVISION2_C_EQ_AM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[BBindex_min_v39]
THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
      (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[IN];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC]);;



let MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=
prove_by_refinement(
`
   is_scs_v39 s /\    3< scs_k_v39 s /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
    MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) 
==> 
 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,

[
STRIP_TAC
THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
THEN REPEAT RESA_TAC
THEN REWRITE_TAC[override;REAL_ARITH`~(c<c)`]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC]);;



let UAGHHBM=
prove_by_refinement(
`!s i j c .
    is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)/\
    ~(scs_J_v39 s i j) /\
    scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j/\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (&2 < scs_a_v39 s i j \/ &2 * h0 < scs_b_v39 s i j))
/\ 3< scs_k_v39 s  /\
((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) 
==>
    scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))`,

[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;subdiv_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC
;



POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
THEN RESA_TAC;


ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
THEN RESA_TAC;



MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
THEN RESA_TAC;


ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN REPEAT RESA_TAC;




REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];



MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
THEN RESA_TAC
;


MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;



MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
THEN RESA_TAC
;


MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC
;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);




MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
THEN RESA_TAC
;



MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
THEN RESA_TAC;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);



MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


MP_TAC C_LE_2_IS_SCS
THEN REWRITE_TAC[is_scs_v39]
THEN ASM_TAC
THEN REPEAT RESA_TAC
;




REPLICATE_TAC (33-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;



STRIP_TAC
THEN REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;



REPLICATE_TAC (30-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;




SUBGOAL_THEN`CARD
 {i' | i' < k /\
       (&2 * h0 < scs_b_v39 s i' (SUC i') \/
        &2 <
        (if psort k (i,j) = psort k (i',SUC i')
         then c
         else scs_a_v39 s i' (SUC i')))}
= CARD
      {i | i < k /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
ASSUME_TAC;



MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\i:num. i)`
THEN STRIP_TAC;



MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;


STRIP_TAC;


REPEAT RESA_TAC
;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC
;



MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
THEN RESA_TAC
THEN MP_TAC C_LT_2_IS_SCS
THEN REWRITE_TAC[is_scs_v39]
THEN ASM_TAC
THEN REPEAT RESA_TAC
;




REPEAT RESA_TAC
;


REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC
;



REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
THEN RESA_TAC
;





MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
THEN STRIP_TAC
THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN RESA_TAC)
;



ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;





ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;




POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
THEN STRIP_TAC
THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN RESA_TAC)
;



ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;





ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;


REPEAT RESA_TAC
;



ASM_REWRITE_TAC[]
;



(**********c < scs_bm_v39 s i j *******)

MP_TAC(SET_RULE`c < scs_bm_v39 s i j \/ ~(c < scs_bm_v39 s i j)`)
THEN RESA_TAC;



ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
THEN RESA_TAC;


(**********restriction_cs1_v39 s i j c *******)



ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN REPEAT RESA_TAC;



REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];





REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];




REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;



MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;



REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j) ==>  scs_am_v39 s i j<= c`)
THEN RESA_TAC
;


ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;




ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;



REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


REAL_ARITH_TAC
;



POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
THEN REPLICATE_TAC (34-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;




REPLICATE_TAC (32-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
;




MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
THEN REPLICATE_TAC (34-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;


REPLICATE_TAC (32-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
;




REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC
;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;




REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;




SUBGOAL_THEN`CARD
 {i' | i' < k /\
       (&2 * h0 <
        (if psort k (i,j) = psort k (i',SUC i')
         then c
         else scs_b_v39 s i' (SUC i')) \/
        &2 < scs_a_v39 s i' (SUC i'))}
<= CARD
 {i' | i' < k /\
       (&2 * h0 <
        (scs_b_v39 s i' (SUC i')) \/
        &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
;





MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN STRIP_TAC;



REPEAT RESA_TAC
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
THEN RESA_TAC
;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (34-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;


RESA_TAC;



MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;



REPLICATE_TAC (31-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC
;



(**********restriction_cs2_v39 s i j c *******)


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN REPEAT RESA_TAC;




REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];






MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
THEN RESA_TAC
;





REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];




MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;



MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
THEN RESA_TAC
;



REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;



MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
THEN RESA_TAC
THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC
;


REAL_ARITH_TAC;



MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
THEN RESA_TAC
THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;





MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j ==> c <= scs_bm_v39 s i j`)
THEN RESA_TAC;





MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
THEN RESA_TAC;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);



MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


MP_TAC C_LE_2_IS_SCS
THEN REWRITE_TAC[is_scs_v39]
THEN ASM_TAC
THEN REPEAT RESA_TAC
;




REPLICATE_TAC (34-15)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;



STRIP_TAC
THEN REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;



REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;




SUBGOAL_THEN`CARD
 {i' | i' < k /\
       (&2 * h0 < scs_b_v39 s i' (SUC i') \/
        &2 <
        (if psort k (i,j) = psort k (i',SUC i')
         then c
         else scs_a_v39 s i' (SUC i')))}
= CARD
      {i | i < k /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
ASSUME_TAC;



MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`(\i:num. i)`
THEN STRIP_TAC;



MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;


STRIP_TAC;


REPEAT RESA_TAC
;


MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
THEN RESA_TAC
;



MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
THEN RESA_TAC
THEN MP_TAC C_LT_2_IS_SCS
THEN REWRITE_TAC[is_scs_v39]
THEN ASM_TAC
THEN REPEAT RESA_TAC
;




REPEAT RESA_TAC
;


REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN REPEAT RESA_TAC
;



REWRITE_TAC[EXISTS_UNIQUE]
THEN EXISTS_TAC`y:num`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
THEN RESA_TAC
;





MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
THEN STRIP_TAC
THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN RESA_TAC)
;



ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;





ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;




POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MP_TAC th)
THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
THEN STRIP_TAC
THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN RESA_TAC)
;



ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;





ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;


REPEAT RESA_TAC
;



ASM_REWRITE_TAC[]
;



(**********restriction_cs1_v39 s i j c *******)

MP_TAC(SET_RULE`c < scs_b_v39 s i j \/ ~(c < scs_b_v39 s i j)`)
THEN RESA_TAC;



ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN REPEAT RESA_TAC;



REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN REPEAT GEN_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
;


POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN ASM_REWRITE_TAC[];







 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
;





REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC;


MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN MP_TAC(REAL_ARITH`~(c < scs_bm_v39 s i j) ==>  scs_bm_v39 s i j<= c`)
THEN RESA_TAC
;


ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;




ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;




POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
THEN REPLICATE_TAC (35-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;




REPLICATE_TAC (33-16)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
;




MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
THEN RESA_TAC;




MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
THEN REPLICATE_TAC (35-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;


REPLICATE_TAC (33-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`i':num`)
;




REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC
;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
;




REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`i':num`;`j':num`])
;




SUBGOAL_THEN`CARD
 {i' | i' < k /\
       (&2 * h0 <
        (if psort k (i,j) = psort k (i',SUC i')
         then c
         else scs_b_v39 s i' (SUC i')) \/
        &2 < scs_a_v39 s i' (SUC i'))}
<= CARD
 {i' | i' < k /\
       (&2 * h0 <
        (scs_b_v39 s i' (SUC i')) \/
        &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
;





MATCH_MP_TAC CARD_SUBSET
THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
THEN STRIP_TAC;



REPEAT RESA_TAC
;


POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
THEN RESA_TAC
;



MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
THEN REAL_ARITH_TAC;


RESA_TAC;



MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`0..k`
THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;



REPLICATE_TAC (32-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC
;



ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
THEN RESA_TAC
;



DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);


ASM_REWRITE_TAC[]
;



ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?ww. A ww`;]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
THEN RESA_TAC;



ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;IN]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[];



MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
THEN RESA_TAC;


SUBGOAL_THEN`c<= norm(ww i- (ww:num->real^3) j)` ASSUME_TAC;




ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (22-19)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC
;





MP_TAC(REAL_ARITH`c <= norm ((ww:num->real^3) i - ww j)==> c = norm (ww i - ww j)\/ c < norm (ww i - ww j)`)
THEN RESA_TAC;



SUBGOAL_THEN`c=scs_am_v39 s i j` ASSUME_TAC
;




ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (25-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
THEN REPLICATE_TAC (1)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN REWRITE_TAC[th])
THEN REAL_ARITH_TAC;




REPLICATE_TAC (15-8)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th)
THEN RESA_TAC
THEN STRIP_TAC
THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[dist;]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[];






ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION
THEN RESA_TAC;






MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==>  scs_am_v39 s i j<c`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j \/ scs_bm_v39 s i j <=c`)
THEN RESA_TAC
;




ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
THEN MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
THEN RESA_TAC;






EXISTS_TAC`restriction_cs2_v39 s i j c`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION
THEN RESA_TAC;



EXISTS_TAC`restriction_cs1_v39 s i j c`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION1
THEN ASM_REWRITE_TAC[dist]
;




MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c ==> ~(c<scs_bm_v39 s i j)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`c < scs_b_v39 s i j \/ scs_b_v39 s i j<= c`)
THEN RESA_TAC;




MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
THEN RESA_TAC;





ASM_TAC
THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (28-21)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
THEN REPLICATE_TAC (28-23)(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;









MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION1
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[dist]
THEN STRIP_TAC
THEN EXISTS_TAC`restriction_cs1_v39 s i j c`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
;



MP_TAC(REAL_ARITH`scs_b_v39 s i j <= c==> ~(c< scs_b_v39 s i j )`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. A ww`;]
THEN EXISTS_TAC`ww:num->real^3`
THEN ASM_REWRITE_TAC[]
 ;


]);;









 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)