(* ========================================================================== *)
(* 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)/\ 1<k`)
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`][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)/\ 1<k`)
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`][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)/\ 1<k`)
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`][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)/\ 1<k`)
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`][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<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i+x:num`;`1`;`k:num`]
THEN REWRITE_TAC[ADD_AC]
THEN 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_a_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_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<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i+x:num`;`1`;`k:num`]
THEN REWRITE_TAC[ADD_AC]
THEN RESA_TAC;


REWRITE_TAC[EXISTS_UNIQUE]
THEN REPEAT RESA_TAC
;

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<k/\ y - i MOD k<k/\ i MOD k+ y - i MOD k= y/\ i MOD k+ SUC(y - i MOD k)= SUC y /\ i + SUC (y - i MOD k)= SUC(i + y - i MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`y- i MOD k`;`k:num`]
THEN MRESA_TAC MOD_LT[`y:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y- i MOD k`;`k:num`]
THEN POP_ASSUM(fun th-> 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<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i MOD k:num`;`(y + k - i MOD k)`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`y:num`][ARITH_RULE`1*k+y=k+y`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`(y + k - i MOD k) MOD k`;`k:num`]
THEN POP_ASSUM(fun th-> 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<k/\ y - i MOD k<k/\ i MOD k+ y - i MOD k= y/\ i MOD k+ SUC(y - i MOD k)= SUC y /\ i + SUC (y - i MOD k)= SUC(i + y - i MOD k)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`y- i MOD k`;`k:num`]
THEN MRESA_TAC MOD_LT[`y:num`;`k:num`]
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`y- i MOD k`;`k:num`]
THEN POP_ASSUM(fun th-> 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<k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`1:num`;`k:num`]
THEN MRESA_TAC MOD_ADD_MOD[`i MOD k:num`;`(y + k - i MOD k)`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`y:num`][ARITH_RULE`1*k+y=k+y`]
THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`(y + k - i MOD k) MOD k`;`k:num`]
THEN POP_ASSUM(fun th-> 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<k ==> (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==> ~(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/\ 0<k/\ 2<k`)
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;


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 <k/\ k - i MOD k + i MOD k =k/\ 0< k`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`k- i MOD k`;`k:num`]
THEN MRESA_TAC MOD_LT[`0`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`0:num`][ARITH_RULE`1*k=k/\ k+0=k`]
THEN MRESA_TAC MOD_ADD_MOD[`k- i MOD k`;`i:num`;`k:num`]
THEN MRESAL_TAC MOD_ADD_MOD[`k- i MOD k +i`;`j:num`;`k:num`][ARITH_RULE`(k - i MOD k + i) + j =k - i MOD k + i + j`]
THEN POP_ASSUM(fun th-> 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<k`)
THEN RESA_TAC
THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ
THEN EXISTS_TAC`(\j. (j+ k- i MOD k) MOD k)`
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;

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;

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) 
*)