(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Yxionxl = struct open Polyhedron;; open Sphere;; open Topology;; open Fan_misc;; open Planarity;; open Conforming;; open Hypermap;; open Fan;; open Topology;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Collect_geom;; open Dih2k_hypermap;; open Wjscpro;; open Tecoxbm;; open Hdplygy;; open Nkezbfc_local;; open Flyspeck_constants;; open Gbycpxs;; open Pcrttid;; open Local_lemmas1;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Hypermap;; open Fan;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Flyspeck_constants;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Zithlqn;; open Xwitccn;; open Ayqjtmd;; open Jkqewgv;; open Mtuwlun;; open Uxckfpe;; open Sgtrnaf;; open Qknvmlb;; let TRANSFER_SUBSET_BB=prove_by_refinement( `is_scs_v39 s /\ is_scs_v39 t/\ scs_k_v39 t= scs_k_v39 s/\ transfer_v39 s t /\ BBs_v39 s ww ==> BBs_v39 t ww`, [REWRITE_TAC[transfer_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39] THEN REPEAT RESA_TAC; REPLICATE_TAC 1(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 7(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; REPLICATE_TAC 1(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 6(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; REPLICATE_TAC 1(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 7(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; REPLICATE_TAC 1(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 6(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]) THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);; let DSV_LE_DSV_TRANSFER=prove_by_refinement( `is_scs_v39 s /\ is_scs_v39 t/\ scs_k_v39 t= scs_k_v39 s/\ transfer_v39 s t /\ BBs_v39 s vv ==> dsv_v39 s vv <= dsv_v39 t vv`, [ REWRITE_TAC[transfer_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39;dsv_v39] THEN REPEAT RESA_TAC; ASM_TAC THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`) THEN RESA_TAC; REPEAT DISCH_TAC THEN REPLICATE_TAC (17-4)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN` sum {i | i < scs_k_v39 s /\ scs_J_v39 t i (SUC i)} (\i. cstab - dist ((vv:num->real^3) i,vv (SUC i))) <= sum {i | i < scs_k_v39 s /\ scs_J_v39 s i (SUC i)} (\i. cstab - dist (vv i,vv (SUC i)))`ASSUME_TAC; MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN REPEAT STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. (scs_k_v39 s)` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]); POP_ASSUM MP_TAC THEN REWRITE_TAC[DIFF;IN_ELIM_THM] THEN STRIP_TAC THEN REPLICATE_TAC (19-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (58-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REAL_ARITH_TAC; SUBGOAL_THEN` &0 <= sum {i | i < scs_k_v39 s /\ scs_J_v39 t i (SUC i)} (\i. cstab - dist ((vv:num->real^3) i,vv (SUC i)))`ASSUME_TAC; MATCH_MP_TAC SUM_POS_LE THEN REPEAT STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. (scs_k_v39 s)` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[DIFF;IN_ELIM_THM] THEN STRIP_TAC THEN REPLICATE_TAC (19-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (58-50)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REPLICATE_TAC (57-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REAL_ARITH_TAC; REPLICATE_TAC (18-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`is_ear_v39 t \/ ~(is_ear_v39 t)`) THEN RESA_TAC; REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH`a<= a1 /\ b1<= b/\ &0<= b1 ==> a+ #0.1 * -- &1 * b <= a1+ #0.1 * &1 * b1`) THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH`a<= a1 /\ b1<= b/\ &0<= b1 ==> a+ #0.1 * -- &1 * b <= a1+ #0.1 * -- &1 * b1`) THEN ASM_REWRITE_TAC[]; ASM_TAC THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`) THEN RESA_TAC; REPEAT DISCH_TAC THEN REPLICATE_TAC (17-4)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN` sum {i | i < scs_k_v39 s /\ scs_J_v39 t i (SUC i)} (\i. cstab - dist ((vv:num->real^3) i,vv (SUC i))) <= sum {i | i < scs_k_v39 s /\ scs_J_v39 s i (SUC i)} (\i. cstab - dist (vv i,vv (SUC i)))`ASSUME_TAC; MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN REPEAT STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. (scs_k_v39 s)` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]); POP_ASSUM MP_TAC THEN REWRITE_TAC[DIFF;IN_ELIM_THM] THEN STRIP_TAC THEN REPLICATE_TAC (19-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (58-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REAL_ARITH_TAC; SUBGOAL_THEN` &0 <= sum {i | i < scs_k_v39 s /\ scs_J_v39 t i (SUC i)} (\i. cstab - dist ((vv:num->real^3) i,vv (SUC i)))`ASSUME_TAC; MATCH_MP_TAC SUM_POS_LE THEN REPEAT STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. (scs_k_v39 s)` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[DIFF;IN_ELIM_THM] THEN STRIP_TAC THEN REPLICATE_TAC (19-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (58-50)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REPLICATE_TAC (57-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN REAL_ARITH_TAC; REPLICATE_TAC (18-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`is_ear_v39 t \/ ~(is_ear_v39 t)`) THEN RESA_TAC; REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH`a<= a1 /\ b1<= b/\ &0<= b1 ==> a+ #0.1 * -- &1 * b <= a1+ #0.1 * &1 * b1`) THEN ASM_REWRITE_TAC[]; REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH`a<= a1 /\ b1<= b/\ &0<= b1 ==> a+ #0.1 * -- &1 * b <= a1+ #0.1 * -- &1 * b1`) THEN ASM_REWRITE_TAC[]]);; let TAUSTAR_LE_TAUSTAR_TRANSFER=prove( `is_scs_v39 s /\ is_scs_v39 t/\ scs_k_v39 t= scs_k_v39 s/\ transfer_v39 s t /\ BBs_v39 s vv ==> taustar_v39 t vv <= taustar_v39 s vv`, STRIP_TAC THEN MP_TAC DSV_LE_DSV_TRANSFER THEN RESA_TAC THEN REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF] THEN ASM_TAC THEN REWRITE_TAC[transfer_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39;taustar_v39] THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`scs_k_v39 s <= 3 \/ ~(scs_k_v39 s <= 3)`) THEN RESA_TAC THEN REAL_ARITH_TAC);; let TRANSTER_IS_UNADORNED=prove(`transfer_v39 s t ==> unadorned_v39 t`, REWRITE_TAC[transfer_v39] THEN RESA_TAC);; let NOT_EMPETY_MMS_TRANSFER=prove(`is_scs_v39 s /\ is_scs_v39 t/\ scs_k_v39 t= scs_k_v39 s/\ transfer_v39 s t /\ MMs_v39 s vv ==> ?ww. MMs_v39 t ww`, REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39] THEN REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL TRANSFER_SUBSET_BB)[`s:scs_v39`;`t:scs_v39`;`vv:num->real^3`] THEN MP_TAC TAUSTAR_LE_TAUSTAR_TRANSFER THEN RESA_TAC THEN MP_TAC(REAL_ARITH`taustar_v39 t vv <= taustar_v39 s vv/\ taustar_v39 s vv< &0 ==> taustar_v39 t vv < &0`) THEN RESA_TAC THEN MP_TAC TRANSTER_IS_UNADORNED THEN RESA_TAC THEN MRESAL_TAC SGTRNAF[`t:scs_v39`;`vv:num->real^3`][SET_RULE`~(A={})<=> ?a. a IN A`;IN;BBprime_v39;BBprime2_v39;MMs_v39]);; let YXIONXL1 = prove_by_refinement(`!s t. is_scs_v39 s /\ transfer_v39 s t ==> scs_arrow_v39 {s} {t}`, [ REWRITE_TAC[transfer_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39] THEN REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN EXISTS_TAC`t:scs_v39` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv. vv IN A`;IN] THEN STRIP_TAC THEN MP_TAC NOT_EMPETY_MMS_TRANSFER THEN RESA_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[transfer_v39;unadorned_v39]]);; (************YXIONXL3************) let TRANS_V=prove_by_refinement(` is_scs_v39 s /\ BBs_v39 s vv ==> IMAGE (\x. vv (i + x)) (:num)= IMAGE vv (:num)`, [ REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39;IMAGE] THEN RESA_TAC THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC 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 EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD1] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] 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`i + (x' + k - i MOD k) MOD k:num`); RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC 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 EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD1] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] 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`i + (x' + k - i MOD k) MOD k:num`)]);; let TRANS_FF=prove_by_refinement(`is_scs_v39 s /\ BBs_v39 s vv ==> IMAGE (\i'. vv (i + i'), vv (i + SUC i')) (:num) =IMAGE (\i. vv i, vv (SUC i)) (:num)`, [REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39;IMAGE;IN_ELIM_THM] THEN RESA_TAC THEN ONCE_REWRITE_TAC[EXTENSION;] THEN REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`;ARITH_RULE`i + SUC a= SUC(i+a)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) THEN EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_ADD_MOD[`x':num`;`1`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] THEN MRESAL_TAC MOD_ADD_MOD[`i+(x' + k - i MOD k) MOD k`;`1:num`;`k:num`][ADD_AC] 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`i + (x' + k - i MOD k) MOD k:num` THEN MRESA1_TAC th`x'+1:num` THEN MRESA1_TAC th`i + (x' + k - i MOD k) MOD k +1:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]); RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`;ARITH_RULE`i + SUC a= SUC(i+a)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) THEN EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_ADD_MOD[`x':num`;`1`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] THEN MRESAL_TAC MOD_ADD_MOD[`i+(x' + k - i MOD k) MOD k`;`1:num`;`k:num`][ADD_AC] 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`i + (x' + k - i MOD k) MOD k:num` THEN MRESA1_TAC th`x'+1:num` THEN MRESA1_TAC th`i + (x' + k - i MOD k) MOD k +1:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);; let TRANS_E=prove_by_refinement(`is_scs_v39 s /\ BBs_v39 s vv ==> IMAGE (\i'. {vv (i + i'), vv (i + SUC i')}) (:num) =IMAGE (\i. {vv i, vv (SUC i)}) (:num)`, [REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39;IMAGE;IN_ELIM_THM] THEN RESA_TAC THEN ONCE_REWRITE_TAC[EXTENSION;] THEN REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC; RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`;ARITH_RULE`i + SUC a= SUC(i+a)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) THEN EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_ADD_MOD[`x':num`;`1`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] THEN MRESAL_TAC MOD_ADD_MOD[`i+(x' + k - i MOD k) MOD k`;`1:num`;`k:num`][ADD_AC] 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`i + (x' + k - i MOD k) MOD k:num` THEN MRESA1_TAC th`x'+1:num` THEN MRESA1_TAC th`i + (x' + k - i MOD k) MOD k +1:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]); RESA_TAC THEN EXISTS_TAC`i+x':num` THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN(:num)`;ARITH_RULE`i + SUC a= SUC(i+a)`]; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`) THEN EXISTS_TAC`(x'+ k- i MOD k) MOD k` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`] THEN MRESA_TAC DIVISION[`x' + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> i MOD k + x' + k - i MOD k= k+ x'`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`(x' + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`(i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i MOD k:num`;`(x' + k - i MOD k)`;`k:num`][ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`(x' + k - i MOD k) MOD k`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_ADD_MOD[`x':num`;`1`;`k:num`][ADD_AC] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`x':num`][ARITH_RULE`1*k+y=k+y`] THEN MRESAL_TAC MOD_ADD_MOD[`i+(x' + k - i MOD k) MOD k`;`1:num`;`k:num`][ADD_AC] 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`i + (x' + k - i MOD k) MOD k:num` THEN MRESA1_TAC th`x'+1:num` THEN MRESA1_TAC th`i + (x' + k - i MOD k) MOD k +1:num`) THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);; let BB_TRANS_SUBSET_BB=prove(` is_scs_v39 s /\ BBs_v39 s vv ==> BBs_v39 (scs_prop_equ_v39 s i) (\x. vv (i+x))`, STRIP_TAC THEN MP_TAC TRANS_V THEN RESA_TAC THEN MP_TAC TRANS_E THEN RESA_TAC THEN MP_TAC TRANS_FF THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39] THEN REPEAT RESA_TAC THEN ASM_TAC THEN ASM_REWRITE_TAC[periodic;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (26-21)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]));; let PROP_EQU_IS_SCS= prove_by_refinement(`scs_k_v39 s = k /\ is_scs_v39 s /\ t= (scs_prop_equ_v39 s i) ==> is_scs_v39 t`, [RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[scs_v39_explicit;scs_opp_v39;LET_DEF;LET_END_DEF;is_scs_v39;peropp;scs_prop_equ_v39] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN REPEAT RESA_TAC; ASM_TAC THEN ASM_REWRITE_TAC[periodic;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-4)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-5)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic2;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-7)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+j:num`;`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic2;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-8)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+j:num`;`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic2;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+j:num`;`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic2;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-10)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+j:num`;`i+i':num`][ADD_AC]); ASM_TAC THEN ASM_REWRITE_TAC[periodic2;] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (22-11)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+j:num`;`i+i':num`][ADD_AC]); ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i+i')`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+j:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i+j) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+i':num`) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_LT[`i':num`;`k:num`] THEN MRESA_TAC MOD_LT[`j:num`;`k:num`] THEN MRESA_TAC Hdplygy.MOD_EQ_MOD[`i':num`;`j:num`;`i:num`;`k:num`] THEN MRESA_TAC DIVISION[`i+i':num`;`k:num`] THEN MRESA_TAC DIVISION[`i+j:num`;`k:num`] THEN REPLICATE_TAC (33-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`(i+i') MOD k:num`;`(i+j) MOD k:num`][ADD_AC]) ; ASM_REWRITE_TAC[ARITH_RULE`i+ SUC i'= SUC(i+i')`] THEN REPLICATE_TAC (23-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]); ASM_REWRITE_TAC[ARITH_RULE`i+ SUC i'= SUC(i+i')`] THEN REPLICATE_TAC (23-17)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`][ADD_AC]) ; REPLICATE_TAC (23-18)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i+i':num`;`i+j:num`][ADD_AC;ARITH_RULE` SUC(i+i')=i+ SUC i'`]) ; MRESA_TAC Hdplygy.MOD_EQ_MOD[`j:num`;`SUC i':num`;`i:num`;`k:num`] ; MRESA_TAC Hdplygy.MOD_EQ_MOD[`i':num`;`SUC j:num`;`i:num`;`k:num`] ; SUBGOAL_THEN` CARD {i | i < k /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} =CARD {i' | i' < k /\ (&2 * h0 < scs_b_v39 s (i + i') (i + SUC i') \/ &2 < scs_a_v39 s (i + i') (i + SUC i'))} ` ASSUME_TAC ; MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`(\x:num. (i+x) MOD k)` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. k` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC ; STRIP_TAC; REPEAT RESA_TAC ; MRESA_TAC DIVISION[`i+x:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i+x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+SUC x:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i+ SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+x:num`) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i+x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC ((i + x) MOD k):num`) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REWRITE_TAC[ADD1] THEN MP_TAC(ARITH_RULE`3<=k==> 1 MRESA1_TAC th`i+SUC x:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i+ SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+x: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+x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC ((i + x) MOD k):num`) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN REWRITE_TAC[ADD1] THEN MP_TAC(ARITH_RULE`3<=k==> 1 1 ASSUME_TAC(SYM th)) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + y - i MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + SUC (y - i MOD k):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + SUC (y - i MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + y - i MOD k:num`) THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i+y- i MOD k`;`1`;`k:num`][ADD1] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y+1:num`) THEN REWRITE_TAC[ARITH_RULE`a+1= SUC a`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESA_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y- i MOD k:num`;`i MOD k:num`;`k:num`] ; EXISTS_TAC`(y+ k- i MOD k)MOD k` THEN MRESA_TAC DIVISION[`y + k- i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MRESA_TAC MOD_LT[`(y + k- i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`i MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k ==> i MOD k + y + k - i MOD k= k+y/\ 1 ASSUME_TAC(SYM th)) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + (y + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + SUC ((y + k - i MOD k) MOD k):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + ((y + k - i MOD k) MOD k):num`) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i + (y + k - i MOD k) MOD k`;`1`;`k:num`][ADD_AC] 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 y`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y+1:num`) THEN REWRITE_TAC[ARITH_RULE`a+1= SUC a`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESA_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y +k- i MOD k:num`;`i MOD k:num`;`k:num`] ; MP_TAC(ARITH_RULE`i MOD k<=y\/ y< i MOD k`) THEN RESA_TAC ; EXISTS_TAC`y- i MOD k` THEN MP_TAC(ARITH_RULE`i MOD k<=y /\ y< k/\ 3<=k ==> 1 ASSUME_TAC(SYM th)) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i + y - i MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + SUC (y - i MOD k):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + SUC (y - i MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + y - i MOD k:num`) THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i+y- i MOD k`;`1`;`k:num`][ADD1] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y+1:num`) THEN REWRITE_TAC[ARITH_RULE`a+1= SUC a`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESA_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y- i MOD k:num`;`i MOD k:num`;`k:num`] ; EXISTS_TAC`(y+ k- i MOD k)MOD k` THEN MRESA_TAC DIVISION[`y + k- i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MRESA_TAC MOD_LT[`(y + k- i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`i MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k ==> i MOD k + y + k - i MOD k= k+y/\ 1 ASSUME_TAC(SYM th)) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i + (y + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + SUC ((y + k - i MOD k) MOD k):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i + ((y + k - i MOD k) MOD k):num`) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESAL_TAC MOD_ADD_MOD[`i + (y + k - i MOD k) MOD k`;`1`;`k:num`][ADD_AC] 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 y`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y+1:num`) THEN REWRITE_TAC[ARITH_RULE`a+1= SUC a`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) THEN REPEAT STRIP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESA_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y +k- i MOD k:num`;`i MOD k:num`;`k:num`] ; POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) ; ]);; let TRANS_MOD_EQ=prove(`~(k=0)==> (i+ (x+ k- i MOD k)MOD k) MOD k= x MOD k`, STRIP_TAC THEN MRESA_TAC DIVISION[`x + k - i MOD k`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MRESA_TAC MOD_LT[`(x + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_LT[`i MOD k`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k < k ==> i MOD k + x + k - i MOD k= k+x`) THEN RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`(x + k - i MOD k) MOD k`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i MOD k`;`(x + k - i MOD k)`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`x:num`][ARITH_RULE`1*k=k`]);; let TRANS_MOD_EQ_SUC=prove(`1 (i+ SUC ((x+ k- i MOD k)MOD k)) MOD k= SUC x MOD k`, STRIP_TAC THEN REWRITE_TAC[ADD1] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MP_TAC TRANS_MOD_EQ THEN RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i +(x + k - i MOD k) MOD k`;`1`;`k:num`] THEN ASM_REWRITE_TAC[ADD_AC]);; let TRANS_PROPERTY=prove(`(!i. vv (i MOD k) = vv i) /\ ~(k=0) ==> ( (!j:num. vv j) <=> (!j:num. vv (i+ j)))`, REPEAT STRIP_TAC THEN EQ_TAC THENL[ REPEAT STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`i+j:num`); REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> MRESA_TAC th[`(j+ k- i MOD k) MOD k`]) THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`j:num`;`k:num`] THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i + (j + k - i MOD k) MOD k`] THEN MRESA_TAC th[`j:num`] THEN ASSUME_TAC th)]);; let TRANS_PROPERTY_IN=prove(`(!i. (i MOD k) IN vv <=> i IN vv ) /\ ~(k=0) ==> ( (!j:num. j IN vv ) <=> (!j:num. (i+ j) IN vv ))`, REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ REPEAT STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`i+j:num`); REPEAT STRIP_TAC THEN POP_ASSUM (fun th-> MRESA_TAC th[`(j+ k- i MOD k) MOD k`]) THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`j:num`;`k:num`] THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i + (j + k - i MOD k) MOD k`] THEN MRESA_TAC th[`j:num`] THEN ASSUME_TAC th)]);; let PRO_EQU_IS_EAR=prove_by_refinement(` is_scs_v39 s ==> (is_ear_v39 s <=> is_ear_v39 (scs_prop_equ_v39 s i))`, [REWRITE_TAC[is_ear_v39] THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39;] THEN ONCE_REWRITE_TAC[EXTENSION;] THEN STRIP_TAC THEN EQ_TAC ; RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MRESAL_TAC(GEN_ALL PROP_EQU_IS_SCS)[`k:num`;`s:scs_v39`;`i:num`;`(scs_prop_equ_v39 s i)`;][scs_prop_equ_v39;LET_DEF;LET_END_DEF;unadorned_v39;scs_v39_explicit] THEN ASM_TAC THEN REWRITE_TAC[unadorned_v39;] THEN REPEAT RESA_TAC; SET_TAC[]; MRESAL_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`i':num`;`k:num`][ARITH_RULE`~(3=0)`] THEN EXISTS_TAC`(i'+ k- i MOD k)MOD k` THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC; REWRITE_TAC[IN_ELIM_THM;IN_SING] THEN EQ_TAC; STRIP_TAC THEN 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+x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+ SUC x:num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i+SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i+ x:num`) THEN REWRITE_TAC[ARITH_RULE`i+ SUC x= SUC(i+x)`] THEN MRESAL_TAC DIVISION[`i+x:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i+x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC ((i + x) MOD 3):num`) THEN REPLICATE_TAC (60-28)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING] THEN MRESAL_TAC th[`(i+x) MOD k`][IN_ELIM_THM;IN_SING]) THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPLICATE_TAC (2) STRIP_TAC THEN REWRITE_TAC[SYM th;ADD1]) THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1`;`3`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`x:num`;`3`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESAL_TAC MOD_LT[`x:num`;`k:num`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN MRESAL_TAC MOD_LT[`i':num`;`k:num`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3 + i' + 3 - i MOD 3= 3+i'`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i':num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`x:num`;`i'+ 3- i MOD 3:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] ; RESA_TAC THEN MRESAL_TAC DIVISION[`i'+3- i MOD 3`;`3`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`i':num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (i + (i' + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + SUC ((i' + 3 - i MOD 3) MOD 3)):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC ((i' + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + (i' + 3 - i MOD 3) MOD 3):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`SUC i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (SUC i' MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) THEN REPLICATE_TAC (61-28)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) ; ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`i':num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i + (i' + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + SUC ((i' + 3 - i MOD 3) MOD 3)):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((i + SUC ((i' + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + (i' + 3 - i MOD 3) MOD 3):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (SUC i' MOD k)`][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 TRANS_MOD_EQ_SUC)[`i:num`;`i':num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i + (i' + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + SUC ((i' + 3 - i MOD 3) MOD 3)):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((i + SUC ((i' + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + (i' + 3 - i MOD 3) MOD 3):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i':num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (SUC i' MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`) ; REPLICATE_TAC (17-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) THEN MRESAL_TAC MOD_LT[`i':num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESA_TAC MOD_LT[`j:num`;`3`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`i+j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3+ i' +3 - i MOD 3= 3+i'`) THEN RESA_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i':num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`j MOD k:num`;`i'+ 3- i MOD 3:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN REPLICATE_TAC (28-11)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`(i+j)MOD k:num`][IN_ELIM_THM;IN_SING]) THEN MRESAL_TAC MOD_ADD_MOD[`i+j:num`;`1`;`k:num`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1`;GSYM ADD1] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`i':num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i + SUC j)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + j):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((i + j) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + SUC j):num` THEN MRESAL1_TAC th`SUC((i + j) MOD 3):num`[ARITH_RULE`SUC(i +j)= i+ SUC j`]) ; REPLICATE_TAC (17-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) THEN MRESAL_TAC MOD_LT[`i':num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESA_TAC MOD_LT[`j:num`;`3`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC DIVISION[`i+j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3+ i' +3 - i MOD 3= 3+i'`) THEN RESA_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i':num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`j MOD k:num`;`i'+ 3- i MOD 3:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ (i + x) + 1= i +SUC x`] THEN REPLICATE_TAC (28-11)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`(i+j)MOD k:num`][IN_ELIM_THM;IN_SING]) THEN MRESAL_TAC MOD_ADD_MOD[`i+j:num`;`1`;`k:num`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1`;GSYM ADD1] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`i':num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i + SUC j)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + j):num`) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((i + j) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM (fun th-> MRESA1_TAC th`(i + SUC j):num` THEN MRESAL1_TAC th`SUC((i + j) MOD 3):num`[ARITH_RULE`SUC(i +j)= i+ SUC j`]) ; ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;unadorned_v39;scs_v39_explicit;is_scs_v39] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`) THEN RESA_TAC THEN REPLICATE_TAC (46-38)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN ASSUME_TAC th THEN REPEAT RESA_TAC) ; ASM_TAC THEN REWRITE_TAC[SET_RULE`A={} <=> ~(?a. A a)`] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (49-36)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`(a+ k- i MOD k)MOD k` THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_lo_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`a:num`] THEN MRESA_TAC th[`(i + (a + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`a:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[SET_RULE`A={} <=> ~(?a. A a)`] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (47-35)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`(a+ k- i MOD k)MOD k` THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_hi_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`a:num`] THEN MRESA_TAC th[`(i + (a + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`a:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[SET_RULE`A={} <=> ~(?a. A a)`] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC (47-36)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`(a+ k- i MOD k)MOD k` THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_str_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`a:num`] THEN MRESA_TAC th[`(i + (a + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`a:num`;`k:num`] ; REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN REPLICATE_TAC (46-37)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN REWRITE_TAC[FUN_EQ_THM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`((x + 3 - i MOD 3) MOD 3)`;`((x' + 3 - i MOD 3) MOD 3)`]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`x:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i + (x + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x' + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + (x' + 3 - i MOD 3) MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i + (x + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x' + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((i + (x' + 3 - i MOD 3) MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (x' MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s x`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (x' MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]) ; REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN REPLICATE_TAC (46-38)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN REWRITE_TAC[FUN_EQ_THM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`((x + 3 - i MOD 3) MOD 3)`;`((x' + 3 - i MOD 3) MOD 3)`]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`x:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + (x + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x' + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + (x' + 3 - i MOD 3) MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i + (x + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x' + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((i + (x' + 3 - i MOD 3) MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (x' MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s x`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (x' MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]) ; REPLICATE_TAC (46-40)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(i''+k- i MOD k)MOD k:num`]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`i'':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + (i'' + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (i'' + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + (i'' + 3 - i MOD 3) MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (i'' + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM 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-> MRESA_TAC th[`i'':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i'' MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i'':num`]) ; EXISTS_TAC`(i+i') MOD k:num` THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(A+B)= A+ SUC B`] THEN REPEAT RESA_TAC; REWRITE_TAC[IN_ELIM_THM;IN_SING] THEN EQ_TAC ; REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`x+3- i MOD 3`;`k:num`] THEN REPLICATE_TAC (50-41)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING] THEN MRESAL_TAC th[`(x +k-i MOD k) MOD k:num`][IN_ELIM_THM;IN_SING]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`x:num`;`k:num`] THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`x:num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (i + (x + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + SUC ((x + 3 - i MOD 3) MOD 3))`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC((x + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + (x + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s x`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (SUC x MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`]) THEN STRIP_TAC THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`] THEN MRESA_TAC MOD_LT[`i':num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k ==> (i' MOD 3 + i MOD 3) + 3 - i MOD 3= i' MOD 3 +3`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i' MOD 3:num`][ARITH_RULE`1*k+a=a+k`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`i':num`;`k:num`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`i' MOD k + i MOD k:num`;`x:num`;`3- i MOD 3:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ 3 - i MOD 3 + x= x+ 3- i MOD 3`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`i' + i MOD 3= i MOD 3+i'`] THEN RESA_TAC THEN MRESA_TAC MOD_LT[`x:num`;`k:num`] ; RESA_TAC THEN MRESA_TAC DIVISION[`i+i':num`;`k:num`] THEN REPLICATE_TAC (49-41)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`x:num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (i+i')`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + i') MOD 3)`] THEN MRESA_TAC th[`(i + SUC i')`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (SUC ((i+i') MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + i') :num`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESAL_TAC MOD_ADD_MOD[`i+i':num`;`1:num`;`k:num`][ARITH_RULE`1 MOD 3=1`;ADD_AC]; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`x:num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i+i')`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + i') MOD 3)`] THEN MRESA_TAC th[`(i + SUC i')`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC ((i+i') MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + i') :num`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESAL_TAC MOD_ADD_MOD[`i+i':num`;`1:num`;`k:num`][ARITH_RULE`1 MOD 3=1`;ADD_AC]; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`x:num`;`k:num`][ARITH_RULE`1<3`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i+i')`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + i') MOD 3)`] THEN MRESA_TAC th[`(i + SUC i')`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC ((i+i') MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(i + i') :num`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESAL_TAC MOD_ADD_MOD[`i+i':num`;`1:num`;`k:num`][ARITH_RULE`1 MOD 3=1`;ADD_AC]; REPLICATE_TAC (48-41)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) THEN MRESA_TAC DIVISION[`j+3- i MOD 3`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> (i MOD 3 + i' MOD 3) + 3 - i MOD 3= 3+ i' MOD 3`) THEN RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`i':num`;`k:num`] THEN MRESA_TAC MOD_LT[`j:num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i' MOD 3:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`j:num`;`i MOD k + i' MOD k:num`;`3- i MOD 3:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ 3 - i MOD 3 + x= x+ 3- i MOD 3`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_LT[`i':num`;`k:num`] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`j:num`;`k:num`] THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`j:num`;`k:num`][ARITH_RULE`1<3`] THEN REPLICATE_TAC (61-43)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`(j+k-i MOD k) MOD k:num`][IN_ELIM_THM;IN_SING]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 2(POP_ASSUM MP_TAC) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i + (j + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((j + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + SUC ((j + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((j + 3 - i MOD 3) MOD 3)`]) 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`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC j`]) THEN REPEAT RESA_TAC; REPLICATE_TAC (48-41)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`i':num`][IN_ELIM_THM;IN_SING]) THEN MRESA_TAC DIVISION[`j+3- i MOD 3`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> (i MOD 3 + i' MOD 3) + 3 - i MOD 3= 3+ i' MOD 3`) THEN RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`i':num`;`k:num`] THEN MRESA_TAC MOD_LT[`j:num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i' MOD 3:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`j:num`;`i MOD k + i' MOD k:num`;`3- i MOD 3:num`;`k:num`] [ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ 3 - i MOD 3 + x= x+ 3- i MOD 3`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_LT[`i':num`;`k:num`] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`j:num`;`k:num`] THEN MRESAL_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`j:num`;`k:num`][ARITH_RULE`1<3`] THEN REPLICATE_TAC (61-43)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`(j+k-i MOD k) MOD k:num`][IN_ELIM_THM;IN_SING]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 2(POP_ASSUM MP_TAC) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + (j + 3 - i MOD 3) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((j + 3 - i MOD 3) MOD 3)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + SUC ((j + 3 - i MOD 3) MOD 3)) MOD 3)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((j + 3 - i MOD 3) MOD 3)`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s j`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC j`]) THEN REPEAT RESA_TAC; ]);; let PRO_EQU_DSV_EQ=prove_by_refinement(` is_scs_v39 s /\ BBs_v39 s vv ==> dsv_v39 (scs_prop_equ_v39 s i) (\x. vv (i+x)) = dsv_v39 s vv`, [STRIP_TAC THEN MP_TAC PRO_EQU_IS_EAR THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<= k==> ~(k=0)/\ 1< k`) THEN RESA_TAC THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`) THEN RESA_TAC; MATCH_MP_TAC(REAL_ARITH`a=b==> a1+ #0.1 * &1 *a=a1+ #0.1 * &1 *b`) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\j. (i+j)MOD k)` THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC ; REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC`(y+k- i MOD k) MOD k` THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC DIVISION[`y+k- i MOD k`;`k:num`] THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + (y + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (y)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC y`]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k==> i MOD k + y + k - i MOD k= k+ y`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y+k-i MOD k:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)`] ; MRESA_TAC DIVISION[`i+x:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x)MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC((i +x) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] ; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`(vv:num->real^3)`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x +1`] THEN MRESA_TAC th[`i + x:num`] THEN MRESA_TAC th[`SUC ((i + x) MOD k)`]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] THEN RESA_TAC; MATCH_MP_TAC(REAL_ARITH`a=b==> a1+ #0.1 * -- &1 *a=a1+ #0.1 * -- &1 *b`) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\j. (i+j)MOD k)` THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC ; REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC`(y+k- i MOD k) MOD k` THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC DIVISION[`y+k- i MOD k`;`k:num`] THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + (y + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (y)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC y`]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k==> i MOD k + y + k - i MOD k= k+ y`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y+k-i MOD k:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)`] ; MRESA_TAC DIVISION[`i+x:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x)MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC((i +x) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] ; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`(vv:num->real^3)`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x +1`] THEN MRESA_TAC th[`i + x:num`] THEN MRESA_TAC th[`SUC ((i + x) MOD k)`]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] THEN RESA_TAC; MATCH_MP_TAC(REAL_ARITH`a=b==> a1+ #0.1 * &1 *a=a1+ #0.1 * &1 *b`) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\j. (i+j)MOD k)` THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC ; REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC`(y+k- i MOD k) MOD k` THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC DIVISION[`y+k- i MOD k`;`k:num`] THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + (y + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (y)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC y`]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k==> i MOD k + y + k - i MOD k= k+ y`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y+k-i MOD k:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)`] ; MRESA_TAC DIVISION[`i+x:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x)MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC((i +x) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] ; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`(vv:num->real^3)`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x +1`] THEN MRESA_TAC th[`i + x:num`] THEN MRESA_TAC th[`SUC ((i + x) MOD k)`]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] THEN RESA_TAC; MATCH_MP_TAC(REAL_ARITH`a=b==> a1+ #0.1 * -- &1 *a=a1+ #0.1 * -- &1 *b`) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\j. (i+j)MOD k)` THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC ; REWRITE_TAC[EXISTS_UNIQUE] THEN EXISTS_TAC`(y+k- i MOD k) MOD k` THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC (GEN_ALL TRANS_MOD_EQ_SUC)[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC DIVISION[`y+k- i MOD k`;`k:num`] THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + (y + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC ((y + k - i MOD k) MOD k)) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((y + k - i MOD k) MOD k)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (y)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC y`]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k/\ 3<=k==> i MOD k + y + k - i MOD k= k+ y`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y':num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`y+k-i MOD k:num`;`i MOD k:num`;`k:num`] [ARITH_RULE`~(3=0)`] ; MRESA_TAC DIVISION[`i+x:num`;`k:num`] ; ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + SUC x) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i +x)MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC((i +x) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] ; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`(vv:num->real^3)`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + x +1`] THEN MRESA_TAC th[`i + x:num`] THEN MRESA_TAC th[`SUC ((i + x) MOD k)`]) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`i+x:num`;`1:num`;`k:num`][ADD_AC] THEN RESA_TAC; ]);; let PRO_EQU_TAUSTAR_EQ=prove_by_refinement(` is_scs_v39 s /\ BBs_v39 s vv ==> taustar_v39 (scs_prop_equ_v39 s i) (\j. vv (i+j)) = taustar_v39 s vv`, [ STRIP_TAC THEN MP_TAC PRO_EQU_DSV_EQ THEN RESA_TAC THEN REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN REPEAT RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC(ARITH_RULE`3<= k==> ~(k=0)/\ 1< k/\ 0real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i+0`] THEN MRESA_TAC th[`i+1`] THEN MRESA_TAC th[`i+2`]) THEN REPLICATE_TAC (3)(POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN MRESA_TAC MOD_LT[`0`;`k:num`] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESA_TAC MOD_LT[`2`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`0`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`2`;`k:num`] THEN REPLICATE_TAC (3)(POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN MP_TAC(ARITH_RULE`3<=k /\ k<= 3==> k=3`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD 3<3==> i MOD 3=0\/ i MOD 3=1\/ i MOD 3=2`) THEN RESA_TAC THEN REWRITE_TAC[tau3; ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 0 MOD 3=0/\ 4 MOD 3=1/\ 5 MOD 3=2/\ 3 MOD 3=0/\ 0+A=A/\ 1+2=3/\ 2+1=3/\ 2+2=4/\ 2+3=5/\ 3+2=5/\ 1+1=2/\1+0=1/\ 2+0=2`] THEN REAL_ARITH_TAC; MP_TAC(ARITH_RULE` k<=3\/ ~(k<=3)`) THEN RESA_TAC; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i+0`] THEN MRESA_TAC th[`i+1`] THEN MRESA_TAC th[`i+2`]) THEN REPLICATE_TAC (3)(POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN MRESA_TAC MOD_LT[`0`;`k:num`] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESA_TAC MOD_LT[`2`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`0`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`2`;`k:num`] THEN REPLICATE_TAC (3)(POP_ASSUM (fun th-> REWRITE_TAC[SYM th])) THEN MP_TAC(ARITH_RULE`3<=k /\ k<= 3==> k=3`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD 3<3==> i MOD 3=0\/ i MOD 3=1\/ i MOD 3=2`) THEN RESA_TAC THEN REWRITE_TAC[tau3; ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 0 MOD 3=0/\ 4 MOD 3=1/\ 5 MOD 3=2/\ 3 MOD 3=0/\ 0+A=A/\ 1+2=3/\ 2+1=3/\ 2+2=4/\ 2+3=5/\ 3+2=5/\ 1+1=2/\1+0=1/\ 2+0=2`] THEN REAL_ARITH_TAC; MATCH_MP_TAC(REAL_ARITH`a=b==> a-c=b-c`) THEN REWRITE_TAC[tau_fun] THEN MP_TAC TRANS_FF THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN RESA_TAC THEN MATCH_MP_TAC(REAL_ARITH`a=b==> a-c=b-c`) THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SYM th;]) THEN MRESAL_TAC (GEN_ALL SUM_AZIM_EQ_ANGLE_LE4) [`IMAGE (vv:num->real^3) (:num)`;`vv:num->real^3`;`i:num`;`s:scs_v39`;`(vv:num->real^3)(i MOD k)`;`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)`][BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MP_TAC BB_TRANS_SUBSET_BB THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL PROP_EQU_IS_SCS)[`k:num`;`s:scs_v39`;`i:num`;`scs_prop_equ_v39 s i`] [BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN MRESAL_TAC (GEN_ALL SUM_AZIM_EQ_ANGLE_LE4) [`IMAGE (\x. (vv:num->real^3) (i + x)) (:num)`;`(\x. (vv:num->real^3) (i+x)) `;`0:num`;`scs_prop_equ_v39 s i`;`(\x. (vv:num->real^3) (i+x))(0 MOD k)`;`IMAGE (\i'. vv (i + i'),(vv:num->real^3) (i + SUC i')) (:num)`;`IMAGE (\i'. {(vv:num->real^3) (i + i'), vv (i + SUC i')}) (:num)`][BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN MRESAL_TAC MOD_LT[`0`;`k:num`][ARITH_RULE`A+0=A`] THEN MP_TAC TRANS_FF THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC THEN REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN MATCH_MP_TAC(SET_RULE`A==> A\/ B`) THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> STRIP_TAC THEN MRESA_TAC th[`i+x:num`] THEN MRESA_TAC th[`x +i MOD k:num`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_LT[`x:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`x:num`;`k:num`] THEN ASM_REWRITE_TAC[ARITH_RULE`x+ i MOD k= i MOD k+ x`]]);; let TRANS_ID_INDEX=prove(`~(k=0) ==> (k- i MOD k +i+ j) MOD k= j MOD k`, STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k=0 \/ ~(i MOD k=0)`) THEN RESA_TAC THENL[ REWRITE_TAC[ARITH_RULE`k-0=k`] THEN MRESA_TAC MOD_REFL[`j:num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i+j:num`][ARITH_RULE`1*k=k`] THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`j:num`;`k:num`][ARITH_RULE`1*k=k/\ 0+A=A`]; MP_TAC(ARITH_RULE`~(i MOD k = 0) /\ i MOD k< k/\ ~(k=0)==> k -i MOD k REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`0+A=A`]) THEN MRESA_TAC MOD_REFL[`j:num`;`k:num`]]);; let TRANS_SCS_A_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_a_v39 s (k - i MOD k + i + j) (k - i MOD k + i + j')) = scs_a_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k - i MOD k + i + x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x'`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((k - i MOD k + i + x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; search[`(i + (x + k - i MOD k) MOD k) MOD k`] ;; let TRANS_SCS_A_ID_MOD=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_a_v39 s (i+ (j+ k - i MOD k) MOD k) (i+ (j'+ k - i MOD k) MOD k)) = scs_a_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i + (x + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x' + k - i MOD k) MOD k`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + (x' + k - i MOD k) MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x + k - i MOD k) MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_B_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_b_v39 s (k - i MOD k + i + j) (k - i MOD k + i + j')) = scs_b_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (k - i MOD k + i + x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x'`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((k - i MOD k + i + x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_B_ID_MOD=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_b_v39 s (i+ (j+ k - i MOD k) MOD k) (i+ (j'+ k - i MOD k) MOD k)) = scs_b_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i + (x + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x' + k - i MOD k) MOD k`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((i + (x' + k - i MOD k) MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x + k - i MOD k) MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_AM_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_am_v39 s (k - i MOD k + i + j) (k - i MOD k + i + j')) = scs_am_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (k - i MOD k + i + x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x'`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((k - i MOD k + i + x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_AM_ID_MOD=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_am_v39 s (i+ (j+ k - i MOD k) MOD k) (i+ (j'+ k - i MOD k) MOD k)) = scs_am_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i + (x + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x' + k - i MOD k) MOD k`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((i + (x' + k - i MOD k) MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x + k - i MOD k) MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_BM_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_bm_v39 s (k - i MOD k + i + j) (k - i MOD k + i + j')) = scs_bm_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (k - i MOD k + i + x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x'`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((k - i MOD k + i + x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_BM_ID_MOD=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_bm_v39 s (i+ (j+ k - i MOD k) MOD k) (i+ (j'+ k - i MOD k) MOD k)) = scs_bm_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i + (x + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x' + k - i MOD k) MOD k`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((i + (x' + k - i MOD k) MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x + k - i MOD k) MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_J_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_J_v39 s (k - i MOD k + i + j) (k - i MOD k + i + j')) = scs_J_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (k - i MOD k + i + x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x'`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((k - i MOD k + i + x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_J_ID_MOD=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j j'. scs_J_v39 s (i+ (j+ k - i MOD k) MOD k) (i+ (j'+ k - i MOD k) MOD k)) = scs_J_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (i + (x + k - i MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x' + k - i MOD k) MOD k`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + (x' + k - i MOD k) MOD k) MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + (x + k - i MOD k) MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (x)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x':num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((x') MOD k)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[` x:num`]));; let TRANS_SCS_LO_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j. scs_lo_v39 s (k - i MOD k + i + j)) = scs_lo_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_lo_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`] THEN MRESA_TAC th[`x:num`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX]);; let TRANS_SCS_HI_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j. scs_hi_v39 s (k - i MOD k + i + j)) = scs_hi_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_hi_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`] THEN MRESA_TAC th[`x:num`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX]);; let TRANS_SCS_STR_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> (\j. scs_str_v39 s (k - i MOD k + i + j)) = scs_str_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_str_v39 s `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`] THEN MRESA_TAC th[`x:num`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX]);; let PRO_EQU_ID=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> s= scs_prop_equ_v39 (scs_prop_equ_v39 s (k- i MOD k)) i`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN STRIP_TAC THEN ASM_SIMP_TAC[TRANS_SCS_STR_ID;TRANS_SCS_HI_ID;TRANS_SCS_LO_ID; TRANS_SCS_A_ID;TRANS_SCS_B_ID;TRANS_SCS_AM_ID;TRANS_SCS_BM_ID;TRANS_SCS_J_ID;] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;scs_v39_explicit;scs_k_v39; scs_d_v39;scs_a_v39 ; scs_am_v39 ; scs_bm_v39 ; scs_b_v39 ; scs_J_v39 ; scs_lo_v39 ; scs_hi_v39 ; scs_str_v39; scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST; Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1; Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.drop2; Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop3; Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop0; Misc_defs_and_lemmas.part5; Misc_defs_and_lemmas.part7; Misc_defs_and_lemmas.part8; Misc_defs_and_lemmas.part0;]));; let PRO_EQU_ID1=prove(` scs_k_v39 s =k /\ is_scs_v39 s ==> s= scs_prop_equ_v39 (scs_prop_equ_v39 s i) (k- i MOD k)`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;scs_diag;scs_v39_explicit;is_scs_slice_v39;] THEN STRIP_TAC THEN REWRITE_TAC[ARITH_RULE`i + k - i MOD k+j =k - i MOD k +i +j`] THEN ASM_SIMP_TAC[TRANS_SCS_STR_ID;TRANS_SCS_HI_ID;TRANS_SCS_LO_ID; TRANS_SCS_A_ID;TRANS_SCS_B_ID;TRANS_SCS_AM_ID;TRANS_SCS_BM_ID;TRANS_SCS_J_ID;] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;scs_v39_explicit;scs_k_v39; scs_d_v39;scs_a_v39 ; scs_am_v39 ; scs_bm_v39 ; scs_b_v39 ; scs_J_v39 ; scs_lo_v39 ; scs_hi_v39 ; scs_str_v39; scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST; Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1; Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.drop2; Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop3; Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop0; Misc_defs_and_lemmas.part5; Misc_defs_and_lemmas.part7; Misc_defs_and_lemmas.part8; Misc_defs_and_lemmas.part0;]));; let PROP_EQU_EQ_BB=prove(` is_scs_v39 s/\ is_scs_v39 (scs_prop_equ_v39 s i) /\ BBs_v39 (scs_prop_equ_v39 s i) vv /\ scs_k_v39 s=k ==> BBs_v39 s (\x. vv (k- i MOD k +x))`, STRIP_TAC THEN MP_TAC PRO_EQU_ID1 THEN RESA_TAC THEN MRESA_TAC(GEN_ALL BB_TRANS_SUBSET_BB)[`scs_prop_equ_v39 s i`;`(vv:num->real^3) `;`k- i MOD k`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));; let TRANS_SCS_WW_ID=prove(`scs_k_v39 s= k/\ 3<= k /\ BBs_v39 (scs_prop_equ_v39 s i) ww ==> (\j. ww (k - i MOD k + i + j)) = ww`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - i MOD k + i + x`] THEN MRESA_TAC th[`x:num`]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_ID_INDEX]);; let scs_k_le_3=prove(`is_scs_v39 s ==> 3<= scs_k_v39 s`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2] THEN REPEAT RESA_TAC);; let TRANS_SCS_BBPRIME=prove(` is_scs_v39 s /\ BBprime_v39 s vv ==> BBprime_v39 (scs_prop_equ_v39 s i) (\x. vv (i+x))`, REWRITE_TAC[BBprime_v39] THEN STRIP_TAC THEN MP_TAC BB_TRANS_SUBSET_BB THEN RESA_TAC THEN MP_TAC PRO_EQU_TAUSTAR_EQ THEN RESA_TAC THEN REPEAT STRIP_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN MRESAL_TAC(GEN_ALL PROP_EQU_IS_SCS)[`k:num`;`s:scs_v39`;`i:num`;`(scs_prop_equ_v39 s i)`;][LET_DEF;LET_END_DEF;unadorned_v39;scs_v39_explicit] THEN MP_TAC scs_k_le_3 THEN RESA_TAC THEN MP_TAC TRANS_SCS_WW_ID THEN RESA_TAC THEN MRESA_TAC(GEN_ALL PROP_EQU_EQ_BB)[`s:scs_v39`;`ww:num->real^3`;`i:num`;`k:num`] THEN MRESA_TAC (GEN_ALL PRO_EQU_TAUSTAR_EQ)[`i:num`;`s:scs_v39`;`(\x. (ww:num->real^3) (k - i MOD k + x))`] THEN REPLICATE_TAC (12-2)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MATCH_MP_TAC th) THEN ASM_REWRITE_TAC[]);; let TRANS_BBINDEX_ID= prove_by_refinement(` scs_k_v39 s= k/\ is_scs_v39 s /\ BBs_v39 s vv ==> BBindex_v39 (scs_prop_equ_v39 s i) (\x. vv (i + x)) = BBindex_v39 s vv`, [ STRIP_TAC THEN MP_TAC TRANS_SCS_A_ID_MOD THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2;BBindex_v39] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1 REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + (x + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((SUC x + k - i MOD k) MOD k)`] THEN MRESA_TAC th[`i + SUC ((x + k - i MOD k) MOD k)`] ) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[TRANS_MOD_EQ_SUC;TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`] THEN MRESA_TAC th[`SUC x`] THEN MRESA_TAC th[`i + ((x + k - i MOD k) MOD k)`] THEN MRESA_TAC th[`i + SUC ((x + k - i MOD k) MOD k)`] ) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ_SUC;TRANS_MOD_EQ]; REWRITE_TAC[IN_ELIM_THM;EXISTS_UNIQUE] THEN GEN_TAC THEN RESA_TAC THEN EXISTS_TAC`(i +y) MOD k` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC DIVISION[`i+y:num`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k==> (i MOD k + y MOD k) + k - i MOD k= k + y MOD k`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESA_TAC MOD_REFL[`i+y:num`;`k:num`] THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i MOD k +y MOD k :num`;`k- i MOD k:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`(i +y) MOD k :num`;`k- i MOD k:num`;`k: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 (SUC ((i + y) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + y:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ( ((i + y)))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESA_TAC MOD_LT[`1:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i +y :num`;`1:num`;`k:num`] THEN ASM_REWRITE_TAC[GSYM ADD1] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ( ((i + y)))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y))`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y) MOD k)`] THEN MRESA_TAC th[`((i + y)):num`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;ADD1]) THEN ASM_REWRITE_TAC[GSYM ADD1] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y))`]) THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(i+j)= i+ SUC j`] THEN REPEAT RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`(i +y) :num`;`k- i MOD k:num`;`k:num`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`i+y:num`;`k-i MOD k:num`;`k:num`] [ARITH_RULE`k - i MOD k + y'= y' + k- i MOD k`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN RESA_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0.. k` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; STRIP_TAC; REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN RESA_TAC THEN MRESA_TAC DIVISION[`x+k- i MOD k`;`k:num`] THEN REPLICATE_TAC (31-25)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x:num`;`SUC x`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ((i + (x + k - i MOD k) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + ((SUC x + k - i MOD k) MOD k)`] THEN MRESA_TAC th[`i + SUC ((x + k - i MOD k) MOD k)`] ) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[TRANS_MOD_EQ_SUC;TRANS_MOD_EQ] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`] THEN MRESA_TAC th[`SUC x`] THEN MRESA_TAC th[`i + ((x + k - i MOD k) MOD k)`] THEN MRESA_TAC th[`i + SUC ((x + k - i MOD k) MOD k)`] ) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[TRANS_MOD_EQ_SUC;TRANS_MOD_EQ]; REWRITE_TAC[IN_ELIM_THM;EXISTS_UNIQUE] THEN GEN_TAC THEN RESA_TAC THEN EXISTS_TAC`(i +y) MOD k` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC DIVISION[`i+y:num`;`k:num`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k< k==> (i MOD k + y MOD k) + k - i MOD k= k + y MOD k`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`y:num`][ARITH_RULE`1*k=k`] THEN MRESA_TAC MOD_REFL[`i+y:num`;`k:num`] THEN MRESA_TAC MOD_LT[`y:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i MOD k +y MOD k :num`;`k- i MOD k:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`(i +y) MOD k :num`;`k- i MOD k:num`;`k: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 (SUC ((i + y) MOD k))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`i + y:num`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ( ((i + y)))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y) MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESA_TAC MOD_LT[`1:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i +y :num`;`1:num`;`k:num`] THEN ASM_REWRITE_TAC[GSYM ADD1] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s ( ((i + y)))`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y))`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y) MOD k)`] THEN MRESA_TAC th[`((i + y)):num`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;ADD1]) THEN ASM_REWRITE_TAC[GSYM ADD1] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC ((i + y))`]) THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(i+j)= i+ SUC j`] THEN REPEAT RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`(i +y) :num`;`k- i MOD k:num`;`k:num`] THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y':num`;`i+y:num`;`k-i MOD k:num`;`k:num`] [ARITH_RULE`k - i MOD k + y'= y' + k- i MOD k`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN RESA_TAC]);; let PROP_EQU_EQ_BBPRIME=prove(`is_scs_v39 s/\ is_scs_v39 (scs_prop_equ_v39 s i) /\ BBprime_v39 (scs_prop_equ_v39 s i) vv /\ scs_k_v39 s=k ==> BBprime_v39 s (\x. vv (k- i MOD k +x))`, STRIP_TAC THEN MP_TAC PRO_EQU_ID1 THEN RESA_TAC THEN MRESA_TAC (GEN_ALL TRANS_SCS_BBPRIME)[`scs_prop_equ_v39 s i`;`(vv:num->real^3) `;`k- i MOD k`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));; let TRANS_IMAGE_BBINDEX_EQ=prove(`scs_k_v39 s = k /\ is_scs_v39 s ==> IMAGE (BBindex_v39 (scs_prop_equ_v39 s i)) (BBprime_v39 (scs_prop_equ_v39 s i)) =IMAGE (BBindex_v39 s) (BBprime_v39 s)`, STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC THENL[ REWRITE_TAC[IN] THEN REPEAT RESA_TAC THEN EXISTS_TAC`(\x1. (x':num->real^3) (k- i MOD k +x1))` THEN MRESA_TAC(GEN_ALL PROP_EQU_IS_SCS)[`k:num`;`s:scs_v39`;`i:num`;`(scs_prop_equ_v39 s i)`;] THEN MRESA_TAC (GEN_ALL PROP_EQU_EQ_BBPRIME)[`s:scs_v39`;`x':num->real^3`;`i:num`;`k:num`] THEN MP_TAC scs_k_le_3 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39] THEN REPEAT RESA_TAC THEN MRESA_TAC (GEN_ALL TRANS_SCS_WW_ID)[`s:scs_v39`;`k:num`;`i:num`;`x':num->real^3`] THEN MRESA_TAC(GEN_ALL TRANS_BBINDEX_ID)[`k:num`;`i:num`;`s:scs_v39`;`(\x1. (x':num->real^3) (k - i MOD k + x1))`]; REWRITE_TAC[IN] THEN REPEAT RESA_TAC THEN EXISTS_TAC`(\x1. (x':num->real^3) (i +x1))` THEN MRESA_TAC(GEN_ALL TRANS_SCS_BBPRIME)[`s:scs_v39`;`x':num->real^3`;`i:num`] THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39] THEN REPEAT RESA_TAC THEN MRESA_TAC(GEN_ALL TRANS_BBINDEX_ID)[`k:num`;`i:num`;`s:scs_v39`;`x':num->real^3`]]);; let TRANS_BBINDEX_MIN_EQ=prove(` scs_k_v39 s= k/\ is_scs_v39 s /\ BBs_v39 s vv ==> BBindex_min_v39 (scs_prop_equ_v39 s i) = BBindex_min_v39 s`, SIMP_TAC[BBindex_min_v39;] THEN STRIP_TAC THEN MP_TAC TRANS_IMAGE_BBINDEX_EQ THEN RESA_TAC);; let TRANS_BBPRIME2_SUBSET=prove(` is_scs_v39 s /\ BBprime2_v39 s vv ==> BBprime2_v39 (scs_prop_equ_v39 s i) (\x. vv (i+x))`, REWRITE_TAC[BBprime2_v39] THEN STRIP_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MP_TAC TRANS_SCS_BBPRIME THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39] THEN REPEAT RESA_TAC THEN MP_TAC TRANS_BBINDEX_MIN_EQ THEN RESA_TAC THEN MP_TAC TRANS_BBINDEX_ID THEN RESA_TAC);; let TRANS_MMS_SUBSET=prove(` is_scs_v39 s /\ MMs_v39 s vv ==> MMs_v39 (scs_prop_equ_v39 s i) (\x. vv (i+x))`, REWRITE_TAC[MMs_v39] THEN RESA_TAC THEN MP_TAC TRANS_BBPRIME2_SUBSET THEN RESA_TAC THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;FUN_EQ_THM;periodic2;BBindex_v39] THEN REPEAT RESA_TAC THEN REWRITE_TAC[ARITH_RULE`i + SUC j= SUC(i+j)/\ i + i' + scs_k_v39 s - 1= (i + i') + scs_k_v39 s - 1`] THEN REPLICATE_TAC (8-2)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i+i':num`]));; let YXIONXL3=prove_by_refinement(`!s i. is_scs_v39 s ==> scs_arrow_v39 {s} {scs_prop_equ_v39 s i}`, [REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; MRESA_TAC(GEN_ALL PROP_EQU_IS_SCS)[`k:num`;`s:scs_v39`;`i:num`;`(scs_prop_equ_v39 s i)`;]; DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN EXISTS_TAC`scs_prop_equ_v39 s i` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv. vv IN A`;IN] THEN STRIP_TAC THEN EXISTS_TAC`(\x. (vv:num->real^3) (i+x))` THEN ASM_SIMP_TAC[TRANS_MMS_SUBSET]]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)