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


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


module Uxckfpe = struct

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

open Hales_tactic;;

open Appendix;;





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

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


let NOT_EMPTY_CASE_4_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ dimindex(:M)= scs_k_v39 s ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;] THEN STRIP_TAC THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M` THEN ABBREV_TAC`a=matvec (v:real^3^M) ` THEN EXISTS_TAC`a:real^(M,3)finite_product` THEN MATCH_MP_TAC IN_IS_SCS_CASE_4 THEN ASM_REWRITE_TAC[]]);;
let ARITH_4_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 4 MOD 4=0/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 4=1/\ 1<=1/\ 1<=4/\ 1 MOD 4=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 4=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 4=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 4=1/\ ~(4=0)/\ 0 MOD 4=0`;;
let VV_IN_BALL_ANNULUS_TAC_4= fun (so:term)-> REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th so[ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN]) ;; let SCS_A_LE_NORM_4_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_4= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`) THEN RESA_TAC THENL[ SCS_A_LE_NORM_4_IS_SCS th `4`; SCS_A_LE_NORM_4_IS_SCS th `1`; SCS_A_LE_NORM_4_IS_SCS th `2`; SCS_A_LE_NORM_4_IS_SCS th `3`];; let SCS_B_LE_NORM_4_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (4)`][ARITH_RULE`~(4=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_4B= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`) THEN RESA_TAC THENL[ SCS_B_LE_NORM_4_IS_SCS th `4`; SCS_B_LE_NORM_4_IS_SCS th `1`; SCS_B_LE_NORM_4_IS_SCS th `2`; SCS_B_LE_NORM_4_IS_SCS th `3`];; let V_SY_EQ_IMAGE_VV_TAC4= fun (th:term)-> ASM_REWRITE_TAC[] THEN EXISTS_TAC th THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_4_TAC];; let PROVE_E_SY_EQ_MOD_TAC_4= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_4_TAC] ;; let PROOF_E_EQ_TAC_4= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_4_TAC;] ;; let PROVE_E_SY_EQ_IMAGE_VV_4= fun (so:term) (so1:term)-> MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_4_TAC] THEN EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_4_TAC];;
let  IN_NOT_EMPTY_B1_SY_4_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ scs_k_v39 s=4 /\ dimindex(:M) = scs_k_v39 s/\ matvec (v:real^3^M) =a/\ (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v /\ (!i. vv i = if i MOD scs_k_v39 s = 0 then row 4 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else row 3 v) ==> vv IN BBs_v39 s`,
[ REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;] THEN REPEAT RESA_TAC; ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`x' MOD 4<4 ==> x' MOD 4 = 0 \/ x' MOD 4 = 1 \/ x' MOD 4 = 2 \/ x' MOD 4 = 3`) THEN RESA_TAC THENL[ VV_IN_BALL_ANNULUS_TAC_4 `4`; VV_IN_BALL_ANNULUS_TAC_4 `1`; VV_IN_BALL_ANNULUS_TAC_4 `2`; VV_IN_BALL_ANNULUS_TAC_4 `3`]; ASM_REWRITE_TAC[periodic] THEN GEN_TAC THEN MRESAL_TAC MOD_EQ[`i+4:num`;`i:num`;`4:num`;`1`][ARITH_RULE`1*A=A`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`]; MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_4 `4`; PROVE_INEQUALITY_TAC_4 `1`; PROVE_INEQUALITY_TAC_4 `2`; PROVE_INEQUALITY_TAC_4 `3`] ; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`]; MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_4B `4`; PROVE_INEQUALITY_TAC_4B `1`; PROVE_INEQUALITY_TAC_4B `2`; PROVE_INEQUALITY_TAC_4B `3`] ; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`~(4<=3)`] THEN STRIP_TAC THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC; ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`] THEN STRIP_TAC THENL[ V_SY_EQ_IMAGE_VV_TAC4 `1`; V_SY_EQ_IMAGE_VV_TAC4 `2`; V_SY_EQ_IMAGE_VV_TAC4 `3`; V_SY_EQ_IMAGE_VV_TAC4 `4`]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_MOD_TAC_4 `4`; PROVE_E_SY_EQ_MOD_TAC_4 `1`; PROVE_E_SY_EQ_MOD_TAC_4 `2`; PROVE_E_SY_EQ_MOD_TAC_4 `3`] ; SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[E_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC ; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_4`1`; PROOF_E_EQ_TAC_4`2`; PROOF_E_EQ_TAC_4`3`; PROOF_E_EQ_TAC_4`4`] ; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`; PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`]; SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[F_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC ; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_4`1`; PROOF_E_EQ_TAC_4`2`; PROOF_E_EQ_TAC_4`3`; PROOF_E_EQ_TAC_4`4`] ; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 4<4)==> (x' MOD 4=0) \/ (x' MOD 4=1) \/ (x' MOD 4=2)\/ (x' MOD 4=3)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`; PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`]; REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let XWITCCN_CASE_4_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ BBs_v39 s vv /\ scs_k_v39 s=4 /\ dimindex(:M) =scs_k_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`,
(* {{{ proof *) [ STRIP_TAC THEN MP_TAC IS_SCS_STABLE_SYSTEM THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`] THEN STRIP_TAC THEN MP_TAC NOT_EMPTY_CASE_4_IS_SCS THEN RESA_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`] THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1), (change_type_v3 (scs_a_v39 s)), (change_type_v3 (scs_b_v39 s)), (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)), (\i. (1 + i) MOD scs_k_v39 s))` THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;` (change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;` (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;` (\i. (1 + i) MOD scs_k_v39 s)`] THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<4`;] THEN POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN REWRITE_TAC[BBprime_v39;IN] THEN ABBREV_TAC`( vv1 i = if i MOD scs_k_v39 s = 0 then row 4 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else row 3 (v:real^3^M))` THEN EXISTS_TAC`vv1:num->real^3` THEN STRIP_TAC; ONCE_REWRITE_TAC[GSYM IN] THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS) THEN EXISTS_TAC`x:real^(M,3)finite_product` THEN EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC ; SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 0] = v:real^3^M` ASSUME_TAC; POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 0 MOD 4=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;] THEN ONCE_REWRITE_TAC[CART_EQ] THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=4 <=>i=1\/ i=2\/ i=3\/ i=4`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA]; STRIP_TAC; GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4) [`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;] THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th THEN REWRITE_TAC[IN] THEN STRIP_TAC) THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC THEN REWRITE_TAC[th] THEN RESA_TAC) THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`); MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4) [`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;] THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN ASM_REWRITE_TAC[IN] THEN STRIP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`) THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *) (*************CASE 5****************)
let NOT_EMPTY_CASE_5_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ dimindex(:M)= scs_k_v39 s ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;] THEN STRIP_TAC THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M` THEN ABBREV_TAC`a=matvec (v:real^3^M) ` THEN EXISTS_TAC`a:real^(M,3)finite_product` THEN MATCH_MP_TAC IN_IS_SCS_CASE_5 THEN ASM_REWRITE_TAC[]]);;
let ARITH_5_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=5/\3<=5/\5<=5 /\ 4<=5/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=4/\ 4 MOD 5=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 5=0/\ ~(4=0)/\ 0 MOD 5=0
/\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)
`;;
let VV_IN_BALL_ANNULUS_TAC_5= fun (so:term)-> REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th so[ARITH_5_TAC;IN]) ;; let SCS_A_LE_NORM_5_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_5= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`) THEN RESA_TAC THENL[ SCS_A_LE_NORM_5_IS_SCS th `5`; SCS_A_LE_NORM_5_IS_SCS th `1`; SCS_A_LE_NORM_5_IS_SCS th `2`; SCS_A_LE_NORM_5_IS_SCS th `3`; SCS_A_LE_NORM_5_IS_SCS th `4`];; let SCS_B_LE_NORM_5_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (5)`][ARITH_RULE`~(5=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_5B= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`) THEN RESA_TAC THENL[ SCS_B_LE_NORM_5_IS_SCS th `5`; SCS_B_LE_NORM_5_IS_SCS th `1`; SCS_B_LE_NORM_5_IS_SCS th `2`; SCS_B_LE_NORM_5_IS_SCS th `3`; SCS_B_LE_NORM_5_IS_SCS th `4`];; let V_SY_EQ_IMAGE_VV_TAC5= fun (th:term)-> ASM_REWRITE_TAC[] THEN EXISTS_TAC th THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_5_TAC];; let PROVE_E_SY_EQ_MOD_TAC_5= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_5_TAC] ;; let PROOF_E_EQ_TAC_5= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_5_TAC;] ;; let PROVE_E_SY_EQ_IMAGE_VV_5= fun (so:term) (so1:term)-> MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_5_TAC] THEN EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_5_TAC];;
let  IN_NOT_EMPTY_B1_SY_5_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ scs_k_v39 s=5 /\ dimindex(:M) = scs_k_v39 s/\ matvec (v:real^3^M) =a/\ (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v /\ (!i. vv i = if i MOD scs_k_v39 s = 0 then row 5 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else if i MOD scs_k_v39 s = 3 then row 3 v else row 4 v) ==> vv IN BBs_v39 s`,
[ REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39;] THEN REPEAT RESA_TAC; ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`x' MOD 5<5 ==> x' MOD 5 = 0 \/ x' MOD 5 = 1 \/ x' MOD 5 = 2 \/ x' MOD 5 = 3\/ x' MOD 5 = 4`) THEN RESA_TAC THENL[ VV_IN_BALL_ANNULUS_TAC_5 `5`; VV_IN_BALL_ANNULUS_TAC_5 `1`; VV_IN_BALL_ANNULUS_TAC_5 `2`; VV_IN_BALL_ANNULUS_TAC_5 `3`; VV_IN_BALL_ANNULUS_TAC_5 `4`]; ASM_REWRITE_TAC[periodic] THEN GEN_TAC THEN MRESAL_TAC MOD_EQ[`i+5:num`;`i:num`;`5:num`;`1`][ARITH_RULE`1*A=A`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`]; MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_5 `5`; PROVE_INEQUALITY_TAC_5 `1`; PROVE_INEQUALITY_TAC_5 `2`; PROVE_INEQUALITY_TAC_5 `3`; PROVE_INEQUALITY_TAC_5 `4`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`]; MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_5B `5`; PROVE_INEQUALITY_TAC_5B `1`; PROVE_INEQUALITY_TAC_5B `2`; PROVE_INEQUALITY_TAC_5B `3`; PROVE_INEQUALITY_TAC_5B `4`]; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`] THEN STRIP_TAC THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC; ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5`] THEN STRIP_TAC THENL[ V_SY_EQ_IMAGE_VV_TAC5 `1`; V_SY_EQ_IMAGE_VV_TAC5 `2`; V_SY_EQ_IMAGE_VV_TAC5 `3`; V_SY_EQ_IMAGE_VV_TAC5 `4`; V_SY_EQ_IMAGE_VV_TAC5 `5`;]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3)\/ (x' MOD 5=4)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_MOD_TAC_5 `5`; PROVE_E_SY_EQ_MOD_TAC_5 `1`; PROVE_E_SY_EQ_MOD_TAC_5 `2`; PROVE_E_SY_EQ_MOD_TAC_5 `3`; PROVE_E_SY_EQ_MOD_TAC_5 `4`]; SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[E_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_5`1`; PROOF_E_EQ_TAC_5`2`; PROOF_E_EQ_TAC_5`3`; PROOF_E_EQ_TAC_5`4`; PROOF_E_EQ_TAC_5`5`]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`; PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`; PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`]; SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[F_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_5`1`; PROOF_E_EQ_TAC_5`2`; PROOF_E_EQ_TAC_5`3`; PROOF_E_EQ_TAC_5`4`; PROOF_E_EQ_TAC_5`5`]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 5<5)==> (x' MOD 5=0) \/ (x' MOD 5=1) \/ (x' MOD 5=2)\/ (x' MOD 5=3) \/ (x' MOD 5=4)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`; PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`; PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`]; REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let XWITCCN_CASE_5_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ BBs_v39 s vv /\ scs_k_v39 s=5 /\ dimindex(:M) =scs_k_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`,
(* {{{ proof *) [ STRIP_TAC THEN MP_TAC IS_SCS_STABLE_SYSTEM THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`] THEN STRIP_TAC THEN MP_TAC NOT_EMPTY_CASE_5_IS_SCS THEN RESA_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`] THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1), (change_type_v3 (scs_a_v39 s)), (change_type_v3 (scs_b_v39 s)), (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)), (\i. (1 + i) MOD scs_k_v39 s))` THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;` (change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;` (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;` (\i. (1 + i) MOD scs_k_v39 s)`] THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<5`;] THEN POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN REWRITE_TAC[BBprime_v39;IN] THEN ABBREV_TAC`( vv1 i = if i MOD scs_k_v39 s = 0 then row 5 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else if i MOD scs_k_v39 s = 3 then row 3 v else row 4 (v:real^3^M))` THEN EXISTS_TAC`vv1:num->real^3` THEN STRIP_TAC; ONCE_REWRITE_TAC[GSYM IN] THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS) THEN EXISTS_TAC`x:real^(M,3)finite_product` THEN EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC; SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 0] = v:real^3^M` ASSUME_TAC; POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 0 MOD 5=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 5=4`;] THEN ONCE_REWRITE_TAC[CART_EQ] THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=5 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN REWRITE_TAC[num_CONV `4`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA]; STRIP_TAC; GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5) [`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;] THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th THEN REWRITE_TAC[IN] THEN STRIP_TAC) THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC THEN REWRITE_TAC[th] THEN RESA_TAC) THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`); MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5) [`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;] THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN ASM_REWRITE_TAC[IN] THEN STRIP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`) THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *) (*************CASE 6****************)
let NOT_EMPTY_CASE_6_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ dimindex(:M)= scs_k_v39 s ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }={})`,
[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;] THEN STRIP_TAC THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M` THEN ABBREV_TAC`a=matvec (v:real^3^M) ` THEN EXISTS_TAC`a:real^(M,3)finite_product` THEN MATCH_MP_TAC IN_IS_SCS_CASE_6 THEN ASM_REWRITE_TAC[]]);;
let ARITH_6_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=6/\3<=6/\5<=6 /\ 4<=6/\5<=6/\ 6<=6/\ 1<=6 /\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=4/\ 4 MOD 6=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 6=5/\ ~(4=0)/\ 0 MOD 6=0/\ 6 MOD 6=0/\ 7 MOD 6=1 /\ SUC 6=7
/\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)/\ ~(6=0)
/\ ~(5=1)/\ ~(5=2)/\ ~(5=3)/\ ~(5=4)`;;
let VV_IN_BALL_ANNULUS_TAC_6= fun (so:term)-> REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th so[ARITH_6_TAC;IN]) ;; let SCS_A_LE_NORM_6_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_6= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`) THEN RESA_TAC THENL[ SCS_A_LE_NORM_6_IS_SCS th `6`; SCS_A_LE_NORM_6_IS_SCS th `1`; SCS_A_LE_NORM_6_IS_SCS th `2`; SCS_A_LE_NORM_6_IS_SCS th `3`; SCS_A_LE_NORM_6_IS_SCS th `4`; SCS_A_LE_NORM_6_IS_SCS th `5`];; let SCS_B_LE_NORM_6_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (6)`][ARITH_RULE`~(6=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_6B= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`) THEN RESA_TAC THENL[ SCS_B_LE_NORM_6_IS_SCS th `6`; SCS_B_LE_NORM_6_IS_SCS th `1`; SCS_B_LE_NORM_6_IS_SCS th `2`; SCS_B_LE_NORM_6_IS_SCS th `3`; SCS_B_LE_NORM_6_IS_SCS th `4`; SCS_B_LE_NORM_6_IS_SCS th `5`];; let V_SY_EQ_IMAGE_VV_TAC6= fun (th:term)-> ASM_REWRITE_TAC[] THEN EXISTS_TAC th THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_6_TAC];; let PROVE_E_SY_EQ_MOD_TAC_6= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_6_TAC] ;; let PROOF_E_EQ_TAC_6= fun (so:term)-> EXISTS_TAC so THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_6_TAC;] ;; let PROVE_E_SY_EQ_IMAGE_VV_6= fun (so:term) (so1:term)-> MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_6_TAC] THEN EXISTS_TAC so THEN ASM_REWRITE_TAC[ARITH_6_TAC];;
let  IN_NOT_EMPTY_B1_SY_6_IS_SCS=
prove_by_refinement(`is_scs_v39 s /\ scs_k_v39 s=6 /\ dimindex(:M) = scs_k_v39 s/\ matvec (v:real^3^M) =a/\ (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v /\ (!i. vv i = if i MOD scs_k_v39 s = 0 then row 6 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else if i MOD scs_k_v39 s = 3 then row 3 v else if i MOD scs_k_v39 s = 4 then row 4 v else row 5 v) ==> vv IN BBs_v39 s`,
[ REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39;] THEN REPEAT RESA_TAC; ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`x' MOD 6<6 ==> x' MOD 6 = 0 \/ x' MOD 6 = 1 \/ x' MOD 6 = 2 \/ x' MOD 6 = 3\/ x' MOD 6 = 4\/ x' MOD 6 = 5`) THEN RESA_TAC THENL[ VV_IN_BALL_ANNULUS_TAC_6 `6`; VV_IN_BALL_ANNULUS_TAC_6 `1`; VV_IN_BALL_ANNULUS_TAC_6 `2`; VV_IN_BALL_ANNULUS_TAC_6 `3`; VV_IN_BALL_ANNULUS_TAC_6 `4`; VV_IN_BALL_ANNULUS_TAC_6 `5`]; ASM_REWRITE_TAC[periodic] THEN GEN_TAC THEN MRESAL_TAC MOD_EQ[`i+6:num`;`i:num`;`6:num`;`1`][ARITH_RULE`1*A=A`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`]; MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_6 `6`; PROVE_INEQUALITY_TAC_6 `1`; PROVE_INEQUALITY_TAC_6 `2`; PROVE_INEQUALITY_TAC_6 `3`; PROVE_INEQUALITY_TAC_6 `4`; PROVE_INEQUALITY_TAC_6 `5`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`]; MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_6B `6`; PROVE_INEQUALITY_TAC_6B `1`; PROVE_INEQUALITY_TAC_6B `2`; PROVE_INEQUALITY_TAC_6B `3`; PROVE_INEQUALITY_TAC_6B `4`; PROVE_INEQUALITY_TAC_6B `5`]; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`] THEN STRIP_TAC THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC; ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5\/ i=6`] THEN STRIP_TAC THENL[ V_SY_EQ_IMAGE_VV_TAC6 `1`; V_SY_EQ_IMAGE_VV_TAC6 `2`; V_SY_EQ_IMAGE_VV_TAC6 `3`; V_SY_EQ_IMAGE_VV_TAC6 `4`; V_SY_EQ_IMAGE_VV_TAC6 `5`; V_SY_EQ_IMAGE_VV_TAC6 `6`;]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3)\/ (x' MOD 6=4)\/ (x' MOD 6=5)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_MOD_TAC_6 `6`; PROVE_E_SY_EQ_MOD_TAC_6 `1`; PROVE_E_SY_EQ_MOD_TAC_6 `2`; PROVE_E_SY_EQ_MOD_TAC_6 `3`; PROVE_E_SY_EQ_MOD_TAC_6 `4`; PROVE_E_SY_EQ_MOD_TAC_6 `5`;]; SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[E_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_6`1`; PROOF_E_EQ_TAC_6`2`; PROOF_E_EQ_TAC_6`3`; PROOF_E_EQ_TAC_6`4`; PROOF_E_EQ_TAC_6`5`; PROOF_E_EQ_TAC_6`6`]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`; PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`; PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`; PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`]; SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC; ASM_REWRITE_TAC[F_SY;rows;IMAGE;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`] THEN RESA_TAC THENL[ PROOF_E_EQ_TAC_6`1`; PROOF_E_EQ_TAC_6`2`; PROOF_E_EQ_TAC_6`3`; PROOF_E_EQ_TAC_6`4`; PROOF_E_EQ_TAC_6`5`; PROOF_E_EQ_TAC_6`6`]; RESA_TAC THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`] THEN MP_TAC(ARITH_RULE`(x' MOD 6<6)==> (x' MOD 6=0) \/ (x' MOD 6=1) \/ (x' MOD 6=2)\/ (x' MOD 6=3) \/ (x' MOD 6=4)\/ (x' MOD 6=5)`) THEN RESA_TAC THENL[ PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`; PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`; PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`; PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`; PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`; PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`]; REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let XWITCCN_CASE_6_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ BBs_v39 s vv /\ scs_k_v39 s=6 /\ dimindex(:M) =scs_k_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`,
(* {{{ proof *) [ STRIP_TAC THEN MP_TAC IS_SCS_STABLE_SYSTEM THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`] THEN STRIP_TAC THEN MP_TAC NOT_EMPTY_CASE_6_IS_SCS THEN RESA_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`] THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1), (change_type_v3 (scs_a_v39 s)), (change_type_v3 (scs_b_v39 s)), (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)), (\i. (1 + i) MOD scs_k_v39 s))` THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;` (change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;` (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;` (\i. (1 + i) MOD scs_k_v39 s)`] THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<6`;] THEN POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN REWRITE_TAC[BBprime_v39;IN] THEN ABBREV_TAC`( vv1 i = if i MOD scs_k_v39 s = 0 then row 6 v else if i MOD scs_k_v39 s = 1 then row 1 v else if i MOD scs_k_v39 s = 2 then row 2 v else if i MOD scs_k_v39 s = 3 then row 3 v else if i MOD scs_k_v39 s = 4 then row 4 v else row 5 (v:real^3^M))` THEN EXISTS_TAC`vv1:num->real^3` THEN STRIP_TAC; ONCE_REWRITE_TAC[GSYM IN] THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS) THEN EXISTS_TAC`x:real^(M,3)finite_product` THEN EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC; SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 5; vv1 0] = v:real^3^M` ASSUME_TAC; POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 0 MOD 6 =0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 6=4/\ 5 MOD 6=5/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)/\ ~(0=5)`;] THEN ONCE_REWRITE_TAC[CART_EQ] THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=6 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5\/ i=6`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN REWRITE_TAC[num_CONV `4`;num_CONV `5`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA]; STRIP_TAC; GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6) [`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;] THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th THEN REWRITE_TAC[IN] THEN STRIP_TAC) THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC THEN REWRITE_TAC[th] THEN RESA_TAC) THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`); MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`] THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6) [`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;] THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;] THEN ASM_REWRITE_TAC[IN] THEN STRIP_TAC THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5;vv 0]:real^3^M):real^(M,3)finite_product`) THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *) (****************CASE 3**************) let IS_SCS_IN_BALL_ANNULUS_3= fun (so:term)-> REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]) THEN STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC so THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1) /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`] ;;
let IN_IS_SCS_CASE_3=
prove_by_refinement( ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv /\ dimindex(:M)= scs_k_v39 s /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v /\ matvec (v:real^3^M) =a ==> a IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v }`,
(* {{{ proof *) [ REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist] THEN STRIP_TAC; EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`] THEN REPEAT STRIP_TAC THENL[ IS_SCS_IN_BALL_ANNULUS_3 `1`; IS_SCS_IN_BALL_ANNULUS_3 `2`; IS_SCS_IN_BALL_ANNULUS_3 `0`]; REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`) THEN RESA_TAC THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1) /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN STRIP_TAC THEN REPEAT DISCH_TAC THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;]) THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`]; EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`] THEN REPEAT STRIP_TAC THENL[ IS_SCS_IN_BALL_ANNULUS_3 `1`; IS_SCS_IN_BALL_ANNULUS_3 `2`; IS_SCS_IN_BALL_ANNULUS_3 `0`]; REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`) THEN RESA_TAC THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1) /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN STRIP_TAC THEN REPEAT DISCH_TAC THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB]) THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`]) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;]) THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`]; ]);;
let ARITH_3_TAC =ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 0 MOD 3=0/\ 1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ SUC 0=1 /\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ 0<3/\ a+0=a/\ 0+a=a/\ 3-1=2/\ 3-2=1/\ 3-0=3/\ 3-3=0`;;
let VV_IN_BALL_ANNULUS_TAC_3= fun (so:term)-> REPLICATE_TAC (30-23)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th so[ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN]) ;; let SCS_A_LE_NORM_3_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_3= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`) THEN RESA_TAC THENL[ SCS_A_LE_NORM_3_IS_SCS th `3`; SCS_A_LE_NORM_3_IS_SCS th `1`; SCS_A_LE_NORM_3_IS_SCS th `2`;];; let SCS_B_LE_NORM_3_IS_SCS= fun (so:term) (so1:term)-> REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]) THEN REPEAT RESA_TAC ;; let PROVE_INEQUALITY_TAC_3B= fun (th:term)-> MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`) THEN RESA_TAC THENL[ SCS_B_LE_NORM_3_IS_SCS th `3`; SCS_B_LE_NORM_3_IS_SCS th `1`; SCS_B_LE_NORM_3_IS_SCS th `2`;];;
let  IN_NOT_EMPTY_B1_SY_3_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ scs_k_v39 s=3 /\ dimindex(:M) = scs_k_v39 s/\ matvec (v:real^3^M) =a/\ (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ (!i. vv i = if i MOD scs_k_v39 s = 0 then row 3 v else if i MOD scs_k_v39 s = 1 then row 1 v else row 2 v) ==> vv IN BBs_v39 s`,
[ REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;] THEN REPEAT RESA_TAC; ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`x' MOD 3<3 ==> x' MOD 3 = 0 \/ x' MOD 3 = 1 \/ x' MOD 3 = 2 `) THEN RESA_TAC THENL[ VV_IN_BALL_ANNULUS_TAC_3 `3`; VV_IN_BALL_ANNULUS_TAC_3 `1`; VV_IN_BALL_ANNULUS_TAC_3 `2`;]; ASM_REWRITE_TAC[periodic] THEN GEN_TAC THEN MRESAL_TAC MOD_EQ[`i+3:num`;`i:num`;`3:num`;`1`][ARITH_RULE`1*A=A`]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`]; MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_3 `3`; PROVE_INEQUALITY_TAC_3 `1`; PROVE_INEQUALITY_TAC_3 `2`;]; REWRITE_TAC[dist] THEN REPEAT GEN_TAC THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC; POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN GEN_TAC THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`]; MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`) THEN RESA_TAC THENL[ PROVE_INEQUALITY_TAC_3B `3`; PROVE_INEQUALITY_TAC_3B `1`; PROVE_INEQUALITY_TAC_3B `2`;]; REWRITE_TAC[ARITH_RULE`3<=3`]; ]);;
(* }}} *)
let NOT_EMPTY_CASE_3_IS_SCS=
prove_by_refinement( ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv /\ dimindex(:M)= scs_k_v39 s ==> ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v }={})`,
[REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;] THEN STRIP_TAC THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M` THEN ABBREV_TAC`a=matvec (v:real^3^M) ` THEN EXISTS_TAC`a:real^(M,3)finite_product` THEN MATCH_MP_TAC IN_IS_SCS_CASE_3 THEN ASM_REWRITE_TAC[]]);;
let J1_TS=new_definition `J1_TS (s:tri_sy)= {x| ?i. {i MOD 3,f_ts s (i MOD (3))} IN J_TS s /\ i IN 1..3 /\ x=i,SUC(i MOD (3))}`;;
let d_fun3=new_definition `d_fun3 (s1:scs_v39)(s:tri_sy,l:real^(M,3)finite_product) = (d_ts s) + #0.1 * (if is_ear_v39 s1 then &1 else -- &1) * sum (J1_TS s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;
let FINITE_J1_TS=
prove(`!s:tri_sy . FINITE (J1_TS s)`,
GEN_TAC THEN REWRITE_TAC[J1_TS] THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (3)))`;`1..3`][FINITE_NUMSEG;IMAGE] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`{y | ?x. x IN 1..(3) /\ y = x,SUC(x MOD (3))}` THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]);;
let INDEX_J1_TS=
prove(`!s:tri_sy . x IN J1_TS s ==> 1 <= FST x /\ FST x <= 3`,
REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
let CONTINUOUS_ON_D_FUN3=
prove(`!s:tri_sy . k=3 /\ k_ts s =k /\ dimindex(:M) =k/\ I_TS s= 0..k-1 /\ f_ts s=(\i. ((1+i):num MOD k)) ==> lift o(\l:real^(M,3)finite_product. d_fun3 s1 (s,l)) continuous_on ( {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (a_ts s) (b_ts s) v })`,
REPEAT STRIP_TAC THEN REWRITE_TAC[d_fun3;LIFT_ADD;o_DEF;] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN ASSUME_TAC FINITE_J1_TS THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:tri_sy`) THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF] THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;] THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN STRIP_TAC THENL[ MATCH_MP_TAC CONTINUOUS_ON_ROW THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG] THEN REPEAT RESA_TAC; MATCH_MP_TAC CONTINUOUS_ON_ROW THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC]);;
let tri_sy_explicit = 
prove_by_refinement( `!k d s a b J f. tri_stable k d s a b J f ==> k_ts (tri_sy (k,d,s, a,b,J,f)) = k/\ d_ts (tri_sy (k,d,s, a,b,J,f)) = d /\ a_ts (tri_sy (k,d,s, a,b,J,f)) = a /\ b_ts (tri_sy (k,d,s, a,b,J,f)) = b /\ J_TS (tri_sy (k,d,s, a,b,J,f)) = J /\ I_TS (tri_sy (k,d,s, a,b,J,f)) = s /\ f_ts (tri_sy (k,d,s, a,b,J,f)) = f `,
(* {{{ proof *) [ REWRITE_TAC[k_ts;d_ts;a_ts;b_ts;J_TS;I_TS;f_ts;tri_sy_tybij;] THEN MP_TAC tri_sy_tybij THEN STRIP_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> POP_ASSUM (fun th1-> ASSUME_TAC th THEN MRESA1_TAC th1`(k,d,s,a,b,J,f):(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num))`)) ]);;
(* }}} *)
let IN_B_SY1_COLLINEAR_CASE_3_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ scs_k_v39 s=3/\ dimindex(:M)= scs_k_v39 s ==> (!a. a IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v } ==> ~collinear{vec 0, row 1 (vecmats a),row 2 (vecmats a)}/\ ~collinear{vec 0, row 1 (vecmats a),row 3 (vecmats a)}/\ ~collinear{vec 0, row 2 (vecmats a),row 3 (vecmats a)})`,
(* {{{ proof *) [ REWRITE_TAC[IN_ELIM_THM;] THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC THEN ABBREV_TAC`( vv i = if i MOD scs_k_v39 s = 0 then row 3 v else if i MOD scs_k_v39 s = 1 then row 1 v else row 2 (v:real^3^M))` THEN MP_TAC IN_NOT_EMPTY_B1_SY_3_IS_SCS THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID] THEN RESA_TAC THEN STRIP_TAC THEN MP_TAC IS_SCS_NOT_COLLINEAR_BBs_CASE_3 THEN RESA_TAC; SUBGOAL_THEN`vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M =v`ASSUME_TAC; REPLICATE_TAC 4 (REMOVE_ASSUM_TAC) THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;] THEN ONCE_REWRITE_TAC[CART_EQ] THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA]; MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]; ]);;
(* }}} *)
let HDPLYGY_CASE_30=
prove_by_refinement( `tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k /\ ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v } = {}:real^(M,3)finite_product->bool) /\ (!l. l IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v } ==> ~collinear{vec 0, row 1 (vecmats l),row 2 (vecmats l)}/\ ~collinear{vec 0, row 1 (vecmats l),row 3 (vecmats l)}/\ ~collinear{vec 0, row 2 (vecmats l),row 3 (vecmats l)}) /\ k_ts s = 3 /\ I_TS s = 0..3 - 1 /\ f_ts s = (\i. (1 + i) MOD 3) /\ a_ts s =a /\ b_ts s =b ==> ?x:real^(M,3)finite_product. x IN ({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }) /\ (!y:real^(M,3)finite_product. y IN ({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }) ==> tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x)) - d_fun3 s1 (s,x) <= tau3 (row 1 (vecmats y)) (row 2 (vecmats y)) (row 3 (vecmats y)) - d_fun3 s1 (s,y) )`,
(* {{{ proof *) [ REPEAT STRIP_TAC THEN MP_TAC TRI_STABLE_K_EQ_3 THEN RESA_TAC THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\x:real^(M,3)finite_product. tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))- d_fun3 s1 (s,x))`;`{matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }:real^(M,3)finite_product->bool`] THEN POP_ASSUM MATCH_MP_TAC THEN STRIP_TAC; POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MATCH_MP_TAC COMPACT_TRI_STABLE THEN ASM_REWRITE_TAC[]; SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN ONCE_REWRITE_TAC[SET_RULE`A/\B <=> B/\ A`] THEN STRIP_TAC; MRESAL_TAC(GEN_ALL CONTINUOUS_ON_D_FUN3)[`k:num`;`s1:scs_v39`;`s:tri_sy`][o_DEF]; POP_ASSUM MP_TAC THEN REPLICATE_TAC 5(REMOVE_ASSUM_TAC) THEN STRIP_TAC THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG;tau3; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN SIMP_TAC[o_DEF;LIFT_ADD;] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN STRIP_TAC; SIMP_TAC[o_DEF;LIFT_ADD;] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN STRIP_TAC; SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN STRIP_TAC; REWRITE_TAC[rho;o_DEF;LIFT_ADD] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN MATCH_MP_TAC CONTINUOUS_ON_ROW THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF] THEN REPEAT STRIP_TAC THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH) THEN REWRITE_TAC[o_DEF] THEN STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`] THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`] THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`]) THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESA1_TAC th `a':real^(M,3)finite_product` THEN ASSUME_TAC th) THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`) ; SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN STRIP_TAC; REWRITE_TAC[rho;o_DEF;LIFT_ADD] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN MATCH_MP_TAC CONTINUOUS_ON_ROW THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF] THEN REPEAT STRIP_TAC THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH) THEN REWRITE_TAC[o_DEF] THEN STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`] THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`] THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`]) THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESA1_TAC th `a':real^(M,3)finite_product` THEN ASSUME_TAC th) THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`) THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[] ; SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN STRIP_TAC; REWRITE_TAC[rho;o_DEF;LIFT_ADD] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;] THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN MATCH_MP_TAC CONTINUOUS_ON_ROW THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF] THEN REPEAT STRIP_TAC THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH) THEN REWRITE_TAC[o_DEF] THEN STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX] THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`] THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`] THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`]) THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESA1_TAC th `a':real^(M,3)finite_product` THEN ASSUME_TAC th) THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`) THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let TAUSTAR_EQ_TAU_STAR_3_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ BBs_v39 s vv /\ scs_k_v39 s=3 /\ dimindex (:M)=3 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v /\ matvec (v:real^3^M) =a /\ tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1), (change_type_v3 (scs_a_v39 s)), (change_type_v3 (scs_b_v39 s)), (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)), (\i. (1 + i) MOD scs_k_v39 s))=s1 ==> taustar_v39 s vv = tau3 (vv 1) (vv 2) (vv 0) -d_fun3 s (s1,a)`,
(* {{{ proof *) [ REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[taustar_v39;tau_star;LET_DEF;LET_END_DEF;ARITH_RULE`3<=3`;] THEN MATCH_MP_TAC(REAL_ARITH`a=b /\ c=d==> a -c= b- d`) THEN STRIP_TAC ; REWRITE_TAC[tau3] THEN REAL_ARITH_TAC; REWRITE_TAC[dsv_v39;d_fun3] THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM THEN RESA_TAC THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;` (change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;` (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;` (\i. (1 + i) MOD scs_k_v39 s)`] THEN EXPAND_TAC"a" THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID] THEN MATCH_MP_TAC(REAL_ARITH`a=b ==> d+ a=d+b`) THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`) THEN RESA_TAC ; MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * &1 * a= #0.1 * &1 *b`) THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM] THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN REWRITE_TAC[IN_ELIM_THM;dist] THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else i, SUC(i MOD 3))` THEN STRIP_TAC; REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`) THEN RESA_TAC; REWRITE_TAC[ARITH_3_TAC] THEN EXISTS_TAC`0` THEN ASM_REWRITE_TAC[ARITH_3_TAC] THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_3_TAC] THEN REPEAT DISCH_TAC) THEN STRIP_TAC ; MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`) THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) ; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) ; REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC] THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC]; EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC; MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`) THEN RESA_TAC THEN REWRITE_TAC[ARITH_3_TAC] ; ASM_REWRITE_TAC[] THEN STRIP_TAC ; REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC] THEN STRIP_TAC THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3} ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`) THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`) THEN REWRITE_TAC[ADD1;] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`) THEN REWRITE_TAC[ADD1;] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC] THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`) THEN RESA_TAC ; REWRITE_TAC[PAIR_EQ] THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC; REPEAT RESA_TAC THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC] ; MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`) THEN RESA_TAC ; EXISTS_TAC`3` THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC] THEN EXISTS_TAC`x:num` THEN EXISTS_TAC`SUC x:num` THEN ASM_REWRITE_TAC[ARITH_3_TAC]; EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`) THEN RESA_TAC THEN EXISTS_TAC`x:num` THEN EXISTS_TAC`SUC x` THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD1] ; MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`) THEN RESA_TAC THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC]) ; (*************-1*************) MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * -- &1 * a= #0.1 * -- &1 *b`) THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM] THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN REWRITE_TAC[IN_ELIM_THM;dist] THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else i, SUC(i MOD 3))` THEN STRIP_TAC; REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`) THEN RESA_TAC; REWRITE_TAC[ARITH_3_TAC] THEN EXISTS_TAC`0` THEN ASM_REWRITE_TAC[ARITH_3_TAC] THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_3_TAC] THEN REPEAT DISCH_TAC) THEN STRIP_TAC ; MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`) THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) ; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) ; REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC] THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC]; EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC; MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`) THEN RESA_TAC THEN REWRITE_TAC[ARITH_3_TAC] ; ASM_REWRITE_TAC[] THEN STRIP_TAC ; REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC] THEN STRIP_TAC THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3} ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`) THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`) THEN REWRITE_TAC[ADD1;] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`) THEN REWRITE_TAC[ADD1;] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC] THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`) THEN RESA_TAC ; REWRITE_TAC[PAIR_EQ] THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`) THEN RESA_TAC; REWRITE_TAC[PAIR_EQ] THEN RESA_TAC; REPEAT RESA_TAC THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC] ; MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`) THEN RESA_TAC ; EXISTS_TAC`3` THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC] THEN EXISTS_TAC`x:num` THEN EXISTS_TAC`SUC x:num` THEN ASM_REWRITE_TAC[ARITH_3_TAC]; EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`) THEN RESA_TAC THEN EXISTS_TAC`x:num` THEN EXISTS_TAC`SUC x` THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD1] ; MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`) THEN RESA_TAC THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC]) ; ]);;
let XWITCCN_CASE_3_IS_SCS=
prove_by_refinement( `is_scs_v39 s /\ BBs_v39 s vv /\ scs_k_v39 s=3 /\ dimindex(:M) =scs_k_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`,
(* {{{ proof *) [ STRIP_TAC THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM THEN RESA_TAC THEN MP_TAC NOT_EMPTY_CASE_3_IS_SCS THEN RESA_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`] THEN MP_TAC IN_B_SY1_COLLINEAR_CASE_3_IS_SCS THEN RESA_TAC THEN ABBREV_TAC`s1 =tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1), (change_type_v3 (scs_a_v39 s)), (change_type_v3 (scs_b_v39 s)), (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)), (\i. (1 + i) MOD scs_k_v39 s))` THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;` (change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;` (change_type_v2 (scs_J_v39 s)(scs_k_v39 s))`;` (\i. (1 + i) MOD scs_k_v39 s)`] THEN MRESAL_TAC (GEN_ALL HDPLYGY_CASE_30)[`scs_d_v39 s`;`(change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`scs_k_v39 s`;`(change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;`s:scs_v39`;`s1:tri_sy`][ARITH_RULE`2<3`] THEN POP_ASSUM (fun th-> POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN REWRITE_TAC[BBprime_v39;IN] THEN ABBREV_TAC`( vv1 i = if i MOD scs_k_v39 s = 0 then row 3 v else if i MOD scs_k_v39 s = 1 then row 1 v else row 2 (v:real^3^M))` THEN EXISTS_TAC`vv1:num->real^3` THEN STRIP_TAC; ONCE_REWRITE_TAC[GSYM IN] THEN MATCH_MP_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS) THEN EXISTS_TAC`x:real^(M,3)finite_product` THEN EXISTS_TAC`v:real^3^M` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN RESA_TAC; SUBGOAL_THEN`vector [ vv1 1; (vv1:num->real^3) 2;vv1 0] = v:real^3^M` ASSUME_TAC; POP_ASSUM(fun th-> REWRITE_TAC[GSYM th]) THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;] THEN ONCE_REWRITE_TAC[CART_EQ] THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA]; STRIP_TAC; GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`] THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(ww:num->real^3) 1; ww 2; ww 0]:real^3^M`;`ww:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`] THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`] THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`] THEN MRESAL_TAC VECTOR_3_3[`(ww:num->real^3) 1`;`(ww:num->real^3) 2`;`(ww:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`] THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th `matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID]); MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS) [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`] THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M`;`vv:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`] THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`] THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`] THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`] THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th `matvec(vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID]) THEN REPLICATE_TAC (31-4) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th THEN ASM_REWRITE_TAC[]) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let UXCKFPE=
prove_by_refinement( ` !s vv . is_scs_v39 s /\ vv IN BBs_v39 s /\ taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`,
(* {{{ proof *) [ REPEAT GEN_TAC THEN REWRITE_TAC[IN] THEN DISCH_TAC THEN SUBGOAL_THEN`3<= scs_k_v39 s /\ scs_k_v39 s<=6` ASSUME_TAC; ASM_TAC THEN REWRITE_TAC[is_scs_v39] THEN RESA_TAC; MP_TAC(ARITH_RULE`3<= scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s=6`) THEN RESA_TAC; MP_TAC(INST_TYPE [`:3`,`:M`]XWITCCN_CASE_3_IS_SCS) THEN ASM_REWRITE_TAC[DIMINDEX_3] THEN STRIP_TAC ; MP_TAC(INST_TYPE [`:2+2`,`:M`]XWITCCN_CASE_4_IS_SCS) THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4] THEN STRIP_TAC; MP_TAC(INST_TYPE [`:2+3`,`:M`]XWITCCN_CASE_5_IS_SCS) THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5] THEN STRIP_TAC ; MP_TAC(INST_TYPE [`:3+3`,`:M`]XWITCCN_CASE_6_IS_SCS) THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6] THEN STRIP_TAC ]);;
end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)