legacy/oldpacking/packing/development/working.hl

   1 loads "/home/ky/flyspeck/working/REUHADY.hl";;
   2 loads "/home/ky/flyspeck/working/TSKAJXY_lemmas.hl";;
   3
   4 let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;
   5
   6
   7 let cell3_from_ineq =
   8  `!y4 y5 y6.
   9          &2 <= y4 /\
  10          &2 <= y5 /\
  11          &2 <= y6 /\
  12          y4 <= &2 * sqrt (&2) /\
  13          y5 <= &2 * sqrt (&2) /\
  14          y6 <= &2 * sqrt (&2) /\
  15          eta_y y4 y5 y6 < sqrt (&2)
  16          ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;
  17
  18 let GRKIBMP_concl =
  19   `!y. &2 <= y /\ y <= sqrt8 ==>
  20      &0 <= gamma2_x_div_azim (h0cut y) (y*y)`;;
  21
  22 let tsk_hyp_new = mk_conj(GRKIBMP_concl,
  23                               mk_conj(cell3_from_ineq,tsk_hyp));;
  24