text_formalization/local/ZITHLQN.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Zithlqn = struct
  16
  17
  18 open Hypermap;;
  19 open Fan;;
  20 open Wrgcvdr_cizmrrh;;
  21 open Local_lemmas;;
  22 open Flyspeck_constants;;
  23 open Pack_defs;;
  24
  25 open Hales_tactic;;
  26
  27 open Appendix;;
  28
  29
  30
  31
  32 let s_init_J_empty= prove_by_refinement(
  33 `!s. MEM s  s_init_list_v39   ==> scs_J_v39 s = (\i j. F)`,
  34   (* {{{ proof *)
  35 [
  36 REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;LET_DEF;LET_END_DEF;set_of_list; FORALL_IN_CLAUSES;
  37 scs_J_v39_explicit;mk_unadorned_v39]
  38 ]);;
  39   (* }}} *)
  40
  41 let dsv_scs_init= prove_by_refinement(
  42 ` MEM s  s_init_list_v39   ==> dsv_v39 s vv = scs_d_v39 s`,
  43   (* {{{ proof *)
  44 [
  45 SIMP_TAC[s_init_J_empty;dsv_J_empty]
  46 ]);;
  47   (* }}} *)
  48
  49
  50 let exists_point_in_V= prove_by_refinement(
  51 `  convex_local_fan (V,E,FF) /\
  52     packing V /\
  53     V SUBSET ball_annulus /\
  54     3 <= CARD V /\ CARD V <= 6
  55 ==> ?v. v IN V`,
  56   (* {{{ proof *)
  57 [
  58 ONCE_REWRITE_TAC[SET_RULE`(?v. v IN V)<=> ~(V={})`]
  59 THEN REPEAT STRIP_TAC
  60 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;CARD_CLAUSES])
  61 THEN ARITH_TAC
  62 ]);;
  63   (* }}} *)
  64
  65
  66
  67
  68
  69
  70 let exists_vv_FF= prove_by_refinement(
  71 `  convex_local_fan (V,E,FF) /\
  72     packing V /\
  73     V SUBSET ball_annulus /\
  74     3 <= CARD V /\ CARD V <= 6
  75 /\ v, w IN FF
  76 ==> ?vv.
  77  vv 0=v /\ vv 1= w
  78 /\ (!i. vv i= vv (i MOD (CARD V)))
  79 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
  80 /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
  81 /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,
  82   (* {{{ proof *)
  83 [
  84 REPEAT STRIP_TAC
  85 THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
  86 THEN REWRITE_TAC[IMAGE;]
  87 THEN STRIP_TAC;
  88
  89 REWRITE_TAC[ITER];
  90
  91 STRIP_TAC;
  92
  93 REWRITE_TAC[ARITH_RULE`1= SUC 0`; ITER]
  94 THEN MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE
  95 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;];
  96
  97 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
  98 THEN
  99 MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`(V:real^3->bool)`]
 100 THEN REMOVE_ASSUM_TAC
 101 THEN POP_ASSUM MP_TAC
 102 THEN REMOVE_ASSUM_TAC
 103 THEN REMOVE_ASSUM_TAC
 104 THEN REMOVE_ASSUM_TAC
 105 THEN REMOVE_ASSUM_TAC
 106 THEN STRIP_TAC
 107 THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;
 108
 109 GEN_TAC
 110 THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
 111 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
 112 THEN RESA_TAC
 113 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
 114 THEN REMOVE_ASSUM_TAC
 115 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
 116 THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
 117 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 118 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 119 THEN RESA_TAC
 120 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
 121 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
 122 THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];
 123
 124 STRIP_TAC;
 125
 126 POP_ASSUM MP_TAC
 127 THEN SET_TAC[];
 128
 129 STRIP_TAC;
 130
 131 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 132 THEN REPEAT GEN_TAC
 133 THEN STRIP_TAC
 134 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 135 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
 136 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
 137 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
 138 THEN POP_ASSUM MATCH_MP_TAC
 139 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
 140 THEN RESA_TAC
 141 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
 142 THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];
 143
 144 REMOVE_ASSUM_TAC
 145 THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;
 146
 147 REWRITE_TAC[EXTENSION]
 148 THEN GEN_TAC
 149 THEN EQ_TAC;
 150
 151 REWRITE_TAC[IN_ELIM_THM]
 152 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 153 THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
 154 THEN STRIP_TAC
 155 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
 156 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
 157 THEN REWRITE_TAC[IN_ELIM_THM]
 158 THEN STRIP_TAC
 159 THEN EXISTS_TAC`n:num`
 160 THEN ASM_REWRITE_TAC[]
 161 THEN SET_TAC[];
 162
 163 REWRITE_TAC[IN_ELIM_THM]
 164 THEN STRIP_TAC
 165 THEN ASM_REWRITE_TAC[]
 166 THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
 167 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 168 THEN STRIP_TAC
 169 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);
 170
 171 ASM_REWRITE_TAC[]
 172 THEN STRIP_TAC;
 173
 174 ONCE_REWRITE_TAC[EXTENSION]
 175 THEN GEN_TAC
 176 THEN EQ_TAC;
 177
 178 STRIP_TAC
 179 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 180 THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
 181 THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
 182 THEN POP_ASSUM MP_TAC
 183 THEN REMOVE_ASSUM_TAC
 184 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 185 THEN STRIP_TAC
 186 THEN REWRITE_TAC[IN_ELIM_THM]
 187 THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 188 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
 189 THEN REMOVE_ASSUM_TAC
 190 THEN POP_ASSUM MP_TAC
 191 THEN REWRITE_TAC[IN_ELIM_THM]
 192 THEN STRIP_TAC
 193 THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;
 194
 195 POP_ASSUM MP_TAC
 196 THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];
 197
 198 POP_ASSUM MP_TAC
 199 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
 200 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
 201 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
 202 THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
 203 THEN STRIP_TAC;
 204
 205 EXISTS_TAC`x:num`
 206 THEN ASM_REWRITE_TAC[ITER];
 207
 208 MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
 209 THEN STRIP_TAC;
 210
 211 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
 212 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
 213 THEN ASM_REWRITE_TAC[]
 214 THEN STRIP_TAC
 215 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
 216 THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
 217 THEN ASM_REWRITE_TAC[]
 218 THEN MP_TAC Tecoxbm.RHO_IVS_IDD
 219 THEN ASM_REWRITE_TAC[]
 220 THEN STRIP_TAC
 221 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 222 THEN SET_TAC[];
 223
 224 SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);
 225
 226 EXISTS_TAC`x-1`
 227 THEN POP_ASSUM MP_TAC
 228 THEN ARITH_TAC;
 229
 230 EXISTS_TAC`x'':num`
 231 THEN ASM_REWRITE_TAC[ITER]
 232 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 233 THEN ASM_REWRITE_TAC[]
 234 THEN STRIP_TAC
 235 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
 236 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
 237 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
 238 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 239 THEN SET_TAC[];
 240
 241 REWRITE_TAC[IN_ELIM_THM]
 242 THEN STRIP_TAC
 243 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 244 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 245 THEN ASM_REWRITE_TAC[]
 246 THEN STRIP_TAC
 247 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
 248 THEN REWRITE_TAC[ITER]
 249 THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;
 250
 251 ONCE_REWRITE_TAC[EXTENSION]
 252 THEN GEN_TAC
 253 THEN EQ_TAC;
 254
 255 STRIP_TAC
 256 THEN REWRITE_TAC[IN_ELIM_THM]
 257 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 258 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
 259 THEN ASM_REWRITE_TAC[]
 260 THEN STRIP_TAC
 261 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
 262 THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 263 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
 264 THEN REMOVE_ASSUM_TAC
 265 THEN POP_ASSUM MP_TAC
 266 THEN REWRITE_TAC[IN_ELIM_THM]
 267 THEN STRIP_TAC
 268 THEN ASM_REWRITE_TAC[ITER]
 269 THEN EXISTS_TAC`x':num`
 270 THEN ASM_REWRITE_TAC[];
 271
 272 REWRITE_TAC[IN_ELIM_THM]
 273 THEN STRIP_TAC
 274 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 275 THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
 276 THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
 277 THEN STRIP_TAC
 278 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
 279 ]);;
 280   (* }}} *)
 281
 282
 283
 284
 285
 286
 287
 288 let exists_vv= prove_by_refinement(
 289 `  convex_local_fan (V,E,FF) /\
 290     packing V /\
 291     V SUBSET ball_annulus /\
 292     3 <= CARD V /\ CARD V <= 6
 293 ==> ?vv. (!i. vv i= vv (i MOD (CARD V)))
 294 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
 295 /\ V = IMAGE vv (:num) /\ E = IMAGE (\i. {vv i, vv (SUC i)}) (:num)
 296 /\ FF = IMAGE (\i. vv i,vv (SUC i)) (:num)`,
 297   (* {{{ proof *)
 298 [
 299 REPEAT STRIP_TAC
 300 THEN MP_TAC exists_point_in_V
 301 THEN ASM_REWRITE_TAC[]
 302 THEN STRIP_TAC
 303 THEN EXISTS_TAC`(\i:num. ITER i (rho_node1 FF) v)`
 304 THEN REWRITE_TAC[IMAGE;]
 305 THEN SUBGOAL_THEN`!i. ITER i (rho_node1 FF) v = ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v` ASSUME_TAC;
 306
 307 GEN_TAC
 308 THEN REWRITE_TAC[GSYM Wrgcvdr_cizmrrh.POWER_TO_ITER]
 309 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
 310 THEN RESA_TAC
 311 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
 312 THEN REMOVE_ASSUM_TAC
 313 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[th])
 314 THEN REWRITE_TAC[Hypermap.lemma_add_exponent_function;Wrgcvdr_cizmrrh.POWER_TO_ITER]
 315 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 316 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 317 THEN RESA_TAC
 318 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i MOD CARD (V:real^3->bool)`)
 319 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2)[`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`]
 320 THEN MRESAL_TAC Hypermap.power_map_fix_point[`CARD (V:real^3->bool)`;`(rho_node1 FF)`;`ITER (i MOD CARD (V:real^3->bool)) (rho_node1 FF) v`][Wrgcvdr_cizmrrh.POWER_TO_ITER];
 321
 322 STRIP_TAC;
 323
 324 POP_ASSUM MP_TAC
 325 THEN SET_TAC[];
 326
 327 STRIP_TAC;
 328
 329 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 330 THEN REPEAT GEN_TAC
 331 THEN STRIP_TAC
 332 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 333 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LT_CARD_MONO_LOFA)
 334 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`v:real^3`]
 335 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD CARD(V:real^3->bool)`;`j MOD CARD(V:real^3->bool)`])
 336 THEN POP_ASSUM MATCH_MP_TAC
 337 THEN MP_TAC(ARITH_RULE`3<= CARD V==> ~(CARD (V:real^3->bool) = 0)`)
 338 THEN RESA_TAC
 339 THEN MRESA_TAC DIVISION [`i:num`;`CARD (V:real^3->bool)`]
 340 THEN MRESA_TAC DIVISION [`j:num`;`CARD (V:real^3->bool)`];
 341
 342 REMOVE_ASSUM_TAC
 343 THEN SUBGOAL_THEN`V = {y | ?x. x IN (:num) /\ y = ITER x (rho_node1 FF) v}` ASSUME_TAC;
 344
 345 REWRITE_TAC[EXTENSION]
 346 THEN GEN_TAC
 347 THEN EQ_TAC;
 348
 349 REWRITE_TAC[IN_ELIM_THM]
 350 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 351 THEN MP_TAC Local_lemmas.LOFA_IMP_LT_CARD_SET_V
 352 THEN STRIP_TAC
 353 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
 354 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
 355 THEN REWRITE_TAC[IN_ELIM_THM]
 356 THEN STRIP_TAC
 357 THEN EXISTS_TAC`n:num`
 358 THEN ASM_REWRITE_TAC[]
 359 THEN SET_TAC[];
 360
 361 REWRITE_TAC[IN_ELIM_THM]
 362 THEN STRIP_TAC
 363 THEN ASM_REWRITE_TAC[]
 364 THEN MP_TAC Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
 365 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 366 THEN STRIP_TAC
 367 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`x':num`]);
 368
 369 ASM_REWRITE_TAC[]
 370 THEN STRIP_TAC;
 371
 372 ONCE_REWRITE_TAC[EXTENSION]
 373 THEN GEN_TAC
 374 THEN EQ_TAC;
 375
 376 STRIP_TAC
 377 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 378 THEN MRESAL_TAC local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;][LET_DEF;LET_END_DEF]
 379 THEN MRESA_TAC Topology.expand_edge_graph_fan[`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x:real^3->bool`]
 380 THEN POP_ASSUM MP_TAC
 381 THEN REMOVE_ASSUM_TAC
 382 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 383 THEN STRIP_TAC
 384 THEN REWRITE_TAC[IN_ELIM_THM]
 385 THEN POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 386 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
 387 THEN REMOVE_ASSUM_TAC
 388 THEN POP_ASSUM MP_TAC
 389 THEN REWRITE_TAC[IN_ELIM_THM]
 390 THEN STRIP_TAC
 391 THEN SUBGOAL_THEN `(w:real^3) IN EE v' E`ASSUME_TAC;
 392
 393 POP_ASSUM MP_TAC
 394 THEN ASM_REWRITE_TAC[EE;IN_ELIM_THM];
 395
 396 POP_ASSUM MP_TAC
 397 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOCAL_E_SUB_V)[`FF:real^3#real^3->bool`;`(E:(real^3->bool)->bool)`;`v':real^3`;`w:real^3`;`(V:real^3->bool)`]
 398 THEN MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)
 399 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`v':real^3`;]
 400 THEN REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B\/ A=C`]
 401 THEN STRIP_TAC;
 402
 403 EXISTS_TAC`x:num`
 404 THEN ASM_REWRITE_TAC[ITER];
 405
 406 MP_TAC(ARITH_RULE`x =0 \/ 0<x`)
 407 THEN STRIP_TAC;
 408
 409 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th;ITER] THEN REPEAT STRIP_TAC)
 410 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
 411 THEN ASM_REWRITE_TAC[]
 412 THEN STRIP_TAC
 413 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v':real^3`)
 414 THEN EXISTS_TAC`CARD (V:real^3->bool) -1`
 415 THEN ASM_REWRITE_TAC[]
 416 THEN MP_TAC Tecoxbm.RHO_IVS_IDD
 417 THEN ASM_REWRITE_TAC[]
 418 THEN STRIP_TAC
 419 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 420 THEN SET_TAC[];
 421
 422 SUBGOAL_THEN`(?x'. x = SUC x')` (fun th-> MP_TAC th THEN STRIP_TAC);
 423
 424 EXISTS_TAC`x-1`
 425 THEN POP_ASSUM MP_TAC
 426 THEN ARITH_TAC;
 427
 428 EXISTS_TAC`x'':num`
 429 THEN ASM_REWRITE_TAC[ITER]
 430 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 431 THEN ASM_REWRITE_TAC[]
 432 THEN STRIP_TAC
 433 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x'':num`)
 434 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)
 435 [`(E:(real^3->bool)->bool)`;`(V:real^3->bool)`;`FF:real^3#real^3->bool`;`ITER x'' (rho_node1 FF) v:real^3`;]
 436 THEN ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 437 THEN SET_TAC[];
 438
 439 REWRITE_TAC[IN_ELIM_THM]
 440 THEN STRIP_TAC
 441 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 442 THEN MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
 443 THEN ASM_REWRITE_TAC[]
 444 THEN STRIP_TAC
 445 THEN POP_ASSUM(fun th -> MRESA1_TAC th `x':num`)
 446 THEN REWRITE_TAC[ITER]
 447 THEN MRESA1_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E`ITER x' (rho_node1 FF) v`;
 448
 449 ONCE_REWRITE_TAC[EXTENSION]
 450 THEN GEN_TAC
 451 THEN EQ_TAC;
 452
 453 STRIP_TAC
 454 THEN REWRITE_TAC[IN_ELIM_THM]
 455 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 456 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
 457 THEN ASM_REWRITE_TAC[]
 458 THEN STRIP_TAC
 459 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x:real^3#real^3`)
 460 THEN POP_ASSUM (fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 461 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)[`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`(V:real^3->bool)`]
 462 THEN REMOVE_ASSUM_TAC
 463 THEN POP_ASSUM MP_TAC
 464 THEN REWRITE_TAC[IN_ELIM_THM]
 465 THEN STRIP_TAC
 466 THEN ASM_REWRITE_TAC[ITER]
 467 THEN EXISTS_TAC`x':num`
 468 THEN ASM_REWRITE_TAC[];
 469
 470 REWRITE_TAC[IN_ELIM_THM]
 471 THEN STRIP_TAC
 472 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
 473 THEN MP_TAC Local_lemmas1.LOCAL_FAN_ORBIT_MAP_VITERFF
 474 THEN ASM_REWRITE_TAC[ITER;ARITH_RULE`A+1= SUC A`]
 475 THEN STRIP_TAC
 476 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
 477 ]);;
 478   (* }}} *)
 479
 480
 481
 482
 483 let SUC_MOD_NOT_EQ=prove_by_refinement(
 484 `~(i MOD 3 = SUC i MOD 3)`,
 485   (* {{{ proof *)
 486 [
 487 REWRITE_TAC[ADD1]
 488 THEN STRIP_TAC
 489 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
 490 THEN POP_ASSUM MP_TAC
 491 THEN POP_ASSUM MP_TAC
 492 THEN DISCH_THEN(LABEL_TAC"YEU")
 493 THEN DISCH_THEN(LABEL_TAC"EM")
 494 THEN MRESAL_TAC DIV_MONO[`i:num`;`i+1`;`3`][ARITH_RULE`~(3=0)/\ i<= i+1`]
 495 THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
 496 THEN POP_ASSUM MP_TAC
 497 THEN MP_TAC(ARITH_RULE`i DIV 3 <= (i + 1) DIV 3 ==>  (i + 1) DIV 3 = i DIV 3 \/ i DIV 3 < (i + 1) DIV 3`)
 498 THEN RESA_TAC;
 499
 500 REMOVE_ASSUM_TAC
 501 THEN REMOVE_ASSUM_TAC
 502 THEN REMOVE_ASSUM_TAC
 503 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM th])
 504 THEN ARITH_TAC;
 505
 506 STRIP_TAC
 507 THEN POP_ASSUM MP_TAC
 508 THEN REMOVE_THEN "YEU"(fun th-> GEN_REWRITE_TAC(LAND_CONV  o LAND_CONV  o ONCE_DEPTH_CONV)[th])
 509 THEN REWRITE_TAC[ARITH_RULE`(i DIV 3 * 3 + (i + 1) MOD 3) + 1 = (i + 1) DIV 3 * 3 + (i + 1) MOD 3
 510 <=>  1 = ((i + 1) DIV 3 - i DIV 3) * 3`]
 511 THEN MP_TAC(ARITH_RULE`i DIV 3 < (i + 1) DIV 3 ==> 1<= ( (i + 1) DIV 3 -i DIV 3 )`)
 512 THEN ASM_REWRITE_TAC[]
 513 THEN STRIP_TAC
 514 THEN MP_TAC(ARITH_RULE` 1<= ( (i + 1) DIV 3 -i DIV 3 )==> 3<= ( (i + 1) DIV 3 -i DIV 3 ) *3`)
 515 THEN ASM_REWRITE_TAC[]
 516 THEN ARITH_TAC
 517 ]);;
 518   (* }}} *)
 519
 520
 521
 522
 523 let SUC_MOD_EQ1=prove_by_refinement(
 524 `(SUC i MOD 3 = SUC j MOD 3)
 525 /\ i<=j
 526 ==>
 527 (i MOD 3 = j MOD 3) `,
 528   (* {{{ proof *)
 529 [
 530 REWRITE_TAC[ADD1]
 531 THEN STRIP_TAC
 532 THEN MRESAL_TAC DIVISION[`i+1:num`;`3`][ARITH_RULE`~(3=0)`]
 533 THEN REMOVE_ASSUM_TAC
 534 THEN POP_ASSUM MP_TAC
 535 THEN REWRITE_TAC[ARITH_RULE`i + 1 = (i + 1) DIV 3 * 3 + (j + 1) MOD 3
 536 <=>  (j + 1) MOD 3= (i + 1) - ((i + 1) DIV 3 * 3) `]
 537 THEN STRIP_TAC
 538 THEN MRESAL_TAC DIVISION[`j+1:num`;`3`][ARITH_RULE`~(3=0)`]
 539 THEN REMOVE_ASSUM_TAC
 540 THEN POP_ASSUM MP_TAC
 541 THEN REWRITE_TAC[ARITH_RULE`j + 1 = (j + 1) DIV 3 * 3 + (i + 1) - (i + 1) DIV 3 * 3 <=> j+ (i + 1) DIV 3 * 3  =   (j + 1) DIV 3 * 3 +i `]
 542 THEN STRIP_TAC
 543 THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
 544 THEN RESA_TAC
 545 THEN MRESAL_TAC DIV_MONO[`i+1`;`j+1`;`3`][ARITH_RULE`~(3=0)`]
 546 THEN MP_TAC(ARITH_RULE`j + (i + 1) DIV 3 * 3 = (j + 1) DIV 3 * 3 + i
 547 /\ i<= j /\ (i + 1) DIV 3 <= (j + 1) DIV 3
 548 ==> j -i = 3*((j + 1) DIV 3 - (i + 1) DIV 3) `)
 549 THEN ASM_REWRITE_TAC[]
 550 THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`3`][ARITH_RULE`~(3=0)`]
 551 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
 552 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
 553 THEN MP_TAC(ARITH_RULE`j = j DIV 3 * 3 + j MOD 3
 554 /\ i = i DIV 3 * 3 + i MOD 3 /\ i<= j/\ i DIV 3<= j DIV 3
 555 ==> j-i = ((j DIV 3 - i DIV 3) * 3 + j MOD 3)  -i MOD 3 `)
 556 THEN ASM_REWRITE_TAC[]
 557 THEN REMOVE_ASSUM_TAC
 558 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 559 THEN ASM_REWRITE_TAC[]
 560 THEN REMOVE_ASSUM_TAC
 561 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o  DEPTH_CONV)[th])
 562 THEN ASM_REWRITE_TAC[]
 563 THEN STRIP_TAC
 564 THEN STRIP_TAC
 565 THEN MRESAL_TAC MOD_MULT[`3`;`(j + 1) DIV 3 - (i + 1) DIV 3`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
 566 THEN POP_ASSUM MP_TAC
 567 THEN ONCE_REWRITE_TAC[ARITH_RULE`a*b=b*a`]
 568 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 569 THEN MP_TAC(ARITH_RULE`i MOD 3 <=j MOD 3 \/ j MOD 3 < i MOD 3:num`)
 570 THEN STRIP_TAC;
 571
 572 MP_TAC(ARITH_RULE`
 573 i MOD 3 <=j MOD 3
 574 ==>
 575 ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
 576 = (j DIV 3 - i DIV 3) * 3 + j MOD 3 - i MOD 3
 577 `)
 578 THEN RESA_TAC
 579 THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3)`;`3`;`j MOD 3 - i MOD 3`]
 580 THEN MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
 581 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
 582 THEN MP_TAC(ARITH_RULE`j MOD 3 < 3 /\ i MOD 3 <=j MOD 3
 583  ==> j MOD 3 - i MOD 3 < 3 `)
 584 THEN ASM_REWRITE_TAC[]
 585 THEN STRIP_TAC
 586 THEN MRESA_TAC MOD_LT[`j MOD 3 - i MOD 3`;`3`]
 587 THEN ASM_TAC
 588 THEN ARITH_TAC;
 589
 590 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
 591 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
 592 THEN MP_TAC(ARITH_RULE`i MOD 3 < 3/\ j MOD 3< i MOD 3
 593  ==> (3+ j MOD 3) - i MOD 3 < 3  /\ 0< (3+ j MOD 3) - i MOD 3`)
 594 THEN ASM_REWRITE_TAC[]
 595 THEN MP_TAC(ARITH_RULE`j DIV 3 - i DIV 3 =0  \/ 1<= j DIV 3 - i DIV 3:num`)
 596 THEN STRIP_TAC;
 597
 598 POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * 3 + j MOD 3) - i MOD 3= j MOD 3 - i MOD 3`])
 599 THEN REPEAT STRIP_TAC
 600 THEN MP_TAC(ARITH_RULE`j MOD 3 < i MOD 3
 601 /\ j - i = j MOD 3 - i MOD 3 /\ i<= j ==>  j=i `)
 602 THEN ASM_REWRITE_TAC[]
 603 THEN RESA_TAC;
 604
 605 STRIP_TAC
 606 THEN MP_TAC(ARITH_RULE`1 <= j DIV 3 - i DIV 3 /\ 0 < (3 + j MOD 3) - i MOD 3
 607 ==> ((j DIV 3 - i DIV 3) * 3 + j MOD 3) - i MOD 3
 608 =((j DIV 3 - i DIV 3)-1) * 3 +(3+ j MOD 3) - i MOD 3`)
 609 THEN RESA_TAC
 610 THEN MRESA_TAC MOD_MULT_ADD[`(j DIV 3 - i DIV 3 -1)`;`3`;`(3+ j MOD 3) - i MOD 3`]
 611 THEN MRESA_TAC MOD_LT[`(3+j MOD 3) - i MOD 3`;`3`]
 612 THEN REMOVE_ASSUM_TAC
 613 THEN REMOVE_ASSUM_TAC
 614 THEN REMOVE_ASSUM_TAC
 615 THEN POP_ASSUM MP_TAC
 616 THEN ARITH_TAC
 617 ]);;
 618   (* }}} *)
 619
 620 let SUC_MOD_EQ=prove_by_refinement(
 621 `(SUC i MOD 3 = SUC j MOD 3)
 622 ==>
 623 (i MOD 3 = j MOD 3) `,
 624   (* {{{ proof *)
 625 [
 626 REPEAT STRIP_TAC
 627 THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
 628 THEN STRIP_TAC;
 629
 630 MATCH_MP_TAC SUC_MOD_EQ1
 631 THEN ASM_REWRITE_TAC[];
 632
 633 MRESA_TAC (GEN_ALL SUC_MOD_EQ1)[`j:num`;`i:num`]
 634 THEN ASM_REWRITE_TAC[]
 635 ]);;
 636   (* }}} *)
 637
 638
 639 let NOT_IMP_SUC_MOD_EQ=prove_by_refinement(
 640 `~(i MOD 3 = j MOD 3)
 641 ==> ~(SUC i MOD 3 = SUC j MOD 3)`,
 642 [SIMP_TAC[CONTRAPOS_THM;]
 643 THEN REWRITE_TAC[SUC_MOD_EQ]]);;
 644
 645
 646
 647 let IMP_SUC_MOD_EQ1=prove_by_refinement(
 648 ` ~(k=0) /\ (i MOD k = j MOD k)
 649 /\ i<= j
 650 ==> (SUC i MOD k = SUC j MOD k)`,
 651   (* {{{ proof *)
 652 [
 653 REWRITE_TAC[ADD1]
 654 THEN STRIP_TAC
 655 THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][ARITH_RULE`~(3=0)`]
 656 THEN REMOVE_ASSUM_TAC
 657 THEN MP_TAC(ARITH_RULE`i:num = i  DIV k * k + j  MOD k
 658 ==>  j  MOD k = i - (i DIV k * k) `)
 659 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th] THEN ASSUME_TAC th)
 660 THEN RESA_TAC
 661 THEN MRESAL_TAC DIVISION[`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
 662 THEN REMOVE_ASSUM_TAC
 663 THEN POP_ASSUM MP_TAC
 664 THEN MP_TAC(ARITH_RULE`i<=j==> i+1<= j+1`)
 665 THEN RESA_TAC
 666 THEN MRESAL_TAC DIV_MONO[`i:num`;`j:num`;`k:num`][ARITH_RULE`~(3=0)`]
 667 THEN STRIP_TAC
 668 THEN MP_TAC(ARITH_RULE`j = (j  DIV k) * k + i -  (i  DIV k) * k
 669 /\ i +1 <= j+1 /\ i  DIV k <= j  DIV k /\ ~(k=0)
 670 ==> j -i =  (j DIV k) *k - (i  DIV k) *k `)
 671 THEN ASM_REWRITE_TAC[]
 672 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 673 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
 674 THEN ONCE_REWRITE_TAC[MULT_AC]
 675 THEN MRESAL_TAC DIV_MONO[`i+1:num`;`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 676 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 677 THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 678 THEN MRESA_TAC LE_MULT_RCANCEL[`((i+1) DIV k)`;`((j+1) DIV k)`;`k:num`]
 679 THEN MP_TAC(ARITH_RULE`i + 1 = (i + 1) DIV k * k + (i + 1) MOD k
 680 /\ j + 1 = (j + 1) DIV k * k + (j + 1) MOD k /\ i<= j/\ ((i+1) DIV k)*k<= ((j+1) DIV k)*k
 681 ==> j-i = (((j + 1) DIV k * k  - (i + 1) DIV k * k) + (j + 1) MOD k) - (i + 1) MOD k`)
 682 THEN ASM_REWRITE_TAC[]
 683 THEN REMOVE_ASSUM_TAC
 684 THEN REMOVE_ASSUM_TAC
 685 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 686 THEN ASM_REWRITE_TAC[]
 687 THEN REMOVE_ASSUM_TAC
 688 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[th])
 689 THEN ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
 690 THEN STRIP_TAC
 691 THEN STRIP_TAC
 692 THEN MRESAL_TAC MOD_MULT[`k:num`;`j DIV k - i DIV k`][ARITH_RULE`~(3=0)/\ (a*b=b*a)`]
 693 THEN POP_ASSUM MP_TAC
 694 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
 695 THEN MP_TAC(ARITH_RULE`(i+1) MOD k <=(j+1) MOD k \/ (j+1) MOD k < (i+1) MOD k:num`)
 696 THEN STRIP_TAC;
 697
 698 MP_TAC(ARITH_RULE`
 699 (i+1) MOD k <=(j+1) MOD k
 700 ==>
 701 ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)=
 702 (((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k - (i + 1) MOD k)`)
 703 THEN RESA_TAC
 704 THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`;`(j + 1) MOD k - (i + 1) MOD k`]
 705 THEN MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 706 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 707 THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < k /\ (i + 1) MOD k <=(j + 1) MOD k
 708  ==> (j + 1) MOD k  - (i + 1) MOD k < k `)
 709 THEN ASM_REWRITE_TAC[]
 710 THEN STRIP_TAC
 711 THEN MRESA_TAC MOD_LT[`(j + 1) MOD k  - (i + 1) MOD k`;` k:num`]
 712 THEN REPLICATE_TAC 8 (REMOVE_ASSUM_TAC)
 713 THEN POP_ASSUM MP_TAC
 714 THEN ARITH_TAC;
 715
 716 MRESAL_TAC DIVISION[`i+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 717 THEN MRESAL_TAC DIVISION[`j+1:num`;`k:num`][ARITH_RULE`~(3=0)`]
 718 THEN MP_TAC(ARITH_RULE`(i+1) MOD k < k/\ (j+1) MOD k< (i+1) MOD k
 719  ==> (k+ (j+1) MOD k) - (i+1) MOD k < k  /\ 0< (k+ (j+1) MOD k) - (i+1) MOD k`)
 720 THEN ASM_REWRITE_TAC[]
 721 THEN MP_TAC(ARITH_RULE`(j+1) DIV k - (i+1) DIV k =0  \/ 1<= (j+1) DIV k - (i+1) DIV k`)
 722 THEN STRIP_TAC;
 723
 724 POP_ASSUM (fun th -> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE` (0 * k + (j + 1) MOD k) - (i + 1) MOD k= (j + 1) MOD k - (i + 1) MOD k`])
 725 THEN REPEAT STRIP_TAC
 726 THEN MP_TAC(ARITH_RULE`(j + 1) MOD k < (i + 1) MOD k
 727 /\ j - i = (j + 1) MOD k - (i + 1) MOD k /\ i<= j ==>  j=i `)
 728 THEN ASM_REWRITE_TAC[]
 729 THEN RESA_TAC;
 730
 731 STRIP_TAC
 732 THEN MRESAL_TAC LE_MULT_RCANCEL[`1`;`((j + 1) DIV k - (i + 1) DIV k)`;`k:num`][ARITH_RULE`1*k=k`]
 733 THEN MP_TAC(ARITH_RULE`k <= ((j + 1) DIV k - (i + 1) DIV k)*k /\ 0 < (k + (j + 1) MOD k) - (i + 1) MOD k
 734 ==> ((((j + 1) DIV k - (i + 1) DIV k) * k + (j + 1) MOD k) - (i + 1) MOD k)
 735 =
 736 ((((j + 1) DIV k - (i + 1) DIV k) * k- 1*k)+(k+ (j + 1) MOD k) - (i + 1) MOD k)
 737 `)
 738 THEN RESA_TAC
 739 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
 740 THEN MRESA_TAC MOD_MULT_ADD[`((j + 1) DIV k - (i + 1) DIV k - 1)`;`k:num`;`(k + (j + 1) MOD k) - (i + 1) MOD k`]
 741 THEN MRESA_TAC MOD_LT[`(k + (j + 1) MOD k) - (i + 1) MOD k`;`k:num`]
 742 THEN REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
 743 THEN POP_ASSUM MP_TAC
 744 THEN ARITH_TAC
 745 ]);;
 746   (* }}} *)
 747
 748
 749 let IMP_SUC_MOD_EQ=prove_by_refinement(
 750 ` ~(k=0) /\ (i MOD k = j MOD k)
 751 ==> (SUC i MOD k = SUC j MOD k)`,
 752   (* {{{ proof *)
 753 [
 754 REPEAT STRIP_TAC
 755 THEN MP_TAC(ARITH_RULE`i<=j\/ j<=i:num`)
 756 THEN STRIP_TAC;
 757 MATCH_MP_TAC IMP_SUC_MOD_EQ1
 758 THEN ASM_REWRITE_TAC[];
 759 MRESA_TAC (GEN_ALL IMP_SUC_MOD_EQ1)[`j:num`;`i:num`;`k:num`]
 760 THEN ASM_REWRITE_TAC[]
 761 ]);;
 762   (* }}} *)
 763
 764
 765
 766 let CHOOSE_MOD_3=prove_by_refinement(
 767 `~(i MOD 3 = j MOD 3) /\ ~(SUC j MOD 3 = i MOD 3)
 768 ==> j MOD 3 = SUC i MOD 3`,
 769   (* {{{ proof *)
 770 [
 771 MP_TAC(ARITH_RULE`i MOD 3= 0 \/ i MOD 3= 1 \/ i MOD 3= 2`)
 772 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
 773 THEN MP_TAC(ARITH_RULE`j MOD 3= 0 \/ j MOD 3= 1 \/ j MOD 3= 2`)
 774 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
 775 THEN MP_TAC(ARITH_RULE`SUC j MOD 3= 0 \/ SUC j MOD 3= 1 \/ SUC j MOD 3= 2`)
 776 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
 777 THEN REPEAT STRIP_TAC
 778 THEN MP_TAC(SET_RULE`SUC j MOD 3 IN {0, 1, 2} /\
 779  j MOD 3 IN {0, 1, 2} /\ i MOD 3 IN {0, 1, 2}
 780 ==> {SUC j MOD 3, j MOD 3, i MOD 3 }SUBSET {0, 1, 2}`)
 781 THEN RESA_TAC
 782 THEN SUBGOAL_THEN`CARD {SUC j MOD 3, j MOD 3, i MOD 3 }=3` ASSUME_TAC;
 783
 784 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 785                  IN_INSERT; NOT_IN_EMPTY;]
 786 THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`j:num`
 787 THEN ARITH_TAC;
 788
 789 SUBGOAL_THEN`CARD {0, 1, 2 }=3` ASSUME_TAC;
 790
 791 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 792                  IN_INSERT; NOT_IN_EMPTY;]
 793 THEN ARITH_TAC;
 794
 795 SUBGOAL_THEN`FINITE {0, 1, 2 }` ASSUME_TAC;
 796
 797 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 798                  IN_INSERT; NOT_IN_EMPTY;];
 799
 800 MRESA_TAC CARD_SUBSET_EQ[`{SUC j MOD 3, j MOD 3, i MOD 3 }`;`{0, 1, 2}`]
 801 THEN MP_TAC(ARITH_RULE`SUC i MOD 3= 0 \/ SUC i MOD 3= 1 \/ SUC i MOD 3= 2`)
 802 THEN ONCE_REWRITE_TAC[SET_RULE`(A=B\/ A=C\/A=D)<=> A IN {B,C,D}`]
 803 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 804 THEN ONCE_REWRITE_TAC[SET_RULE` A IN {B,C,D}<=> (A=B\/ A=C\/A=D)`]
 805 THEN MRESA1_TAC(GEN_ALL SUC_MOD_NOT_EQ)`i:num`
 806 THEN MRESA_TAC(GEN_ALL NOT_IMP_SUC_MOD_EQ)[`i:num`;`j:num`]
 807 THEN RESA_TAC
 808 ]);;
 809   (* }}} *)
 810
 811
 812
 813
 814 let SMALL_BALL_ANNULUS_6=prove_by_refinement(
 815 `   convex_local_fan (V,E,FF) /\
 816     packing V /\
 817     V SUBSET ball_annulus /\
 818     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))
 819 ==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) /\ dist(v,w)<= &6 )`,
 820   (* {{{ proof *)
 821 [
 822 REPEAT STRIP_TAC;
 823 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 824 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
 825 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
 826 THEN ASM_REWRITE_TAC[];
 827 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
 828 ==> v IN ball_annulus /\ w IN ball_annulus`)
 829 THEN ASM_REWRITE_TAC[]
 830 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
 831 THEN STRIP_TAC
 832 THEN REMOVE_ASSUM_TAC
 833 THEN POP_ASSUM MP_TAC
 834 THEN ONCE_REWRITE_TAC[DIST_SYM]
 835 THEN STRIP_TAC
 836 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
 837 THEN POP_ASSUM MP_TAC
 838 THEN POP_ASSUM MP_TAC
 839 THEN REMOVE_ASSUM_TAC
 840 THEN POP_ASSUM MP_TAC
 841 THEN REWRITE_TAC[h0]
 842 THEN REAL_ARITH_TAC
 843 ]);;
 844   (* }}} *)
 845
 846
 847
 848
 849
 850 let SMALL_BALL_ANNULUS_6_sqrt8=prove_by_refinement(
 851 `   convex_local_fan (V,E,FF) /\
 852     packing V /\
 853     V SUBSET ball_annulus /\
 854     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w))
 855 ==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w) /\ dist(v,w)<= &6 )`,
 856   (* {{{ proof *)
 857 [
 858 REPEAT STRIP_TAC;
 859 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 860 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
 861 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
 862 THEN ASM_REWRITE_TAC[];
 863 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
 864 ==> v IN ball_annulus /\ w IN ball_annulus`)
 865 THEN ASM_REWRITE_TAC[]
 866 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
 867 THEN STRIP_TAC
 868 THEN REMOVE_ASSUM_TAC
 869 THEN POP_ASSUM MP_TAC
 870 THEN ONCE_REWRITE_TAC[DIST_SYM]
 871 THEN STRIP_TAC
 872 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
 873 THEN POP_ASSUM MP_TAC
 874 THEN POP_ASSUM MP_TAC
 875 THEN REMOVE_ASSUM_TAC
 876 THEN POP_ASSUM MP_TAC
 877 THEN REWRITE_TAC[h0]
 878 THEN REAL_ARITH_TAC
 879 ]);;
 880   (* }}} *)
 881
 882
 883
 884 let SMALL_BALL_ANNULUS_6_3=prove_by_refinement(
 885 `   convex_local_fan (V,E,FF) /\
 886     packing V /\
 887     V SUBSET ball_annulus /\
 888     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w))
 889 ==>     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) /\ dist(v,w)<= &6 )`,
 890   (* {{{ proof *)
 891 [
 892 REPEAT STRIP_TAC;
 893 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 894 THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
 895 THEN POP_ASSUM (fun th -> REPEAT STRIP_TAC THEN MP_TAC th)
 896 THEN ASM_REWRITE_TAC[];
 897 MP_TAC(SET_RULE`v IN V /\ w IN V /\ V SUBSET ball_annulus
 898 ==> v IN ball_annulus /\ w IN ball_annulus`)
 899 THEN ASM_REWRITE_TAC[]
 900 THEN REWRITE_TAC[ball_annulus;DIFF;IN_ELIM_THM;cball]
 901 THEN STRIP_TAC
 902 THEN REMOVE_ASSUM_TAC
 903 THEN POP_ASSUM MP_TAC
 904 THEN ONCE_REWRITE_TAC[DIST_SYM]
 905 THEN STRIP_TAC
 906 THEN MRESA_TAC DIST_TRIANGLE[`w:real^3`;`vec 0:real^3`;`v:real^3`]
 907 THEN POP_ASSUM MP_TAC
 908 THEN POP_ASSUM MP_TAC
 909 THEN REMOVE_ASSUM_TAC
 910 THEN POP_ASSUM MP_TAC
 911 THEN REWRITE_TAC[h0]
 912 THEN REAL_ARITH_TAC
 913 ]);;
 914   (* }}} *)
 915
 916
 917
 918 let CS_ADJ=prove(`cs_adj = (\k a1 a2 i j. (if (i MOD k = j MOD k) then &0
 919                                else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))`,
 920 MP_TAC( GENL [`k:num`;`a1:real`;`a2:real`;`i:num`;`j:num`] (SPEC_ALL cs_adj))
 921 THEN REWRITE_TAC[GSYM FUN_EQ_THM]
 922 THEN STRIP_TAC
 923 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
 924 THEN SIMP_TAC[FUN_EQ_THM]);;
 925
 926
 927
 928
 929 let ZITHLQN_CASE_3=prove_by_refinement(
 930 `    V SUBSET ball_annulus /\
 931      CARD V =3 /\
 932     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
 933 /\ (s=let upperbd = &6 in
 934   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
 935                                 else (if {i MOD k,j MOD k}={0,1} then p
 936                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
 937          mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))
 938 /\ (!i.  vv (i MOD (CARD V))= vv i)
 939 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
 940 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
 941 ==>  vv IN BBs_v39 s`,
 942   (* {{{ proof *)
 943 [
 944 REPEAT STRIP_TAC
 945 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;Oxl_def.periodic;mk_unadorned_v39;CS_ADJ]
 946 THEN STRIP_TAC;
 947
 948 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
 949 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
 950 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
 951 THEN ASM_REWRITE_TAC[]
 952 THEN REPEAT STRIP_TAC
 953 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
 954
 955 STRIP_TAC
 956 THEN REPEAT GEN_TAC;
 957
 958 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
 959 THEN MP_TAC(ARITH_RULE`i MOD 3 = j MOD 3 \/ ~(i MOD 3 = j MOD 3)`)
 960 THEN STRIP_TAC;
 961
 962 ASM_REWRITE_TAC[DIST_POS_LE]
 963 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 964 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
 965 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
 966 THEN REPEAT RESA_TAC
 967 THEN REWRITE_TAC[DIST_REFL]
 968 THEN REAL_ARITH_TAC;
 969
 970 ASM_REWRITE_TAC[]
 971 THEN MP_TAC(ARITH_RULE`SUC j MOD 3 = i MOD 3 \/ ~(SUC j MOD 3 = i MOD 3)`)
 972 THEN STRIP_TAC;
 973
 974 ASM_REWRITE_TAC[]
 975 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
 976
 977 POP_ASSUM MP_TAC
 978 THEN POP_ASSUM MP_TAC
 979 THEN POP_ASSUM MP_TAC
 980 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 981 THEN REPEAT STRIP_TAC
 982 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
 983 THEN EXISTS_TAC`j:num`
 984 THEN ASM_REWRITE_TAC[]
 985 THEN POP_ASSUM MP_TAC
 986 THEN POP_ASSUM MP_TAC
 987 THEN POP_ASSUM MP_TAC
 988 THEN POP_ASSUM MP_TAC
 989 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
 990 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
 991 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
 992 THEN REPEAT RESA_TAC
 993 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
 994
 995 POP_ASSUM MP_TAC
 996 THEN REPLICATE_TAC 7 REMOVE_ASSUM_TAC
 997 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
 998
 999 MP_TAC CHOOSE_MOD_3
1000 THEN ASM_REWRITE_TAC[]
1001 THEN RESA_TAC;
1002
1003 ASM_REWRITE_TAC[]
1004 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1005
1006 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1007 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1008 THEN REPEAT STRIP_TAC
1009 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1010 THEN EXISTS_TAC`i:num`
1011 THEN ASM_REWRITE_TAC[]
1012 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1013 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1014 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1015 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1016 THEN REPEAT RESA_TAC;
1017
1018 POP_ASSUM MP_TAC
1019 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1020 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1021
1022 ASM_REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;]
1023 THEN ARITH_TAC
1024 ]);;
1025   (* }}} *)
1026
1027
1028
1029 let ZITHLQN_CASE_4=prove_by_refinement(
1030 `   convex_local_fan (V,E,FF) /\
1031     packing V /\
1032     V SUBSET ball_annulus /\
1033      CARD V =4 /\
1034     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
1035     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1036 /\ (s=let upperbd = &6 in
1037   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1038                                 else (if {i MOD k,j MOD k}={0,1} then p
1039                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1040          mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))
1041 /\ (!i.  vv (i MOD (CARD V))= vv i)
1042 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1043 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1044 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1045 ==>  vv IN BBs_v39 s`,
1046   (* {{{ proof *)
1047 [
1048 REPEAT STRIP_TAC
1049 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1050 THEN MP_TAC SMALL_BALL_ANNULUS_6
1051 THEN ASM_REWRITE_TAC[]
1052 THEN REMOVE_ASSUM_TAC
1053 THEN REPEAT STRIP_TAC
1054 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1055 THEN STRIP_TAC;
1056
1057 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1058 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1059 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1060 THEN ASM_REWRITE_TAC[]
1061 THEN REPEAT STRIP_TAC
1062 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1063
1064 STRIP_TAC
1065 THEN REPEAT GEN_TAC;
1066
1067 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1068 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
1069 THEN STRIP_TAC;
1070
1071 ASM_REWRITE_TAC[DIST_POS_LE]
1072 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1073 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1074 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1075 THEN REPEAT RESA_TAC
1076 THEN REWRITE_TAC[DIST_REFL]
1077 THEN REAL_ARITH_TAC;
1078
1079 ASM_REWRITE_TAC[]
1080 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
1081 THEN STRIP_TAC;
1082
1083 ASM_REWRITE_TAC[]
1084 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1085
1086 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1087 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1088 THEN REPEAT STRIP_TAC
1089 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1090 THEN EXISTS_TAC`j:num`
1091 THEN ASM_REWRITE_TAC[]
1092 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1093 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1094 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1095 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1096 THEN REPEAT RESA_TAC
1097 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1098
1099 POP_ASSUM MP_TAC
1100 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1101 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1102
1103 ASM_REWRITE_TAC[]
1104 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
1105 THEN STRIP_TAC;
1106
1107 ASM_REWRITE_TAC[]
1108 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1109
1110 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1111 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1112 THEN REPEAT STRIP_TAC
1113 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1114 THEN EXISTS_TAC`i:num`
1115 THEN ASM_REWRITE_TAC[]
1116 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1117 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1118 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1119 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1120 THEN REPEAT RESA_TAC
1121 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1122
1123 POP_ASSUM MP_TAC
1124 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1125 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1126
1127 ASM_REWRITE_TAC[]
1128 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1129
1130 STRIP_TAC
1131 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1132 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1133 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1134 THEN POP_ASSUM MP_TAC
1135 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1136 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1137 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1138 THEN REWRITE_TAC[th])
1139 THEN REPEAT STRIP_TAC
1140 THEN POP_ASSUM MP_TAC
1141 THEN REWRITE_TAC[PAIR_EQ]
1142 THEN STRIP_TAC
1143 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1144
1145 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1146 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1147 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1148
1149 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1150 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1151 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1152
1153
1154 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1155
1156
1157 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1158 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1159
1160
1161  REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1162 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1163 THEN POP_ASSUM MATCH_MP_TAC
1164 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1165 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1166 THEN STRIP_TAC;
1167
1168 EXISTS_TAC`i:num`
1169 THEN SET_TAC[];
1170
1171 EXISTS_TAC`j:num`
1172 THEN SET_TAC[];
1173 ]);;
1174   (* }}} *)
1175
1176
1177
1178
1179
1180 let ZITHLQN_CASE_5=prove_by_refinement(
1181 `   convex_local_fan (V,E,FF) /\
1182     packing V /\
1183     V SUBSET ball_annulus /\
1184      CARD V =5 /\
1185     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w) ) /\
1186     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1187 /\ (s=let upperbd = &6 in
1188   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1189                                 else (if {i MOD k,j MOD k}={0,1} then p
1190                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1191      mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd))
1192 /\ (!i.  vv (i MOD (CARD V))= vv i)
1193 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1194 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1195 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1196 ==>  vv IN BBs_v39 s`,
1197   (* {{{ proof *)
1198 [
1199 REPEAT STRIP_TAC
1200 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1201 THEN MP_TAC SMALL_BALL_ANNULUS_6
1202 THEN ASM_REWRITE_TAC[]
1203 THEN REMOVE_ASSUM_TAC
1204 THEN REPEAT STRIP_TAC
1205 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1206 THEN STRIP_TAC;
1207
1208 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1209 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1210 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1211 THEN ASM_REWRITE_TAC[]
1212 THEN REPEAT STRIP_TAC
1213 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1214
1215 STRIP_TAC
1216 THEN REPEAT GEN_TAC;
1217
1218 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1219 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1220 THEN STRIP_TAC;
1221
1222 ASM_REWRITE_TAC[DIST_POS_LE]
1223 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1224 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1225 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1226 THEN REPEAT RESA_TAC
1227 THEN REWRITE_TAC[DIST_REFL]
1228 THEN REAL_ARITH_TAC;
1229
1230 ASM_REWRITE_TAC[]
1231 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1232 THEN STRIP_TAC;
1233
1234 ASM_REWRITE_TAC[]
1235 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1236
1237 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1239 THEN REPEAT STRIP_TAC
1240 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1241 THEN EXISTS_TAC`j:num`
1242 THEN ASM_REWRITE_TAC[]
1243 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1244 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1245 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1246 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1247 THEN REPEAT RESA_TAC
1248 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1249
1250 POP_ASSUM MP_TAC
1251 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1252 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1253
1254 ASM_REWRITE_TAC[]
1255 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1256 THEN STRIP_TAC;
1257
1258 ASM_REWRITE_TAC[]
1259 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1260
1261 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1262 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1263 THEN REPEAT STRIP_TAC
1264 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1265 THEN EXISTS_TAC`i:num`
1266 THEN ASM_REWRITE_TAC[]
1267 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1268 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1269 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1270 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1271 THEN REPEAT RESA_TAC
1272 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1273
1274 POP_ASSUM MP_TAC
1275 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1276 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1277
1278 ASM_REWRITE_TAC[]
1279 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1280
1281 STRIP_TAC
1282 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1283 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1284 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1285 THEN POP_ASSUM MP_TAC
1286 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1288 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1289 THEN REWRITE_TAC[th])
1290 THEN REPEAT STRIP_TAC
1291 THEN POP_ASSUM MP_TAC
1292 THEN REWRITE_TAC[PAIR_EQ]
1293 THEN STRIP_TAC
1294 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1295
1296 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1297 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1298 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1299
1300 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1301 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1302 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1303
1304 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1305
1306 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1307 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1308
1309 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1310 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1311 THEN POP_ASSUM MATCH_MP_TAC
1312 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1313 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1314 THEN STRIP_TAC;
1315
1316 EXISTS_TAC`i:num`
1317 THEN SET_TAC[];
1318
1319 EXISTS_TAC`j:num`
1320 THEN SET_TAC[];
1321
1322 ]);;
1323   (* }}} *)
1324
1325
1326
1327
1328
1329 let ZITHLQN_CASE_6=prove_by_refinement(
1330 `   convex_local_fan (V,E,FF) /\
1331     packing V /\
1332     V SUBSET ball_annulus /\
1333      CARD V =6 /\
1334     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)  ) /\
1335     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1336 /\ (s=let upperbd = &6 in
1337   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1338                                 else (if {i MOD k,j MOD k}={0,1} then p
1339                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1340      mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd))
1341 /\ (!i.  vv (i MOD (CARD V))= vv i)
1342 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1343 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1344 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1345 ==>  vv IN BBs_v39 s`,
1346   (* {{{ proof *)
1347 [
1348 REPEAT STRIP_TAC
1349 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1350 THEN MP_TAC SMALL_BALL_ANNULUS_6
1351 THEN ASM_REWRITE_TAC[]
1352 THEN REMOVE_ASSUM_TAC
1353 THEN REPEAT STRIP_TAC
1354 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1355 THEN STRIP_TAC;
1356
1357 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1358 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1359 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1360 THEN ASM_REWRITE_TAC[]
1361 THEN REPEAT STRIP_TAC
1362 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1363
1364 STRIP_TAC
1365 THEN REPEAT GEN_TAC;
1366
1367 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1368 THEN MP_TAC(ARITH_RULE`i MOD 6 = j MOD 6 \/ ~(i MOD 6 = j MOD 6)`)
1369 THEN STRIP_TAC;
1370
1371 ASM_REWRITE_TAC[DIST_POS_LE]
1372 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1373 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1374 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1375 THEN REPEAT RESA_TAC
1376 THEN REWRITE_TAC[DIST_REFL]
1377 THEN REAL_ARITH_TAC;
1378
1379 ASM_REWRITE_TAC[]
1380 THEN MP_TAC(ARITH_RULE`SUC j MOD 6 = i MOD 6 \/ ~(SUC j MOD 6 = i MOD 6)`)
1381 THEN STRIP_TAC;
1382
1383 ASM_REWRITE_TAC[]
1384 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1385
1386 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1387 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1388 THEN REPEAT STRIP_TAC
1389 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1390 THEN EXISTS_TAC`j:num`
1391 THEN ASM_REWRITE_TAC[]
1392 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1393 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1394 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1395 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1396 THEN REPEAT RESA_TAC
1397 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1398
1399 POP_ASSUM MP_TAC
1400 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1401 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1402
1403 ASM_REWRITE_TAC[]
1404 THEN MP_TAC(ARITH_RULE`SUC i MOD 6 = j MOD 6 \/ ~(SUC i MOD 6 = j MOD 6)`)
1405 THEN STRIP_TAC;
1406
1407 ASM_REWRITE_TAC[]
1408 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1409
1410 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1411 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1412 THEN REPEAT STRIP_TAC
1413 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1414 THEN EXISTS_TAC`i:num`
1415 THEN ASM_REWRITE_TAC[]
1416 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1417 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1418 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1419 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1420 THEN REPEAT RESA_TAC
1421 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1422
1423 POP_ASSUM MP_TAC
1424 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1425 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1426
1427 ASM_REWRITE_TAC[]
1428 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1429
1430 STRIP_TAC
1431 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1432 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1433 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1434 THEN POP_ASSUM MP_TAC
1435 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1436 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1437 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1438 THEN REWRITE_TAC[th])
1439 THEN REPEAT STRIP_TAC
1440 THEN POP_ASSUM MP_TAC
1441 THEN REWRITE_TAC[PAIR_EQ]
1442 THEN STRIP_TAC
1443 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1444
1445 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1446 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1447 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];
1448
1449 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1450 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1451 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`6`][ARITH_RULE`~(6=0)`];
1452
1453 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1454
1455 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1456 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1457
1458 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1459 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1460 THEN POP_ASSUM MATCH_MP_TAC
1461 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1462 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1463 THEN STRIP_TAC;
1464
1465 EXISTS_TAC`i:num`
1466 THEN SET_TAC[];
1467
1468 EXISTS_TAC`j:num`
1469 THEN SET_TAC[];
1470 ]);;
1471   (* }}} *)
1472
1473
1474
1475
1476
1477
1478 let ZITHLQN_CASE_5_pro_cs=prove_by_refinement(
1479  `   convex_local_fan (V,E,FF) /\
1480     packing V /\
1481     V SUBSET ball_annulus /\
1482      CARD V =5 /\
1483 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
1484        (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
1485        {v0,w0} IN E /\
1486        &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
1487 /\ (s=let upperbd = &6 in
1488   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1489                                 else (if {i MOD k ,j MOD k}={0,1} then p
1490                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1491 mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd))
1492 /\ (!i.  vv (i MOD (CARD V))= vv i)
1493 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1494 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1495 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1496 /\ vv 0= v0 /\ vv 1= w0
1497 ==>  vv IN BBs_v39 s`,
1498   (* {{{ proof *)
1499 [
1500 REPEAT STRIP_TAC
1501 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1502 THEN MP_TAC SMALL_BALL_ANNULUS_6
1503 THEN ASM_REWRITE_TAC[]
1504 THEN REMOVE_ASSUM_TAC
1505 THEN REPEAT STRIP_TAC
1506 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1507 THEN STRIP_TAC;
1508
1509 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1510 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1511 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1512 THEN ASM_REWRITE_TAC[]
1513 THEN REPEAT STRIP_TAC
1514 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1515
1516 STRIP_TAC
1517 THEN REPEAT GEN_TAC;
1518
1519 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1520 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1521 THEN STRIP_TAC;
1522
1523 ASM_REWRITE_TAC[DIST_POS_LE]
1524 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1525 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1526 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1527 THEN REPEAT RESA_TAC
1528 THEN REWRITE_TAC[DIST_REFL]
1529 THEN REAL_ARITH_TAC;
1530
1531 ASM_REWRITE_TAC[]
1532 THEN MP_TAC(SET_RULE`{i MOD 5,j MOD 5}={0,1} \/ ~({i MOD 5,j MOD 5}={0,1})`)
1533 THEN STRIP_TAC;
1534
1535 ASM_REWRITE_TAC[]
1536 THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;
1537
1538 STRIP_TAC
1539 THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);
1540
1541 MP_TAC(SET_RULE`{i MOD 5,j MOD 5} = {0, 1} /\ ~(i MOD 5=j MOD 5)/\ ~(0=1)==> (i MOD 5=0 /\ j MOD 5=1)\/ (i MOD 5=1 /\ j MOD 5=0)`)
1542 THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
1543 THEN STRIP_TAC
1544 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
1545 THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
1546 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
1547 THEN MP_TAC th)
1548 THEN ASM_REWRITE_TAC[]
1549 THEN STRIP_TAC
1550 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1551 THEN STRIP_TAC
1552 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1553 THEN ONCE_REWRITE_TAC[DIST_SYM]
1554 THEN ASM_REWRITE_TAC[];
1555
1556 ASM_REWRITE_TAC[]
1557 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1558 THEN STRIP_TAC;
1559
1560 ASM_REWRITE_TAC[]
1561 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1562
1563 REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1564 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1565 THEN REPEAT STRIP_TAC
1566 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1567 THEN EXISTS_TAC`j:num`
1568 THEN ASM_REWRITE_TAC[]
1569 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
1570 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1571 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1572 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1573 THEN REPEAT RESA_TAC
1574 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1575
1576 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
1577
1578 REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1579 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
1580 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1581 THEN ASM_REWRITE_TAC[];
1582
1583 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
1584
1585 STRIP_TAC
1586 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
1587 `)
1588 THEN ASM_REWRITE_TAC[]
1589 THEN STRIP_TAC;
1590
1591 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1592 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
1593 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1594 THEN MP_TAC th)
1595 THEN ASM_REWRITE_TAC[]
1596 THEN STRIP_TAC
1597 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1598 THEN REPEAT STRIP_TAC
1599 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1600 THEN REPEAT STRIP_TAC
1601 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
1602 THEN POP_ASSUM MP_TAC
1603 THEN ARITH_TAC;
1604
1605 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1606 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
1607 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1608 THEN MP_TAC th)
1609 THEN ASM_REWRITE_TAC[]
1610 THEN STRIP_TAC
1611 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1612 THEN REPEAT STRIP_TAC
1613 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1614 THEN REPEAT STRIP_TAC
1615 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
1616 THEN POP_ASSUM MP_TAC
1617 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
1618 THEN SET_TAC[];
1619
1620 POP_ASSUM MP_TAC
1621 THEN REMOVE_ASSUM_TAC
1622 THEN POP_ASSUM MP_TAC
1623 THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
1624 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1625
1626 ASM_REWRITE_TAC[]
1627 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1628 THEN STRIP_TAC;
1629
1630 ASM_REWRITE_TAC[]
1631 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1632
1633 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1634 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1635 THEN REPEAT STRIP_TAC
1636 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1637 THEN EXISTS_TAC`i:num`
1638 THEN ASM_REWRITE_TAC[]
1639 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1640 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1641 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1642 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1643 THEN REPEAT RESA_TAC
1644 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1645
1646 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
1647
1648 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
1649 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
1650 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1651 THEN ASM_REWRITE_TAC[];
1652
1653 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
1654
1655 STRIP_TAC
1656 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
1657 `)
1658 THEN ASM_REWRITE_TAC[]
1659 THEN STRIP_TAC;
1660
1661 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1662 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
1663 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1664 THEN MP_TAC th)
1665 THEN ASM_REWRITE_TAC[]
1666 THEN STRIP_TAC
1667 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1668 THEN REPEAT STRIP_TAC
1669 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1670 THEN REPEAT STRIP_TAC
1671 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1672 THEN POP_ASSUM MP_TAC
1673 THEN ARITH_TAC;
1674
1675 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1676 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
1677 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
1678 THEN MP_TAC th)
1679 THEN ASM_REWRITE_TAC[]
1680 THEN STRIP_TAC
1681 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1682 THEN REPEAT STRIP_TAC
1683 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1684 THEN REPEAT STRIP_TAC
1685 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1686 THEN POP_ASSUM MP_TAC
1687 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0`]
1688 THEN SET_TAC[];
1689
1690 POP_ASSUM MP_TAC
1691 THEN REMOVE_ASSUM_TAC
1692 THEN POP_ASSUM MP_TAC
1693 THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
1694 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1695
1696 ASM_REWRITE_TAC[]
1697 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1698
1699 STRIP_TAC
1700 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1701 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1702 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1703 THEN POP_ASSUM MP_TAC
1704 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
1705 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1706 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1707 THEN REWRITE_TAC[th])
1708 THEN REPEAT STRIP_TAC
1709 THEN POP_ASSUM MP_TAC
1710 THEN REWRITE_TAC[PAIR_EQ]
1711 THEN STRIP_TAC
1712 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);
1713
1714 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1715 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1716 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1717
1718 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1719 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1720 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
1721
1722 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1723
1724 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
1725 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1726
1727 REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
1728 THEN POP_ASSUM (fun th -> REPLICATE_TAC 18  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1729 THEN POP_ASSUM MATCH_MP_TAC
1730 THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
1731 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1732 THEN STRIP_TAC;
1733
1734 EXISTS_TAC`i:num`
1735 THEN SET_TAC[];
1736
1737 EXISTS_TAC`j:num`
1738 THEN SET_TAC[];
1739 ]);;
1740   (* }}} *)
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750 let ZITHLQN_CASE_4_3=prove_by_refinement(
1751 `   convex_local_fan (V,E,FF) /\
1752     packing V /\
1753     V SUBSET ball_annulus /\
1754      CARD V =4 /\
1755     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w) ) /\
1756     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1757 /\ (s=let upperbd = &6 in
1758   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1759                                 else (if {i MOD k,j MOD k}={0,1} then p
1760                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1761       mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))
1762 /\ (!i.  vv (i MOD (CARD V))= vv i)
1763 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1764 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1765 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1766 ==>  vv IN BBs_v39 s`,
1767   (* {{{ proof *)
1768 [
1769 REPEAT STRIP_TAC
1770 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1771 THEN MP_TAC SMALL_BALL_ANNULUS_6_3
1772 THEN ASM_REWRITE_TAC[]
1773 THEN REMOVE_ASSUM_TAC
1774 THEN REPEAT STRIP_TAC
1775 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1776 THEN STRIP_TAC;
1777
1778 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1779 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1780 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1781 THEN ASM_REWRITE_TAC[]
1782 THEN REPEAT STRIP_TAC
1783 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1784
1785 STRIP_TAC
1786 THEN REPEAT GEN_TAC;
1787
1788 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1789 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
1790 THEN STRIP_TAC;
1791
1792 ASM_REWRITE_TAC[DIST_POS_LE]
1793 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1794 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1795 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1796 THEN REPEAT RESA_TAC
1797 THEN REWRITE_TAC[DIST_REFL]
1798 THEN REAL_ARITH_TAC;
1799
1800 ASM_REWRITE_TAC[]
1801 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
1802 THEN STRIP_TAC;
1803
1804 ASM_REWRITE_TAC[]
1805 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1806
1807 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1808 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1809 THEN REPEAT STRIP_TAC
1810 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1811 THEN EXISTS_TAC`j:num`
1812 THEN ASM_REWRITE_TAC[]
1813 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1814 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1815 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1816 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1817 THEN REPEAT RESA_TAC
1818 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1819
1820 POP_ASSUM MP_TAC
1821 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1822 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1823
1824 ASM_REWRITE_TAC[]
1825 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
1826 THEN STRIP_TAC;
1827
1828 ASM_REWRITE_TAC[]
1829 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1830
1831 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1832 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1833 THEN REPEAT STRIP_TAC
1834 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1835 THEN EXISTS_TAC`i:num`
1836 THEN ASM_REWRITE_TAC[]
1837 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1838 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1839 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1840 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1841 THEN REPEAT RESA_TAC
1842 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1843
1844 POP_ASSUM MP_TAC
1845 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1846 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1847
1848 ASM_REWRITE_TAC[]
1849 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
1850
1851 STRIP_TAC
1852 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
1853 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
1854 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
1855 THEN POP_ASSUM MP_TAC
1856 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1857 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
1858 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1859 THEN REWRITE_TAC[th])
1860 THEN REPEAT STRIP_TAC
1861 THEN POP_ASSUM MP_TAC
1862 THEN REWRITE_TAC[PAIR_EQ]
1863 THEN STRIP_TAC
1864 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
1865
1866 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
1867 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1868 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1869
1870 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
1871 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1872 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
1873
1874 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
1875
1876 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1877 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
1878
1879  REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1880 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
1881 THEN POP_ASSUM MATCH_MP_TAC
1882 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
1883 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
1884 THEN STRIP_TAC;
1885
1886 EXISTS_TAC`i:num`
1887 THEN SET_TAC[];
1888
1889 EXISTS_TAC`j:num`
1890 THEN SET_TAC[];
1891 ]);;
1892   (* }}} *)
1893
1894
1895
1896
1897
1898
1899
1900
1901 let ZITHLQN_CASE_5_sqrt8=prove_by_refinement(
1902 `   convex_local_fan (V,E,FF) /\
1903     packing V /\
1904     V SUBSET ball_annulus /\
1905      CARD V =5 /\
1906     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8  <= dist(v,w) ) /\
1907     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)
1908 /\ (s=let upperbd = &6 in
1909   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
1910                                 else (if {i MOD k,j MOD k}={0,1} then p
1911                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
1912      mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd))
1913 /\ (!i.  vv (i MOD (CARD V))= vv i)
1914 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
1915 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
1916 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
1917 ==>  vv IN BBs_v39 s`,
1918   (* {{{ proof *)
1919 [
1920 REPEAT STRIP_TAC
1921 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1922 THEN MP_TAC  SMALL_BALL_ANNULUS_6_sqrt8
1923 THEN ASM_REWRITE_TAC[]
1924 THEN REMOVE_ASSUM_TAC
1925 THEN REPEAT STRIP_TAC
1926 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
1927 THEN STRIP_TAC;
1928
1929 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
1930 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1931 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
1932 THEN ASM_REWRITE_TAC[]
1933 THEN REPEAT STRIP_TAC
1934 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
1935
1936 STRIP_TAC
1937 THEN REPEAT GEN_TAC;
1938
1939 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
1940 THEN MP_TAC(ARITH_RULE`i MOD 5 = j MOD 5 \/ ~(i MOD 5 = j MOD 5)`)
1941 THEN STRIP_TAC;
1942
1943 ASM_REWRITE_TAC[DIST_POS_LE]
1944 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1945 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
1946 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
1947 THEN REPEAT RESA_TAC
1948 THEN REWRITE_TAC[DIST_REFL]
1949 THEN REAL_ARITH_TAC;
1950
1951 ASM_REWRITE_TAC[]
1952 THEN MP_TAC(ARITH_RULE`SUC j MOD 5 = i MOD 5 \/ ~(SUC j MOD 5 = i MOD 5)`)
1953 THEN STRIP_TAC;
1954
1955 ASM_REWRITE_TAC[]
1956 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1957
1958 REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
1959 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1960 THEN REPEAT STRIP_TAC
1961 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1962 THEN EXISTS_TAC`j:num`
1963 THEN ASM_REWRITE_TAC[]
1964 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
1965 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
1966 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1967 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
1968 THEN REPEAT RESA_TAC
1969 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1970
1971 POP_ASSUM MP_TAC
1972 THEN REPLICATE_TAC 8 REMOVE_ASSUM_TAC
1973 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1974
1975 ASM_REWRITE_TAC[]
1976 THEN MP_TAC(ARITH_RULE`SUC i MOD 5 = j MOD 5 \/ ~(SUC i MOD 5 = j MOD 5)`)
1977 THEN STRIP_TAC;
1978
1979 ASM_REWRITE_TAC[]
1980 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
1981
1982 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1983 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1984 THEN REPEAT STRIP_TAC
1985 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
1986 THEN EXISTS_TAC`i:num`
1987 THEN ASM_REWRITE_TAC[]
1988 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1989 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
1990 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1991 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
1992 THEN REPEAT RESA_TAC
1993 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
1994
1995 POP_ASSUM MP_TAC
1996 THEN REPLICATE_TAC 9 REMOVE_ASSUM_TAC
1997 THEN POP_ASSUM (fun th -> STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
1998
1999 ASM_REWRITE_TAC[]
2000 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
2001
2002 STRIP_TAC
2003 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2004 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2005 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
2006 THEN POP_ASSUM MP_TAC
2007 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2008 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
2009 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2010 THEN REWRITE_TAC[th])
2011 THEN REPEAT STRIP_TAC
2012 THEN POP_ASSUM MP_TAC
2013 THEN REWRITE_TAC[PAIR_EQ]
2014 THEN STRIP_TAC
2015 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC);
2016
2017 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
2018 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2019 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
2020
2021 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
2022 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2023 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`5`][ARITH_RULE`~(5=0)`];
2024
2025 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
2026
2027 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2028 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
2029
2030 REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2031 THEN POP_ASSUM (fun th -> REPLICATE_TAC 12  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
2032 THEN POP_ASSUM MATCH_MP_TAC
2033 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2034 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
2035 THEN STRIP_TAC;
2036
2037 EXISTS_TAC`i:num`
2038 THEN SET_TAC[];
2039
2040 EXISTS_TAC`j:num`
2041 THEN SET_TAC[];
2042 ]);;
2043   (* }}} *)
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057 let ZITHLQN_CASE_4_pro_cs=prove_by_refinement(
2058  `   convex_local_fan (V,E,FF) /\
2059     packing V /\
2060     V SUBSET ball_annulus /\
2061      CARD V =4 /\
2062 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
2063        (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
2064        {v0,w0} IN E /\
2065        &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8
2066 /\ (s=let upperbd = &6 in
2067   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2068                                 else (if {i MOD k ,j MOD k}={0,1} then p
2069                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2070      mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd))
2071 /\ (!i.  vv (i MOD (CARD V))= vv i)
2072 /\ (! i j. vv i = vv j ==> i MOD CARD V = j MOD CARD V)
2073 /\  IMAGE vv (:num) = V /\  IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E
2074 /\  IMAGE (\i. vv i,vv (SUC i)) (:num) = FF
2075 /\ vv 0= v0 /\ vv 1= w0
2076 ==>  vv IN BBs_v39 s`,
2077   (* {{{ proof *)
2078 [
2079 REPEAT STRIP_TAC
2080 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2081 THEN MP_TAC SMALL_BALL_ANNULUS_6_sqrt8
2082 THEN ASM_REWRITE_TAC[]
2083 THEN REMOVE_ASSUM_TAC
2084 THEN REPEAT STRIP_TAC
2085 THEN ASM_REWRITE_TAC[BBs_v39;IN;LET_DEF;LET_END_DEF;mk_unadorned_v39;CS_ADJ]
2086 THEN STRIP_TAC;
2087
2088 ASM_REWRITE_TAC[scs_k_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;Oxl_def.periodic]
2089 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2090 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
2091 THEN ASM_REWRITE_TAC[]
2092 THEN REPEAT STRIP_TAC
2093 THEN MRESAL_TAC MOD_EQ[`i+CARD(V:real^3->bool)`;`i:num`;`CARD(V:real^3->bool)`;`1`][ARITH_RULE`1*A=A`];
2094
2095 STRIP_TAC
2096 THEN REPEAT GEN_TAC;
2097
2098 ASM_REWRITE_TAC[scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF]
2099 THEN MP_TAC(ARITH_RULE`i MOD 4 = j MOD 4 \/ ~(i MOD 4 = j MOD 4)`)
2100 THEN STRIP_TAC;
2101
2102 ASM_REWRITE_TAC[DIST_POS_LE]
2103 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2104 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num` THEN MRESA1_TAC th`i :num`)
2105 THEN REPLICATE_TAC 2 (POP_ASSUM (fun th-> REWRITE_TAC[SYM th]))
2106 THEN REPEAT RESA_TAC
2107 THEN REWRITE_TAC[DIST_REFL]
2108 THEN REAL_ARITH_TAC;
2109
2110 ASM_REWRITE_TAC[]
2111 THEN MP_TAC(SET_RULE`{i MOD 4,j MOD 4}={0,1} \/ ~({i MOD 4,j MOD 4}={0,1})`)
2112 THEN STRIP_TAC;
2113
2114 ASM_REWRITE_TAC[]
2115 THEN SUBGOAL_THEN`(~(i=j:num))`ASSUME_TAC;
2116
2117 STRIP_TAC
2118 THEN POP_ASSUM (fun th-> REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[th]);
2119
2120 MP_TAC(SET_RULE`{i MOD 4,j MOD 4} = {0, 1} /\ ~(i MOD 4=j MOD 4)/\ ~(0=1)==> (i MOD 4=0 /\ j MOD 4=1)\/ (i MOD 4=1 /\ j MOD 4=0)`)
2121 THEN ASM_REWRITE_TAC[ARITH_RULE`~(0=1)`]
2122 THEN STRIP_TAC
2123 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
2124 THEN POP_ASSUM (fun th-> MRESA1_TAC th` j:num` THEN MRESA1_TAC th`i :num`)
2125 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MP_TAC th1)
2126 THEN MP_TAC th)
2127 THEN ASM_REWRITE_TAC[]
2128 THEN STRIP_TAC
2129 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2130 THEN STRIP_TAC
2131 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
2132 THEN ONCE_REWRITE_TAC[DIST_SYM]
2133 THEN ASM_REWRITE_TAC[];
2134
2135 ASM_REWRITE_TAC[]
2136 THEN MP_TAC(ARITH_RULE`SUC j MOD 4 = i MOD 4 \/ ~(SUC j MOD 4 = i MOD 4)`)
2137 THEN STRIP_TAC;
2138
2139 ASM_REWRITE_TAC[]
2140 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
2141
2142 REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2143 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2144 THEN REPEAT STRIP_TAC
2145 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2146 THEN EXISTS_TAC`j:num`
2147 THEN ASM_REWRITE_TAC[]
2148 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
2149 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC j` THEN MRESA1_TAC th`i :num`)
2150 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
2151 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`j IN (:num)`])
2152 THEN REPEAT RESA_TAC
2153 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
2154
2155 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
2156
2157 REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2158 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
2159 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2160 THEN ASM_REWRITE_TAC[];
2161
2162 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
2163
2164 STRIP_TAC
2165 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
2166 `)
2167 THEN ASM_REWRITE_TAC[]
2168 THEN STRIP_TAC;
2169
2170 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2171 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
2172 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2173 THEN MP_TAC th)
2174 THEN ASM_REWRITE_TAC[]
2175 THEN STRIP_TAC
2176 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2177 THEN REPEAT STRIP_TAC
2178 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2179 THEN REPEAT STRIP_TAC
2180 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
2181 THEN POP_ASSUM MP_TAC
2182 THEN ARITH_TAC;
2183
2184 REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2185 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
2186 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2187 THEN MP_TAC th)
2188 THEN ASM_REWRITE_TAC[]
2189 THEN STRIP_TAC
2190 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2191 THEN REPEAT STRIP_TAC
2192 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2193 THEN REPEAT STRIP_TAC
2194 THEN REPLICATE_TAC 6 (REMOVE_ASSUM_TAC)
2195 THEN POP_ASSUM MP_TAC
2196 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
2197 THEN SET_TAC[];
2198
2199 POP_ASSUM MP_TAC
2200 THEN REMOVE_ASSUM_TAC
2201 THEN POP_ASSUM MP_TAC
2202 THEN REPLICATE_TAC 14 REMOVE_ASSUM_TAC
2203 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
2204
2205 ASM_REWRITE_TAC[]
2206 THEN MP_TAC(ARITH_RULE`SUC i MOD 4 = j MOD 4 \/ ~(SUC i MOD 4 = j MOD 4)`)
2207 THEN STRIP_TAC;
2208
2209 ASM_REWRITE_TAC[]
2210 THEN SUBGOAL_THEN`{vv (i:num), (vv j)} IN (E:(real^3->bool)->bool)` ASSUME_TAC;
2211
2212 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2213 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2214 THEN REPEAT STRIP_TAC
2215 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2216 THEN EXISTS_TAC`i:num`
2217 THEN ASM_REWRITE_TAC[]
2218 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2219 THEN POP_ASSUM (fun th-> MRESA1_TAC th`SUC i` THEN MRESA1_TAC th`j :num`)
2220 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
2221 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th;SET_RULE`i IN (:num)`])
2222 THEN REPEAT RESA_TAC
2223 THEN REWRITE_TAC[SET_RULE`{A,B}={B,A}`];
2224
2225 SUBGOAL_THEN`~((vv:num->real^3) i= vv j)`ASSUME_TAC;
2226
2227 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
2228 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`j:num`])
2229 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2230 THEN ASM_REWRITE_TAC[];
2231
2232 SUBGOAL_THEN`~({(vv:num->real^3) i, vv j}= {v0,w0})`ASSUME_TAC;
2233
2234 STRIP_TAC
2235 THEN MP_TAC(SET_RULE`{(vv:num->real^3) i, vv j} = {v0, w0} /\ ~(vv i = vv j) ==> (vv i = v0 /\ vv j= w0) \/( vv i = w0 /\ vv j= v0)
2236 `)
2237 THEN ASM_REWRITE_TAC[]
2238 THEN STRIP_TAC;
2239
2240 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2241 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`0:num`] THEN MRESA_TAC th[`j:num`;`1:num`])
2242 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2243 THEN MP_TAC th)
2244 THEN ASM_REWRITE_TAC[]
2245 THEN STRIP_TAC
2246 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2247 THEN REPEAT STRIP_TAC
2248 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2249 THEN REPEAT STRIP_TAC
2250 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2251 THEN POP_ASSUM MP_TAC
2252 THEN ARITH_TAC;
2253
2254 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2255 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`1:num`] THEN MRESA_TAC th[`j:num`;`0:num`])
2256 THEN POP_ASSUM (fun th-> POP_ASSUM(fun th1-> REPEAT STRIP_TAC THEN MP_TAC th1)
2257 THEN MP_TAC th)
2258 THEN ASM_REWRITE_TAC[]
2259 THEN STRIP_TAC
2260 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2261 THEN REPEAT STRIP_TAC
2262 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
2263 THEN REPEAT STRIP_TAC
2264 THEN REPLICATE_TAC 7 (REMOVE_ASSUM_TAC)
2265 THEN POP_ASSUM MP_TAC
2266 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0`]
2267 THEN SET_TAC[];
2268
2269 POP_ASSUM MP_TAC
2270 THEN REMOVE_ASSUM_TAC
2271 THEN POP_ASSUM MP_TAC
2272 THEN REPLICATE_TAC 15 REMOVE_ASSUM_TAC
2273 THEN POP_ASSUM (fun th -> STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`]);
2274
2275 ASM_REWRITE_TAC[]
2276 THEN SUBGOAL_THEN`~({(vv:num->real^3) i, vv j} IN E)` ASSUME_TAC;
2277
2278 STRIP_TAC
2279 THEN MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2280 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2281 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(vv:num->real^3) j`;`(vv:num->real^3) i`;`FF:real^3#real^3->bool`;]
2282 THEN POP_ASSUM MP_TAC
2283 THEN REPLICATE_TAC 9 (POP_ASSUM MP_TAC)
2284 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]
2285 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
2286 THEN REWRITE_TAC[th])
2287 THEN REPEAT STRIP_TAC
2288 THEN POP_ASSUM MP_TAC
2289 THEN REWRITE_TAC[PAIR_EQ]
2290 THEN STRIP_TAC
2291 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC);
2292
2293 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`x:num`] THEN MRESA_TAC th[`j:num`;`SUC x:num`])
2294 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2295 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`i:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
2296
2297 POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`j:num`;`x:num`] THEN MRESA_TAC th[`i:num`;`SUC x:num`])
2298 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2299 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`j:num`;`x:num`;`4`][ARITH_RULE`~(4=0)`];
2300
2301 SUBGOAL_THEN`~(vv i =(vv:num->real^3) j)`ASSUME_TAC;
2302
2303 REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
2304 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`i:num`;`j:num`]);
2305
2306 REPLICATE_TAC 18 (POP_ASSUM MP_TAC)
2307 THEN POP_ASSUM (fun th -> REPLICATE_TAC 18  STRIP_TAC  THEN MRESA_TAC th[`(vv:num->real^3) i`;`(vv:num->real^3) j`])
2308 THEN POP_ASSUM MATCH_MP_TAC
2309 THEN REPLICATE_TAC 10 (REMOVE_ASSUM_TAC)
2310 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;IMAGE;IN_ELIM_THM])
2311 THEN STRIP_TAC;
2312
2313 EXISTS_TAC`i:num`
2314 THEN SET_TAC[];
2315
2316 EXISTS_TAC`j:num`
2317 THEN SET_TAC[];
2318 ]);;
2319   (* }}} *)
2320
2321
2322
2323
2324
2325 let exists_vv3=prove_by_refinement(
2326 `&2 <= norm v1 /\
2327     &2 <= norm v2 /\
2328     &2 <= norm v3 /\
2329     norm v1 <= &2 * h0 /\
2330     norm v2 <= &2 * h0 /\
2331     norm v3 <= &2 * h0 /\
2332     &2 <= dist(v1,v2) /\
2333     &2 <= dist(v1,v3) /\
2334     &2 <= dist(v2,v3) /\
2335     dist(v1,v2) <= &2 * h0 /\
2336     dist(v1,v3) <= &2 * h0 /\
2337     dist(v2,v3) <= &2 * h0
2338 /\ (!i. vv i =
2339 if i MOD 3 = 0 then v1 else
2340 if i MOD 3 = 1 then v2 else v3)
2341 /\ V= IMAGE vv (:num)  /\  E=  IMAGE (\i. {vv i, vv (SUC i)}) (:num)
2342 /\  FF= IMAGE (\i. vv i,vv (SUC i)) (:num)
2343 ==>
2344        (!i.  vv (i MOD (CARD V))= vv i)
2345 /\    V SUBSET ball_annulus  /\
2346 CARD V =3/\
2347     (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0)`,
2348   (* {{{ proof *)
2349 [
2350 STRIP_TAC
2351 THEN SUBGOAL_THEN`(!i.  (vv:num->real^3) (i MOD 3)= vv i)`ASSUME_TAC;
2352
2353 ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
2354
2355 SUBGOAL_THEN`(V:real^3->bool)={v1,v2,v3}`ASSUME_TAC;
2356
2357 ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
2358 THEN GEN_TAC
2359 THEN EQ_TAC;
2360
2361 STRIP_TAC
2362 THEN ASM_REWRITE_TAC[]
2363 THEN MP_TAC(ARITH_RULE`x' MOD 3= 0 \/ x' MOD 3= 1\/ x' MOD 3=2`)
2364 THEN STRIP_TAC
2365 THEN ASM_REWRITE_TAC[]
2366 THEN SET_TAC[];
2367
2368 STRIP_TAC
2369 THEN MP_TAC(SET_RULE`x IN {v1, v2, v3:real^3} ==> x = v1 \/ x= v2 \/ x= v3`)
2370 THEN RESA_TAC;
2371
2372 EXISTS_TAC`0:num`
2373 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 3 = 0`]
2374 THEN SET_TAC[];
2375
2376 EXISTS_TAC`1:num`
2377 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3 = 1/\ ~(1 MOD 3 = 0)`]
2378 THEN SET_TAC[];
2379
2380 EXISTS_TAC`2:num`
2381 THEN ASM_REWRITE_TAC[ARITH_RULE`~(2 MOD 3 = 1) /\ ~(2 MOD 3 = 0)`]
2382 THEN SET_TAC[];
2383
2384 SUBGOAL_THEN(`~(v1=v2:real^3) /\ ~(v1=v3:real^3) /\ ~(v3=v2:real^3)`)ASSUME_TAC;
2385
2386 STRIP_TAC;
2387
2388 STRIP_TAC
2389 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
2390 THEN REAL_ARITH_TAC;
2391
2392 STRIP_TAC
2393 THEN STRIP_TAC
2394 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DIST_REFL])
2395 THEN REAL_ARITH_TAC;
2396
2397 SUBGOAL_THEN`CARD (V:real^3->bool)=3` ASSUME_TAC;
2398
2399 POP_ASSUM MP_TAC
2400 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2401 THEN ASM_REWRITE_TAC[]
2402 THEN STRIP_TAC
2403 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
2404                  IN_INSERT; NOT_IN_EMPTY;]
2405 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2406 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2407 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2408 THEN ARITH_TAC;
2409
2410 POP_ASSUM(fun th-> REWRITE_TAC[th])
2411 THEN POP_ASSUM(fun th->
2412  POP_ASSUM(fun th-> REWRITE_TAC[th])
2413 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[GSYM th])
2414 THEN ASSUME_TAC th)
2415 THEN ASM_SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
2416 THEN STRIP_TAC;
2417
2418 MATCH_MP_TAC(SET_RULE`(v1 IN  ball_annulus
2419 /\ v2 IN  ball_annulus /\ v3 IN  ball_annulus)==> {v1, v2, v3} SUBSET ball_annulus  `)
2420 THEN RESA_TAC
2421 THEN ASM_REWRITE_TAC[ball_annulus;DIFF;cball;ball;IN_ELIM_THM; REAL_ARITH`~(a< &2)<=> &2<=a`;DIST_0];
2422
2423 REWRITE_TAC[IMAGE;IN_ELIM_THM]
2424 THEN REPEAT GEN_TAC
2425 THEN STRIP_TAC
2426 THEN POP_ASSUM MP_TAC
2427 THEN MP_TAC(ARITH_RULE`x MOD 3= 0 \/ x MOD 3= 1\/ x MOD 3=2`)
2428 THEN STRIP_TAC
2429 THEN ASM_REWRITE_TAC[];
2430
2431 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`0`;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0 MOD 3=1/\ ~(1=0)`]
2432 THEN STRIP_TAC
2433 THEN MP_TAC(SET_RULE`{v, w} = {v1, v2} /\ ~(v1=v2) ==>(v=v1 /\ w=v2)\/ (v=v2 /\
2434  w=v1:real^3)`)
2435 THEN ASM_REWRITE_TAC[]
2436 THEN STRIP_TAC
2437 THEN ASM_REWRITE_TAC[]
2438 THEN ONCE_REWRITE_TAC[DIST_SYM]
2439 THEN ASM_REWRITE_TAC[];
2440
2441 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`1`;`3`][ARITH_RULE`~(3=0)/\ 1 MOD 3=1/\ SUC 1 MOD 3=2/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
2442 THEN STRIP_TAC
2443 THEN MP_TAC(SET_RULE`{v, w} = {v2, v3} /\ ~(v3=v2) ==>(v=v2 /\ w=v3)\/ (v=v3 /\
2444  w=v2:real^3)`)
2445 THEN ASM_REWRITE_TAC[]
2446 THEN STRIP_TAC
2447 THEN ASM_REWRITE_TAC[]
2448 THEN ONCE_REWRITE_TAC[DIST_SYM]
2449 THEN ASM_REWRITE_TAC[];
2450
2451 MRESAL_TAC (GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`2`;`3`][ARITH_RULE`~(3=0)/\ 2 MOD 3=2/\ SUC 2 MOD 3=0/\ ~(1=0)/\ ~(2=1)/\ ~(2=0)`]
2452 THEN STRIP_TAC
2453 THEN MP_TAC(SET_RULE`{v, w} = {v3, v1} /\ ~(v1=v3) ==>(v=v1 /\ w=v3)\/ (v=v3 /\
2454  w=v1:real^3)`)
2455 THEN ASM_REWRITE_TAC[]
2456 THEN STRIP_TAC
2457 THEN ASM_REWRITE_TAC[]
2458 THEN ONCE_REWRITE_TAC[DIST_SYM]
2459 THEN ASM_REWRITE_TAC[]
2460 ]);;
2461   (* }}} *)
2462
2463
2464
2465 let ZITHLQN=prove_by_refinement(`(!s vv. MEM s  s_init_list_v39 /\ vv IN
2466                          BBs_v39 s ==>
2467                          &0 <= taustar_v39 s vv)  ==> JEJTVGB_assume_v39`,
2468   (* {{{ proof *)
2469 [
2470 REWRITE_TAC[IMP_CONJ]
2471 THEN REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2472 THEN REPEAT STRIP_TAC;
2473
2474 MP_TAC(ARITH_RULE`4<= CARD(V:real^3->bool) /\ CARD(V:real^3->bool)<= 6
2475 ==>  CARD V= 4\/ CARD V=5 \/ CARD V=6 `)
2476 THEN RESA_TAC;
2477
2478 ABBREV_TAC`(s=let upperbd = &6 in
2479   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2480                                 else (if {i MOD k,j MOD k}={0,1} then p
2481                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2482          mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd))`
2483 THEN SUBGOAL_THEN
2484 `s IN
2485           set_of_list
2486           (let upperbd = &6 in
2487            let a_pro =
2488                (\k p a1 a2 i j.
2489                     if i MOD k = j MOD k
2490                     then &0
2491                     else if {i MOD k, j MOD k} = {0, 1}
2492                          then p
2493                          else if j MOD k = SUC i MOD k \/
2494                                  SUC j MOD k = i MOD k
2495                               then a1
2496                               else a2) in
2497            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2498             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2499                                           (cs_adj 5 (&2) (&2 * h0))
2500                                           (cs_adj 5 (&2 * h0) upperbd);
2501            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2502            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2503                                          (cs_adj 3 (&2) (&2 * h0))
2504                                          (cs_adj 3 (&2 * h0) upperbd);
2505            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2506            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2507                                          (cs_adj 4 (&2) (&3))
2508                                          (cs_adj 4 (&2 * h0) upperbd);
2509            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2510            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2511                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2512                                               (a_pro 4 sqrt8 (&2 * h0)
2513                                               upperbd)])` ASSUME_TAC;
2514
2515 EXPAND_TAC"s"
2516 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;]
2517 THEN SET_TAC[];
2518
2519 MP_TAC exists_vv
2520 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4`]
2521 THEN STRIP_TAC
2522 THEN MP_TAC ZITHLQN_CASE_4
2523 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2524 THEN ASM_REWRITE_TAC[]
2525 THEN STRIP_TAC
2526 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2527 THEN POP_ASSUM MP_TAC
2528 THEN ASM_REWRITE_TAC[]
2529 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2530 THEN ASM_REWRITE_TAC[])
2531 THEN STRIP_TAC
2532 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2533 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2534 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2535 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2536 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2537
2538 EXPAND_TAC"s"
2539 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2540 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
2541
2542 ASM_REWRITE_TAC[d_tame]
2543 THEN MP_TAC dsv_scs_init
2544 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2545 THEN STRIP_TAC
2546 THEN ASM_REWRITE_TAC[]
2547 THEN EXPAND_TAC"s"
2548 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2549 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2550 THEN REAL_ARITH_TAC;
2551
2552 ABBREV_TAC`(s=let upperbd = &6 in
2553   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2554                                 else (if {i MOD k,j MOD k}={0,1} then p
2555                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2556      mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd) )`
2557 THEN SUBGOAL_THEN
2558 `s IN
2559           set_of_list
2560           (let upperbd = &6 in
2561            let a_pro =
2562                (\k p a1 a2 i j.
2563                     if i MOD k = j MOD k
2564                     then &0
2565                     else if {i MOD k, j MOD k} = {0, 1}
2566                          then p
2567                          else if j MOD k = SUC i MOD k \/
2568                                  SUC j MOD k = i MOD k
2569                               then a1
2570                               else a2) in
2571            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2572             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2573                                           (cs_adj 5 (&2) (&2 * h0))
2574                                           (cs_adj 5 (&2 * h0) upperbd);
2575            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2576            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2577                                          (cs_adj 3 (&2) (&2 * h0))
2578                                          (cs_adj 3 (&2 * h0) upperbd);
2579            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2580            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2581                                          (cs_adj 4 (&2) (&3))
2582                                          (cs_adj 4 (&2 * h0) upperbd);
2583            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2584            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2585                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2586                                               (a_pro 4 sqrt8 (&2 * h0)
2587                                               upperbd)])` ASSUME_TAC;
2588
2589 EXPAND_TAC"s"
2590 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2591 THEN SET_TAC[];
2592
2593 MP_TAC exists_vv
2594 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5`]
2595 THEN STRIP_TAC
2596 THEN MP_TAC ZITHLQN_CASE_5
2597 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2598 THEN ASM_REWRITE_TAC[]
2599 THEN STRIP_TAC
2600 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2601 THEN POP_ASSUM MP_TAC
2602 THEN ASM_REWRITE_TAC[]
2603 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2604 THEN ASM_REWRITE_TAC[])
2605 THEN STRIP_TAC
2606 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2607 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2608 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2609 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2610 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2611
2612 EXPAND_TAC"s"
2613 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2614 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2615
2616 ASM_REWRITE_TAC[d_tame]
2617 THEN MP_TAC dsv_scs_init
2618 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2619 THEN STRIP_TAC
2620 THEN ASM_REWRITE_TAC[]
2621 THEN EXPAND_TAC"s"
2622 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2623 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2624 THEN REAL_ARITH_TAC;
2625
2626 ABBREV_TAC`(s=let upperbd = &6 in
2627   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2628                                 else (if {i MOD k,j MOD k}={0,1} then p
2629                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2630      mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd) )`
2631 THEN SUBGOAL_THEN
2632 `s IN
2633           set_of_list
2634           (let upperbd = &6 in
2635            let a_pro =
2636                (\k p a1 a2 i j.
2637                     if i MOD k = j MOD k
2638                     then &0
2639                     else if {i MOD k, j MOD k} = {0, 1}
2640                          then p
2641                          else if j MOD k = SUC i MOD k \/
2642                                  SUC j MOD k = i MOD k
2643                               then a1
2644                               else a2) in
2645            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2646             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2647                                           (cs_adj 5 (&2) (&2 * h0))
2648                                           (cs_adj 5 (&2 * h0) upperbd);
2649            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2650            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2651                                          (cs_adj 3 (&2) (&2 * h0))
2652                                          (cs_adj 3 (&2 * h0) upperbd);
2653            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2654            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2655                                          (cs_adj 4 (&2) (&3))
2656                                          (cs_adj 4 (&2 * h0) upperbd);
2657            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2658            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2659                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2660                                               (a_pro 4 sqrt8 (&2 * h0)
2661                                               upperbd)])` ASSUME_TAC;
2662
2663 EXPAND_TAC"s"
2664 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2665 THEN SET_TAC[];
2666
2667 MP_TAC exists_vv
2668 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=6`]
2669 THEN STRIP_TAC
2670 THEN MP_TAC ZITHLQN_CASE_6
2671 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2672 THEN ASM_REWRITE_TAC[]
2673 THEN STRIP_TAC
2674 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2675 THEN POP_ASSUM MP_TAC
2676 THEN ASM_REWRITE_TAC[]
2677 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2678 THEN ASM_REWRITE_TAC[])
2679 THEN STRIP_TAC
2680 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
2681 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2682 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2683 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2684 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2685
2686 EXPAND_TAC"s"
2687 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2688 ;ARITH_RULE`~(6<=3)`;mk_unadorned_v39;CS_ADJ];
2689
2690 ASM_REWRITE_TAC[d_tame]
2691 THEN MP_TAC dsv_scs_init
2692 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2693 THEN STRIP_TAC
2694 THEN ASM_REWRITE_TAC[]
2695 THEN EXPAND_TAC"s"
2696 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2697 ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2698 THEN REAL_ARITH_TAC;
2699
2700 ABBREV_TAC `(vv i =
2701 if i MOD 3 = 0 then v1 else
2702 if i MOD 3 = 1 then v2 else v3:real^3)`
2703 THEN ABBREV_TAC`V = IMAGE (vv:num->real^3) (:num)`
2704 THEN ABBREV_TAC`  E=  IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num) `
2705 THEN ABBREV_TAC` FF= IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num) `
2706 THEN ABBREV_TAC`(s=let upperbd = &6 in
2707   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2708                                 else (if {i MOD k,j MOD k}={0,1} then p
2709                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2710               mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd))`
2711 THEN SUBGOAL_THEN
2712 `s IN
2713           set_of_list
2714           (let upperbd = &6 in
2715            let a_pro =
2716                (\k p a1 a2 i j.
2717                     if i MOD k = j MOD k
2718                     then &0
2719                     else if {i MOD k, j MOD k} = {0, 1}
2720                          then p
2721                          else if j MOD k = SUC i MOD k \/
2722                                  SUC j MOD k = i MOD k
2723                               then a1
2724                               else a2) in
2725            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2726             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2727                                           (cs_adj 5 (&2) (&2 * h0))
2728                                           (cs_adj 5 (&2 * h0) upperbd);
2729            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2730            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2731                                          (cs_adj 3 (&2) (&2 * h0))
2732                                          (cs_adj 3 (&2 * h0) upperbd);
2733            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2734            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2735                                          (cs_adj 4 (&2) (&3))
2736                                          (cs_adj 4 (&2 * h0) upperbd);
2737            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2738            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2739                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2740                                               (a_pro 4 sqrt8 (&2 * h0)
2741                                               upperbd)])` ASSUME_TAC;
2742
2743 EXPAND_TAC"s"
2744 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2745 THEN SET_TAC[];
2746
2747 MP_TAC exists_vv3
2748 THEN ASM_REWRITE_TAC[]
2749 THEN STRIP_TAC
2750 THEN MP_TAC ZITHLQN_CASE_3
2751 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
2752 THEN ASM_REWRITE_TAC[]
2753 THEN STRIP_TAC
2754 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2755 THEN POP_ASSUM MP_TAC
2756 THEN ASM_REWRITE_TAC[]
2757 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2758 THEN ASM_REWRITE_TAC[])
2759 THEN SIMP_TAC[MOD_MOD_REFL;ARITH_RULE`~(3=0)`]
2760 THEN STRIP_TAC
2761 THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
2762 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2763 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2764 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2765 THEN SUBGOAL_THEN`(scs_k_v39 s <= 3)` ASSUME_TAC;
2766
2767 EXPAND_TAC"s"
2768 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2769 ;ARITH_RULE`(3<=3)`;mk_unadorned_v39;CS_ADJ];
2770
2771 ASM_REWRITE_TAC[d_tame]
2772 THEN MP_TAC dsv_scs_init
2773 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2774 THEN STRIP_TAC
2775 THEN ASM_REWRITE_TAC[]
2776 THEN EXPAND_TAC"s"
2777 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2778 ;ARITH_RULE`~(6=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2779 THEN REPLICATE_TAC 11 (POP_ASSUM MP_TAC)
2780 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th;])
2781 THEN REPEAT STRIP_TAC
2782 THEN POP_ASSUM MP_TAC
2783 THEN REWRITE_TAC[ARITH_RULE`0 MOD 3=0/\ 1 MOD 3=1 /\ 2 MOD 3=2/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)`]
2784 THEN REAL_ARITH_TAC;
2785
2786 ABBREV_TAC`(s=let upperbd = &6 in
2787   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2788                                 else (if {i MOD k,j MOD k}={0,1} then p
2789                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2790       mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd) )`
2791 THEN SUBGOAL_THEN
2792 `s IN
2793           set_of_list
2794           (let upperbd = &6 in
2795            let a_pro =
2796                (\k p a1 a2 i j.
2797                     if i MOD k = j MOD k
2798                     then &0
2799                     else if {i MOD k, j MOD k} = {0, 1}
2800                          then p
2801                          else if j MOD k = SUC i MOD k \/
2802                                  SUC j MOD k = i MOD k
2803                               then a1
2804                               else a2) in
2805            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2806             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2807                                           (cs_adj 5 (&2) (&2 * h0))
2808                                           (cs_adj 5 (&2 * h0) upperbd);
2809            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2810            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2811                                          (cs_adj 3 (&2) (&2 * h0))
2812                                          (cs_adj 3 (&2 * h0) upperbd);
2813            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2814            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2815                                          (cs_adj 4 (&2) (&3))
2816                                          (cs_adj 4 (&2 * h0) upperbd);
2817            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2818            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2819                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2820                                               (a_pro 4 sqrt8 (&2 * h0)
2821                                               upperbd)])` ASSUME_TAC;
2822
2823 EXPAND_TAC"s"
2824 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2825 THEN SET_TAC[];
2826
2827 MP_TAC exists_vv
2828 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=5/\ 5<=6`]
2829 THEN STRIP_TAC
2830 THEN MP_TAC ZITHLQN_CASE_5_sqrt8
2831 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2832 THEN ASM_REWRITE_TAC[]
2833 THEN STRIP_TAC
2834 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2835 THEN POP_ASSUM MP_TAC
2836 THEN ASM_REWRITE_TAC[]
2837 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2838 THEN ASM_REWRITE_TAC[])
2839 THEN STRIP_TAC
2840 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2841 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2842 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2843 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2844 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2845
2846 EXPAND_TAC"s"
2847 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2848 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2849
2850 ASM_REWRITE_TAC[d_tame]
2851 THEN MP_TAC dsv_scs_init
2852 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2853 THEN STRIP_TAC
2854 THEN ASM_REWRITE_TAC[]
2855 THEN EXPAND_TAC"s"
2856 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2857 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2858 THEN REAL_ARITH_TAC;
2859
2860 ABBREV_TAC`(s=let upperbd = &6 in
2861   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2862                                 else (if {i MOD k,j MOD k}={0,1} then p
2863                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2864       mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd) )`
2865 THEN SUBGOAL_THEN
2866 `s IN
2867           set_of_list
2868           (let upperbd = &6 in
2869            let a_pro =
2870                (\k p a1 a2 i j.
2871                     if i MOD k = j MOD k
2872                     then &0
2873                     else if {i MOD k, j MOD k} = {0, 1}
2874                          then p
2875                          else if j MOD k = SUC i MOD k \/
2876                                  SUC j MOD k = i MOD k
2877                               then a1
2878                               else a2) in
2879            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
2880             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
2881                                           (cs_adj 5 (&2) (&2 * h0))
2882                                           (cs_adj 5 (&2 * h0) upperbd);
2883            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
2884            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
2885                                          (cs_adj 3 (&2) (&2 * h0))
2886                                          (cs_adj 3 (&2 * h0) upperbd);
2887            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
2888            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
2889                                          (cs_adj 4 (&2) (&3))
2890                                          (cs_adj 4 (&2 * h0) upperbd);
2891            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
2892            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
2893                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
2894                                               (a_pro 4 sqrt8 (&2 * h0)
2895                                               upperbd)])` ASSUME_TAC;
2896
2897 EXPAND_TAC"s"
2898 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
2899 THEN SET_TAC[];
2900
2901 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
2902 THEN  MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
2903 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];
2904
2905 MRESA_TAC(GEN_ALL exists_vv_FF)
2906 [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
2907 THEN POP_ASSUM MP_TAC
2908 THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
2909 THEN STRIP_TAC
2910 THEN MP_TAC ZITHLQN_CASE_5_pro_cs
2911 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2912 THEN ASM_REWRITE_TAC[]
2913 THEN STRIP_TAC
2914 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2915 THEN POP_ASSUM MP_TAC
2916 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2917 )
2918 THEN ASM_REWRITE_TAC[]
2919 THEN STRIP_TAC
2920 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
2921 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2922 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2923 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2924 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2925
2926 EXPAND_TAC"s"
2927 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2928 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2929
2930 ASM_REWRITE_TAC[d_tame]
2931 THEN MP_TAC dsv_scs_init
2932 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2933 THEN STRIP_TAC
2934 THEN ASM_REWRITE_TAC[]
2935 THEN EXPAND_TAC"s"
2936 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2937 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2938 THEN REAL_ARITH_TAC;
2939
2940 MRESA_TAC(GEN_ALL exists_vv_FF)
2941 [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
2942 THEN POP_ASSUM MP_TAC
2943 THEN REWRITE_TAC[ARITH_RULE`3<=5 /\ 5<=6`]
2944 THEN STRIP_TAC
2945 THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
2946 (GEN_ALL ZITHLQN_CASE_5_pro_cs))
2947 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
2948 THEN ASM_REWRITE_TAC[]
2949 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2950 THEN ASM_REWRITE_TAC[DIST_SYM]
2951 THEN STRIP_TAC
2952 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2953 THEN POP_ASSUM MP_TAC
2954 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
2955 )
2956 THEN ASM_REWRITE_TAC[]
2957 THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
2958 THEN POP_ASSUM MP_TAC
2959 THEN POP_ASSUM MP_TAC
2960 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2961 THEN STRIP_TAC
2962 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
2963 THEN ASSUME_TAC th)
2964 THEN STRIP_TAC
2965 THEN STRIP_TAC
2966 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
2967 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
2968 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
2969 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
2970 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
2971
2972 EXPAND_TAC"s"
2973 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2974 ;ARITH_RULE`~(5<=3)`;mk_unadorned_v39;CS_ADJ];
2975
2976 ASM_REWRITE_TAC[d_tame]
2977 THEN MP_TAC dsv_scs_init
2978 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
2979 THEN STRIP_TAC
2980 THEN ASM_REWRITE_TAC[]
2981 THEN EXPAND_TAC"s"
2982 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
2983 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
2984 THEN REAL_ARITH_TAC;
2985
2986 ABBREV_TAC`(s=let upperbd = &6 in
2987   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
2988                                 else (if {i MOD k,j MOD k}={0,1} then p
2989                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
2990       mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) )`
2991 THEN SUBGOAL_THEN
2992 `s IN
2993           set_of_list
2994           (let upperbd = &6 in
2995            let a_pro =
2996                (\k p a1 a2 i j.
2997                     if i MOD k = j MOD k
2998                     then &0
2999                     else if {i MOD k, j MOD k} = {0, 1}
3000                          then p
3001                          else if j MOD k = SUC i MOD k \/
3002                                  SUC j MOD k = i MOD k
3003                               then a1
3004                               else a2) in
3005            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
3006             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
3007                                           (cs_adj 5 (&2) (&2 * h0))
3008                                           (cs_adj 5 (&2 * h0) upperbd);
3009            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
3010            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
3011                                          (cs_adj 3 (&2) (&2 * h0))
3012                                          (cs_adj 3 (&2 * h0) upperbd);
3013            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
3014            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
3015                                          (cs_adj 4 (&2) (&3))
3016                                          (cs_adj 4 (&2 * h0) upperbd);
3017            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
3018            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
3019                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
3020                                               (a_pro 4 sqrt8 (&2 * h0)
3021                                               upperbd)])` ASSUME_TAC;
3022
3023 EXPAND_TAC"s"
3024 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
3025 THEN SET_TAC[];
3026
3027 MRESA_TAC convex_local_fan [`FF:real^3#real^3->bool`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;]
3028 THEN  MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IN_E_IMP_IN_FF)
3029 [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`w0:real^3`;`v0:real^3`;`FF:real^3#real^3->bool`;];
3030
3031 MRESA_TAC(GEN_ALL exists_vv_FF)
3032 [`v0:real^3`;`w0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
3033 THEN POP_ASSUM MP_TAC
3034 THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
3035 THEN STRIP_TAC
3036 THEN MP_TAC ZITHLQN_CASE_4_pro_cs
3037 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3038 THEN ASM_REWRITE_TAC[]
3039 THEN STRIP_TAC
3040 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3041 THEN POP_ASSUM MP_TAC
3042 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
3043 )
3044 THEN ASM_REWRITE_TAC[]
3045 THEN STRIP_TAC
3046 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
3047 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3048 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3049 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3050 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3051
3052 EXPAND_TAC"s"
3053 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3054 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3055
3056 ASM_REWRITE_TAC[d_tame]
3057 THEN MP_TAC dsv_scs_init
3058 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3059 THEN STRIP_TAC
3060 THEN ASM_REWRITE_TAC[]
3061 THEN EXPAND_TAC"s"
3062 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3063 ;ARITH_RULE`~(5=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3064 THEN REAL_ARITH_TAC;
3065
3066 MRESA_TAC(GEN_ALL exists_vv_FF)
3067 [`w0:real^3`;`v0:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;]
3068 THEN POP_ASSUM MP_TAC
3069 THEN REWRITE_TAC[ARITH_RULE`3<=4 /\ 4<=6`]
3070 THEN STRIP_TAC
3071 THEN MP_TAC (ISPECL [`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`FF:real^3#real^3->bool`;`w0:real^3`;`v0:real^3`;`vv:num->real^3`;`s:scs_v39`]
3072 (GEN_ALL ZITHLQN_CASE_4_pro_cs))
3073 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3074 THEN ASM_REWRITE_TAC[]
3075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3076 THEN ASM_REWRITE_TAC[DIST_SYM]
3077 THEN STRIP_TAC
3078 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3079 THEN POP_ASSUM MP_TAC
3080 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
3081 )
3082 THEN ASM_REWRITE_TAC[]
3083 THEN ONCE_REWRITE_TAC[SET_RULE`{w, v} = {v0, w0}<=> {w, v} = {w0, v0}`]
3084 THEN POP_ASSUM MP_TAC
3085 THEN POP_ASSUM MP_TAC
3086 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3087 THEN STRIP_TAC
3088 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]
3089 THEN ASSUME_TAC th)
3090 THEN STRIP_TAC
3091 THEN STRIP_TAC
3092 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
3093 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3094 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3095 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3096 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3097
3098 EXPAND_TAC"s"
3099 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3100 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3101
3102 ASM_REWRITE_TAC[d_tame]
3103 THEN MP_TAC dsv_scs_init
3104 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3105 THEN STRIP_TAC
3106 THEN ASM_REWRITE_TAC[]
3107 THEN EXPAND_TAC"s"
3108 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3109 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3110 THEN REAL_ARITH_TAC;
3111
3112 ABBREV_TAC`(s=let upperbd = &6 in
3113   let a_pro = (\k p a1 a2 i j. (if (i MOD k = j MOD k) then &0
3114                                 else (if {i MOD k,j MOD k}={0,1} then p
3115                                       else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
3116          mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd))`
3117 THEN SUBGOAL_THEN
3118 `s IN
3119           set_of_list
3120           (let upperbd = &6 in
3121            let a_pro =
3122                (\k p a1 a2 i j.
3123                     if i MOD k = j MOD k
3124                     then &0
3125                     else if {i MOD k, j MOD k} = {0, 1}
3126                          then p
3127                          else if j MOD k = SUC i MOD k \/
3128                                  SUC j MOD k = i MOD k
3129                               then a1
3130                               else a2) in
3131            [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0))
3132             (cs_adj 6 (&2 * h0) upperbd); mk_unadorned_v39 5 (d_tame 5)
3133                                           (cs_adj 5 (&2) (&2 * h0))
3134                                           (cs_adj 5 (&2 * h0) upperbd);
3135            mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0))
3136            (cs_adj 4 (&2 * h0) upperbd); mk_unadorned_v39 3 (d_tame 3)
3137                                          (cs_adj 3 (&2) (&2 * h0))
3138                                          (cs_adj 3 (&2 * h0) upperbd);
3139            mk_unadorned_v39 5 #0.616 (cs_adj 5 (&2) sqrt8)
3140            (cs_adj 5 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.467
3141                                          (cs_adj 4 (&2) (&3))
3142                                          (cs_adj 4 (&2 * h0) upperbd);
3143            mk_unadorned_v39 5 #0.616 (a_pro 5 (&2 * h0) (&2) (&2 * h0))
3144            (a_pro 5 sqrt8 (&2 * h0) upperbd); mk_unadorned_v39 4 #0.477
3145                                               (a_pro 4 (&2 * h0) (&2) sqrt8)
3146                                               (a_pro 4 sqrt8 (&2 * h0)
3147                                               upperbd)])` ASSUME_TAC;
3148
3149 EXPAND_TAC"s"
3150 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM;mk_unadorned_v39]
3151 THEN SET_TAC[];
3152
3153 MP_TAC exists_vv
3154 THEN ASM_REWRITE_TAC[ARITH_RULE`3<=4/\ 4<=6`]
3155 THEN STRIP_TAC
3156 THEN MP_TAC ZITHLQN_CASE_4_3
3157 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
3158 THEN ASM_REWRITE_TAC[]
3159 THEN STRIP_TAC
3160 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3161 THEN POP_ASSUM MP_TAC
3162 THEN ASM_REWRITE_TAC[]
3163 THEN GEN_REWRITE_TAC( LAND_CONV   o  ONCE_DEPTH_CONV)[GSYM th]
3164 THEN ASM_REWRITE_TAC[])
3165 THEN STRIP_TAC
3166 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
3167 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])
3168 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
3169 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM]
3170 THEN SUBGOAL_THEN`~(scs_k_v39 s <= 3)` ASSUME_TAC;
3171
3172 EXPAND_TAC"s"
3173 THEN REWRITE_TAC[scs_k_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3174 ;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ];
3175
3176 ASM_REWRITE_TAC[d_tame]
3177 THEN MP_TAC dsv_scs_init
3178 THEN ASM_REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;taustar_v39]
3179 THEN STRIP_TAC
3180 THEN ASM_REWRITE_TAC[]
3181 THEN EXPAND_TAC"s"
3182 THEN REWRITE_TAC[scs_d_v39_explicit;LET_DEF;LET_END_DEF;set_of_list; IN_ELIM_THM
3183 ;ARITH_RULE`~(4=3)`;d_tame;mk_unadorned_v39;CS_ADJ]
3184 THEN REAL_ARITH_TAC;
3185 ]);;
3186   (* }}} *)
3187
3188
3189
3190
3191
3192  end;;
3193
3194
3195 (*
3196 let check_completeness_claimA_concl =
3197   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
3198 *)
3199
3200
3201
3202