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


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


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


let IS_SCS_STABLE_SYSTEM=
prove_by_refinement(
`is_scs_v39 s /\ 3< scs_k_v39 s
==>
stable_system (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):num MOD (scs_k_v39 s)))
`,

  (* {{{ proof *)
[
REWRITE_TAC[is_scs_v39;stable_system;constraint_system;torsor;change_type_v2;change_type_v3]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
/\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)`)
THEN RESA_TAC
THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
THEN REMOVE_ASSUM_TAC
THEN REPEAT DISCH_TAC
THEN STRIP_TAC;

STRIP_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
x2 <= scs_k_v39 s - 1
==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
THEN 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
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC);

MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<i /\ i< 4==> i=1 \/ i=2 \/ i=3`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 4-1==> x=0 \/ x=1 \/ x=2 \/ x=3`)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<i /\ i< 5==> i=1 \/ i=2 \/ i=3\/ i=4`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 5-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;

MP_TAC(ARITH_RULE`0<i /\ i< 6==> i=1 \/ i=2 \/ i=3\/ i=4\/ i=5`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 6-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
THEN RESA_TAC 
THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];

STRIP_TAC;

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

STRIP_TAC;

REPEAT GEN_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC 
THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
THEN STRIP_TAC;

MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];

MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];

STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
THEN REPEAT DISCH_TAC 
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);

EXISTS_TAC`i MOD scs_k_v39 s`
THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
/\ 3<= scs_k_v39 s
==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];

EXISTS_TAC`j MOD scs_k_v39 s`
THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
/\ 3<= scs_k_v39 s
==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN SET_TAC[];

SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
ASSUME_TAC;

REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN GEN_TAC
THEN RESA_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);

EXISTS_TAC`i:num MOD scs_k_v39 s`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][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 (i MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> 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)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
THEN REWRITE_TAC[h0;cstab;sqrt8]
THEN REAL_ARITH_TAC;

EXISTS_TAC`j:num MOD scs_k_v39 s`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
THEN REWRITE_TAC[h0;cstab;sqrt8]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}
SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 ASSUME_TAC;

 REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];

SUBGOAL_THEN` {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
SUBSET 0.. scs_k_v39 s`
 ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
THEN ARITH_TAC;

MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
`0.. scs_k_v39 s`][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
`0.. scs_k_v39 s`][FINITE_NUMSEG]
THEN MRESAL_TAC CARD_SUBSET_IMAGE
[`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_IMAGE
[`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`;
`IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 16 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 24 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`i:num`[ADD1]) 
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/ 
(j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
THEN REWRITE_TAC[sqrt8]
]);;






















let IS_SCS_TRI_STABLE_SYSTEM=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=3
==>
tri_stable (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):num MOD (scs_k_v39 s)))
`,

[
REWRITE_TAC[is_scs_v39;tri_stable;constraint_system;torsor;change_type_v2;change_type_v3]
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
/\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)/\ 3-0=3`)
THEN RESA_TAC
THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
THEN REMOVE_ASSUM_TAC
THEN REPEAT DISCH_TAC
THEN STRIP_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
x2 <= scs_k_v39 s - 1
==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
THEN RESA_TAC 
THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];

STRIP_TAC;

REPLICATE_TAC 16 (REMOVE_ASSUM_TAC)
THEN REPEAT STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`j:num`])
THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

STRIP_TAC;

REPEAT GEN_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT DISCH_TAC 
THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
THEN STRIP_TAC;

MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];

MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];

STRIP_TAC;

ASM_TAC
THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
THEN REPEAT DISCH_TAC 
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);

EXISTS_TAC`i MOD scs_k_v39 s`
THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
/\ 3<= scs_k_v39 s
==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];

EXISTS_TAC`j MOD scs_k_v39 s`
THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
/\ 3<= scs_k_v39 s
==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN SET_TAC[];

SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
ASSUME_TAC;

REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN GEN_TAC
THEN RESA_TAC
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);

EXISTS_TAC`i:num MOD scs_k_v39 s`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][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 (i MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> 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)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
THEN REWRITE_TAC[h0;cstab;sqrt8]
THEN REAL_ARITH_TAC;

EXISTS_TAC`j:num MOD scs_k_v39 s`
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
THEN REPEAT DISCH_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
THEN REWRITE_TAC[h0;cstab;sqrt8]
THEN REAL_ARITH_TAC;

SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}
SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 ASSUME_TAC;

 REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];

SUBGOAL_THEN` {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
SUBSET 0.. scs_k_v39 s`
 ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
THEN ARITH_TAC;



MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
`0.. scs_k_v39 s`][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
`0.. scs_k_v39 s`][FINITE_NUMSEG]
THEN MRESAL_TAC CARD_SUBSET_IMAGE
[`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_IMAGE
[`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
][FINITE_NUMSEG]
THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`;
`IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
           (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
                                                    (&2 * h0 <
                                                     scs_b_v39 s i (SUC i) \/
                                                     &2 <
                                                     scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
THEN POP_ASSUM (fun th->
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[th])
THEN ARITH_TAC;


REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 17 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 25 (REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;


STRIP_TAC;

REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`i:num`[ADD1]) 
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
THEN POP_ASSUM MP_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/ 
(j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
THEN REPLICATE_TAC (42 -16) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
THEN REWRITE_TAC[sqrt8];
]);;




let IS_SCS_IN_BALL_ANNULUS_4=
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_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(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 IS_SCS_IN_V_SY_4=
fun (so:term)->
 EXISTS_TAC so
THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(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)/\ 1<=1/\ 1<=2 /\ 1<=3/\ SUC 1=2/\ SUC 2=3 /\ SUC 3=4/\ SUC 0=1`;SET_RULE`(a:num) IN (:num)`]
;;


let PROVE_E_SY_INV_TAC_4=
fun (th:term)->
MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`4`][ARITH_RULE`~(4=0)/\ 4 MOD 4=0/\ SUC 0  MOD 4=1/\ 1 MOD 4=1 /\ 2 MOD 4=2 /\ 3 MOD 4=3`]
THEN EXISTS_TAC th
THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(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)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4/\ 1<=1 /\ 1<=2 /\ 1<=3`];;




let V_E_FF_IS_SCS_CASES_4=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=4 /\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
/\ matvec (v:real^3^M) =a
==> 
V_SY (v:real^3^M)=IMAGE vv (:num)/\
  E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`
,

  (* {{{ proof *)
[
STRIP_TAC
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[scs_k_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 STRIP_TAC;

REWRITE_TAC[V_SY;rows]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`] 
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`] 
THEN GEN_TAC
THEN EQ_TAC;

REPEAT STRIP_TAC
THENL[
IS_SCS_IN_V_SY_4`1`;
IS_SCS_IN_V_SY_4`2`;
IS_SCS_IN_V_SY_4`3`;
IS_SCS_IN_V_SY_4`0`];

REPEAT STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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[
IS_SCS_IN_V_SY_4`4`;
IS_SCS_IN_V_SY_4`1`;
IS_SCS_IN_V_SY_4`2`;
IS_SCS_IN_V_SY_4`3`];

REWRITE_TAC[E_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_4`1`;
IS_SCS_IN_V_SY_4`2`;
IS_SCS_IN_V_SY_4`3`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_4`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_4 `4`;
PROVE_E_SY_INV_TAC_4 `1`;
PROVE_E_SY_INV_TAC_4 `2`;
PROVE_E_SY_INV_TAC_4 `3`];

REWRITE_TAC[F_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_4`1`;
IS_SCS_IN_V_SY_4`2`;
IS_SCS_IN_V_SY_4`3`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_4`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_4 `4`;
PROVE_E_SY_INV_TAC_4 `1`;
PROVE_E_SY_INV_TAC_4 `2`;
PROVE_E_SY_INV_TAC_4 `3`]]);;



let IN_IS_SCS_CASE_4=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=4 /\ 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) 3;(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 /\ CONDITION2_SY 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;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

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

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

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`] 
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 4==> (i=1\/ i=2\/ i=3 \/ i=4)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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 4`][periodic;ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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 4`][periodic;ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=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`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);

MP_TAC V_E_FF_IS_SCS_CASES_4
THEN ASM_REWRITE_TAC[]
THEN ASM_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;IN]
THEN RESA_TAC]);;




let  IS_EAR_V25_EQ_EAR_SY=
prove(`is_scs_v39 s /\ 3< scs_k_v39 s
/\ 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))=s1
==>
(is_ear_v39 s <=> ear_sy s1)`,

REPEAT STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN REWRITE_TAC[is_ear_v39;ear_sy]
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 MP_TAC (ARITH_RULE`3< scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
/\ ~(scs_k_v39 s=3)`)
THEN RESA_TAC
THEN MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`][HAS_SIZE]);;





let INJ_H_FUN_TAC=
fun (so:term)->
STRIP_TAC
THENL[
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 4=2/\ 1+2=3 /\ 3 MOD 4=3/\ 1+3=4 /\ 4 MOD 4=0/\ 1+0=1`]
THEN REPEAT STRIP_TAC)
THEN EXISTS_TAC so
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(1=0)/\ 2<4 /\ 2 MOD 4=2 /\ ~(2=0)/\ SUC 2=3/\ 3<4/\ 3 MOD 4=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 4=0/\ 0<4/\ SUC 0=1`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
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 (j MOD 4)`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 4, j MOD 4}
==> (1 =i' MOD 4 /\ 2= j MOD 4)\/ (2 =i' MOD 4 /\ 1= j MOD 4)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 4, j MOD 4}
==> (2 =i' MOD 4 /\ 3= j MOD 4)\/ (3 =i' MOD 4 /\ 2= j MOD 4)`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 3`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{3,0} = {i' MOD 4, j MOD 4}
==> (3 =i' MOD 4 /\ 0= j MOD 4)\/ (0 =i' MOD 4 /\ 3= j MOD 4)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 4, j MOD 4}
==> (i' MOD 4=1 /\ j MOD 4=0)\/ (i' MOD 4=0 /\ j MOD 4=1)`)
THEN RESA_TAC;
REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]];;


let EXISTS_SCS_J_TAC=
fun (so:term) (so1:term) (so2:term)->
EXPAND_TAC "h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4`]
THEN STRIP_TAC
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_RULE`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)`]
THEN EXISTS_TAC so1
THEN EXISTS_TAC so2
THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ 1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 4 MOD 4=0`]
;;




let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=4
/\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
/\ matvec (v:real^3^M) =a
/\ 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))=s1
==>  taustar_v39 s vv = tau_star s1 a`
,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC V_E_FF_IS_SCS_CASES_4
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
THEN ASM_REWRITE_TAC[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 ASM_SIMP_TAC[dsv_J_empty]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
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 ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;

MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
THEN RESA_TAC
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[J1_SY ]
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ABBREV_TAC`h =(\i. if (i MOD 4 = 0) then (4,1) 
else (i MOD 4, SUC(i MOD 4)))`
THEN SUBGOAL_THEN`(!x x'.
      (x < 4 /\ scs_J_v39 s x (SUC x))  /\
      (x' < 4 /\ scs_J_v39 s x' (SUC x')) /\
      h x' = (h:num->num #num) x
      ==> x = x')` ASSUME_TAC;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE` x< 4 ==> x=0\/ x=1\/ x=2 \/ x=3 `)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE` x'< 4 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3 `)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0/\ 2 MOD 4=2/\ 3 MOD 4=3 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ SUC 1=2/\ ~(1=4)/\ ~(2=4)/\ ~(3=4)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
THEN RESA_TAC;

EXISTS_TAC`h:num->(num#num)`
THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
THEN STRIP_TAC
THEN REPEAT STRIP_TAC;

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

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
THEN RESA_TAC
THENL[
EXISTS_SCS_J_TAC `4` `0` `1`;
EXISTS_SCS_J_TAC `1` `1` `2`;
EXISTS_SCS_J_TAC `2` `2` `3`;
EXISTS_SCS_J_TAC `3` `3` `4`];

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ SUC 0=1`]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)/\ ~(2=0)
/\ ~(3=0)/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4 /\ SUC 4=5`;SET_RULE`(a:num)IN (:num)`;dist]
THEN REPLICATE_TAC 25 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])]);;



let JKQEWGV1_CASE_4=
prove( 
`!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s
 ==>
  (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
   (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_4
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_4
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`pi <=
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/ 
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
THEN RESA_TAC
THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC);;


let IS_SCS_IN_V_SY_5=
fun (so:term)->
 EXISTS_TAC so
THEN MRESAL_TAC VECTOR_3_5[`(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`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
/\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
/\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
;;


let PROVE_E_SY_INV_TAC_5=
fun (th:term)->
MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`5`][ARITH_RULE`~(5=0)/\ 4 MOD 5=4/\ SUC 0  MOD 5=1/\ 1 MOD 5=1 /\ 2 MOD 5=2 /\ 3 MOD 5=3/\ 5 MOD 5=0`]
THEN EXISTS_TAC th
THEN MRESAL_TAC VECTOR_3_5[`(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`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
/\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
/\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
;;








let V_E_FF_IS_SCS_CASES_5=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=5 /\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ 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= v
/\ matvec (v:real^3^M) =a
==> 
V_SY (v:real^3^M)=IMAGE vv (:num)/\
  E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,

  (* {{{ proof *)
[

STRIP_TAC
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[scs_k_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 STRIP_TAC;

REWRITE_TAC[V_SY;rows]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`] 
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`] 
THEN GEN_TAC
THEN EQ_TAC;

REPEAT STRIP_TAC
THENL[
IS_SCS_IN_V_SY_5`1`;
IS_SCS_IN_V_SY_5`2`;
IS_SCS_IN_V_SY_5`3`;
IS_SCS_IN_V_SY_5`4`;
IS_SCS_IN_V_SY_5`0`];

REPEAT STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)<=> (1<= i /\ i<= 5)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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[
IS_SCS_IN_V_SY_5`5`;
IS_SCS_IN_V_SY_5`1`;
IS_SCS_IN_V_SY_5`2`;
IS_SCS_IN_V_SY_5`3`;
IS_SCS_IN_V_SY_5`4`];

REWRITE_TAC[E_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_5`1`;
IS_SCS_IN_V_SY_5`2`;
IS_SCS_IN_V_SY_5`3`;
IS_SCS_IN_V_SY_5`4`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_5`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_5 `5`;
PROVE_E_SY_INV_TAC_5 `1`;
PROVE_E_SY_INV_TAC_5 `2`;
PROVE_E_SY_INV_TAC_5 `3`;
PROVE_E_SY_INV_TAC_5 `4`];

REWRITE_TAC[F_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_5`1`;
IS_SCS_IN_V_SY_5`2`;
IS_SCS_IN_V_SY_5`3`;
IS_SCS_IN_V_SY_5`4`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_5`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_5 `5`;
PROVE_E_SY_INV_TAC_5 `1`;
PROVE_E_SY_INV_TAC_5 `2`;
PROVE_E_SY_INV_TAC_5 `3`;
PROVE_E_SY_INV_TAC_5 `4`];
]);;


let IS_SCS_IN_BALL_ANNULUS_5=
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_5[`(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`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
/\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
/\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
;;




let IN_IS_SCS_CASE_5=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=5 /\ 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) 3;(vv:num->real^3) 4;(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 /\ CONDITION2_SY 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;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

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

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

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`] 
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 5==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_5[`(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`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
/\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
/\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; 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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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 4`][periodic;ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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 4`][periodic;ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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 5`][periodic;ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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 5`][periodic;ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=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`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);

MP_TAC V_E_FF_IS_SCS_CASES_5
THEN ASM_REWRITE_TAC[]
THEN ASM_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;IN]
THEN RESA_TAC]);;



let INJ_H_FUN_TAC=
fun (so:term)->
STRIP_TAC
THENL[
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 5=2/\ 1+2=3 /\ 3 MOD 5=3/\ 1+3=4 /\ 5 MOD 5=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 5=4`]
THEN REPEAT STRIP_TAC)
THEN EXISTS_TAC so
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(1=0)/\ 2<5 /\ 2 MOD 5=2 /\ ~(2=0)/\ SUC 2=3/\ 3<5/\ 3 MOD 5=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 5=0/\ 0<5/\ SUC 0=1/\4<5 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 5=4`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
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 (j MOD 5)`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 5, j MOD 5}
==> (1 =i' MOD 5 /\ 2= j MOD 5)\/ (2 =i' MOD 5 /\ 1= j MOD 5)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 5, j MOD 5}
==> (2 =i' MOD 5 /\ 3= j MOD 5)\/ (3 =i' MOD 5 /\ 2= j MOD 5)`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 4`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 5, j MOD 5}
==> (3 =i' MOD 5 /\ 4= j MOD 5)\/ (4 =i' MOD 5 /\ 3= j MOD 5)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{4,0} = {i' MOD 5, j MOD 5}
==> (4=i' MOD 5 /\ 0=j MOD 5)\/ (0=i' MOD 5 /\  4=j MOD 5)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 5, j MOD 5}
==> (i' MOD 5=1 /\ j MOD 5=0)\/ (i' MOD 5=0 /\ j MOD 5=1)`)
THEN RESA_TAC;
REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]];;





let EXISTS_SCS_J_TAC=
fun (so:term) (so1:term) (so2:term)->
EXPAND_TAC "h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5`]
THEN STRIP_TAC
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_RULE`5 MOD 5=0/\ SUC 0=1/\ 1<=5/\ 5<=5/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=5/\ 1 MOD 5=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=5/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=5/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=5/\ SUC 4=5/\ 4 MOD 5=4/\ 1+4=5`]
THEN EXISTS_TAC so1
THEN EXISTS_TAC so2
THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ 1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 5 MOD 5=0/\ 4 MOD 5=4`]
;;





let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=5
/\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ 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= v
/\ matvec (v:real^3^M) =a
/\ 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))=s1
==>  taustar_v39 s vv = tau_star s1 a`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC V_E_FF_IS_SCS_CASES_5
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
THEN ASM_REWRITE_TAC[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 ASM_SIMP_TAC[dsv_J_empty]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
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 ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;

MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
THEN RESA_TAC
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[J1_SY ]
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ABBREV_TAC`h =(\i. if (i MOD 5 = 0) then (5,1) 
else (i MOD 5, SUC(i MOD 5)))`
THEN SUBGOAL_THEN`(!x x'.
      (x < 5 /\ scs_J_v39 s x (SUC x))  /\
      (x' < 5 /\ scs_J_v39 s x' (SUC x')) /\
      h x' = (h:num->num #num) x
      ==> x = x')` ASSUME_TAC;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE` x< 5 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4 `)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE` x'< 5 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3  \/ x'=4`)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0/\ 2 MOD 5=2/\ 3 MOD 5=3 /\ 4 MOD 5=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
THEN RESA_TAC;

EXISTS_TAC`h:num->(num#num)`
THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
THEN STRIP_TAC
THEN REPEAT STRIP_TAC;

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

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
THEN RESA_TAC
THENL[
EXISTS_SCS_J_TAC `5` `0` `1`;
EXISTS_SCS_J_TAC `1` `1` `2`;
EXISTS_SCS_J_TAC `2` `2` `3`;
EXISTS_SCS_J_TAC `3` `3` `4`;
EXISTS_SCS_J_TAC `4` `4` `5`];

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ SUC 0=1`]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MRESAL_TAC VECTOR_3_5[`(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`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1/\ ~(2=0) /\ ~(3=0)/\ ~(4=0)
/\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
/\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`;dist]
THEN REPLICATE_TAC 26 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(5=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`]);]);;



let JKQEWGV1_CASE_5=
prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s
 ==>
  (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
   (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_5
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_5
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`pi <=
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/ 
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
THEN RESA_TAC
THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC);;



let IS_SCS_IN_V_SY_6=
fun (so:term)->
 EXISTS_TAC so
THEN MRESAL_TAC VECTOR_3_6[`(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`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
/\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
;;


let PROVE_E_SY_INV_TAC_6=
fun (th:term)->
MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`6`][ARITH_RULE`~(6=0)/\ 4 MOD 6=4/\ SUC 0  MOD 6=1/\ 1 MOD 6=1 /\ 2 MOD 6=2 /\ 3 MOD 6=3/\ 6 MOD 6=0/\ 5 MOD 6=5`]
THEN EXISTS_TAC th
THEN MRESAL_TAC VECTOR_3_6[`(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`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
/\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
;;








let V_E_FF_IS_SCS_CASES_6=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=6 /\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ 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= v
/\ matvec (v:real^3^M) =a
==> 
V_SY (v:real^3^M)=IMAGE vv (:num)/\
  E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,

  (* {{{ proof *)
[
STRIP_TAC
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[scs_k_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 STRIP_TAC;

REWRITE_TAC[V_SY;rows]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`] 
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`] 
THEN GEN_TAC
THEN EQ_TAC;

REPEAT STRIP_TAC
THENL[
IS_SCS_IN_V_SY_6`1`;
IS_SCS_IN_V_SY_6`2`;
IS_SCS_IN_V_SY_6`3`;
IS_SCS_IN_V_SY_6`4`;
IS_SCS_IN_V_SY_6`5`;
IS_SCS_IN_V_SY_6`0`];

REPEAT STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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[
IS_SCS_IN_V_SY_6`6`;
IS_SCS_IN_V_SY_6`1`;
IS_SCS_IN_V_SY_6`2`;
IS_SCS_IN_V_SY_6`3`;
IS_SCS_IN_V_SY_6`4`;
IS_SCS_IN_V_SY_6`5`];

REWRITE_TAC[E_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_6`1`;
IS_SCS_IN_V_SY_6`2`;
IS_SCS_IN_V_SY_6`3`;
IS_SCS_IN_V_SY_6`4`;
IS_SCS_IN_V_SY_6`5`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_6`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_6 `6`;
PROVE_E_SY_INV_TAC_6 `1`;
PROVE_E_SY_INV_TAC_6 `2`;
PROVE_E_SY_INV_TAC_6 `3`;
PROVE_E_SY_INV_TAC_6 `4`;
PROVE_E_SY_INV_TAC_6 `5`;];

REWRITE_TAC[F_SY;rows]
THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`] 
THEN GEN_TAC
THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
THEN EQ_TAC;

RESA_TAC
THENL[
IS_SCS_IN_V_SY_6`1`;
IS_SCS_IN_V_SY_6`2`;
IS_SCS_IN_V_SY_6`3`;
IS_SCS_IN_V_SY_6`4`;
IS_SCS_IN_V_SY_6`5`
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
IS_SCS_IN_V_SY_6`0`];

STRIP_TAC
THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
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_INV_TAC_6 `6`;
PROVE_E_SY_INV_TAC_6 `1`;
PROVE_E_SY_INV_TAC_6 `2`;
PROVE_E_SY_INV_TAC_6 `3`;
PROVE_E_SY_INV_TAC_6 `4`;
PROVE_E_SY_INV_TAC_6 `5`;]]);;





let IS_SCS_IN_BALL_ANNULUS_6=
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_6[`(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`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
/\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
;;




let IN_IS_SCS_CASE_6=
prove_by_refinement(
` is_scs_v39 s /\ scs_k_v39 s=6 /\ 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) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(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 /\ CONDITION2_SY 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;

REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

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

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

STRIP_TAC;

REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`] 
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 6==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`)
THEN RESA_TAC
THEN MRESAL_TAC VECTOR_3_6[`(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`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
/\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; 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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 4`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 4`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 5`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 5`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 6`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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 6`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=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`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);

MP_TAC V_E_FF_IS_SCS_CASES_6
THEN ASM_REWRITE_TAC[]
THEN ASM_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;IN]
THEN RESA_TAC]);;



let INJ_H_FUN_TAC=
fun (so:term)->
STRIP_TAC
THENL[
POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 6=2/\ 1+2=3 /\ 3 MOD 6=3/\ 1+3=4 /\ 6 MOD 6=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 6=4/\ 1+5=6/\ 5 MOD 6=5`]
THEN REPEAT STRIP_TAC)
THEN EXISTS_TAC so
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(1=0)/\ 2<6 /\ 2 MOD 6=2 /\ ~(2=0)/\ SUC 2=3/\ 3<6/\ 3 MOD 6=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 6=0/\ 0<6/\ SUC 0=1/\4<6 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 6=4/\ SUC 5=6/\ ~(5=0)/\ 5 MOD 6=5/\ 5<6`]
THEN ASM_TAC
THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
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 (j MOD 6)`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 6, j MOD 6}
==> (1 =i' MOD 6 /\ 2= j MOD 6)\/ (2 =i' MOD 6 /\ 1= j MOD 6)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 6, j MOD 6}
==> (2 =i' MOD 6 /\ 3= j MOD 6)\/ (3 =i' MOD 6 /\ 2= j MOD 6)`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 5`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 6, j MOD 6}
==> (3 =i' MOD 6 /\ 4= j MOD 6)\/ (4 =i' MOD 6 /\ 3= j MOD 6)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{4,5} = {i' MOD 6, j MOD 6}
==> (4=i' MOD 6 /\ 5=j MOD 6)\/ (5=i' MOD 6 /\  4=j MOD 6)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{5,0} = {i' MOD 6, j MOD 6}
==> (5=i' MOD 6 /\ 0=j MOD 6)\/ (0=i' MOD 6 /\  5=j MOD 6)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 6, j MOD 6}
==> (i' MOD 6=1 /\ j MOD 6=0)\/ (i' MOD 6=0 /\ j MOD 6=1)`)
THEN RESA_TAC;
REPEAT STRIP_TAC
THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]];;










let EXISTS_SCS_J_TAC=
fun (so:term) (so1:term) (so2:term)->
EXPAND_TAC "h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`]
THEN STRIP_TAC
THEN EXISTS_TAC so
THEN ASM_REWRITE_TAC[ARITH_RULE`6 MOD 6=0/\ SUC 0=1/\ 1<=6/\ 6<=6/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=6/\ 1 MOD 6=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=6/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=6/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=6/\ SUC 4=5/\ 4 MOD 6=4/\ 1+4=5
/\ ~(5=0)/\ 1<=5/\ 5<=6/\ SUC 5=6/\ 5 MOD 6=5/\ 1+5=6`]
THEN EXISTS_TAC so1
THEN EXISTS_TAC so2
THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ 1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 6 MOD 6=0/\ 4 MOD 6=4/\ 5 MOD 6=5`]
;;











let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6=
prove_by_refinement(
`is_scs_v39 s /\ scs_k_v39 s=6
/\ vv IN BBs_v39 s
/\  dimindex(:M)=scs_k_v39 s
/\ 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= v
/\ matvec (v:real^3^M) =a
/\ 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))=s1
==>  taustar_v39 s vv = tau_star s1 a`,

  (* {{{ proof *)
[
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC V_E_FF_IS_SCS_CASES_6
THEN ASM_REWRITE_TAC[IN]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
THEN ASM_REWRITE_TAC[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 ASM_SIMP_TAC[dsv_J_empty]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
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 ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;

MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
THEN RESA_TAC
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[J1_SY ]
THEN MATCH_MP_TAC SUM_EQ_GENERAL
THEN ASM_REWRITE_TAC[IN_ELIM_THM]
THEN ABBREV_TAC`h =(\i. if (i MOD 6 = 0) then (6,1) 
else (i MOD 6, SUC(i MOD 6)))`
THEN SUBGOAL_THEN`(!x x'.
      (x < 6 /\ scs_J_v39 s x (SUC x))  /\
      (x' < 6 /\ scs_J_v39 s x' (SUC x')) /\
      h x' = (h:num->num #num) x
      ==> x = x')` ASSUME_TAC;

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE` x< 6 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4\/ x=5 `)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE` x'< 6 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3  \/ x'=4\/ x'=5`)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ 0 MOD 6=0/\ 2 MOD 6=2/\ 3 MOD 6=3 /\ 4 MOD 6=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=6)/\ ~(2=6)/\ ~(3=6)/\ ~(4=6)/\ ~(5=0)/\ 5 MOD 6=5 /\ SUC 5=6`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
THEN RESA_TAC;

EXISTS_TAC`h:num->(num#num)`
THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
THEN STRIP_TAC
THEN REPEAT STRIP_TAC;

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

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
THEN RESA_TAC
THENL[
EXISTS_SCS_J_TAC `6` `0` `1`;
EXISTS_SCS_J_TAC `1` `1` `2`;
EXISTS_SCS_J_TAC `2` `2` `3`;
EXISTS_SCS_J_TAC `3` `3` `4`;
EXISTS_SCS_J_TAC `4` `4` `5`;
EXISTS_SCS_J_TAC `5` `5` `6`];

POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
THEN RESA_TAC
THEN EXPAND_TAC"h"
THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ SUC 0=1`]
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MRESAL_TAC VECTOR_3_6[`(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`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ ~(5=0)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
/\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`;dist]
THEN REPLICATE_TAC 27 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(6=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])]);;



let JKQEWGV1_CASE_6=
prove(
`!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s
 ==>
  (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
   (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_6
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_6
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`pi <=
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/ 
  sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
  (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
THEN RESA_TAC
THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC);;



let IN_IMAGE_VV_EQ_3 =
fun (th:term)->
 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0  MOD 3=1/\ 1 MOD 3=1/\ SUC 1=2 /\ 2 MOD 3=2 /\ 3 MOD 3=0/\ SUC 2=3`]
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x'`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;SET_RULE`A IN {A,B,C} /\ B IN {A,B,C}/\ C IN {A,B,C}  `])
;;




let V_E_FF_IS_SCS_CASES_3=
prove_by_refinement(
` scs_k_v39 s=3/\ is_scs_v39 s  /\ BBs_v39 s vv 
/\ dimindex(:M)=scs_k_v39 s
 ==>
  ((IMAGE (\i. {vv i, vv (SUC i)}) (:num) ={{vv 0,vv 1},{vv 1, vv 2},{vv 2, vv 0}})
/\   (IMAGE (\i. (vv i,vv (SUC i))) (:num)= {(vv 0,vv 1),(vv 1, vv 2),(vv 2, vv 0)})  )`,

  (* {{{ proof *)
[
STRIP_TAC
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[scs_k_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 RESA_TAC
THEN REWRITE_TAC[ARITH_RULE`3<=3`]
THEN REPEAT STRIP_TAC;




ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN GEN_TAC
THEN EQ_TAC;

RESA_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[
IN_IMAGE_VV_EQ_3 `0`;
IN_IMAGE_VV_EQ_3 `1`;
IN_IMAGE_VV_EQ_3 `2`];


REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
THEN RESA_TAC;

EXISTS_TAC`0`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];

EXISTS_TAC`1`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];

EXISTS_TAC`2`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
;


ONCE_REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
THEN GEN_TAC
THEN EQ_TAC;

RESA_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[
IN_IMAGE_VV_EQ_3 `0`;
IN_IMAGE_VV_EQ_3 `1`;
IN_IMAGE_VV_EQ_3 `2`];


REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
THEN RESA_TAC
;

EXISTS_TAC`0`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];

EXISTS_TAC`1`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];

EXISTS_TAC`2`
THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]);
]);;


let IS_SCS_POINT_IN_BBS_IS_NOT_0_3=
prove_by_refinement(
`scs_k_v39 s=3/\ is_scs_v39 s
/\ vv IN BBs_v39 s
==> ~(vv 1= vec 0)/\  ~(vv 2= vec 0) /\ ~(vv 0= vec 0)`,

  (* {{{ proof *)
[
REWRITE_TAC[IN]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
THEN STRIP_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
EXISTS_TAC`2`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
REPLICATE_TAC 5(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;ball]
THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;ball]
THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;ball;])
THEN STRIP_TAC;
STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
STRIP_TAC;
STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
STRIP_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`])
]);;
  (* }}} *)



let IS_SCS_NOT_COLLINEAR_BBs_CASE_3=
prove_by_refinement(
`scs_k_v39 s=3/\ is_scs_v39 s
/\ vv IN BBs_v39 s
==> ~collinear{vec 0, vv 1 ,vv 2}/\
 ~collinear{vec 0, vv 1 ,vv 0}/\
 ~collinear{vec 0, vv 2 ,vv 0}`,

  (* {{{ proof *)
[


REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`]
THEN STRIP_TAC
THEN MP_TAC IS_SCS_POINT_IN_BBS_IS_NOT_0_3
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
THEN POP_ASSUM(fun th->
STRIP_TAC
THEN ASSUME_TAC th)
THEN REPEAT STRIP_TAC;

REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`2`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];


REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
THEN STRIP_TAC
;


 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC
;


MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= (&1 - v) * norm (vv 1)
/\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
;




MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
/\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SYM th])
THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`1`[ARITH_RULE`SUC 1=2`])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;




 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC
;







MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
/\ &2 <= scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
;


MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
/\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;





REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];


REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
THEN STRIP_TAC
;


 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC
;


MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= (&1 - v) * norm (vv 1)
/\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
/\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SYM th])
THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`0`[ARITH_RULE`SUC 0=1`])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC;


MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
/\ &2 <= scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
;


MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
/\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;



REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)/\ ~(0=2)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`2`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;


EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];


REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
THEN STRIP_TAC
;


 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC
;


MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= (&1 - v) * norm (vv 2)
/\ &2 <= v * norm (vv 2) ==> &4<= norm ((vv:num->real^3) 2)`)
THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
;




MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 2)
/\ &2 <= norm (vv 2) ==> &4<=(&1- v) *norm ((vv:num->real^3) 2)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SYM th])
THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MRESAL1_TAC th`2`[ARITH_RULE`SUC 2=3`])
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
THEN ASM_TAC
THEN REWRITE_TAC[periodic2]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s 2`][ARITH_RULE`~(3=0)`;periodic]
THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
THEN REAL_ARITH_TAC;




 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC
;







MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 2)
/\ &2 <= scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= --(&1 - v) * norm (vv 2) ==> &4<= v *norm ((vv:num->real^3) 2)`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC
;


MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 2)
/\ &2 <= --v * norm (vv 2) ==> &4<= (&1-v) *norm ((vv:num->real^3) 2)`)
THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
]);;
  (* }}} *)




let IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3=
prove_by_refinement(
`3<scs_k_v39 s/\ is_scs_v39 s
/\ vv IN BBs_v39 s
==> ~(vv i= vec 0)`,

[REWRITE_TAC[IN]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<scs_k_v39 s==> ~(scs_k_v39 s<=3)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
THEN STRIP_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv i= (vv:num->real^3) x)`ASSUME_TAC;
EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
REPLICATE_TAC 4(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL1_TAC th`(vv:num->real^3) i`[ball_annulus;IN_ELIM_THM;DIFF;ball])
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[DIST_REFL;REAL_ARITH`(&0< &2)`]
]);;
  (* }}} *)




let IS_SCS_NOT_COLLINEAR_BBs_CASE_LE_3=
prove_by_refinement(
`3< scs_k_v39 s/\ is_scs_v39 s
/\ vv IN BBs_v39 s
/\ ~(i MOD (scs_k_v39 s)=j MOD (scs_k_v39 s))
/\ dist(vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))) <= cstab
==> ~collinear{vec 0, vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))}`,

[
REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`;cstab]
THEN STRIP_TAC
THEN MRESA_TAC( GEN_ALL IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3)[`s:scs_v39`;`vv:num->real^3`;`i MOD scs_k_v39 s`]
THEN RESA_TAC
THEN ASM_TAC
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
THEN POP_ASSUM(fun th->
STRIP_TAC
THEN ASSUME_TAC th)
THEN REPEAT STRIP_TAC;

MP_TAC(ARITH_RULE`3 < scs_k_v39 s==> ~(scs_k_v39 s <= 3)`)
THEN RESA_TAC;


ABBREV_TAC`k=scs_k_v39 s`
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN REPLICATE_TAC (35-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (34-22) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
THEN REPLICATE_TAC (35-20)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv (i MOD k) = (vv:num->real^3) x)`ASSUME_TAC;

EXISTS_TAC`i MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ vv (j MOD k) = (vv:num->real^3) x)`ASSUME_TAC;

EXISTS_TAC`j MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
THEN STRIP_TAC
THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) (i MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
THEN MRESAL1_TAC th`(vv:num->real^3) (j MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
THEN STRIP_TAC;

 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC;

MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= (&1 - v) * norm (vv (i MOD k))
/\ &2 <= v * norm (vv (i MOD k)) ==> &4<= norm ((vv:num->real^3) (i MOD k))`)
THEN REPLICATE_TAC 6(POP_ASSUM MP_TAC)
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;


MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv (i MOD k))
/\ &2 <= norm (vv (i MOD k)) ==> &4<=(&1- v) *norm ((vv:num->real^3) (i MOD k) )`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC (45-35)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN ASM_REWRITE_TAC[])
THEN REAL_ARITH_TAC;

MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
THEN STRIP_TAC;


MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv (i MOD k))
/\ &2 <= scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= --(&1 - v) * norm (vv (i MOD k)) ==> &4<= v *norm ((vv:num->real^3) (i MOD k))`)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th; ]
THEN REPEAT STRIP_TAC)
THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv (i MOD k))
/\ &2 <= --v * norm (vv (i MOD k)) ==> &4<= (&1-v) *norm ((vv:num->real^3) (i MOD k))`)
THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
THEN REPLICATE_TAC (45-32)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC (44-32)(POP_ASSUM MP_TAC)
THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
]);;
  (* }}} *)












let JKQEWGV1=
prove(
`!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
 ==>
  (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
   (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,

REPEAT STRIP_TAC
THEN ASM_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[is_scs_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\  scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
THEN RESA_TAC
THENL[
MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV1_CASE_4)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);

MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV1_CASE_5)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);

MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV1_CASE_6)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;



let JKQEWGV2_CASE_4=
prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s 
==>
  (
    let V = IMAGE vv (:num) in
  let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
  ~circular V E)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_4
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_4
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN POP_ASSUM MATCH_MP_TAC
THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC);;


let JKQEWGV2_CASE_5=
prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s 
==>
  (
    let V = IMAGE vv (:num) in
  let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
  ~circular V E)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_5
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_5
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN POP_ASSUM MATCH_MP_TAC
THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC);;




let JKQEWGV2_CASE_6=
prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
/\ dimindex(:M)=scs_k_v39 s 
==>
  (
    let V = IMAGE vv (:num) in
  let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
  ~circular V E)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
THEN STRIP_TAC
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 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 MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
THEN STRIP_TAC
THEN MP_TAC IN_IS_SCS_CASE_6
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC"a"
THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
THEN MP_TAC V_E_FF_IS_SCS_CASES_6
THEN ASM_REWRITE_TAC[IN]
THEN RESA_TAC
THEN ASM_TAC
THEN ASM_REWRITE_TAC[is_scs_v39;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
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[]
THEN POP_ASSUM MATCH_MP_TAC
THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
THEN RESA_TAC);;



let JKQEWGV2=
prove(
`!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
 ==>
  (
    let V = IMAGE vv (:num) in
  let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
  ~circular V E)`,

REPEAT STRIP_TAC
THEN ASM_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[is_scs_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\  scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
THEN RESA_TAC
THENL[
MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV2_CASE_4)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);

MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV2_CASE_5)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);

MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV2_CASE_6)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;




let JKQEWGV3 = 
prove_by_refinement(
`!s vv v w. 
  (let V = IMAGE vv (:num) in
   let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
   let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
     (is_scs_v39 s /\ BBs_v39 s vv /\ 3< scs_k_v39 s /\ taustar_v39 s vv < &0 /\ lunar (v,w) V E ==>
	(interior_angle1 (vec 0) FF v  < pi / &2 )))`,

  (* {{{ proof *)
[
REWRITE_TAC[LET_DEF;LET_END_DEF;]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM(fun th-> MP_TAC th
THEN REWRITE_TAC[lunar]
THEN ASSUME_TAC th)
THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)`
THEN ABBREV_TAC`E= IMAGE (\i. {vv i,(vv:num->real^3) (SUC i)}) (:num)`
THEN ABBREV_TAC`FF= IMAGE (\i. (vv i,(vv:num->real^3) (SUC i))) (:num)`
THEN MRESA_TAC (GEN_ALL HKIRPEP)[`E:(real^3->bool)->bool`;`w:real^3`;`FF:real^3#real^3->bool`;`v:real^3`;`V:real^3->bool`]
THEN ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th
THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s==> ~( scs_k_v39 s<= 3)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
THEN STRIP_TAC
THEN ASSUME_TAC th)
THEN MP_TAC(SET_RULE`{v, w:real^3} SUBSET V ==> v IN V /\ w IN V`)
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
[`IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)`;`IMAGE ((vv:num->real^3)) (:num)`;`IMAGE (\i. ((vv:num->real^3) i,vv (SUC i))) (:num)`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`vv:num->real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[sol_local]
THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th)
THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC 3 STRIP_TAC 
THEN MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
THEN REWRITE_TAC[th]
THEN ASSUME_TAC th
THEN MP_TAC th
THEN REWRITE_TAC[convex_local_fan]
THEN REPEAT STRIP_TAC)
THEN POP_ASSUM MP_TAC
THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF
THEN RESA_TAC
THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`
THEN MRESA1_TAC th`w:real^3`)
THEN MP_TAC(SET_RULE`v,rho_node1 FF v IN FF/\
w,rho_node1 FF w IN FF ==>
{(v,rho_node1 FF v ),(w,rho_node1 FF w)} SUBSET FF`)
THEN RESA_TAC
THEN MRESA_TAC SUM_DIFF[`(\e:real^3#real^3. azim_in_fan e E - pi)`;`FF:real^3#real^3->bool`;`{(v,rho_node1 FF v),(w,rho_node1 FF w)}`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`A=B-C<=> B=A+C`]
THEN RESA_TAC
THEN MRESAL_TAC Geomdetail.SUM_DIS2[`(v,rho_node1 FF v)`;`(w,rho_node1 FF w)`;`(\e:real^3#real^3. azim_in_fan e E - pi)`][PAIR_EQ]
THEN SUBGOAL_THEN`sum (FF DIFF {(v,rho_node1 FF v), (w,rho_node1 FF w)})
 (\e. azim_in_fan e E - pi)= &0` ASSUME_TAC;

MATCH_MP_TAC SUM_EQ_0
THEN REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC 8 STRIP_TAC 
THEN MRESA1_TAC th`x:real^3#real^3`)
THEN POP_ASSUM(fun th->   REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
THEN ONCE_REWRITE_TAC[th]
THEN REWRITE_TAC[PAIR_EQ])
THEN REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`V:real^3->bool`]
THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC 13 STRIP_TAC 
THEN MRESA1_TAC th`FST (x:real^3#real^3)`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN SUBGOAL_THEN`FST (x:real^3#real^3) IN V DIFF {v,w}`ASSUME_TAC;

ASM_REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[];

REPLICATE_TAC (34-7) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC (34-7) STRIP_TAC 
THEN MP_TAC th
THEN RESA_TAC)
THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
THEN POP_ASSUM (fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`)
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC 10 STRIP_TAC 
THEN MRESA1_TAC th`v:real^3`
THEN MRESA1_TAC th`w:real^3`)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPLICATE_TAC (30-7) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC (30-7) STRIP_TAC 
THEN MP_TAC th)
THEN REPLICATE_TAC (12) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th->   REPLICATE_TAC (12) STRIP_TAC 
THEN REWRITE_TAC[th])
THEN STRIP_TAC
THEN REPLICATE_TAC (10) (REMOVE_ASSUM_TAC)
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC]);;






 end;;


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