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


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


module Wkeidft = 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;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;
open Fektyiy;;




let SUR_MOD_FUN=
prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,

STRIP_TAC
THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
THEN RESA_TAC
THENL[
EXISTS_TAC`p' MOD k- p MOD k`
THEN MRESA_TAC DIVISION[`p'`;`k`]
THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
THEN RESA_TAC
THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);

EXISTS_TAC`p' MOD k +k - p MOD k`
THEN MRESA_TAC DIVISION[`p`;`k`]
THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
THEN RESA_TAC
THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;


let TRANS_DIAG=
prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
==> (i+q) MOD k= q' MOD k `,

STRIP_TAC
THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
THEN EXISTS_TAC`p:num`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;


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


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



let scs_components = 
prove_by_refinement(
  `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
                         scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
  REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
  REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
  REWRITE_TAC[scs_str_v39];

BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
  ]);;
  (* }}} *)


let scs_inj = 
prove_by_refinement(
  `!s s'. scs_basic_v39 s /\  scs_basic_v39 s' /\
    scs_d_v39 s = scs_d_v39 s' /\
    scs_k_v39 s = scs_k_v39 s' /\
    (scs_a_v39 s = scs_a_v39 s') /\
    (scs_b_v39 s = scs_b_v39 s')
  ==> (s = s')`,


  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
  REWRITE_TAC[scs_basic;unadorned_v39];
  ONCE_REWRITE_TAC[EQ_SYM_EQ];
  REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
  REPEAT WEAKER_STRIP_TAC;
  ONCE_REWRITE_TAC[GSYM scs_v39];
  AP_TERM_TAC;
  ASM_REWRITE_TAC[scs_components];
  TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
    BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)




let DIAG_PSORT1=
prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
==>  (psort k (i+i',i+j) = psort k (p',q'))`,


[
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC TRANS_DIAG
THEN RESA_TAC
THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];


MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;






let DIAG_PSORT2=
prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
==> 
(psort k (i',j) = psort k (p,q))`,

[
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC TRANS_DIAG
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];

MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
THEN RESA_TAC;


MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];

MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
THEN RESA_TAC;

MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;





let DIAG_PSORT=
prove(
 ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\ 
p' + q = p + q' /\ ~(k=0) 
==>
((psort k (i+i',i+j) = psort k (p',q'))
<=> 
(psort k (i',j) = psort k (p,q)))`,

STRIP_TAC
THEN EQ_TAC
THEN STRIP_TAC
THENL[
MATCH_MP_TAC DIAG_PSORT2
THEN RESA_TAC;
MATCH_MP_TAC DIAG_PSORT1
THEN RESA_TAC]);;


let TRANS_DIAG=
prove(`
~(k=0)
==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,

SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;



let A_EQ_PSORT=
prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
==> scs_a_v39 s i j= scs_a_v39 s p q`,

REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
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`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC
THEN 
REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC);;



let B_EQ_PSORT=
prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
==> scs_b_v39 s i j= scs_b_v39 s p q`,

REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
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`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
THEN RESA_TAC
THEN 
REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC);;


let PROPERTY_OF_K_SCS=
prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,

STRIP_TAC
THEN MP_TAC Axjrpnc.is_scs_k_le_3
THEN RESA_TAC 
THEN DICH_TAC 0
THEN ARITH_TAC);;

let WKEIDFT_A_concl = `!s s' a b a' b' p q p' q' i.
  (let k = scs_k_v39 s in
     (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
       (!i. scs_a_v39 s i (i + 1) = a) /\
       (!i. scs_b_v39 s i (i + 1) = b) /\
       (!i. scs_a_v39 s' i (i + 1) = a) /\
       (!i. scs_b_v39 s' i (i + 1) = b) /\
       scs_k_v39 s' = k /\
       p' + q = p + q' /\
       scs_d_v39 s = scs_d_v39 s' /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
	 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
(\j j'. scs_a_v39 s' (i + j) (i + j')) = scs_a_v39 s))`;;




let WKEIDFT_A=prove_by_refinement( WKEIDFT_A_concl,
[
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
THEN RESA_TAC;

MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC A_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
THEN MRESA_TAC A_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] 
THEN MATCH_DICH_TAC (26-13)
THEN ASM_REWRITE_TAC[];


POP_ASSUM MP_TAC
THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
THEN STRIP_TAC;

MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC;

MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
THEN REWRITE_TAC[ADD1]
THEN THAYTHEL_TAC(26-6)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
THEN THAYTHE_TAC(26-4)[`x`];


MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
THEN REWRITE_TAC[ADD1]
THEN THAYTHEL_TAC(26-6)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
THEN THAYTHE_TAC(26-4)[`x'`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC]);;





let WKEIDFT_B_concl = `!s s' a b a' b' p q p' q' a1 i.
  (let k = scs_k_v39 s in
     (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
       (!i. scs_b_v39 s i i = a1) /\
       (!i. scs_b_v39 s' i i = a1) /\
       (!i. scs_a_v39 s i (i + 1) = a) /\
       (!i. scs_b_v39 s i (i + 1) = b) /\
       (!i. scs_a_v39 s' i (i + 1) = a) /\
       (!i. scs_b_v39 s' i (i + 1) = b) /\
       scs_k_v39 s' = k /\
       p' + q = p + q' /\
       scs_d_v39 s = scs_d_v39 s' /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
	 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
(\j j'. scs_b_v39 s' (i + j) (i + j')) = scs_b_v39 s))`;;




let WKEIDFT_B=prove_by_refinement( WKEIDFT_B_concl,
[
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
THEN RESA_TAC;

MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] 
THEN MATCH_DICH_TAC (26-14)
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
THEN STRIP_TAC;

MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC;

MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
THEN REWRITE_TAC[ADD1]
THEN THAYTHEL_TAC(26-7)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
THEN THAYTHE_TAC(26-5)[`x`];

MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
THEN REWRITE_TAC[ADD1]
THEN THAYTHEL_TAC(26-7)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
THEN THAYTHE_TAC(26-5)[`x'`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC]);;





let WKEIDFT_EQU_concl = `
  (let k = scs_k_v39 s in
     (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
       (!i. scs_b_v39 s i i = a1) /\
       (!i. scs_b_v39 s' i i = a1) /\
       (!i. scs_a_v39 s i (i + 1) = a) /\
       (!i. scs_b_v39 s i (i + 1) = b) /\
       (!i. scs_a_v39 s' i (i + 1) = a) /\
       (!i. scs_b_v39 s' i (i + 1) = b) /\
       scs_k_v39 s' = k /\
       p' + q = p + q' /\
       scs_d_v39 s = scs_d_v39 s' /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
	 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q'  ==>
   ?i.  s'= scs_prop_equ_v39 s i))`;;






let WKEIDFT_EQU=prove( WKEIDFT_EQU_concl,
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN MRESAL_TAC WKEIDFT_B[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`a1:real`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN MRESAL_TAC WKEIDFT_A[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN MATCH_MP_TAC scs_inj
THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN SET_TAC[]);;

let WKEIDFT_concl = `!s s' a b a' b' p q p' q'.
  (let k = scs_k_v39 s in
     (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
       (!i. scs_b_v39 s i i = a1) /\
       (!i. scs_b_v39 s' i i = a1) /\
       (!i. scs_a_v39 s i (i + 1) = a) /\
       (!i. scs_b_v39 s i (i + 1) = b) /\
       (!i. scs_a_v39 s' i (i + 1) = a) /\
       (!i. scs_b_v39 s' i (i + 1) = b) /\
       scs_k_v39 s' = k /\
       p' + q = p + q' /\
       scs_d_v39 s = scs_d_v39 s' /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
       (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
	 scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' ==>
     scs_arrow_v39 {s} {s'}))`;;




let WKEIDFT_PRIME= prove(WKEIDFT_concl,
REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN MP_TAC WKEIDFT_EQU
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN RESA_TAC
THEN MATCH_MP_TAC YXIONXL3
THEN ASM_REWRITE_TAC[]);;



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

let WKEIDFT_B_v2_concl = `!s a b a' b' p q p' q'.
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\ scs_basic_v39 s /\ 
	  (!i. scs_a_v39 s i (i + 1) = a) /\
	  (!i. scs_b_v39 s i (i + 1) = b) /\
	   p' + q = p + q' /\
         scs_diag k p q/\
         scs_diag k p' q'/\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
	   (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
	   (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
	  (!i. scs_b_v39 s i i = b1) /\
 (i+p) MOD k = p' MOD k ==>
(\j j'. scs_b_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_b_v39 (scs_stab_diag_v39 s p q)))`;;



let WKEIDFT_B_V2=prove_by_refinement( WKEIDFT_B_v2_concl,
[
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`;

MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
THEN RESA_TAC;

MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] ;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
THEN STRIP_TAC;

MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`];

MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];


MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
THEN RESA_TAC
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC]);;






let WKEIDFT_A_v2_concl = `!s a b a' b' p q p' q'.
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\ scs_basic_v39 s /\ 
	  (!i. scs_a_v39 s i (i + 1) = a) /\
	  (!i. scs_b_v39 s i (i + 1) = b) /\
	   p' + q = p + q' /\
         scs_diag k p q/\
         scs_diag k p' q'/\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
	   (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
	   (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
	  (!i. scs_b_v39 s i i = b1) /\
 (i+p) MOD k = p' MOD k ==>
(\j j'. scs_a_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_a_v39 (scs_stab_diag_v39 s p q)))`;;



let WKEIDFT_A_V2=prove_by_refinement( WKEIDFT_A_v2_concl,
[
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`;

MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
THEN RESA_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESAS_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`][];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
THEN STRIP_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC;

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];

MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC]);;



let SCS_K_D_A_STAB_EQ=
prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
/\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
/\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,




let WKEIDFT_EQU_v2_concl = `
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\ scs_basic_v39 s /\ 
	  (!i. scs_a_v39 s i (i + 1) = a) /\
	  (!i. scs_b_v39 s i (i + 1) = b) /\
	   p' + q = p + q' /\
         scs_diag k p q/\
         scs_diag k p' q'/\
    3 < k /\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
	   (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
	   (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
	  (!i. scs_b_v39 s i i = b1) ==>
?i.  scs_stab_diag_v39 s p' q'= scs_prop_equ_v39 (scs_stab_diag_v39 s p q) i))`;;



let WKEIDFT_EQU_V2= prove(WKEIDFT_EQU_v2_concl,
REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
THEN REPEAT RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MP_TAC PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
THEN ASM_TAC
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN MRESAL_TAC WKEIDFT_B_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN MRESAL_TAC WKEIDFT_A_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
THEN DICH_TAC 1
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN DICH_TAC 1
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN MATCH_MP_TAC scs_inj
THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p'`;`q'`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
THEN ASM_SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
THEN SET_TAC[]);;

let WKEIDFT_concl = `!s a b a' b' p q p' q'.
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\ scs_basic_v39 s /\ 
	  (!i. scs_a_v39 s i (i + 1) = a) /\
	  (!i. scs_b_v39 s i (i + 1) = b) /\
	   p' + q = p + q' /\
         scs_diag k p q/\
         scs_diag k p' q'/\
    3 < k /\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
	   (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
	   (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
	  (!i. scs_b_v39 s i i = b1) ==>
scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;;



let WKEIDFT=prove(WKEIDFT_concl,
REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN MP_TAC WKEIDFT_EQU_V2
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN RESA_TAC
THEN MATCH_MP_TAC YXIONXL3
THEN ASM_REWRITE_TAC[]
THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]);;






 end;;


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