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


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


module Uxckfpe = 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_lemmas;;
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;;


let NOT_EMPTY_CASE_4_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv 
/\  dimindex(:M)= scs_k_v39 s
==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,

[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
THEN STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
THEN ABBREV_TAC`a=matvec (v:real^3^M) `
THEN EXISTS_TAC`a:real^(M,3)finite_product`
THEN MATCH_MP_TAC IN_IS_SCS_CASE_4
THEN ASM_REWRITE_TAC[]]);;


let ARITH_4_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 4 MOD 4=0/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 4=1/\ 1<=1/\ 1<=4/\ 1 MOD 4=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 4=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 4=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 4=1/\ ~(4=0)/\ 0 MOD 4=0`;;

let VV_IN_BALL_ANNULUS_TAC_4=
fun (so:term)->
REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th so[ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
;;


let SCS_A_LE_NORM_4_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
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-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_4=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
THEN RESA_TAC
THENL[
SCS_A_LE_NORM_4_IS_SCS th `4`;
SCS_A_LE_NORM_4_IS_SCS th `1`;
SCS_A_LE_NORM_4_IS_SCS th `2`;
SCS_A_LE_NORM_4_IS_SCS th `3`];;




let SCS_B_LE_NORM_4_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
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-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (4)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_4B=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
THEN RESA_TAC
THENL[
SCS_B_LE_NORM_4_IS_SCS th `4`;
SCS_B_LE_NORM_4_IS_SCS th `1`;
SCS_B_LE_NORM_4_IS_SCS th `2`;
SCS_B_LE_NORM_4_IS_SCS th `3`];;




let V_SY_EQ_IMAGE_VV_TAC4=
fun (th:term)->
ASM_REWRITE_TAC[]
THEN EXISTS_TAC th
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_4_TAC];;


let PROVE_E_SY_EQ_MOD_TAC_4=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_4_TAC]
;;







let PROOF_E_EQ_TAC_4=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_4_TAC;]
;;


let PROVE_E_SY_EQ_IMAGE_VV_4=
fun (so:term) (so1:term)->
MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_4_TAC]
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_4_TAC];;




let  IN_NOT_EMPTY_B1_SY_4_IS_SCS=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=4 /\ 
dimindex(:M) = scs_k_v39 s/\
 matvec (v:real^3^M) =a/\ 
(!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ 
 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
 CONDITION2_SY v 
/\ (!i. vv i = 
if i MOD scs_k_v39 s = 0 then row 4 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
row 3 v)
==> vv IN BBs_v39 s`,

[

REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
THEN REPEAT RESA_TAC;


ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`x' MOD 4<4 ==> x' MOD 4 = 0 \/ x' MOD 4 = 1 \/ x' MOD 4 = 2 \/ x' MOD 4 = 3`)
THEN RESA_TAC
THENL[
VV_IN_BALL_ANNULUS_TAC_4 `4`;
VV_IN_BALL_ANNULUS_TAC_4 `1`;
VV_IN_BALL_ANNULUS_TAC_4 `2`;
VV_IN_BALL_ANNULUS_TAC_4 `3`];



ASM_REWRITE_TAC[periodic]
THEN GEN_TAC
THEN MRESAL_TAC MOD_EQ[`i+4:num`;`i:num`;`4:num`;`1`][ARITH_RULE`1*A=A`];



REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;


POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];



MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_4 `4`;
PROVE_INEQUALITY_TAC_4 `1`;
PROVE_INEQUALITY_TAC_4 `2`;
PROVE_INEQUALITY_TAC_4 `3`]
;





REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;


POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];



MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_4B `4`;
PROVE_INEQUALITY_TAC_4B `1`;
PROVE_INEQUALITY_TAC_4B `2`;
PROVE_INEQUALITY_TAC_4B `3`]
;











POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`~(4<=3)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;



ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;


ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
THEN STRIP_TAC
THENL[
V_SY_EQ_IMAGE_VV_TAC4 `1`;
V_SY_EQ_IMAGE_VV_TAC4 `2`;
V_SY_EQ_IMAGE_VV_TAC4 `3`;
V_SY_EQ_IMAGE_VV_TAC4 `4`];



RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_MOD_TAC_4 `4`;
PROVE_E_SY_EQ_MOD_TAC_4 `1`;
PROVE_E_SY_EQ_MOD_TAC_4 `2`;
PROVE_E_SY_EQ_MOD_TAC_4 `3`]
;







SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;



ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
;




ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_4`1`;
PROOF_E_EQ_TAC_4`2`;
PROOF_E_EQ_TAC_4`3`;
PROOF_E_EQ_TAC_4`4`]
;



RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];



SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;


ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
;




ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_4`1`;
PROOF_E_EQ_TAC_4`2`;
PROOF_E_EQ_TAC_4`3`;
PROOF_E_EQ_TAC_4`4`]
;



RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];



REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[];
]);;
  (* }}} *)



let XWITCCN_CASE_4_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ BBs_v39 s vv
/\ scs_k_v39 s=4
/\  dimindex(:M) =scs_k_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime_v39 s = {})`,

  (* {{{ proof *)
[


STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
THEN STRIP_TAC
THEN MP_TAC NOT_EMPTY_CASE_4_IS_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))`
THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<4`;]
THEN POP_ASSUM (fun th->
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN REWRITE_TAC[BBprime_v39;IN]
THEN ABBREV_TAC`( vv1 i = 
if i MOD scs_k_v39 s = 0 then row 4 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
row 3 (v:real^3^M))`
THEN EXISTS_TAC`vv1:num->real^3`
THEN STRIP_TAC;


ONCE_REWRITE_TAC[GSYM IN]
THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
THEN EXISTS_TAC`x:real^(M,3)finite_product`
THEN EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
;


SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 0] = v:real^3^M`
ASSUME_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 0 MOD 4=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
THEN ONCE_REWRITE_TAC[CART_EQ]
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=4 <=>i=1\/ i=2\/ i=3\/ i=4`]
THEN REPEAT RESA_TAC
THEN
ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];



STRIP_TAC;

GEN_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
[`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;]
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[IN]
THEN STRIP_TAC)
THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
THEN REWRITE_TAC[th]
THEN RESA_TAC)
THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`);

MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
[`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;]
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`)
THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

]);;
  (* }}} *)

(*************CASE 5****************)

let NOT_EMPTY_CASE_5_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv 
/\  dimindex(:M)= scs_k_v39 s
==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,

[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
THEN STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
THEN ABBREV_TAC`a=matvec (v:real^3^M) `
THEN EXISTS_TAC`a:real^(M,3)finite_product`
THEN MATCH_MP_TAC IN_IS_SCS_CASE_5
THEN ASM_REWRITE_TAC[]]);;




let ARITH_5_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=5/\3<=5/\5<=5 /\ 4<=5/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=4/\ 4 MOD 5=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 5=0/\ ~(4=0)/\ 0 MOD 5=0
/\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)
`;;


let VV_IN_BALL_ANNULUS_TAC_5=
fun (so:term)->
REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th so[ARITH_5_TAC;IN])
;;




let SCS_A_LE_NORM_5_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_5=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
THEN RESA_TAC
THENL[
SCS_A_LE_NORM_5_IS_SCS th `5`;
SCS_A_LE_NORM_5_IS_SCS th `1`;
SCS_A_LE_NORM_5_IS_SCS th `2`;
SCS_A_LE_NORM_5_IS_SCS th `3`;
SCS_A_LE_NORM_5_IS_SCS th `4`];;






let SCS_B_LE_NORM_5_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (5)`][ARITH_RULE`~(5=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_5B=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
THEN RESA_TAC
THENL[
SCS_B_LE_NORM_5_IS_SCS th `5`;
SCS_B_LE_NORM_5_IS_SCS th `1`;
SCS_B_LE_NORM_5_IS_SCS th `2`;
SCS_B_LE_NORM_5_IS_SCS th `3`;
SCS_B_LE_NORM_5_IS_SCS th `4`];;












let V_SY_EQ_IMAGE_VV_TAC5=
fun (th:term)->
ASM_REWRITE_TAC[]
THEN EXISTS_TAC th
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_5_TAC];;


let PROVE_E_SY_EQ_MOD_TAC_5=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_5_TAC]
;;







let PROOF_E_EQ_TAC_5=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_5_TAC;]
;;


let PROVE_E_SY_EQ_IMAGE_VV_5=
fun (so:term) (so1:term)->
MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_5_TAC]
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_5_TAC];;




let  IN_NOT_EMPTY_B1_SY_5_IS_SCS=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=5 /\ 
dimindex(:M) = scs_k_v39 s/\
 matvec (v:real^3^M) =a/\ 
(!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ 
 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
 CONDITION2_SY v 
/\ (!i. vv i = 
if i MOD scs_k_v39 s = 0 then row 5 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
if i MOD scs_k_v39 s = 3 then row 3 v else
row 4 v)
==> vv IN BBs_v39 s`,

[
REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39;]
THEN REPEAT RESA_TAC;

ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`x' MOD 5<5 ==> x' MOD 5 = 0 \/ x' MOD 5 = 1 \/ x' MOD 5 = 2 \/ x' MOD 5 = 3\/ x' MOD 5 = 4`)
THEN RESA_TAC
THENL[
VV_IN_BALL_ANNULUS_TAC_5 `5`;
VV_IN_BALL_ANNULUS_TAC_5 `1`;
VV_IN_BALL_ANNULUS_TAC_5 `2`;
VV_IN_BALL_ANNULUS_TAC_5 `3`;
VV_IN_BALL_ANNULUS_TAC_5 `4`];

ASM_REWRITE_TAC[periodic]
THEN GEN_TAC
THEN MRESAL_TAC MOD_EQ[`i+5:num`;`i:num`;`5:num`;`1`][ARITH_RULE`1*A=A`];

REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];

MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_5 `5`;
PROVE_INEQUALITY_TAC_5 `1`;
PROVE_INEQUALITY_TAC_5 `2`;
PROVE_INEQUALITY_TAC_5 `3`;
PROVE_INEQUALITY_TAC_5 `4`];




REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];



MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_5B `5`;
PROVE_INEQUALITY_TAC_5B `1`;
PROVE_INEQUALITY_TAC_5B `2`;
PROVE_INEQUALITY_TAC_5B `3`;
PROVE_INEQUALITY_TAC_5B `4`];

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;

ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;

ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5`]
THEN STRIP_TAC
THENL[
V_SY_EQ_IMAGE_VV_TAC5 `1`;
V_SY_EQ_IMAGE_VV_TAC5 `2`;
V_SY_EQ_IMAGE_VV_TAC5 `3`;
V_SY_EQ_IMAGE_VV_TAC5 `4`;
V_SY_EQ_IMAGE_VV_TAC5 `5`;];


RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3)\/ (x' MOD 5=4)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_MOD_TAC_5 `5`;
PROVE_E_SY_EQ_MOD_TAC_5 `1`;
PROVE_E_SY_EQ_MOD_TAC_5 `2`;
PROVE_E_SY_EQ_MOD_TAC_5 `3`;
PROVE_E_SY_EQ_MOD_TAC_5 `4`];


SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;

ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;


ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_5`1`;
PROOF_E_EQ_TAC_5`2`;
PROOF_E_EQ_TAC_5`3`;
PROOF_E_EQ_TAC_5`4`;
PROOF_E_EQ_TAC_5`5`];


RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];

SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;

ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;


ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_5`1`;
PROOF_E_EQ_TAC_5`2`;
PROOF_E_EQ_TAC_5`3`;
PROOF_E_EQ_TAC_5`4`;
PROOF_E_EQ_TAC_5`5`];


RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];

REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[];

]);;
  (* }}} *)



let XWITCCN_CASE_5_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ BBs_v39 s vv
/\ scs_k_v39 s=5
/\  dimindex(:M) =scs_k_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime_v39 s = {})`,

  (* {{{ proof *)
[
STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
THEN STRIP_TAC
THEN MP_TAC NOT_EMPTY_CASE_5_IS_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))`
THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<5`;]
THEN POP_ASSUM (fun th->
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN REWRITE_TAC[BBprime_v39;IN]
THEN ABBREV_TAC`( vv1 i = 
if i MOD scs_k_v39 s = 0 then row 5 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
if i MOD scs_k_v39 s = 3 then row 3 v else
row 4 (v:real^3^M))`
THEN EXISTS_TAC`vv1:num->real^3`
THEN STRIP_TAC;

ONCE_REWRITE_TAC[GSYM IN]
THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
THEN EXISTS_TAC`x:real^(M,3)finite_product`
THEN EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC;

SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 0] = v:real^3^M`
ASSUME_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 0 MOD 5=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 5=4`;]
THEN ONCE_REWRITE_TAC[CART_EQ]
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=5 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5`]
THEN REPEAT RESA_TAC
THEN
ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
REWRITE_TAC[num_CONV `4`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];


STRIP_TAC;

GEN_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
[`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;]
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[IN]
THEN STRIP_TAC)
THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
THEN REWRITE_TAC[th]
THEN RESA_TAC)
THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`);

MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
[`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;]
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`)
THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

]);;
  (* }}} *)





(*************CASE 6****************)

let NOT_EMPTY_CASE_6_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv 
/\  dimindex(:M)= scs_k_v39 s
==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,

[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
THEN STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
THEN ABBREV_TAC`a=matvec (v:real^3^M) `
THEN EXISTS_TAC`a:real^(M,3)finite_product`
THEN MATCH_MP_TAC IN_IS_SCS_CASE_6
THEN ASM_REWRITE_TAC[]]);;



let ARITH_6_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=6/\3<=6/\5<=6 /\ 4<=6/\5<=6/\ 6<=6/\ 1<=6 /\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=4/\ 4 MOD 6=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 6=5/\ ~(4=0)/\ 0 MOD 6=0/\ 6 MOD 6=0/\ 7 MOD 6=1 /\ SUC 6=7
/\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)/\ ~(6=0)
/\ ~(5=1)/\ ~(5=2)/\ ~(5=3)/\ ~(5=4)`;;


let VV_IN_BALL_ANNULUS_TAC_6=
fun (so:term)->
REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th so[ARITH_6_TAC;IN])
;;




let SCS_A_LE_NORM_6_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_6=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`)
THEN RESA_TAC
THENL[
SCS_A_LE_NORM_6_IS_SCS th `6`;
SCS_A_LE_NORM_6_IS_SCS th `1`;
SCS_A_LE_NORM_6_IS_SCS th `2`;
SCS_A_LE_NORM_6_IS_SCS th `3`;
SCS_A_LE_NORM_6_IS_SCS th `4`;
SCS_A_LE_NORM_6_IS_SCS th `5`];;






let SCS_B_LE_NORM_6_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (6)`][ARITH_RULE`~(6=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_6B=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/  (j MOD 6=5)`)
THEN RESA_TAC
THENL[
SCS_B_LE_NORM_6_IS_SCS th `6`;
SCS_B_LE_NORM_6_IS_SCS th `1`;
SCS_B_LE_NORM_6_IS_SCS th `2`;
SCS_B_LE_NORM_6_IS_SCS th `3`;
SCS_B_LE_NORM_6_IS_SCS th `4`;
SCS_B_LE_NORM_6_IS_SCS th `5`];;












let V_SY_EQ_IMAGE_VV_TAC6=
fun (th:term)->
ASM_REWRITE_TAC[]
THEN EXISTS_TAC th
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_6_TAC];;


let PROVE_E_SY_EQ_MOD_TAC_6=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_6_TAC]
;;







let PROOF_E_EQ_TAC_6=
fun (so:term)->
EXISTS_TAC so
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_6_TAC;]
;;


let PROVE_E_SY_EQ_IMAGE_VV_6=
fun (so:term) (so1:term)->
MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_6_TAC]
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_6_TAC];;




let  IN_NOT_EMPTY_B1_SY_6_IS_SCS=
prove_by_refinement(`is_scs_v39 s /\ scs_k_v39 s=6 /\ 
dimindex(:M) = scs_k_v39 s/\
 matvec (v:real^3^M) =a/\ 
(!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ 
 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
 CONDITION2_SY v 
/\ (!i. vv i = 
if i MOD scs_k_v39 s = 0 then row 6 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
if i MOD scs_k_v39 s = 3 then row 3 v else
if i MOD scs_k_v39 s = 4 then row 4 v else
row 5 v)
==> vv IN BBs_v39 s`,

[
REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39;]
THEN REPEAT RESA_TAC;


ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`x' MOD 6<6 ==> x' MOD 6 = 0 \/ x' MOD 6 = 1 \/ x' MOD 6 = 2 \/ x' MOD 6 = 3\/ x' MOD 6 = 4\/ x' MOD 6 = 5`)
THEN RESA_TAC
THENL[
VV_IN_BALL_ANNULUS_TAC_6 `6`;
VV_IN_BALL_ANNULUS_TAC_6 `1`;
VV_IN_BALL_ANNULUS_TAC_6 `2`;
VV_IN_BALL_ANNULUS_TAC_6 `3`;
VV_IN_BALL_ANNULUS_TAC_6 `4`;
VV_IN_BALL_ANNULUS_TAC_6 `5`];


ASM_REWRITE_TAC[periodic]
THEN GEN_TAC
THEN MRESAL_TAC MOD_EQ[`i+6:num`;`i:num`;`6:num`;`1`][ARITH_RULE`1*A=A`];


REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;


POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];


MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_6 `6`;
PROVE_INEQUALITY_TAC_6 `1`;
PROVE_INEQUALITY_TAC_6 `2`;
PROVE_INEQUALITY_TAC_6 `3`;
PROVE_INEQUALITY_TAC_6 `4`;
PROVE_INEQUALITY_TAC_6 `5`];





REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;


POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];


MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_6B `6`;
PROVE_INEQUALITY_TAC_6B `1`;
PROVE_INEQUALITY_TAC_6B `2`;
PROVE_INEQUALITY_TAC_6B `3`;
PROVE_INEQUALITY_TAC_6B `4`;
PROVE_INEQUALITY_TAC_6B `5`];



POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;


ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;


ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5\/ i=6`]
THEN STRIP_TAC
THENL[
V_SY_EQ_IMAGE_VV_TAC6 `1`;
V_SY_EQ_IMAGE_VV_TAC6 `2`;
V_SY_EQ_IMAGE_VV_TAC6 `3`;
V_SY_EQ_IMAGE_VV_TAC6 `4`;
V_SY_EQ_IMAGE_VV_TAC6 `5`;
V_SY_EQ_IMAGE_VV_TAC6 `6`;];


RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3)\/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_MOD_TAC_6 `6`;
PROVE_E_SY_EQ_MOD_TAC_6 `1`;
PROVE_E_SY_EQ_MOD_TAC_6 `2`;
PROVE_E_SY_EQ_MOD_TAC_6 `3`;
PROVE_E_SY_EQ_MOD_TAC_6 `4`;
PROVE_E_SY_EQ_MOD_TAC_6 `5`;];



SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;


ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;



ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_6`1`;
PROOF_E_EQ_TAC_6`2`;
PROOF_E_EQ_TAC_6`3`;
PROOF_E_EQ_TAC_6`4`;
PROOF_E_EQ_TAC_6`5`;
PROOF_E_EQ_TAC_6`6`];



RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];


SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;


ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
THEN ONCE_REWRITE_TAC[EXTENSION;]
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;



ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
THEN RESA_TAC
THENL[
PROOF_E_EQ_TAC_6`1`;
PROOF_E_EQ_TAC_6`2`;
PROOF_E_EQ_TAC_6`3`;
PROOF_E_EQ_TAC_6`4`;
PROOF_E_EQ_TAC_6`5`;
PROOF_E_EQ_TAC_6`6`];



RESA_TAC
THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`)
THEN RESA_TAC
THENL[
PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];


REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[];


]);;
  (* }}} *)


let XWITCCN_CASE_6_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ BBs_v39 s vv
/\ scs_k_v39 s=6
/\  dimindex(:M) =scs_k_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime_v39 s = {})`,

  (* {{{ proof *)
[
STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
THEN STRIP_TAC
THEN MP_TAC NOT_EMPTY_CASE_6_IS_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))`
THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<6`;]
THEN POP_ASSUM (fun th->
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN REWRITE_TAC[BBprime_v39;IN]
THEN ABBREV_TAC`( vv1 i = 
if i MOD scs_k_v39 s = 0 then row 6 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
if i MOD scs_k_v39 s = 2 then row 2 v else
if i MOD scs_k_v39 s = 3 then row 3 v else
if i MOD scs_k_v39 s = 4 then row 4 v else
row 5 (v:real^3^M))`
THEN EXISTS_TAC`vv1:num->real^3`
THEN STRIP_TAC;

ONCE_REWRITE_TAC[GSYM IN]
THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
THEN EXISTS_TAC`x:real^(M,3)finite_product`
THEN EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC;

SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 5; vv1 0] = v:real^3^M`
ASSUME_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 0 MOD 6
=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 6=4/\ 5 MOD 6=5/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)/\ ~(0=5)`;]
THEN ONCE_REWRITE_TAC[CART_EQ]
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=6
 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5\/ i=6`]
THEN REPEAT RESA_TAC
THEN
ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
REWRITE_TAC[num_CONV `4`;num_CONV `5`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];


STRIP_TAC;

GEN_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
[`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;]
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[IN]
THEN STRIP_TAC)
THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
THEN REWRITE_TAC[th]
THEN RESA_TAC)
THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`);

MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
[`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;]
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5;vv 0]:real^3^M):real^(M,3)finite_product`)
THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

]);;
  (* }}} *)


(****************CASE 3**************)

let IS_SCS_IN_BALL_ANNULUS_3=
fun (so:term)->
REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
THEN STRIP_TAC 
THEN POP_ASSUM MATCH_MP_TAC
THEN EXISTS_TAC so
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
;;



let IN_IS_SCS_CASE_3=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv 
/\  dimindex(:M)= scs_k_v39 s
/\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
/\ matvec (v:real^3^M) =a
==> 
a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v }`,

  (* {{{ proof *)
[
REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
THEN STRIP_TAC;

EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`] 
THEN REPEAT STRIP_TAC
THENL[
IS_SCS_IN_BALL_ANNULUS_3 `1`;
IS_SCS_IN_BALL_ANNULUS_3 `2`;
IS_SCS_IN_BALL_ANNULUS_3 `0`];

REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`] 
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN STRIP_TAC
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];

EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`] 
THEN REPEAT STRIP_TAC
THENL[
IS_SCS_IN_BALL_ANNULUS_3 `1`;
IS_SCS_IN_BALL_ANNULUS_3 `2`;
IS_SCS_IN_BALL_ANNULUS_3 `0`];

REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`] 
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN STRIP_TAC
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];
]);;


let ARITH_3_TAC =ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 0 MOD 3=0/\ 1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ SUC 0=1 /\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ 0<3/\ a+0=a/\ 0+a=a/\ 3-1=2/\ 3-2=1/\ 3-0=3/\ 3-3=0`;;



let VV_IN_BALL_ANNULUS_TAC_3=
fun (so:term)->
REPLICATE_TAC (30-23)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th so[ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
;;


let SCS_A_LE_NORM_3_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_3=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
THEN RESA_TAC
THENL[
SCS_A_LE_NORM_3_IS_SCS th `3`;
SCS_A_LE_NORM_3_IS_SCS th `1`;
SCS_A_LE_NORM_3_IS_SCS th `2`;];;




let SCS_B_LE_NORM_3_IS_SCS=
fun (so:term) (so1:term)->
REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> 
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
THEN ASSUME_TAC th)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (3)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
THEN REPEAT RESA_TAC
;;

let PROVE_INEQUALITY_TAC_3B=
fun (th:term)->
MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
THEN RESA_TAC
THENL[
SCS_B_LE_NORM_3_IS_SCS th `3`;
SCS_B_LE_NORM_3_IS_SCS th `1`;
SCS_B_LE_NORM_3_IS_SCS th `2`;];;



let  IN_NOT_EMPTY_B1_SY_3_IS_SCS=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=3 /\ 
dimindex(:M) = scs_k_v39 s/\
 matvec (v:real^3^M) =a/\ 
(!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ 
 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ (!i. vv i = 
if i MOD scs_k_v39 s = 0 then row 3 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
row 2 v)
==> vv IN BBs_v39 s`,

[
REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
THEN REPEAT RESA_TAC;

ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`x' MOD 3<3 ==> x' MOD 3 = 0 \/ x' MOD 3 = 1 \/ x' MOD 3 = 2 `)
THEN RESA_TAC
THENL[
VV_IN_BALL_ANNULUS_TAC_3 `3`;
VV_IN_BALL_ANNULUS_TAC_3 `1`;
VV_IN_BALL_ANNULUS_TAC_3 `2`;];


ASM_REWRITE_TAC[periodic]
THEN GEN_TAC
THEN MRESAL_TAC MOD_EQ[`i+3:num`;`i:num`;`3:num`;`1`][ARITH_RULE`1*A=A`];

REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];

MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_3 `3`;
PROVE_INEQUALITY_TAC_3 `1`;
PROVE_INEQUALITY_TAC_3 `2`;];


REWRITE_TAC[dist]
THEN REPEAT GEN_TAC
THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;

POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
THEN GEN_TAC
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];

MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
THEN RESA_TAC
THENL[
PROVE_INEQUALITY_TAC_3B `3`;
PROVE_INEQUALITY_TAC_3B `1`;
PROVE_INEQUALITY_TAC_3B `2`;];

REWRITE_TAC[ARITH_RULE`3<=3`];

]);;
  (* }}} *)


let NOT_EMPTY_CASE_3_IS_SCS=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv 
/\  dimindex(:M)= scs_k_v39 s
==> ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v  }={})`,

[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
THEN STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M`
THEN ABBREV_TAC`a=matvec (v:real^3^M) `
THEN EXISTS_TAC`a:real^(M,3)finite_product`
THEN MATCH_MP_TAC IN_IS_SCS_CASE_3
THEN ASM_REWRITE_TAC[]]);;





let J1_TS=new_definition `J1_TS (s:tri_sy)= {x| ?i. {i MOD 3,f_ts s (i MOD (3))} IN J_TS s /\ i IN 1..3 /\ x=i,SUC(i MOD (3))}`;;



let d_fun3=new_definition `d_fun3 (s1:scs_v39)(s:tri_sy,l:real^(M,3)finite_product) = (d_ts s) + #0.1 * (if is_ear_v39 s1 then &1 else -- &1) * sum (J1_TS s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;


let FINITE_J1_TS=
prove(`!s:tri_sy . 
FINITE (J1_TS s)`,

GEN_TAC
THEN REWRITE_TAC[J1_TS]
THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (3)))`;`1..3`][FINITE_NUMSEG;IMAGE]
THEN MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`{y | ?x. x IN 1..(3) /\ y = x,SUC(x MOD (3))}`
THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]);;
let INDEX_J1_TS=
prove(`!s:tri_sy . 
x IN J1_TS s ==> 1 <= FST x /\ FST x <= 3`,

REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]);;


let CONTINUOUS_ON_D_FUN3=
prove(`!s:tri_sy . 
k=3 /\
k_ts s =k /\ dimindex(:M) =k/\ I_TS s= 0..k-1 /\ f_ts s=(\i. ((1+i):num MOD k))
==> lift o(\l:real^(M,3)finite_product. d_fun3 s1 (s,l)) continuous_on (
{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (a_ts s) (b_ts s) v  })`,

REPEAT STRIP_TAC
THEN REWRITE_TAC[d_fun3;LIFT_ADD;o_DEF;]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN ASSUME_TAC FINITE_J1_TS
THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:tri_sy`)
THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF]
THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM 
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[LIFT_SUB]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN STRIP_TAC
THENL[
MATCH_MP_TAC CONTINUOUS_ON_ROW
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC;

MATCH_MP_TAC CONTINUOUS_ON_ROW
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC]);;





let tri_sy_explicit = 
prove_by_refinement(
 `!k d s a b J f. tri_stable k d s a b J f ==> k_ts (tri_sy (k,d,s, a,b,J,f)) =  k/\
d_ts (tri_sy (k,d,s, a,b,J,f)) =  d /\ 
a_ts (tri_sy (k,d,s, a,b,J,f)) =  a /\ 
b_ts (tri_sy (k,d,s, a,b,J,f)) =  b /\ 
J_TS (tri_sy (k,d,s, a,b,J,f)) =  J /\ 
I_TS (tri_sy (k,d,s, a,b,J,f)) =  s /\ 
f_ts (tri_sy (k,d,s, a,b,J,f)) =  f `,

  (* {{{ proof *)
  [   REWRITE_TAC[k_ts;d_ts;a_ts;b_ts;J_TS;I_TS;f_ts;tri_sy_tybij;]
THEN MP_TAC tri_sy_tybij
THEN STRIP_TAC
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> 
POP_ASSUM (fun th1-> ASSUME_TAC th THEN MRESA1_TAC th1`(k,d,s,a,b,J,f):(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num))`))
]);;
  (* }}} *)




let IN_B_SY1_COLLINEAR_CASE_3_IS_SCS=
prove_by_refinement(
`is_scs_v39 s 
/\ scs_k_v39 s=3/\
dimindex(:M)= scs_k_v39 s
==>
 (!a. a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v  }
==> ~collinear{vec 0, row 1 (vecmats a),row 2 (vecmats a)}/\
~collinear{vec 0, row 1 (vecmats a),row 3 (vecmats a)}/\
~collinear{vec 0, row 2 (vecmats a),row 3 (vecmats a)})`,

  (* {{{ proof *)
[
REWRITE_TAC[IN_ELIM_THM;]
THEN STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN ABBREV_TAC`( vv i = 
if i MOD scs_k_v39 s = 0 then row 3 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
row 2 (v:real^3^M))`
THEN MP_TAC IN_NOT_EMPTY_B1_SY_3_IS_SCS
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN RESA_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_NOT_COLLINEAR_BBs_CASE_3
THEN RESA_TAC;

SUBGOAL_THEN`vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M
=v`ASSUME_TAC;

REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
THEN ONCE_REWRITE_TAC[CART_EQ]
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
THEN REPEAT RESA_TAC
THEN
ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];

MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`];
]);;
  (* }}} *)



let HDPLYGY_CASE_30=
prove_by_refinement(
`tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\ 2<k
/\ ~({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  } = {}:real^(M,3)finite_product->bool)
/\ (!l. l IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }
==> ~collinear{vec 0, row 1 (vecmats l),row 2 (vecmats l)}/\
~collinear{vec 0, row 1 (vecmats l),row 3 (vecmats l)}/\
~collinear{vec 0, row 2 (vecmats l),row 3 (vecmats l)})
/\ k_ts s = 3 /\ I_TS s = 0..3 - 1 /\ f_ts s = (\i. (1 + i) MOD 3)
/\ a_ts s =a /\ b_ts s =b
==> ?x:real^(M,3)finite_product. x IN  ({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
/\ (!y:real^(M,3)finite_product. y IN ({matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
==> tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))
-  d_fun3 s1 (s,x)
 <= tau3 (row 1 (vecmats y)) (row 2 (vecmats y)) (row 3 (vecmats y))
-  d_fun3 s1 (s,y)
)`,

  (* {{{ proof *)
[

REPEAT STRIP_TAC
THEN MP_TAC TRI_STABLE_K_EQ_3
THEN RESA_TAC
THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\x:real^(M,3)finite_product. tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))-  d_fun3 s1 (s,x))`;`{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }:real^(M,3)finite_product->bool`]
THEN POP_ASSUM MATCH_MP_TAC
THEN STRIP_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MATCH_MP_TAC COMPACT_TRI_STABLE
THEN ASM_REWRITE_TAC[];

SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN ONCE_REWRITE_TAC[SET_RULE`A/\B <=> B/\ A`]
THEN STRIP_TAC;

MRESAL_TAC(GEN_ALL CONTINUOUS_ON_D_FUN3)[`k:num`;`s1:scs_v39`;`s:tri_sy`][o_DEF];

POP_ASSUM MP_TAC
THEN REPLICATE_TAC 5(REMOVE_ASSUM_TAC)
THEN STRIP_TAC
THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG;tau3; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN SIMP_TAC[o_DEF;LIFT_ADD;]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN STRIP_TAC;


SIMP_TAC[o_DEF;LIFT_ADD;]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN STRIP_TAC;


SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
THEN STRIP_TAC;


REWRITE_TAC[rho;o_DEF;LIFT_ADD]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
THEN ASM_REWRITE_TAC[IN_NUMSEG]
THEN ARITH_TAC;

REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
THEN REPEAT STRIP_TAC
THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
THEN REWRITE_TAC[o_DEF]
THEN STRIP_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th `a':real^(M,3)finite_product`
THEN ASSUME_TAC th)
THEN GEN_TAC
THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)

;



SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
THEN STRIP_TAC;


REWRITE_TAC[rho;o_DEF;LIFT_ADD]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
THEN ASM_REWRITE_TAC[IN_NUMSEG]
THEN ARITH_TAC;

REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
THEN REPEAT STRIP_TAC
THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
THEN REWRITE_TAC[o_DEF]
THEN STRIP_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th `a':real^(M,3)finite_product`
THEN ASSUME_TAC th)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]

;



SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
THEN STRIP_TAC;


REWRITE_TAC[rho;o_DEF;LIFT_ADD]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
THEN ASM_REWRITE_TAC[IN_NUMSEG]
THEN ARITH_TAC;

REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
THEN REPEAT STRIP_TAC
THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
THEN REWRITE_TAC[o_DEF]
THEN STRIP_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th `a':real^(M,3)finite_product`
THEN ASSUME_TAC th)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th->  MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[];
]);;
  (* }}} *)






let TAUSTAR_EQ_TAU_STAR_3_IS_SCS=
prove_by_refinement(
`is_scs_v39 s /\ BBs_v39 s vv
/\ scs_k_v39 s=3
/\ dimindex (:M)=3
/\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
/\ matvec (v:real^3^M) =a
/\ tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))=s1
==>  taustar_v39 s vv = tau3  (vv 1) (vv 2) (vv 0) -d_fun3 s (s1,a)`,

  (* {{{ proof *)
[

REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[taustar_v39;tau_star;LET_DEF;LET_END_DEF;ARITH_RULE`3<=3`;]
THEN MATCH_MP_TAC(REAL_ARITH`a=b /\ c=d==> a -c= b- d`)
THEN STRIP_TAC
;

REWRITE_TAC[tau3]
THEN REAL_ARITH_TAC;

REWRITE_TAC[dsv_v39;d_fun3]
THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
THEN RESA_TAC
THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MATCH_MP_TAC(REAL_ARITH`a=b ==> d+ a=d+b`)
THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`)
THEN RESA_TAC

;


MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * &1 * a= #0.1 * &1 *b`)
THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN REWRITE_TAC[IN_ELIM_THM;dist]
THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else  i, SUC(i MOD 3))`
THEN STRIP_TAC;


REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
THEN RESA_TAC;

REWRITE_TAC[ARITH_3_TAC]
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_3_TAC]
THEN POP_ASSUM(fun th->
ASM_TAC
THEN REWRITE_TAC[th;ARITH_3_TAC]
THEN REPEAT DISCH_TAC)
THEN STRIP_TAC
;

MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];


EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;

MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_3_TAC]
;

ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
THEN REWRITE_TAC[ADD1;]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN ASM_REWRITE_TAC[];



ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
THEN REWRITE_TAC[ADD1;]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN ASM_REWRITE_TAC[];



REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
THEN RESA_TAC
;

REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC;


REPEAT RESA_TAC
THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
;

MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
THEN RESA_TAC
;

EXISTS_TAC`3`
THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
THEN EXISTS_TAC`x:num`
THEN EXISTS_TAC`SUC x:num`
THEN ASM_REWRITE_TAC[ARITH_3_TAC];

EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[IN_NUMSEG]
THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
THEN RESA_TAC
THEN EXISTS_TAC`x:num`
THEN EXISTS_TAC`SUC x`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN REWRITE_TAC[ADD1]
;


MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])

;


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

MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * -- &1 * a= #0.1 * -- &1 *b`)
THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN REWRITE_TAC[IN_ELIM_THM;dist]
THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else  i, SUC(i MOD 3))`
THEN STRIP_TAC;


REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
THEN RESA_TAC;

REWRITE_TAC[ARITH_3_TAC]
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_3_TAC]
THEN POP_ASSUM(fun th->
ASM_TAC
THEN REWRITE_TAC[th;ARITH_3_TAC]
THEN REPEAT DISCH_TAC)
THEN STRIP_TAC
;

MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN STRIP_TAC
THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];


EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;

MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
THEN RESA_TAC
THEN REWRITE_TAC[ARITH_3_TAC]
;

ASM_REWRITE_TAC[]
THEN STRIP_TAC
;

REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
THEN RESA_TAC;


ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
THEN REWRITE_TAC[ADD1;]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN ASM_REWRITE_TAC[];



ASM_TAC
THEN REWRITE_TAC[is_scs_v39;periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
THEN REWRITE_TAC[ADD1;]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN ASM_REWRITE_TAC[];



REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
THEN RESA_TAC
;

REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
THEN RESA_TAC;

REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC;


REPEAT RESA_TAC
THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
;

MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
THEN RESA_TAC
;

EXISTS_TAC`3`
THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
THEN EXISTS_TAC`x:num`
THEN EXISTS_TAC`SUC x:num`
THEN ASM_REWRITE_TAC[ARITH_3_TAC];

EXISTS_TAC`x:num`
THEN ASM_REWRITE_TAC[IN_NUMSEG]
THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
THEN RESA_TAC
THEN EXISTS_TAC`x:num`
THEN EXISTS_TAC`SUC x`
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ADD_SYM]
THEN REWRITE_TAC[ADD1]
;


MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
THEN ASM_TAC
THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])

;

]);;

let XWITCCN_CASE_3_IS_SCS=
prove_by_refinement(
`is_scs_v39 s /\ BBs_v39 s vv
/\ scs_k_v39 s=3
/\  dimindex(:M) =scs_k_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime_v39 s = {})`,


  (* {{{ proof *)
[
STRIP_TAC
THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
THEN RESA_TAC
THEN MP_TAC NOT_EMPTY_CASE_3_IS_SCS
THEN RESA_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
THEN MP_TAC IN_B_SY1_COLLINEAR_CASE_3_IS_SCS
THEN RESA_TAC
THEN ABBREV_TAC`s1 =tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))`
THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s)(scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN  MRESAL_TAC (GEN_ALL HDPLYGY_CASE_30)[`scs_d_v39 s`;`(change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`scs_k_v39 s`;`(change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;`s:scs_v39`;`s1:tri_sy`][ARITH_RULE`2<3`]
THEN POP_ASSUM (fun th->
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN REWRITE_TAC[BBprime_v39;IN]
THEN ABBREV_TAC`( vv1 i = 
if i MOD scs_k_v39 s = 0 then row 3 v else
if i MOD scs_k_v39 s = 1 then row 1 v else
row 2 (v:real^3^M))`
THEN EXISTS_TAC`vv1:num->real^3`
THEN STRIP_TAC;

ONCE_REWRITE_TAC[GSYM IN]
THEN MATCH_MP_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
THEN EXISTS_TAC`x:real^(M,3)finite_product`
THEN EXISTS_TAC`v:real^3^M`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC;

SUBGOAL_THEN`vector [ vv1 1; (vv1:num->real^3) 2;vv1 0] = v:real^3^M`
ASSUME_TAC;

POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
THEN ONCE_REWRITE_TAC[CART_EQ]
THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
THEN REPEAT RESA_TAC
THEN
ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];

STRIP_TAC;

GEN_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(ww:num->real^3) 1; ww 2; ww 0]:real^3^M`;`ww:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`]
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
THEN MRESAL_TAC VECTOR_3_3[`(ww:num->real^3) 1`;`(ww:num->real^3) 2`;`(ww:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th `matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID]);

MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
[`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M`;`vv:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`]
THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th `matvec(vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID])
THEN REPLICATE_TAC (31-4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN ASM_REWRITE_TAC[])
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
]);;
  (* }}} *)




let UXCKFPE=
prove_by_refinement(
` !s vv . is_scs_v39 s /\ vv IN BBs_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime_v39 s = {})`,


  (* {{{ proof *)
[
REPEAT GEN_TAC
THEN REWRITE_TAC[IN]
THEN DISCH_TAC
THEN SUBGOAL_THEN`3<= scs_k_v39 s /\ scs_k_v39 s<=6` ASSUME_TAC;

ASM_TAC
THEN REWRITE_TAC[is_scs_v39]
THEN RESA_TAC;

MP_TAC(ARITH_RULE`3<= scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s=6`)
THEN RESA_TAC;

MP_TAC(INST_TYPE [`:3`,`:M`]XWITCCN_CASE_3_IS_SCS)
THEN ASM_REWRITE_TAC[DIMINDEX_3]
THEN STRIP_TAC ;

MP_TAC(INST_TYPE [`:2+2`,`:M`]XWITCCN_CASE_4_IS_SCS)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
THEN STRIP_TAC;

MP_TAC(INST_TYPE [`:2+3`,`:M`]XWITCCN_CASE_5_IS_SCS)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
THEN STRIP_TAC ;
MP_TAC(INST_TYPE [`:3+3`,`:M`]XWITCCN_CASE_6_IS_SCS)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
THEN STRIP_TAC ]);;


 end;;


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