(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: nonlinear inequalities                                                             *)
(* Author:  Roland Zumkeller     *)
(* Date: 2010-08-30                                                    *)
(* ========================================================================== *)

(*

Zumkeller's verification of nonlinear inequalities using Sergei package.
http://code.google.com/p/sergei/

Times are given in the format XhMM:SS for hours, minutes, seconds.
*)

module Zumkeller_test = struct

needs "nonlinear/oracle.hl";;
needs "nonlinear/ineq.hl";;
needs "general/update_database_310.ml";;

(* commented out in ineq.hl:
g Ineq.I_3336871894;;
g Ineq.I_8880534953;;
*)

g Ineq.I_5735387903;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.04`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:03 *)

g Ineq.I_5490182221;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.00`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:04 *)

g Ineq.I_2570626711;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.00`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:06 *)

g Ineq.I_3296257235;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 27:51 *)
(*
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
SPEC_RULE;;
e (REWRITE_TAC [SPEC `y1:real` SQRT_POW_2]);;
sqrt;;
prove(`y1 = sqrt y1 * sqrt y1`, MESON_TAC[SQRT_POW_2]);;
INST  ();;
g `y1 >= &0 ==> y1 = sqrt y1 * sqrt y1`;;
e (REWRITE_TAC [sqrt]);;
e (REAL_ARITH_TAC);;
e (MESON_TAC []);;
e (SUBST_ALL_TAC (prove(`y1 = sqrt y1 * sqrt y1`,ARITH_TAC)));;
e (SUBST_ALL_TAC (prove(`y2 = sqrt x2`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y3 = sqrt x3`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y4 = sqrt x4`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y5 = sqrt x5`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y6 = sqrt x6`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y1*y1=x1`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y2*y2=x2`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y3*y3=x3`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y4*y4=x4`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y5*y5=x5`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y6*y6=x6`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(&1 + (y1 - &2) * -- &25 / &13) = (&63 - &25*y1) / &13`,ARITH_TAC)));;
e (SUBST_ALL_TAC (prove(`(&1 + (y2 - &2) * -- &25 / &13) = (&63 - &25*y2) / &13`,ARITH_TAC)));;
e (SUBST_ALL_TAC (prove(`(&1 + (y3 - &2) * -- &25 / &13) = (&63 - &25*y3) / &13`,ARITH_TAC)));;
e (SUBST_ALL_TAC (prove(`y1 = sqrt x1`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y2 = sqrt x2`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y3 = sqrt x3`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y4 = sqrt x4`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y5 = sqrt x5`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`y6 = sqrt x6`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x1 /\ sqrt x1 <= #2.52) = (#4.0 <=  x1 /\ x1 <= #6.3504)`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x2 /\ sqrt x2 <= #2.52) = (#4.0 <=  x2 /\ x2 <= #6.3504)`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x3 /\ sqrt x3 <= #2.52) = (#4.0 <=  x3 /\ x3 <= #6.3504)`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x4 /\ sqrt x4 <= #2.52) = (#4.0 <=  x4 /\ x4 <= #6.3504)`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x5 /\ sqrt x5 <= #2.52) = (#4.0 <=  x5 /\ x5 <= #6.3504)`,CHEAT_TAC)));;
e (SUBST_ALL_TAC (prove(`(#2.0 <= sqrt x6 /\ sqrt x6 <= #2.52) = (#4.0 <=  x6 /\ x6 <= #6.3504)`,CHEAT_TAC)));;
e (ONCE_REWRITE_TAC [INST [(`#1.3`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;;
*)

g Ineq.I_8519146937;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 8:48 *)

g Ineq.I_4667071578;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 5:39 *)

g Ineq.I_1395142356;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 1h57:15 *)

g Ineq.I_7394240696;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.1`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 29:26 *)

g Ineq.I_7726998381;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 6:16 *)

g Ineq.I_4047599236;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:59 *)

g Ineq.I_3526497018;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.94`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:30 *)

g Ineq.I_5957966880;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.9`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:55 *)

g Ineq.I_7043724150;; (* \/ *)
e PREP;;
e DISJ2_TAC;;  (* 'quadratic_root_plus' *)
e DISJ1_TAC;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (ONCE_REWRITE_TAC [INST [(`-- #3.5`,`t:real`)] ATN2_ROT_TAN]);;
e SERGEI_TAC;; (* TODO *)


g Ineq.I_6944699408;; (* TODO \/ *)
g Ineq.I_4240815464;; (* TODO \/ *)
g Ineq.I_3862621143;; (* TODO \/ *)
g Ineq.I_5464178191;; (* TODO \/ *)

g Ineq.I_3020140039;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 3:11 *)

g Ineq.I_9414951439;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.27`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* TODO, sqrt8  *)

g Ineq.I_8248508703;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.95`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 6h39:24 *)

(*
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (SINGLE_REWR_TAC (INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#2.1`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* takes 8h07:51 *)
*)

g Ineq.I_3318775219;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 1:32 *)

g Ineq.I_9922699028;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:27 *)

g Ineq.I_5000076558;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.4`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 2:24 *)

g Ineq.I_9251360200;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 5:19 *)

g Ineq.I_9756015945;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#1.4`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 1:10 *)

g Ineq.I_181212899;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.6`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:28 *)

g Ineq.I_5760733457;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.95`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 2:08 *)

g Ineq.I_2563100177;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (ONCE_REWRITE_TAC [INST [(`#1.3`,`t:real`)] ATN2_ROT_TAN]);;
e SERGEI_TAC;; (* TODO wide domain *)

g Ineq.I_7931207804;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (SINGLE_REWR_TAC (INST [(`#1.2`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.2`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e SERGEI_TAC;; (* done 9h45:15 *)

g Ineq.I_9225295803;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [(`#0.75`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 9h00:00 (less than) *)

g Ineq.I_9291937879;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.8`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 3:30 *)

g Ineq.I_7761782916;; (* TODO \/ *)

g Ineq.I_4840774900;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (SINGLE_REWR_TAC (INST [(`#0.45`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.4`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.02`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e SERGEI_TAC;; (* TODO, sqrt8*)

g Ineq.I_9995621667;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.175`,`t:real`)] ATN2_ROT_TAN]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 11:30 *)

g Ineq.I_5769230427;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (SINGLE_REWR_TAC (INST [(`#0.275`,`t:real`)] ATN2_ROT_TAN));;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`-- #2.5`,`t:real`)] ATN2_ROT_TAN));; (* TO DO establish that this rotation is valid *)


g Ineq.I_9229542852;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.7`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:57 *)

g Ineq.I_1550635295;;
e PREP;;
e (ONCE_REWRITE_TAC [INST [(`#0.7`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e SERGEI_TAC;; (* done 0:46 *)

g Ineq.I_4491491732;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (ONCE_REWRITE_TAC [INST [(`#0.56`,`t:real`)] ATN2_ROT_TAN]);;
e (ONCE_REWRITE_TAC [ATN2_ATN_XPOS]);;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e SERGEI_TAC;; (* done 1h20:00 (less than) *)

g Ineq.I_8282573160;;
e PREP;;
e (CONV_TAC REAL_RAT_REDUCE_CONV);;
e (ONCE_REWRITE_TAC [INST [`sqrt (&2048)`,`x:real`; `-- &16`,`y:real`] ATN2_ATN_XPOS]);;
e (SINGLE_REWR_TAC (INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#0.5`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e (SINGLE_REWR_TAC (INST [(`#1.8`,`t:real`)] ATN2_ROT_TAN));;
e SERGEI_TAC;;
e (SINGLE_REWR_TAC ATN2_ATN_XPOS);;
e SERGEI_TAC;; (* TODO poly factor becomes zero --> rewrite *)


g Ineq.I_8611785756;; (* TODO \/ *)

g Ineq.I_6224332984;; (* TODO \/ *)

g Ineq.I_4198769118;; (* TODO acs *)

g Ineq.I_1965189142;; (* TODO COND *)

g Ineq.I_6096597438;; (* TODO COND *)


end;;