1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Jlxfdmj = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
92 let SCS_M_EQ_0= prove_by_refinement(
93 ` CARD (scs_M s) = 0 /\ is_scs_v39 s
94 ==> (!i. scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
97 THEN POP_ASSUM (fun th-> MP_TAC th
99 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
102 THEN REWRITE_TAC[scs_M]
103 THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
104 THEN SUBGOAL_THEN`FINITE
105 {i | i < scs_k_v39 s /\
106 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
108 MATCH_MP_TAC FINITE_SUBSET
109 THEN EXISTS_TAC`0..6`
110 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
115 ABBREV_TAC`k=scs_k_v39 s`
118 MRESA_TAC CARD_EQ_0[`{i | i < scs_k_v39 s /\
119 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
120 THEN POP_ASSUM MP_TAC
121 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
124 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
126 THEN THAYTHES_TAC 2[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
129 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
130 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
131 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
132 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
133 THEN THAYTHES_TAC (29-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
134 THEN POP_ASSUM MP_TAC
135 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
136 THEN REAL_ARITH_TAC]);;
139 let FINITE_SCS_M=prove(`is_scs_v39 s ==> FINITE (scs_M s)`,
140 REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39;scs_M]
142 THEN MATCH_MP_TAC FINITE_SUBSET
143 THEN EXISTS_TAC`0..(scs_k_v39 s)`
144 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
148 let SCS_A_2=prove(`is_scs_v39 s
149 ==> !i. &2<= scs_a_v39 s i (i+1)`,
150 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;GSYM ADD1]
153 THEN ABBREV_TAC`k=scs_k_v39 s`
154 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;is_scs_v39;LET_DEF;LET_END_DEF]
155 THEN THAYTHES_TAC (21-14)[`i MOD k`;`(SUC i) MOD k`][DIVISION;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;Qknvmlb.SUC_MOD_NOT_EQ;]
156 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`]);;
159 let SCS_M_EQ_1= prove_by_refinement(` scs_M s={x} /\ is_scs_v39 s
160 ==> (!i. ~(i MOD scs_k_v39 s=x )==> scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 )`,
163 THEN POP_ASSUM (fun th-> MP_TAC th
165 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
168 THEN REWRITE_TAC[scs_M]
169 THEN REWRITE_TAC[ARITH_RULE`a<=1 <=> a= 0\/ a=1`]
170 THEN SUBGOAL_THEN`FINITE
171 {i | i < scs_k_v39 s /\
172 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
174 MATCH_MP_TAC FINITE_SUBSET
175 THEN EXISTS_TAC`0..6`
176 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
181 ABBREV_TAC`k=scs_k_v39 s`
185 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING]
189 THEN THAYTHEL_ASM_TAC 1[`x:num`][]
190 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
193 THEN ASM_SIMP_TAC[MOD_LT]
195 THEN THAYTHES_TAC 3[`i MOD k`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`;DIVISION]
198 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
199 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
200 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC(i MOD k) :num`;`s:scs_v39`;`i:num`;`SUC(i MOD k) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
201 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i :num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
202 THEN THAYTHES_TAC (31-15)[`i MOD k`;`SUC i MOD k`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
203 THEN POP_ASSUM MP_TAC
204 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k :num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`;Hypermap.lemma_suc_mod]
205 THEN REAL_ARITH_TAC]);;
207 let SCS_M_LE_K=prove(` scs_M s={x}
209 REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
211 THEN THAYTHE_TAC 0[`x:num`]);;
214 let JLXFDMJ_concl = `
215 main_nonlinear_terminal_v11
216 ==>(!s (v:num->real^3) i.
218 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
219 ( dist(v i,v (i+1)) = &2) /\
220 CARD (scs_M s) <= 1 /\
221 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
222 (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\
223 scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1) <= &2 * h0 ==>
224 (!j. ~(j MOD scs_k_v39 s IN scs_M s)==> dist(v j , v(j+1)) = &2))`;;
227 let JLXFDMJ = prove_by_refinement(
234 THEN ABBREV_TAC`k= scs_k_v39 s`
235 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
236 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
237 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
239 THEN POP_ASSUM MP_TAC
242 THEN SUBGOAL_THEN`!i. &2< scs_b_v39 s i (i + 1)`ASSUME_TAC;
246 THEN THAYTHE_TAC 0[`i'`]
247 THEN THAYTHE_TAC 3[`i'`]
252 MP_TAC(ARITH_RULE`CARD (scs_M s)<=1==> CARD (scs_M s) =0 \/ CARD (scs_M s) =1`)
259 THEN MRESA_TAC CARD_EQ_0[`scs_M s`]
261 THEN REMOVE_ASSUM_TAC
262 THEN MP_TAC(ARITH_RULE`i<=j \/ j<=i:num`)
268 THEN SPEC_TAC (`j:num`,`j:num`)
272 REWRITE_TAC[ARITH_RULE`i<= 0<=> i=0`]
274 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]
275 THEN REPEAT RESA_TAC)
280 THEN MP_TAC(ARITH_RULE`i<= SUC j==> SUC j=i \/ i<=j`)
284 THEN MP_TAC SCS_M_EQ_0
286 THEN THAYTHEL_ASM_TAC(24-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
287 THEN THAYTHEL_ASM_TAC(25-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
288 THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
290 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
291 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
292 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
293 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
294 THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
295 THEN MP_TAC Cqaoqlr.CQAOQLR
297 THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
298 THEN MATCH_DICH_TAC 0
299 THEN THAYTHEL_ASM_TAC (32-22)[`j`][ARITH_RULE`SUC i= i+1`]
300 THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`];
305 THEN ABBREV_TAC`t= i-j:num`
306 THEN POP_ASSUM MP_TAC
307 THEN SPEC_TAC (`j:num`,`j:num`)
308 THEN SPEC_TAC (`t:num`,`t:num`)
315 THEN MP_TAC(ARITH_RULE`i-j=0/\ j<=i ==> j=i:num`)
320 THEN MP_TAC(ARITH_RULE`i-j= SUC t/\ j<=i ==> i- SUC j=t/\ SUC j<= i:num`)
322 THEN THAYTHEL_TAC 4 [`SUC j`][ARITH_RULE`SUC i= i+1/\ (i+1)+1=i+2`]
323 THEN MP_TAC SCS_M_EQ_0
325 THEN THAYTHEL_ASM_TAC(26-17)[`j+1`][ARITH_RULE`(i+1)+1=i+2`]
326 THEN THAYTHEL_ASM_TAC(27-13)[`j+2`][ARITH_RULE`(i+2)+1=i+3`]
327 THEN MP_TAC(ARITH_RULE`3<k==> (j+k-1)+1= 1*k+j`)
329 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
330 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
331 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`1*k+j`;`s:scs_v39`;`j+k-1`;`(1*k+j) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
332 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j+k-1`;`j MOD k`;`s:scs_v39`;`j+k-1`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
333 THEN THAYTHEL_ASM_TAC 5 [`j+k-1`][ARITH_RULE`(i+2)+1=i+3`]
334 THEN MP_TAC Cqaoqlr.CQAOQLR
336 THEN THAYTHES_TAC 0[`s`;`v`;`j`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
337 THEN MATCH_DICH_TAC 0
338 THEN THAYTHEL_ASM_TAC (34-24)[`j`][ARITH_RULE`SUC i= i+1`]
339 THEN THAYTHEL_ASM_TAC (0)[`j+1`][ARITH_RULE`SUC (i+1)= i+2`]
346 THEN MRESAL_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][IN_SING]
347 THEN MP_TAC SCS_M_EQ_1
349 THEN SUBGOAL_THEN`~(i MOD k=x)` ASSUME_TAC;
354 THEN ASM_REWRITE_TAC[scs_M;EXTENSION;IN_ELIM_THM;IN_SING]
356 THEN THAYTHE_TAC 0[`i MOD k`]
357 THEN POP_ASSUM MP_TAC
358 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`x`;`k`][MOD_LT;ARITH_RULE`3<k==> ~(k=0)`]
359 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
360 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x`;`SUC x`;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD;MOD_LT]
361 THEN ASM_REWRITE_TAC[ADD1;REAL_ARITH`~(a<b)<=> b<=a`;REAL_ARITH`a<=a`]
368 MP_TAC(ARITH_RULE`~(i MOD k= x)==> i MOD k< x\/ x< i MOD k`)
375 SUBGOAL_THEN `!t. t< i MOD k + k - x ==> dist ((v:num->real^3) (i MOD k+k - t),v ( (i MOD k+k -t) + 1)) = &2`
386 THEN REWRITE_TAC[ARITH_RULE`a-0=a/\ (1 * k + i MOD k) + 1= 1*k+SUC(i MOD k)/\ i MOD k +k=1*k+ i MOD k`]
390 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
391 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+i MOD k`;`v:num->real^3`;`(1*k+i MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
392 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(i MOD k)`;`v:num->real^3`;`(1*k+SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
393 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
394 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;` i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
400 THEN MP_TAC SCS_M_LE_K
402 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k ==> t< i MOD k+k-x`)
406 THEN POP_ASSUM MP_TAC
407 THEN ABBREV_TAC`j1= i MOD k + k - (t+1)`
408 THEN MRESA_TAC Ssrnat.subn_sub[`t`;`k`;`1`]
409 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> i MOD k+ k-t=(i MOD k +k-t-1)+1 `)
411 THEN ASM_REWRITE_TAC[ADD1;ARITH_RULE`(i+1)+1=i+2`]
413 THEN THAYTHEL_ASM_TAC(30-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
414 THEN THAYTHEL_ASM_TAC(31-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
415 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
417 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
418 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
419 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
420 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
421 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
422 THEN MP_TAC Cqaoqlr.CQAOQLR
424 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
425 THEN MATCH_DICH_TAC 0
426 THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;
428 MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
435 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
437 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
440 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= i MOD k +k-(t+1) ==> i MOD k +k-(t+1) = 1*k+ i MOD k-(t+1)/\ i MOD k-(t+1)<k/\ ~(i MOD k - (t + 1) = x)`)
442 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
448 SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;
450 MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
457 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> ~(i MOD k +k-(t+1) =x) /\ ~((i MOD k +k-(t+1)) +1 =x)`)
459 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
462 MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x ==> (SUC(i MOD k) +k-(t+1)) =(i MOD k +k-(t+1)) +1`)
464 THEN MP_TAC(ARITH_RULE`SUC t < i MOD k + k - x /\ x<k /\ i MOD k<x /\ k<= (SUC(i MOD k) +k-(t+1)) ==> (i MOD k +k-(t+1))+1 = 1*k+ SUC(i MOD k)-(t+1)/\ (i MOD k +k-(t+1)) +1=(SUC(i MOD k) +k-(t+1)) /\ SUC(i MOD k)-(t+1)<k/\ ~(i MOD k - t = x) `)
466 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
467 THEN ASM_REWRITE_TAC[ADD1;SUB_ADD_RCANCEL];
470 THAYTHEL_ASM_TAC (40-19)[`j1`][ARITH_RULE`SUC i= i+1`;MOD_LT]
471 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
477 SUBGOAL_THEN `!t. t< x-i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+ t) + 1)) = &2`
490 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
494 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
495 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
496 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
497 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
501 THEN MP_TAC(ARITH_RULE`i MOD k< x/\ SUC t< x - i MOD k
506 THEN ABBREV_TAC`j1=i MOD k+t`
507 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k + t)+1/\ (j1 + 1) + 1= j1+2`]
508 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
509 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
510 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
512 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
513 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
514 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
515 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
516 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
517 THEN MP_TAC Cqaoqlr.CQAOQLR
519 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
520 THEN MATCH_DICH_TAC 0
521 THEN MP_TAC SCS_M_LE_K
523 THEN MP_TAC(ARITH_RULE`SUC t < x - i MOD k/\ x<k /\ i MOD k<x/\ 3<k==> i MOD k + t <k /\ ~(i MOD k+t= x)/\ ~((i MOD k +t)+1=x)/\ (i MOD k + t)+1 <k/\ ~(k=0)`)
528 THAYTHEL_ASM_TAC (41-19)[`j1`][ARITH_RULE` SUC i= i+1`;]
529 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ARITH_RULE`SUC (i+1)= i+2`;MOD_LT]
532 THEN ASM_SIMP_TAC[MOD_LT];
536 MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
543 THEN MP_TAC(ARITH_RULE`j MOD k <= i MOD k /\ i MOD k< x /\ x<k
544 ==> (i MOD k- j MOD k) < i MOD k + k - x /\ i MOD k + k - (i MOD k - j MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
546 THEN THAYTHE_TAC 6[`i MOD k - j MOD k`]
551 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
552 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+j MOD k`;`v:num->real^3`;`(1*k+j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
553 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
554 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1*k+SUC(j MOD k)`;`v:num->real^3`;`(1*k+ SUC(j MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
555 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
562 THEN MP_TAC(ARITH_RULE`~(j MOD k= x)==> j MOD k< x \/ x< j MOD k`)
567 MP_TAC(ARITH_RULE`j MOD k< x/\ i MOD k<= j MOD k==> j MOD k- i MOD k< x- i MOD k /\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
569 THEN THAYTHE_TAC (30-25)[`j MOD k- i MOD k`]
574 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
575 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
576 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
577 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
582 MP_TAC(ARITH_RULE`i MOD k< x/\ x< j MOD k /\ j MOD k<k==> i MOD k+k- j MOD k< i MOD k+ k- x
583 /\ i MOD k +k -(i MOD k+k- j MOD k)= j MOD k`)
584 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;DIVISION]
586 THEN THAYTHE_TAC (30-24)[`i MOD k+k- j MOD k`]
591 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
592 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
593 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
594 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
602 SUBGOAL_THEN `!t. t< x +k- i MOD k ==> dist ((v:num->real^3) (i MOD k+t),v ( (i MOD k+t) + 1)) = &2`
615 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;GSYM ADD1]
619 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
620 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
621 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
622 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
626 THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t< x +k- i MOD k
627 ==> t< x +k - i MOD k`)
631 THEN ABBREV_TAC`j1=i MOD k+t`
632 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k + t)+1/\ (j1 + 1) + 1= j1+2`]
633 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
634 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
635 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
637 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
638 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
639 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
640 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
641 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
642 THEN MP_TAC Cqaoqlr.CQAOQLR
644 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
645 THEN MATCH_DICH_TAC 0
646 THEN MP_TAC SCS_M_LE_K
648 THEN SUBGOAL_THEN`~(j1 MOD k= x)`ASSUME_TAC;
650 MP_TAC (ARITH_RULE`j1<k\/ k<= j1:num`)
657 MP_TAC(ARITH_RULE`x<i MOD k ==> ~(i MOD k +t =x) `)
659 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
662 MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= i MOD k +t ==> (i MOD k+t) -k<k/\ ~((i MOD k+t) -k= x)/\ i MOD k+t = 1*k+ (i MOD k+t) -k`)
664 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
665 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
671 SUBGOAL_THEN`~((j1+1) MOD k= x)`ASSUME_TAC;
673 MP_TAC (ARITH_RULE`j1+1<k\/ k<= j1+1:num`)
678 MP_TAC(ARITH_RULE`x<i MOD k ==> ~((i MOD k +t) +1=x) `)
680 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`];
683 MP_TAC(ARITH_RULE`SUC t < x + k - i MOD k /\ x<k /\ x<i MOD k /\ k<= (i MOD k +t)+1 ==> ((i MOD k+t)+1) -k<k/\ ~(((i MOD k+t) +1)-k= x)/\ (i MOD k+t)+1 = 1*k+ ((i MOD k+t) +1)-k`)
685 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
686 THEN ASM_SIMP_TAC[MOD_LT;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD];
689 THAYTHEL_ASM_TAC (38-19)[`j1`][ADD1]
690 THEN THAYTHEL_ASM_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`]
697 SUBGOAL_THEN `!t. t< i MOD k- x ==> dist ((v:num->real^3) (i MOD k-t),v ( (i MOD k-t) + 1)) = &2`
708 THEN REWRITE_TAC[ARITH_RULE`a-0=a`;GSYM ADD1]
712 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
713 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`; MOD_MULT_ADD]
714 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(i MOD k)`;`v:num->real^3`;`(SUC(i MOD k)) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD]
715 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i MOD k`;`v:num->real^3`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
719 THEN MP_TAC(ARITH_RULE`x<i MOD k/\ SUC t< i MOD k-x
724 THEN ABBREV_TAC`j1=i MOD k-(t+1)`
725 THEN ASM_REWRITE_TAC[ARITH_RULE`i MOD k + SUC t= (i MOD k + t)+1/\ (j1 + 1) + 1= j1+2`]
726 THEN THAYTHEL_ASM_TAC(27-17)[`j1+1`][ARITH_RULE`(i+1)+1=i+2`]
727 THEN THAYTHEL_ASM_TAC(28-13)[`j1+2`][ARITH_RULE`(i+2)+1=i+3`]
728 THEN MP_TAC(ARITH_RULE`3<k==> (j1+k-1)+1= 1*k+j1`)
730 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
731 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
732 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`1*k+j1`;`s:scs_v39`;`j1+k-1`;`(1*k+j1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
733 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`j1+k-1`;`j1 MOD k`;`s:scs_v39`;`j1+k-1`;`j1`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`;MOD_MULT_ADD]
734 THEN THAYTHEL_ASM_TAC 5 [`j1+k-1`][ARITH_RULE`(i+2)+1=i+3`]
736 THEN MP_TAC(ARITH_RULE`SUC t< i MOD k- x /\ x< i MOD k/\ i MOD k<k==> i MOD k - t=(i MOD k - (t+1)) + 1/\ i MOD k - t +1=(i MOD k - (t+1)) + 2/\ i MOD k - (t+1)<k/\ (i MOD k - (t+1))+1<k/\ ~((i MOD k - (t+1))+1= x)/\ ~((i MOD k - (t+1))= x)`)
737 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
740 THEN MP_TAC Cqaoqlr.CQAOQLR
742 THEN THAYTHES_TAC 0[`s`;`v`;`j1`][ARITH_RULE`SUC j= j+1/\ SUC j+1= j+2`;IN]
743 THEN MATCH_DICH_TAC 0
748 THAYTHEL_ASM_TAC (41-19)[`j1`][ADD1;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
749 THEN THAYTHES_TAC (0)[`j1+1`][ADD1;ARITH_RULE`(j1 + 1) + 1= j1+2`;ARITH_RULE`3<k==> ~(k=0)`; MOD_LT]
757 THEN MP_TAC(ARITH_RULE`~(j MOD k = x)==> j MOD k< x\/ x< j MOD k`)
762 MP_TAC(ARITH_RULE`j MOD k< x/\ x< i MOD k/\ i MOD k<k==> j MOD k+ k- i MOD k< x+k- i MOD k/\ i MOD k+(j MOD k+ k- i MOD k)= 1*k+ j MOD k/\ (1 * k + j MOD k) + 1= 1 * k + SUC(j MOD k) `)
763 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
765 THEN THAYTHE_TAC 6[`j MOD k+ k- i MOD k`]
770 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
771 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + j MOD k`;`v:num->real^3`;`(1 * k + j MOD k)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
772 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
773 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + SUC(j MOD k)`;`v:num->real^3`;`(1 * k + SUC(j MOD k))MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
774 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;` SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;ADD1]
778 MP_TAC(ARITH_RULE`j MOD k<= i MOD k\/ i MOD k<= j MOD k`)
783 MP_TAC(ARITH_RULE`x< j MOD k/\ j MOD k<= i MOD k==> i MOD k- j MOD k< i MOD k - x/\ i MOD k- (i MOD k- j MOD k)= j MOD k`)
785 THEN THAYTHE_TAC (30-25)[`i MOD k- j MOD k`]
790 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
791 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
792 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
793 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
797 MP_TAC(ARITH_RULE`i MOD k<= j MOD k /\ j MOD k< k ==> j MOD k- i MOD k< x+k-i MOD k/\ i MOD k+(j MOD k- i MOD k)= j MOD k`)
798 THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> ~(k=0)`;DIVISION]
800 THEN THAYTHE_TAC (30-24)[`j MOD k- i MOD k`]
805 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
806 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j MOD k`;`v:num->real^3`;`j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;]
807 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC(j MOD k)`;`v:num->real^3`;`SUC(j MOD k) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
808 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j MOD k`;`v:num->real^3`;`SUC j`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)/\ 1<k`; MOD_MULT_ADD;MOD_SUC_MOD;GSYM ADD1]
819 let check_completeness_claimA_concl =
820 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)