legacy/oldnonlinear/nonlinear/experiments/zumkeller_test.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                                             *)
   5 (* Author:  Roland Zumkeller     *)
   6 (* Date: 2010-08-30                                                    *)
   7 (* ========================================================================== *)
   8
   9 (*
  10
  11 Zumkeller's verification of nonlinear inequalities using Sergei package.
  12 http://code.google.com/p/sergei/
  13
  14 Times are given in the format XhMM:SS for hours, minutes, seconds.
  15 *)
  16
  17 module Zumkeller_test = struct
  18
  19 needs "nonlinear/oracle.hl";;
  20 needs "nonlinear/ineq.hl";;
  21 needs "general/update_database_310.ml";;
  22
  23 (* commented out in ineq.hl:
  24 g Ineq.I_3336871894;;
  25 g Ineq.I_8880534953;;
  26 *)
  27
  28 g Ineq.I_5735387903;;
  29 e PREP;;
  30 e (ONCE_REWRITE_TAC [INST [(`#1.04`,`t:real`)] ATN2_ROT_TAN]);;
  31 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
  32 e SERGEI_TAC;; (* done 0:03 *)
  33
  34 g Ineq.I_5490182221;;
  35 e PREP;;
  36 e (ONCE_REWRITE_TAC [INST [(`#1.00`,`t:real`)] ATN2_ROT_TAN]);;
  37 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
  38 e SERGEI_TAC;; (* done 0:04 *)
  39
  40 g Ineq.I_2570626711;;
  41 e PREP;;
  42 e (ONCE_REWRITE_TAC [INST [(`#1.00`,`t:real`)] ATN2_ROT_TAN]);;
  43 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
  44 e SERGEI_TAC;; (* done 0:06 *)
  45
  46 g Ineq.I_3296257235;;
  47 e PREP;;
  48 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
  49 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
  50 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
  51 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
  52 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
  53 e SERGEI_TAC;; (* done 27:51 *)
  54 (*
  55 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
  56 SPEC_RULE;;
  57 e (REWRITE_TAC [SPEC `y1:real` SQRT_POW_2]);;
  58 sqrt;;
  59 prove(`y1 = sqrt y1 * sqrt y1`, MESON_TAC[SQRT_POW_2]);;
  60 INST  ();;
  61 g `y1 >= &0 ==> y1 = sqrt y1 * sqrt y1`;;
  62 e (REWRITE_TAC [sqrt]);;
  63 e (REAL_ARITH_TAC);;
  64 e (MESON_TAC []);;
  65 e (SUBST_ALL_TAC (prove(`y1 = sqrt y1 * sqrt y1`,ARITH_TAC)));;
  66 e (SUBST_ALL_TAC (prove(`y2 = sqrt x2`,CHEAT_TAC)));;
  67 e (SUBST_ALL_TAC (prove(`y3 = sqrt x3`,CHEAT_TAC)));;
  68 e (SUBST_ALL_TAC (prove(`y4 = sqrt x4`,CHEAT_TAC)));;
  69 e (SUBST_ALL_TAC (prove(`y5 = sqrt x5`,CHEAT_TAC)));;
  70 e (SUBST_ALL_TAC (prove(`y6 = sqrt x6`,CHEAT_TAC)));;
  71 e (SUBST_ALL_TAC (prove(`y1*y1=x1`,CHEAT_TAC)));;
  72 e (SUBST_ALL_TAC (prove(`y2*y2=x2`,CHEAT_TAC)));;
  73 e (SUBST_ALL_TAC (prove(`y3*y3=x3`,CHEAT_TAC)));;
  74 e (SUBST_ALL_TAC (prove(`y4*y4=x4`,CHEAT_TAC)));;
  75 e (SUBST_ALL_TAC (prove(`y5*y5=x5`,CHEAT_TAC)));;
  76 e (SUBST_ALL_TAC (prove(`y6*y6=x6`,CHEAT_TAC)));;
  77 e (SUBST_ALL_TAC (prove(`(&1 + (y1 - &2) * -- &25 / &13) = (&63 - &25*y1) / &13`,ARITH_TAC)));;
  78 e (SUBST_ALL_TAC (prove(`(&1 + (y2 - &2) * -- &25 / &13) = (&63 - &25*y2) / &13`,ARITH_TAC)));;
  79 e (SUBST_ALL_TAC (prove(`(&1 + (y3 - &2) * -- &25 / &13) = (&63 - &25*y3) / &13`,ARITH_TAC)));;
  80 e (SUBST_ALL_TAC (prove(`y1 = sqrt x1`,CHEAT_TAC)));;
  81 e (SUBST_ALL_TAC (prove(`y2 = sqrt x2`,CHEAT_TAC)));;
  82 e (SUBST_ALL_TAC (prove(`y3 = sqrt x3`,CHEAT_TAC)));;
  83 e (SUBST_ALL_TAC (prove(`y4 = sqrt x4`,CHEAT_TAC)));;
  84 e (SUBST_ALL_TAC (prove(`y5 = sqrt x5`,CHEAT_TAC)));;
  85 e (SUBST_ALL_TAC (prove(`y6 = sqrt x6`,CHEAT_TAC)));;
  86 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x1 /\ sqrt x1 <= #2.52) = (#4.0 <=  x1 /\ x1 <= #6.3504)`,CHEAT_TAC)));;
  87 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x2 /\ sqrt x2 <= #2.52) = (#4.0 <=  x2 /\ x2 <= #6.3504)`,CHEAT_TAC)));;
  88 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x3 /\ sqrt x3 <= #2.52) = (#4.0 <=  x3 /\ x3 <= #6.3504)`,CHEAT_TAC)));;
  89 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x4 /\ sqrt x4 <= #2.52) = (#4.0 <=  x4 /\ x4 <= #6.3504)`,CHEAT_TAC)));;
  90 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x5 /\ sqrt x5 <= #2.52) = (#4.0 <=  x5 /\ x5 <= #6.3504)`,CHEAT_TAC)));;
  91 e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x6 /\ sqrt x6 <= #2.52) = (#4.0 <=  x6 /\ x6 <= #6.3504)`,CHEAT_TAC)));;
  92 e (ONCE_REWRITE_TAC [INST [(`#1.3`,`t:real`)] ATN2_ROT_TAN]);;
  93 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
  94 e SERGEI_TAC;;
  95 *)
  96
  97 g Ineq.I_8519146937;;
  98 e PREP;;
  99 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 100 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 101 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 102 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 103 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 104 e SERGEI_TAC;; (* done 8:48 *)
 105
 106 g Ineq.I_4667071578;;
 107 e PREP;;
 108 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 109 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 110 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 111 e SERGEI_TAC;; (* done 5:39 *)
 112
 113 g Ineq.I_1395142356;;
 114 e PREP;;
 115 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 116 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 117 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 118 e SERGEI_TAC;; (* done 1h57:15 *)
 119
 120 g Ineq.I_7394240696;;
 121 e PREP;;
 122 e (ONCE_REWRITE_TAC [INST [(`#1.1`,`t:real`)] ATN2_ROT_TAN]);;
 123 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 124 e SERGEI_TAC;; (* done 29:26 *)
 125
 126 g Ineq.I_7726998381;;
 127 e PREP;;
 128 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 129 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 130 e SERGEI_TAC;; (* done 6:16 *)
 131
 132 g Ineq.I_4047599236;;
 133 e PREP;;
 134 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 135 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 136 e SERGEI_TAC;; (* done 0:59 *)
 137
 138 g Ineq.I_3526497018;;
 139 e PREP;;
 140 e (ONCE_REWRITE_TAC [INST [(`#0.94`,`t:real`)] ATN2_ROT_TAN]);;
 141 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 142 e SERGEI_TAC;; (* done 0:30 *)
 143
 144 g Ineq.I_5957966880;;
 145 e PREP;;
 146 e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
 147 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 148 e SERGEI_TAC;; (* done 0:55 *)
 149
 150 g Ineq.I_7043724150;; (* \/ *)
 151 e PREP;;
 152 e DISJ2_TAC;;  (* 'quadratic_root_plus' *)
 153 e DISJ1_TAC;;
 154 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 155 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 156 e (ONCE_REWRITE_TAC [INST [(`-- #3.5`,`t:real`)] ATN2_ROT_TAN]);;
 157 e SERGEI_TAC;; (* TODO *)
 158
 159
 160 g Ineq.I_6944699408;; (* TODO \/ *)
 161 g Ineq.I_4240815464;; (* TODO \/ *)
 162 g Ineq.I_3862621143;; (* TODO \/ *)
 163 g Ineq.I_5464178191;; (* TODO \/ *)
 164
 165 g Ineq.I_3020140039;;
 166 e PREP;;
 167 e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
 168 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 169 e SERGEI_TAC;; (* done 3:11 *)
 170
 171 g Ineq.I_9414951439;;
 172 e PREP;;
 173 e (ONCE_REWRITE_TAC [INST [(`#0.27`,`t:real`)] ATN2_ROT_TAN]);;
 174 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 175 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 176 e SERGEI_TAC;; (* TODO, sqrt8  *)
 177
 178 g Ineq.I_8248508703;;
 179 e PREP;;
 180 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 181 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 182 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 183 e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
 184 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 185 e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
 186 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 187 e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
 188 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 189 e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
 190 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 191 e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
 192 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 193 e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
 194 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 195 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 196 e SERGEI_TAC;; (* done 6h39:24 *)
 197
 198 (*
 199 e PREP;;
 200 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 201 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 202 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 203 e (SINGLE_REWR_TAC (INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN));;
 204 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 205 e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
 206 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 207 e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
 208 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 209 e (SINGLE_REWR_TAC (INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN));;
 210 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 211 e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
 212 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 213 e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
 214 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 215 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 216 e SERGEI_TAC;; (* takes 8h07:51 *)
 217 *)
 218
 219 g Ineq.I_3318775219;;
 220 e PREP;;
 221 e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
 222 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 223 e SERGEI_TAC;; (* done 1:32 *)
 224
 225 g Ineq.I_9922699028;;
 226 e PREP;;
 227 e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
 228 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 229 e SERGEI_TAC;; (* done 0:27 *)
 230
 231 g Ineq.I_5000076558;;
 232 e PREP;;
 233 e (ONCE_REWRITE_TAC [INST [(`#1.4`,`t:real`)] ATN2_ROT_TAN]);;
 234 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 235 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 236 e SERGEI_TAC;; (* done 2:24 *)
 237
 238 g Ineq.I_9251360200;;
 239 e PREP;;
 240 e (ONCE_REWRITE_TAC [INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN]);;
 241 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 242 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 243 e SERGEI_TAC;; (* done 5:19 *)
 244
 245 g Ineq.I_9756015945;;
 246 e PREP;;
 247 e (ONCE_REWRITE_TAC [INST [(`#1.4`,`t:real`)] ATN2_ROT_TAN]);;
 248 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 249 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 250 e SERGEI_TAC;; (* done 1:10 *)
 251
 252 g Ineq.I_181212899;;
 253 e PREP;;
 254 e (ONCE_REWRITE_TAC [INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN]);;
 255 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 256 e SERGEI_TAC;; (* done 0:28 *)
 257
 258 g Ineq.I_5760733457;;
 259 e PREP;;
 260 e (ONCE_REWRITE_TAC [INST [(`#0.95`,`t:real`)] ATN2_ROT_TAN]);;
 261 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 262 e SERGEI_TAC;; (* done 2:08 *)
 263
 264 g Ineq.I_2563100177;;
 265 e PREP;;
 266 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 267 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 268 e (ONCE_REWRITE_TAC [INST [(`#1.3`,`t:real`)] ATN2_ROT_TAN]);;
 269 e SERGEI_TAC;; (* TODO wide domain *)
 270
 271 g Ineq.I_7931207804;;
 272 e PREP;;
 273 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 274 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 275 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 276 e (SINGLE_REWR_TAC (INST [(`#1.2`,`t:real`)] ATN2_ROT_TAN));;
 277 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 278 e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
 279 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 280 e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
 281 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 282 e (SINGLE_REWR_TAC (INST [(`#1.2`,`t:real`)] ATN2_ROT_TAN));;
 283 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 284 e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
 285 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 286 e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
 287 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 288 e SERGEI_TAC;; (* done 9h45:15 *)
 289
 290 g Ineq.I_9225295803;;
 291 e PREP;;
 292 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 293 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 294 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 295 e (ONCE_REWRITE_TAC [INST [(`#0.75`,`t:real`)] ATN2_ROT_TAN]);;
 296 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 297 e SERGEI_TAC;; (* done 9h00:00 (less than) *)
 298
 299 g Ineq.I_9291937879;;
 300 e PREP;;
 301 e (ONCE_REWRITE_TAC [INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN]);;
 302 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 303 e SERGEI_TAC;; (* done 3:30 *)
 304
 305 g Ineq.I_7761782916;; (* TODO \/ *)
 306
 307 g Ineq.I_4840774900;;
 308 e PREP;;
 309 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 310 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 311 e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
 312 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 313 e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
 314 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 315 e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
 316 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 317 e (SINGLE_REWR_TAC (INST [(`#0.4`,`t:real`)] ATN2_ROT_TAN));;
 318 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 319 e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
 320 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 321 e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
 322 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 323 e SERGEI_TAC;; (* TODO, sqrt8*)
 324
 325 g Ineq.I_9995621667;;
 326 e PREP;;
 327 e (ONCE_REWRITE_TAC [INST [(`#0.175`,`t:real`)] ATN2_ROT_TAN]);;
 328 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 329 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 330 e SERGEI_TAC;; (* done 11:30 *)
 331
 332 g Ineq.I_5769230427;;
 333 e PREP;;
 334 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 335 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 336 e (SINGLE_REWR_TAC (INST [(`#0.275`,`t:real`)] ATN2_ROT_TAN));;
 337 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 338 e (SINGLE_REWR_TAC (INST [(`-- #2.5`,`t:real`)] ATN2_ROT_TAN));; (* TO DO establish that this rotation is valid *)
 339
 340
 341 g Ineq.I_9229542852;;
 342 e PREP;;
 343 e (ONCE_REWRITE_TAC [INST [(`#0.7`,`t:real`)] ATN2_ROT_TAN]);;
 344 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 345 e SERGEI_TAC;; (* done 0:57 *)
 346
 347 g Ineq.I_1550635295;;
 348 e PREP;;
 349 e (ONCE_REWRITE_TAC [INST [(`#0.7`,`t:real`)] ATN2_ROT_TAN]);;
 350 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 351 e SERGEI_TAC;; (* done 0:46 *)
 352
 353 g Ineq.I_4491491732;;
 354 e PREP;;
 355 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 356 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 357 e (ONCE_REWRITE_TAC [INST [(`#0.56`,`t:real`)] ATN2_ROT_TAN]);;
 358 e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
 359 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 360 e SERGEI_TAC;; (* done 1h20:00 (less than) *)
 361
 362 g Ineq.I_8282573160;;
 363 e PREP;;
 364 e (CONV_TAC REAL_RAT_REDUCE_CONV);;
 365 e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
 366 e (SINGLE_REWR_TAC (INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN));;
 367 e SERGEI_TAC;;
 368 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 369 e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
 370 e SERGEI_TAC;;
 371 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 372 e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
 373 e SERGEI_TAC;;
 374 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 375 e (SINGLE_REWR_TAC (INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN));;
 376 e SERGEI_TAC;;
 377 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 378 e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
 379 e SERGEI_TAC;;
 380 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 381 e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
 382 e SERGEI_TAC;;
 383 e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
 384 e SERGEI_TAC;; (* TODO poly factor becomes zero --> rewrite *)
 385
 386
 387 g Ineq.I_8611785756;; (* TODO \/ *)
 388
 389 g Ineq.I_6224332984;; (* TODO \/ *)
 390
 391 g Ineq.I_4198769118;; (* TODO acs *)
 392
 393 g Ineq.I_1965189142;; (* TODO COND *)
 394
 395 g Ineq.I_6096597438;; (* TODO COND *)
 396
 397
 398 end;;