(*

This file extends search capabilities to a few additional files.
For example, before this file is loaded the following search finds nothing, but
after the file is loaded it finds the thm SQRT_MUL

# search [`sqrt(x*y)`];;



By modifying the procedure below, search can be extended to the files of your choice.



   * The bulk of this file with created by the emacs macro listed below.

   * The emacs macro was read in by placing the cursor at the end of the macro and typing control-x control-e

   * HOL Light was loaded.  Then the extra files were loaded.
   Multivariate/vectors.ml
   Examples/analysis.ml
   Examples/transc.ml
   definitions_kepler.ml  (from google code)

  * The part of the screen showing the output from the extra files is highlighted, then the macro index-region is executed.

   * The buffer *scratch* is saved out to database_more.ml (this file) and the
   head and tail were slightly edited.

*)

(*

(defun index-region()
  "Build an array of user-added theorms in scratch region"
  (interactive)
  (kill-ring-save (mark) (point))
  (set-buffer (get-buffer-create "*scratch*"))
  (beginning-of-buffer)
  (yank)
  (let ((beg (point)))
    (end-of-buffer)
    (kill-region beg (point)))
  (beginning-of-buffer)
  (let ((pt (point)))
    (end-of-buffer)
    (universal-argument)
    (shell-command-on-region pt (point) 
    "egrep \"[^-] : thm =\"" "*scratch*" t "*scratch*"))
  (beginning-of-buffer)
  (while (re-search-forward " ) :.*$" nil t)
    (replace-match "" nil nil))
  (beginning-of-buffer)
  (while (re-search-forward " :.*$" nil t)
    (replace-match "" nil nil))
  (beginning-of-buffer)
  (while (re-search-forward "^val ( " nil t)
    (replace-match "" nil nil))
  (beginning-of-buffer)
  (while (re-search-forward "^val " nil t)
    (replace-match "" nil nil))
  (beginning-of-buffer)
  (replace-regexp "^.*$" "(\"\\&\",\\&);")
  (delete-backward-char 1)
  (insert "];;")
  (beginning-of-buffer)
  (insert "(* AUTOMATICALLY GENERATED FILE BY EMACS MACRO index-region:")
  (insert " DO NOT EDIT *);;\n\nthm_region_array := [")
  (beginning-of-buffer)
     )


*)

let thm_region_array = ref[];;

(* AUTOMATICALLY GENERATED FILE BY EMACS MACRO index-region: DO NOT EDIT *)

thm_region_array := [("EXISTS_DIFF",EXISTS_DIFF);
("GE_REFL",GE_REFL);
("FORALL_SUC",FORALL_SUC);
("SEQ_MONO_LEMMA",SEQ_MONO_LEMMA);
("REAL_HALF",REAL_HALF);
("UPPER_BOUND_FINITE_SET",UPPER_BOUND_FINITE_SET);
("UPPER_BOUND_FINITE_SET_REAL",UPPER_BOUND_FINITE_SET_REAL);
("LOWER_BOUND_FINITE_SET",LOWER_BOUND_FINITE_SET);
("LOWER_BOUND_FINITE_SET_REAL",LOWER_BOUND_FINITE_SET_REAL);
("REAL_CONVEX_BOUND_LT",REAL_CONVEX_BOUND_LT);
("REAL_CONVEX_BOUND_LE",REAL_CONVEX_BOUND_LE);
("INFINITE_ENUMERATE",INFINITE_ENUMERATE);
("APPROACHABLE_LT_LE",APPROACHABLE_LT_LE);
("REAL_LE_BETWEEN",REAL_LE_BETWEEN);
("REAL_LT_BETWEEN",REAL_LT_BETWEEN);
("TRIANGLE_LEMMA",TRIANGLE_LEMMA);
("LAMBDA_SKOLEM",LAMBDA_SKOLEM);
("LAMBDA_PAIR",LAMBDA_PAIR);
("sup",sup);
("SUP",SUP);
("SUP_FINITE_LEMMA",SUP_FINITE_LEMMA);
("SUP_FINITE",SUP_FINITE);
("REAL_LE_SUP_FINITE",REAL_LE_SUP_FINITE);
("REAL_SUP_LE_FINITE",REAL_SUP_LE_FINITE);
("REAL_LT_SUP_FINITE",REAL_LT_SUP_FINITE);
("REAL_SUP_LT_FINITE",REAL_SUP_LT_FINITE);
("REAL_SUP_UNIQUE",REAL_SUP_UNIQUE);
("REAL_SUP_LE",REAL_SUP_LE);
("REAL_SUP_LE_SUBSET",REAL_SUP_LE_SUBSET);
("REAL_SUP_BOUNDS",REAL_SUP_BOUNDS);
("REAL_ABS_SUP_LE",REAL_ABS_SUP_LE);
("REAL_SUP_ASCLOSE",REAL_SUP_ASCLOSE);
("inf",inf);
("INF",INF);
("INF_FINITE_LEMMA",INF_FINITE_LEMMA);
("INF_FINITE",INF_FINITE);
("REAL_LE_INF",REAL_LE_INF);
("REAL_LE_INF_FINITE",REAL_LE_INF_FINITE);
("REAL_INF_LE_FINITE",REAL_INF_LE_FINITE);
("REAL_LT_INF_FINITE",REAL_LT_INF_FINITE);
("REAL_INF_LT_FINITE",REAL_INF_LT_FINITE);
("REAL_INF_UNIQUE",REAL_INF_UNIQUE);
("REAL_LE_INF",REAL_LE_INF);
("REAL_LE_INF_SUBSET",REAL_LE_INF_SUBSET);
("REAL_ABS_INF_LE",REAL_ABS_INF_LE);
("REAL_INF_BOUNDS",REAL_INF_BOUNDS);
("REAL_ABS_INF_LE",REAL_ABS_INF_LE);
("REAL_INF_ASCLOSE",REAL_INF_ASCLOSE);
("hull",hull);
("HULL_P",HULL_P);
("P_HULL",P_HULL);
("HULL_EQ",HULL_EQ);
("HULL_HULL",HULL_HULL);
("HULL_SUBSET",HULL_SUBSET);
("HULL_MONO",HULL_MONO);
("HULL_ANTIMONO",HULL_ANTIMONO);
("HULL_MINIMAL",HULL_MINIMAL);
("SUBSET_HULL",SUBSET_HULL);
("HULL_UNIQUE",HULL_UNIQUE);
("HULL_UNION_SUBSET",HULL_UNION_SUBSET);
("HULL_UNION",HULL_UNION);
("HULL_REDUNDANT_EQ",HULL_REDUNDANT_EQ);
("HULL_REDUNDANT",HULL_REDUNDANT);
("HULL_INDUCT",HULL_INDUCT);
("HULL_INC",HULL_INC);
("REAL_ARCH_SIMPLE",REAL_ARCH_SIMPLE);
("REAL_ARCH_LT",REAL_ARCH_LT);
("REAL_ARCH",REAL_ARCH);
("REAL_ARCH_INV",REAL_ARCH_INV);
("REAL_POW_LBOUND",REAL_POW_LBOUND);
("REAL_ARCH_POW",REAL_ARCH_POW);
("REAL_ARCH_POW2",REAL_ARCH_POW2);
("REAL_ARCH_POW_INV",REAL_ARCH_POW_INV);
("FORALL_POS_MONO",FORALL_POS_MONO);
("FORALL_POS_MONO_1",FORALL_POS_MONO_1);
("REAL_ARCH_RDIV_EQ_0",REAL_ARCH_RDIV_EQ_0);
("REAL_MAX_SUP",REAL_MAX_SUP);
("REAL_MIN_INF",REAL_MIN_INF);
("sqrt",sqrt);
("SQRT_UNIQUE",SQRT_UNIQUE);
("POW_2_SQRT",POW_2_SQRT);
("SQRT_0",SQRT_0);
("SQRT_1",SQRT_1);
("POW_2_SQRT_ABS",POW_2_SQRT_ABS);
("SUM_GP_BASIC",SUM_GP_BASIC);
("SUM_GP_MULTIPLIED",SUM_GP_MULTIPLIED);
("SUM_GP",SUM_GP);
("SUM_GP_OFFSET",SUM_GP_OFFSET);
("FORALL_1",FORALL_1);
("FORALL_2",FORALL_2);
("FORALL_3",FORALL_3);
("SUM_1",SUM_1);
("SUM_2",SUM_2);
("SUM_3",SUM_3);
("vector_add",vector_add);
("vector_sub",vector_sub);
("vector_neg",vector_neg);
("vector_mul",vector_mul);
("vec",vec);
("dot",dot);
("DOT_1",DOT_1);
("DOT_2",DOT_2);
("DOT_3",DOT_3);
("VEC_COMPONENT",VEC_COMPONENT);
("VECTOR_ADD_COMPONENT",VECTOR_ADD_COMPONENT);
("VECTOR_SUB_COMPONENT",VECTOR_SUB_COMPONENT);
("VECTOR_NEG_COMPONENT",VECTOR_NEG_COMPONENT);
("VECTOR_MUL_COMPONENT",VECTOR_MUL_COMPONENT);
("COND_COMPONENT",COND_COMPONENT);
("VECTOR_ADD_SYM",VECTOR_ADD_SYM);
("VECTOR_ADD_LID",VECTOR_ADD_LID);
("VECTOR_ADD_RID",VECTOR_ADD_RID);
("VECTOR_SUB_REFL",VECTOR_SUB_REFL);
("VECTOR_ADD_LINV",VECTOR_ADD_LINV);
("VECTOR_ADD_RINV",VECTOR_ADD_RINV);
("VECTOR_SUB_RADD",VECTOR_SUB_RADD);
("VECTOR_NEG_SUB",VECTOR_NEG_SUB);
("VECTOR_SUB_EQ",VECTOR_SUB_EQ);
("VECTOR_MUL_ASSOC",VECTOR_MUL_ASSOC);
("VECTOR_MUL_LID",VECTOR_MUL_LID);
("VECTOR_MUL_LZERO",VECTOR_MUL_LZERO);
("VECTOR_SUB_ADD",VECTOR_SUB_ADD);
("VECTOR_SUB_ADD2",VECTOR_SUB_ADD2);
("VECTOR_ADD_LDISTRIB",VECTOR_ADD_LDISTRIB);
("VECTOR_SUB_LDISTRIB",VECTOR_SUB_LDISTRIB);
("VECTOR_ADD_RDISTRIB",VECTOR_ADD_RDISTRIB);
("VECTOR_SUB_RDISTRIB",VECTOR_SUB_RDISTRIB);
("VECTOR_ADD_SUB",VECTOR_ADD_SUB);
("VECTOR_EQ_ADDR",VECTOR_EQ_ADDR);
("VECTOR_SUB",VECTOR_SUB);
("VECTOR_SUB_RZERO",VECTOR_SUB_RZERO);
("VECTOR_MUL_RZERO",VECTOR_MUL_RZERO);
("VECTOR_NEG_MINUS1",VECTOR_NEG_MINUS1);
("VECTOR_ADD_ASSOC",VECTOR_ADD_ASSOC);
("VECTOR_SUB_LZERO",VECTOR_SUB_LZERO);
("VECTOR_NEG_NEG",VECTOR_NEG_NEG);
("VECTOR_MUL_LNEG",VECTOR_MUL_LNEG);
("VECTOR_MUL_RNEG",VECTOR_MUL_RNEG);
("VECTOR_NEG_0",VECTOR_NEG_0);
("VECTOR_ADD_AC",VECTOR_ADD_AC);
("VEC_EQ",VEC_EQ);
("DOT_SYM",DOT_SYM);
("DOT_LADD",DOT_LADD);
("DOT_RADD",DOT_RADD);
("DOT_LSUB",DOT_LSUB);
("DOT_RSUB",DOT_RSUB);
("DOT_LMUL",DOT_LMUL);
("DOT_RMUL",DOT_RMUL);
("DOT_LNEG",DOT_LNEG);
("DOT_RNEG",DOT_RNEG);
("DOT_LZERO",DOT_LZERO);
("DOT_RZERO",DOT_RZERO);
("DOT_POS_LE",DOT_POS_LE);
("DOT_EQ_0",DOT_EQ_0);
("DOT_POS_LT",DOT_POS_LT);
("vector_norm",vector_norm);
("FORALL_DIMINDEX_1",FORALL_DIMINDEX_1);
("VECTOR_ONE",VECTOR_ONE);
("FORALL_REAL_ONE",FORALL_REAL_ONE);
("NORM_REAL",NORM_REAL);
("dist",dist);
("DIST_REAL",DIST_REAL);
("CONNECTED_REAL_LEMMA",CONNECTED_REAL_LEMMA);
("SQUARE_BOUND_LEMMA",SQUARE_BOUND_LEMMA);
("SQUARE_CONTINUOUS",SQUARE_CONTINUOUS);
("SQRT_WORKS",SQRT_WORKS);
("SQRT_POS_LE",SQRT_POS_LE);
("SQRT_POW_2",SQRT_POW_2);
("SQRT_MUL",SQRT_MUL);
("SQRT_INV",SQRT_INV);
("SQRT_DIV",SQRT_DIV);
("SQRT_POW2",SQRT_POW2);
("SQRT_MONO_LT",SQRT_MONO_LT);
("SQRT_MONO_LE",SQRT_MONO_LE);
("SQRT_MONO_LT_EQ",SQRT_MONO_LT_EQ);
("SQRT_MONO_LE_EQ",SQRT_MONO_LE_EQ);
("SQRT_INJ",SQRT_INJ);
("SQRT_LT_0",SQRT_LT_0);
("SQRT_EQ_0",SQRT_EQ_0);
("SQRT_POS_LT",SQRT_POS_LT);
("REAL_LE_LSQRT",REAL_LE_LSQRT);
("REAL_LE_RSQRT",REAL_LE_RSQRT);
("REAL_LT_RSQRT",REAL_LT_RSQRT);
("SQRT_EVEN_POW2",SQRT_EVEN_POW2);
("REAL_DIV_SQRT",REAL_DIV_SQRT);
("NORM_0",NORM_0);
("NORM_POS_LE",NORM_POS_LE);
("NORM_NEG",NORM_NEG);
("NORM_SUB",NORM_SUB);
("NORM_MUL",NORM_MUL);
("NORM_EQ_0_DOT",NORM_EQ_0_DOT);
("NORM_EQ_0",NORM_EQ_0);
("NORM_POS_LT",NORM_POS_LT);
("NORM_POW_2",NORM_POW_2);
("NORM_EQ_0_IMP",NORM_EQ_0_IMP);
("NORM_LE_0",NORM_LE_0);
("VECTOR_MUL_EQ_0",VECTOR_MUL_EQ_0);
("VECTOR_MUL_LCANCEL",VECTOR_MUL_LCANCEL);
("VECTOR_MUL_RCANCEL",VECTOR_MUL_RCANCEL);
("VECTOR_MUL_LCANCEL_IMP",VECTOR_MUL_LCANCEL_IMP);
("VECTOR_MUL_RCANCEL_IMP",VECTOR_MUL_RCANCEL_IMP);
("NORM_CAUCHY_SCHWARZ",NORM_CAUCHY_SCHWARZ);
("NORM_CAUCHY_SCHWARZ_ABS",NORM_CAUCHY_SCHWARZ_ABS);
("NORM_TRIANGLE",NORM_TRIANGLE);
("NORM_TRIANGLE_SUB",NORM_TRIANGLE_SUB);
("NORM_TRIANGLE_LE",NORM_TRIANGLE_LE);
("NORM_TRIANGLE_LT",NORM_TRIANGLE_LT);
("COMPONENT_LE_NORM",COMPONENT_LE_NORM);
("NORM_BOUND_COMPONENT_LE",NORM_BOUND_COMPONENT_LE);
("NORM_BOUND_COMPONENT_LT",NORM_BOUND_COMPONENT_LT);
("NORM_LE_L1",NORM_LE_L1);
("REAL_ABS_NORM",REAL_ABS_NORM);
("REAL_ABS_SUB_NORM",REAL_ABS_SUB_NORM);
("NORM_LE",NORM_LE);
("NORM_LT",NORM_LT);
("NORM_EQ",NORM_EQ);
("NORM_EQ_1",NORM_EQ_1);
("DOT_SQUARE_NORM",DOT_SQUARE_NORM);
("NORM_EQ_SQUARE",NORM_EQ_SQUARE);
("NORM_LE_SQUARE",NORM_LE_SQUARE);
("NORM_GE_SQUARE",NORM_GE_SQUARE);
("NORM_LT_SQUARE",NORM_LT_SQUARE);
("NORM_GT_SQUARE",NORM_GT_SQUARE);
("DOT_NORM",DOT_NORM);
("DOT_NORM_NEG",DOT_NORM_NEG);
("VECTOR_EQ",VECTOR_EQ);
("DIST_REFL",DIST_REFL);
("DIST_SYM",DIST_SYM);
("DIST_POS_LE",DIST_POS_LE);
("DIST_TRIANGLE",DIST_TRIANGLE);
("DIST_TRIANGLE_ALT",DIST_TRIANGLE_ALT);
("DIST_EQ_0",DIST_EQ_0);
("DIST_POS_LT",DIST_POS_LT);
("DIST_NZ",DIST_NZ);
("DIST_TRIANGLE_LE",DIST_TRIANGLE_LE);
("DIST_TRIANGLE_LT",DIST_TRIANGLE_LT);
("DIST_TRIANGLE_HALF_L",DIST_TRIANGLE_HALF_L);
("DIST_TRIANGLE_HALF_R",DIST_TRIANGLE_HALF_R);
("DIST_TRIANGLE_ADD",DIST_TRIANGLE_ADD);
("DIST_MUL",DIST_MUL);
("DIST_TRIANGLE_ADD_HALF",DIST_TRIANGLE_ADD_HALF);
("DIST_LE_0",DIST_LE_0);
("NEUTRAL_VECTOR_ADD",NEUTRAL_VECTOR_ADD);
("MONOIDAL_VECTOR_ADD",MONOIDAL_VECTOR_ADD);
("vsum",vsum);
("VSUM_CLAUSES",VSUM_CLAUSES);
("VSUM",VSUM);
("VSUM_EQ_0",VSUM_EQ_0);
("VSUM_0",VSUM_0);
("VSUM_LMUL",VSUM_LMUL);
("VSUM_RMUL",VSUM_RMUL);
("VSUM_ADD",VSUM_ADD);
("VSUM_SUB",VSUM_SUB);
("VSUM_CONST",VSUM_CONST);
("VSUM_COMPONENT",VSUM_COMPONENT);
("VSUM_IMAGE",VSUM_IMAGE);
("VSUM_UNION",VSUM_UNION);
("VSUM_DIFF",VSUM_DIFF);
("VSUM_DELETE",VSUM_DELETE);
("VSUM_INCL_EXCL",VSUM_INCL_EXCL);
("VSUM_NEG",VSUM_NEG);
("VSUM_EQ",VSUM_EQ);
("VSUM_SUPERSET",VSUM_SUPERSET);
("VSUM_UNION_RZERO",VSUM_UNION_RZERO);
("VSUM_UNION_LZERO",VSUM_UNION_LZERO);
("VSUM_RESTRICT",VSUM_RESTRICT);
("VSUM_RESTRICT_SET",VSUM_RESTRICT_SET);
("VSUM_CASES",VSUM_CASES);
("VSUM_SING",VSUM_SING);
("VSUM_NORM",VSUM_NORM);
("VSUM_NORM_LE",VSUM_NORM_LE);
("VSUM_NORM_BOUND",VSUM_NORM_BOUND);
("VSUM_CLAUSES_NUMSEG",VSUM_CLAUSES_NUMSEG);
("VSUM_CLAUSES_RIGHT",VSUM_CLAUSES_RIGHT);
("VSUM_CMUL_NUMSEG",VSUM_CMUL_NUMSEG);
("VSUM_EQ_NUMSEG",VSUM_EQ_NUMSEG);
("VSUM_IMAGE_GEN",VSUM_IMAGE_GEN);
("VSUM_GROUP",VSUM_GROUP);
("VSUM_VMUL",VSUM_VMUL);
("VSUM_DELTA",VSUM_DELTA);
("VSUM_ADD_NUMSEG",VSUM_ADD_NUMSEG);
("VSUM_ADD_SPLIT",VSUM_ADD_SPLIT);
("VSUM_VSUM_PRODUCT",VSUM_VSUM_PRODUCT);
("VSUM_IMAGE_NONZERO",VSUM_IMAGE_NONZERO);
("VSUM_UNION_NONZERO",VSUM_UNION_NONZERO);
("VSUM_UNIONS_NONZERO",VSUM_UNIONS_NONZERO);
("VSUM_CLAUSES_LEFT",VSUM_CLAUSES_LEFT);
("VSUM_DIFFS",VSUM_DIFFS);
("VSUM_DELETE_CASES",VSUM_DELETE_CASES);
("VSUM_EQ_GENERAL",VSUM_EQ_GENERAL);
("VSUM_EQ_GENERAL_INVERSES",VSUM_EQ_GENERAL_INVERSES);
("VSUM_NORM_ALLSUBSETS_BOUND",VSUM_NORM_ALLSUBSETS_BOUND);
("DOT_LSUM",DOT_LSUM);
("DOT_RSUM",DOT_RSUM);
("VSUM_OFFSET",VSUM_OFFSET);
("VSUM_OFFSET_0",VSUM_OFFSET_0);
("VSUM_TRIV_NUMSEG",VSUM_TRIV_NUMSEG);
("VSUM_CONST_NUMSEG",VSUM_CONST_NUMSEG);
("VSUM_SUC",VSUM_SUC);
("basis",basis);
("NORM_BASIS",NORM_BASIS);
("NORM_BASIS_1",NORM_BASIS_1);
("VECTOR_CHOOSE_SIZE",VECTOR_CHOOSE_SIZE);
("VECTOR_CHOOSE_DIST",VECTOR_CHOOSE_DIST);
("BASIS_INJ",BASIS_INJ);
("BASIS_COMPONENT",BASIS_COMPONENT);
("BASIS_EXPANSION",BASIS_EXPANSION);
("BASIS_EXPANSION_UNIQUE",BASIS_EXPANSION_UNIQUE);
("DOT_BASIS",DOT_BASIS);
("BASIS_EQ_0",BASIS_EQ_0);
("BASIS_NONZERO",BASIS_NONZERO);
("VECTOR_EQ_LDOT",VECTOR_EQ_LDOT);
("VECTOR_EQ_RDOT",VECTOR_EQ_RDOT);
("orthogonal",orthogonal);
("ORTHOGONAL_BASIS",ORTHOGONAL_BASIS);
("ORTHOGONAL_BASIS_BASIS",ORTHOGONAL_BASIS_BASIS);
("ORTHOGONAL_CLAUSES",ORTHOGONAL_CLAUSES);
("ORTHOGONAL_SYM",ORTHOGONAL_SYM);
("vector",vector);
("VECTOR_1",VECTOR_1);
("VECTOR_2",VECTOR_2);
("VECTOR_3",VECTOR_3);
("FORALL_VECTOR_1",FORALL_VECTOR_1);
("FORALL_VECTOR_2",FORALL_VECTOR_2);
("FORALL_VECTOR_3",FORALL_VECTOR_3);
("linear",linear);
("LINEAR_COMPOSE_CMUL",LINEAR_COMPOSE_CMUL);
("LINEAR_COMPOSE_NEG",LINEAR_COMPOSE_NEG);
("LINEAR_COMPOSE_ADD",LINEAR_COMPOSE_ADD);
("LINEAR_COMPOSE_SUB",LINEAR_COMPOSE_SUB);
("LINEAR_COMPOSE",LINEAR_COMPOSE);
("LINEAR_ID",LINEAR_ID);
("LINEAR_ZERO",LINEAR_ZERO);
("LINEAR_COMPOSE_VSUM",LINEAR_COMPOSE_VSUM);
("LINEAR_VMUL_COMPONENT",LINEAR_VMUL_COMPONENT);
("LINEAR_0",LINEAR_0);
("LINEAR_CMUL",LINEAR_CMUL);
("LINEAR_NEG",LINEAR_NEG);
("LINEAR_ADD",LINEAR_ADD);
("LINEAR_SUB",LINEAR_SUB);
("LINEAR_VSUM",LINEAR_VSUM);
("LINEAR_VSUM_MUL",LINEAR_VSUM_MUL);
("LINEAR_INJECTIVE_0",LINEAR_INJECTIVE_0);
("LINEAR_BOUNDED",LINEAR_BOUNDED);
("LINEAR_BOUNDED_POS",LINEAR_BOUNDED_POS);
("bilinear",bilinear);
("BILINEAR_LADD",BILINEAR_LADD);
("BILINEAR_RADD",BILINEAR_RADD);
("BILINEAR_LMUL",BILINEAR_LMUL);
("BILINEAR_RMUL",BILINEAR_RMUL);
("BILINEAR_LNEG",BILINEAR_LNEG);
("BILINEAR_RNEG",BILINEAR_RNEG);
("BILINEAR_LZERO",BILINEAR_LZERO);
("BILINEAR_RZERO",BILINEAR_RZERO);
("BILINEAR_LSUB",BILINEAR_LSUB);
("BILINEAR_RSUB",BILINEAR_RSUB);
("BILINEAR_VSUM",BILINEAR_VSUM);
("BILINEAR_BOUNDED",BILINEAR_BOUNDED);
("BILINEAR_BOUNDED_POS",BILINEAR_BOUNDED_POS);
("adjoint",adjoint);
("ADJOINT_WORKS",ADJOINT_WORKS);
("ADJOINT_LINEAR",ADJOINT_LINEAR);
("ADJOINT_CLAUSES",ADJOINT_CLAUSES);
("ADJOINT_ADJOINT",ADJOINT_ADJOINT);
("ADJOINT_UNIQUE",ADJOINT_UNIQUE);
("matrix_neg",matrix_neg);
("matrix_add",matrix_add);
("matrix_sub",matrix_sub);
("matrix_mul",matrix_mul);
("matrix_vector_mul",matrix_vector_mul);
("vector_matrix_mul",vector_matrix_mul);
("mat",mat);
("transp",transp);
("row",row);
("column",column);
("rows",rows);
("columns",columns);
("MATRIX_ADD_SYM",MATRIX_ADD_SYM);
("MATRIX_ADD_ASSOC",MATRIX_ADD_ASSOC);
("MATRIX_ADD_LID",MATRIX_ADD_LID);
("MATRIX_ADD_RID",MATRIX_ADD_RID);
("MATRIX_ADD_LNEG",MATRIX_ADD_LNEG);
("MATRIX_ADD_RNEG",MATRIX_ADD_RNEG);
("MATRIX_SUB",MATRIX_SUB);
("MATRIX_SUB_REFL",MATRIX_SUB_REFL);
("MATRIX_ADD_LDISTRIB",MATRIX_ADD_LDISTRIB);
("MATRIX_MUL_LID",MATRIX_MUL_LID);
("MATRIX_MUL_RID",MATRIX_MUL_RID);
("MATRIX_MUL_ASSOC",MATRIX_MUL_ASSOC);
("MATRIX_VECTOR_MUL_ASSOC",MATRIX_VECTOR_MUL_ASSOC);
("MATRIX_VECTOR_MUL_LID",MATRIX_VECTOR_MUL_LID);
("MATRIX_TRANSP_MUL",MATRIX_TRANSP_MUL);
("MATRIX_EQ",MATRIX_EQ);
("MATRIX_VECTOR_MUL_COMPONENT",MATRIX_VECTOR_MUL_COMPONENT);
("DOT_LMUL_MATRIX",DOT_LMUL_MATRIX);
("TRANSP_MAT",TRANSP_MAT);
("TRANSP_TRANSP",TRANSP_TRANSP);
("ROW_TRANSP",ROW_TRANSP);
("COLUMN_TRANSP",COLUMN_TRANSP);
("ROWS_TRANSP",ROWS_TRANSP);
("COLUMNS_TRANSP",COLUMNS_TRANSP);
("MATRIX_MUL_DOT",MATRIX_MUL_DOT);
("MATRIX_MUL_VSUM",MATRIX_MUL_VSUM);
("VECTOR_COMPONENTWISE",VECTOR_COMPONENTWISE);
("LINEAR_COMPONENTWISE",LINEAR_COMPONENTWISE);
("invertible",invertible);
("matrix_inv",matrix_inv);
("matrix",matrix);
("MATRIX_VECTOR_MUL_LINEAR",MATRIX_VECTOR_MUL_LINEAR);
("MATRIX_WORKS",MATRIX_WORKS);
("MATRIX_VECTOR_MUL",MATRIX_VECTOR_MUL);
("MATRIX_OF_MATRIX_VECTOR_MUL",MATRIX_OF_MATRIX_VECTOR_MUL);
("MATRIX_COMPOSE",MATRIX_COMPOSE);
("MATRIX_VECTOR_COLUMN",MATRIX_VECTOR_COLUMN);
("ADJOINT_MATRIX",ADJOINT_MATRIX);
("MATRIX_ADJOINT",MATRIX_ADJOINT);
("onorm",onorm);
("NORM_BOUND_GENERALIZE",NORM_BOUND_GENERALIZE);
("ONORM",ONORM);
("ONORM_POS_LE",ONORM_POS_LE);
("ONORM_EQ_0",ONORM_EQ_0);
("ONORM_CONST",ONORM_CONST);
("ONORM_POS_LT",ONORM_POS_LT);
("ONORM_COMPOSE",ONORM_COMPOSE);
("ONORM_NEG_LEMMA",ONORM_NEG_LEMMA);
("ONORM_NEG",ONORM_NEG);
("ONORM_TRIANGLE",ONORM_TRIANGLE);
("ONORM_TRIANGLE_LE",ONORM_TRIANGLE_LE);
("ONORM_TRIANGLE_LT",ONORM_TRIANGLE_LT);
("lift",lift);
("drop",drop);
("LIFT_COMPONENT",LIFT_COMPONENT);
("LIFT_DROP",LIFT_DROP);
("FORALL_LIFT",FORALL_LIFT);
("EXISTS_LIFT",EXISTS_LIFT);
("FORALL_DROP",FORALL_DROP);
("EXISTS_DROP",EXISTS_DROP);
("LIFT_EQ",LIFT_EQ);
("DROP_EQ",DROP_EQ);
("LIFT_IN_IMAGE_LIFT",LIFT_IN_IMAGE_LIFT);
("LIFT_NUM",LIFT_NUM);
("LIFT_ADD",LIFT_ADD);
("LIFT_SUB",LIFT_SUB);
("LIFT_CMUL",LIFT_CMUL);
("LIFT_NEG",LIFT_NEG);
("LIFT_EQ_CMUL",LIFT_EQ_CMUL);
("LIFT_SUM",LIFT_SUM);
("DROP_LAMBDA",DROP_LAMBDA);
("DROP_VEC",DROP_VEC);
("DROP_ADD",DROP_ADD);
("DROP_SUB",DROP_SUB);
("DROP_CMUL",DROP_CMUL);
("DROP_NEG",DROP_NEG);
("DROP_VSUM",DROP_VSUM);
("NORM_LIFT",NORM_LIFT);
("DIST_LIFT",DIST_LIFT);
("ABS_DROP",ABS_DROP);
("LINEAR_VMUL_DROP",LINEAR_VMUL_DROP);
("LINEAR_FROM_REALS",LINEAR_FROM_REALS);
("LINEAR_TO_REALS",LINEAR_TO_REALS);
("DROP_EQ_0",DROP_EQ_0);
("VSUM_REAL",VSUM_REAL);
("DROP_WLOG_LE",DROP_WLOG_LE);
("LINEAR_FSTCART",LINEAR_FSTCART);
("LINEAR_SNDCART",LINEAR_SNDCART);
("FSTCART_VEC",FSTCART_VEC);
("FSTCART_ADD",FSTCART_ADD);
("FSTCART_CMUL",FSTCART_CMUL);
("FSTCART_NEG",FSTCART_NEG);
("FSTCART_SUB",FSTCART_SUB);
("FSTCART_VSUM",FSTCART_VSUM);
("SNDCART_VEC",SNDCART_VEC);
("SNDCART_ADD",SNDCART_ADD);
("SNDCART_CMUL",SNDCART_CMUL);
("SNDCART_NEG",SNDCART_NEG);
("SNDCART_SUB",SNDCART_SUB);
("SNDCART_VSUM",SNDCART_VSUM);
("PASTECART_VEC",PASTECART_VEC);
("PASTECART_ADD",PASTECART_ADD);
("PASTECART_CMUL",PASTECART_CMUL);
("PASTECART_NEG",PASTECART_NEG);
("PASTECART_SUB",PASTECART_SUB);
("PASTECART_VSUM",PASTECART_VSUM);
("NORM_FSTCART",NORM_FSTCART);
("DIST_FSTCART",DIST_FSTCART);
("NORM_SNDCART",NORM_SNDCART);
("DIST_SNDCART",DIST_SNDCART);
("DOT_PASTECART",DOT_PASTECART);
("NORM_PASTECART",NORM_PASTECART);
("subspace",subspace);
("span",span);
("dependent",dependent);
("independent",independent);
("SUBSPACE_UNIV",SUBSPACE_UNIV);
("SUBSPACE_0",SUBSPACE_0);
("SUBSPACE_ADD",SUBSPACE_ADD);
("SUBSPACE_MUL",SUBSPACE_MUL);
("SUBSPACE_NEG",SUBSPACE_NEG);
("SUBSPACE_SUB",SUBSPACE_SUB);
("SUBSPACE_VSUM",SUBSPACE_VSUM);
("SUBSPACE_LINEAR_IMAGE",SUBSPACE_LINEAR_IMAGE);
("SUBSPACE_LINEAR_PREIMAGE",SUBSPACE_LINEAR_PREIMAGE);
("SUBSPACE_TRIVIAL",SUBSPACE_TRIVIAL);
("SUBSPACE_INTER",SUBSPACE_INTER);
("SPAN_SPAN",SPAN_SPAN);
("SPAN_MONO",SPAN_MONO);
("SUBSPACE_SPAN",SUBSPACE_SPAN);
("SPAN_CLAUSES",SPAN_CLAUSES);
("SPAN_INDUCT",SPAN_INDUCT);
("SPAN_EMPTY",SPAN_EMPTY);
("INDEPENDENT_EMPTY",INDEPENDENT_EMPTY);
("INDEPENDENT_MONO",INDEPENDENT_MONO);
("SPAN_SUBSPACE",SPAN_SUBSPACE);
("SPAN_INDUCT_ALT",SPAN_INDUCT_ALT);
("SPAN_SUPERSET",SPAN_SUPERSET);
("SPAN_INC",SPAN_INC);
("SPAN_0",SPAN_0);
("SPAN_ADD",SPAN_ADD);
("SPAN_MUL",SPAN_MUL);
("SPAN_NEG",SPAN_NEG);
("SPAN_SUB",SPAN_SUB);
("SPAN_VSUM",SPAN_VSUM);
("SPAN_ADD_EQ",SPAN_ADD_EQ);
("SPAN_LINEAR_IMAGE",SPAN_LINEAR_IMAGE);
("SPAN_BREAKDOWN",SPAN_BREAKDOWN);
("SPAN_BREAKDOWN_EQ",SPAN_BREAKDOWN_EQ);
("IN_SPAN_INSERT",IN_SPAN_INSERT);
("IN_SPAN_DELETE",IN_SPAN_DELETE);
("SPAN_TRANS",SPAN_TRANS);
("SPAN_EXPLICIT",SPAN_EXPLICIT);
("DEPENDENT_EXPLICIT",DEPENDENT_EXPLICIT);
("SPAN_FINITE",SPAN_FINITE);
("SPAN_STDBASIS",SPAN_STDBASIS);
("HAS_SIZE_STDBASIS",HAS_SIZE_STDBASIS);
("FINITE_STDBASIS",FINITE_STDBASIS);
("CARD_STDBASIS",CARD_STDBASIS);
("INDEPENDENT_STDBASIS_LEMMA",INDEPENDENT_STDBASIS_LEMMA);
("INDEPENDENT_STDBASIS",INDEPENDENT_STDBASIS);
("INDEPENDENT_INSERT",INDEPENDENT_INSERT);
("SPANNING_SUBSET_INDEPENDENT",SPANNING_SUBSET_INDEPENDENT);
("EXCHANGE_LEMMA",EXCHANGE_LEMMA);
("INDEPENDENT_SPAN_BOUND",INDEPENDENT_SPAN_BOUND);
("INDEPENDENT_BOUND",INDEPENDENT_BOUND);
("DEPENDENT_BIGGERSET",DEPENDENT_BIGGERSET);
("MAXIMAL_INDEPENDENT_SUBSET_EXTEND",MAXIMAL_INDEPENDENT_SUBSET_EXTEND);
("MAXIMAL_INDEPENDENT_SUBSET",MAXIMAL_INDEPENDENT_SUBSET);
("dim",dim);
("BASIS_EXISTS",BASIS_EXISTS);
("INDEPENDENT_CARD_LE_DIM",INDEPENDENT_CARD_LE_DIM);
("SPAN_CARD_GE_DIM",SPAN_CARD_GE_DIM);
("BASIS_CARD_EQ_DIM",BASIS_CARD_EQ_DIM);
("DIM_UNIQUE",DIM_UNIQUE);
("DIM_UNIV",DIM_UNIV);
("DIM_SUBSET",DIM_SUBSET);
("DIM_SUBSET_UNIV",DIM_SUBSET_UNIV);
("CARD_GE_DIM_INDEPENDENT",CARD_GE_DIM_INDEPENDENT);
("CARD_LE_DIM_SPANNING",CARD_LE_DIM_SPANNING);
("CARD_EQ_DIM",CARD_EQ_DIM);
("INDEPENDENT_BOUND_GENERAL",INDEPENDENT_BOUND_GENERAL);
("DEPENDENT_BIGGERSET_GENERAL",DEPENDENT_BIGGERSET_GENERAL);
("DIM_SPAN",DIM_SPAN);
("SUBSET_LE_DIM",SUBSET_LE_DIM);
("SPAN_EQ_DIM",SPAN_EQ_DIM);
("SPANS_IMAGE",SPANS_IMAGE);
("DIM_IMAGE_LE",DIM_IMAGE_LE);
("SPANNING_SURJECTIVE_IMAGE",SPANNING_SURJECTIVE_IMAGE);
("INDEPENDENT_INJECTIVE_IMAGE",INDEPENDENT_INJECTIVE_IMAGE);
("VECTOR_SUB_PROJECT_ORTHOGONAL",VECTOR_SUB_PROJECT_ORTHOGONAL);
("BASIS_ORTHOGONAL",BASIS_ORTHOGONAL);
("ORTHOGONAL_BASIS_EXISTS",ORTHOGONAL_BASIS_EXISTS);
("SPAN_EQ",SPAN_EQ);
("SPAN_NOT_UNIV_ORTHOGONAL",SPAN_NOT_UNIV_ORTHOGONAL);
("SPAN_NOT_UNIV_SUBSET_HYPERPLANE",SPAN_NOT_UNIV_SUBSET_HYPERPLANE);
("LOWDIM_SUBSET_HYPERPLANE",LOWDIM_SUBSET_HYPERPLANE);
("LINEAR_INDEP_IMAGE_LEMMA",LINEAR_INDEP_IMAGE_LEMMA);
("LINEAR_INDEPENDENT_EXTEND_LEMMA",LINEAR_INDEPENDENT_EXTEND_LEMMA);
("LINEAR_INDEPENDENT_EXTEND",LINEAR_INDEPENDENT_EXTEND);
("SUBSPACE_ISOMORPHISM",SUBSPACE_ISOMORPHISM);
("SUBSPACE_KERNEL",SUBSPACE_KERNEL);
("LINEAR_EQ_0_SPAN",LINEAR_EQ_0_SPAN);
("LINEAR_EQ_0",LINEAR_EQ_0);
("LINEAR_EQ",LINEAR_EQ);
("LINEAR_EQ_STDBASIS",LINEAR_EQ_STDBASIS);
("BILINEAR_EQ",BILINEAR_EQ);
("BILINEAR_EQ_STDBASIS",BILINEAR_EQ_STDBASIS);
("LEFT_INVERTIBLE_TRANSP",LEFT_INVERTIBLE_TRANSP);
("RIGHT_INVERTIBLE_TRANSP",RIGHT_INVERTIBLE_TRANSP);
("LINEAR_INJECTIVE_LEFT_INVERSE",LINEAR_INJECTIVE_LEFT_INVERSE);
("LINEAR_SURJECTIVE_RIGHT_INVERSE",LINEAR_SURJECTIVE_RIGHT_INVERSE);
("MATRIX_LEFT_INVERTIBLE_INJECTIVE",MATRIX_LEFT_INVERTIBLE_INJECTIVE);
("MATRIX_LEFT_INVERTIBLE_KER",MATRIX_LEFT_INVERTIBLE_KER);
("MATRIX_RIGHT_INVERTIBLE_SURJECTIVE",MATRIX_RIGHT_INVERTIBLE_SURJECTIVE);
("MATRIX_LEFT_INVERTIBLE_INDEPENDENT_COLUMNS",MATRIX_LEFT_INVERTIBLE_INDEPENDENT_COLUMNS);
("MATRIX_RIGHT_INVERTIBLE_INDEPENDENT_ROWS",MATRIX_RIGHT_INVERTIBLE_INDEPENDENT_ROWS);
("MATRIX_RIGHT_INVERTIBLE_SPAN_COLUMNS",MATRIX_RIGHT_INVERTIBLE_SPAN_COLUMNS);
("MATRIX_LEFT_INVERTIBLE_SPAN_ROWS",MATRIX_LEFT_INVERTIBLE_SPAN_ROWS);
("LINEAR_INJECTIVE_IMP_SURJECTIVE",LINEAR_INJECTIVE_IMP_SURJECTIVE);
("LINEAR_SURJECTIVE_IMP_INJECTIVE",LINEAR_SURJECTIVE_IMP_INJECTIVE);
("LEFT_RIGHT_INVERSE_EQ",LEFT_RIGHT_INVERSE_EQ);
("ISOMORPHISM_EXPAND",ISOMORPHISM_EXPAND);
("LINEAR_INJECTIVE_ISOMORPHISM",LINEAR_INJECTIVE_ISOMORPHISM);
("LINEAR_SURJECTIVE_ISOMORPHISM",LINEAR_SURJECTIVE_ISOMORPHISM);
("LINEAR_INVERSE_LEFT",LINEAR_INVERSE_LEFT);
("LEFT_INVERSE_LINEAR",LEFT_INVERSE_LINEAR);
("RIGHT_INVERSE_LINEAR",RIGHT_INVERSE_LINEAR);
("MATRIX_LEFT_RIGHT_INVERSE",MATRIX_LEFT_RIGHT_INVERSE);
("rowvector",rowvector);
("columnvector",columnvector);
("TRANSP_COLUMNVECTOR",TRANSP_COLUMNVECTOR);
("TRANSP_ROWVECTOR",TRANSP_ROWVECTOR);
("DOT_ROWVECTOR_COLUMNVECTOR",DOT_ROWVECTOR_COLUMNVECTOR);
("DOT_MATRIX_PRODUCT",DOT_MATRIX_PRODUCT);
("DOT_MATRIX_VECTOR_MUL",DOT_MATRIX_VECTOR_MUL);
("infnorm",infnorm);
("NUMSEG_DIMINDEX_NONEMPTY",NUMSEG_DIMINDEX_NONEMPTY);
("INFNORM_SET_IMAGE",INFNORM_SET_IMAGE);
("INFNORM_SET_LEMMA",INFNORM_SET_LEMMA);
("INFNORM_POS_LE",INFNORM_POS_LE);
("INFNORM_TRIANGLE",INFNORM_TRIANGLE);
("INFNORM_EQ_0",INFNORM_EQ_0);
("INFNORM_0",INFNORM_0);
("INFNORM_NEG",INFNORM_NEG);
("INFNORM_SUB",INFNORM_SUB);
("REAL_ABS_SUB_INFNORM",REAL_ABS_SUB_INFNORM);
("REAL_ABS_INFNORM",REAL_ABS_INFNORM);
("COMPONENT_LE_INFNORM",COMPONENT_LE_INFNORM);
("INFNORM_MUL_LEMMA",INFNORM_MUL_LEMMA);
("INFNORM_MUL",INFNORM_MUL);
("INFNORM_POS_LT",INFNORM_POS_LT);
("INFNORM_LE_NORM",INFNORM_LE_NORM);
("NORM_LE_INFNORM",NORM_LE_INFNORM);
("NORM_CAUCHY_SCHWARZ_EQ",NORM_CAUCHY_SCHWARZ_EQ);
("NORM_CAUCHY_SCHWARZ_ABS_EQ",NORM_CAUCHY_SCHWARZ_ABS_EQ);
("NORM_TRIANGLE_EQ",NORM_TRIANGLE_EQ);
("collinear",collinear);
("COLLINEAR_EMPTY",COLLINEAR_EMPTY);
("COLLINEAR_SING",COLLINEAR_SING);
("COLLINEAR_2",COLLINEAR_2);
("COLLINEAR_LEMMA",COLLINEAR_LEMMA);
("NORM_CAUCHY_SCHWARZ_EQUAL",NORM_CAUCHY_SCHWARZ_EQUAL);
("F_IMP",F_IMP);
("LEFT_AND_OVER_OR",LEFT_AND_OVER_OR);
("RIGHT_AND_OVER_OR",RIGHT_AND_OVER_OR);
("LESS_EQUAL_ANTISYM",LESS_EQUAL_ANTISYM);
("NOT_LESS_0",NOT_LESS_0);
("LESS_LEMMA1",LESS_LEMMA1);
("LESS_SUC_REFL",LESS_SUC_REFL);
("LESS_EQ_SUC_REFL",LESS_EQ_SUC_REFL);
("LESS_EQUAL_ADD",LESS_EQUAL_ADD);
("LESS_EQ_IMP_LESS_SUC",LESS_EQ_IMP_LESS_SUC);
("LESS_MONO_ADD",LESS_MONO_ADD);
("LESS_SUC",LESS_SUC);
("LESS_ADD_1",LESS_ADD_1);
("SUC_SUB1",SUC_SUB1);
("LESS_ADD_SUC",LESS_ADD_SUC);
("OR_LESS",OR_LESS);
("NOT_SUC_LESS_EQ",NOT_SUC_LESS_EQ);
("LESS_LESS_CASES",LESS_LESS_CASES);
("SUB_SUB",SUB_SUB);
("LESS_CASES_IMP",LESS_CASES_IMP);
("SUB_LESS_EQ",SUB_LESS_EQ);
("SUB_EQ_EQ_0",SUB_EQ_EQ_0);
("SUB_LEFT_LESS_EQ",SUB_LEFT_LESS_EQ);
("SUB_LEFT_GREATER_EQ",SUB_LEFT_GREATER_EQ);
("LESS_0_CASES",LESS_0_CASES);
("LESS_OR",LESS_OR);
("SUB_OLD",SUB_OLD);
("real_le",real_le);
("REAL_10",REAL_10);
("REAL_LDISTRIB",REAL_LDISTRIB);
("REAL_LT_IADD",REAL_LT_IADD);
("REAL_MUL_RID",REAL_MUL_RID);
("REAL_MUL_RINV",REAL_MUL_RINV);
("REAL_RDISTRIB",REAL_RDISTRIB);
("REAL_EQ_LADD",REAL_EQ_LADD);
("REAL_EQ_RADD",REAL_EQ_RADD);
("REAL_ADD_LID_UNIQ",REAL_ADD_LID_UNIQ);
("REAL_ADD_RID_UNIQ",REAL_ADD_RID_UNIQ);
("REAL_LNEG_UNIQ",REAL_LNEG_UNIQ);
("REAL_RNEG_UNIQ",REAL_RNEG_UNIQ);
("REAL_NEG_ADD",REAL_NEG_ADD);
("REAL_MUL_LZERO",REAL_MUL_LZERO);
("REAL_MUL_RZERO",REAL_MUL_RZERO);
("REAL_NEG_LMUL",REAL_NEG_LMUL);
("REAL_NEG_RMUL",REAL_NEG_RMUL);
("REAL_NEGNEG",REAL_NEGNEG);
("REAL_NEG_MUL2",REAL_NEG_MUL2);
("REAL_LT_LADD",REAL_LT_LADD);
("REAL_LT_RADD",REAL_LT_RADD);
("REAL_NOT_LT",REAL_NOT_LT);
("REAL_LT_ANTISYM",REAL_LT_ANTISYM);
("REAL_LT_GT",REAL_LT_GT);
("REAL_NOT_LE",REAL_NOT_LE);
("REAL_LE_TOTAL",REAL_LE_TOTAL);
("REAL_LE_REFL",REAL_LE_REFL);
("REAL_LE_LT",REAL_LE_LT);
("REAL_LT_LE",REAL_LT_LE);
("REAL_LT_IMP_LE",REAL_LT_IMP_LE);
("REAL_LTE_TRANS",REAL_LTE_TRANS);
("REAL_LE_TRANS",REAL_LE_TRANS);
("REAL_NEG_LT0",REAL_NEG_LT0);
("REAL_NEG_GT0",REAL_NEG_GT0);
("REAL_NEG_LE0",REAL_NEG_LE0);
("REAL_NEG_GE0",REAL_NEG_GE0);
("REAL_LT_NEGTOTAL",REAL_LT_NEGTOTAL);
("REAL_LE_NEGTOTAL",REAL_LE_NEGTOTAL);
("REAL_LE_MUL",REAL_LE_MUL);
("REAL_LE_SQUARE",REAL_LE_SQUARE);
("REAL_LT_01",REAL_LT_01);
("REAL_LE_LADD",REAL_LE_LADD);
("REAL_LE_RADD",REAL_LE_RADD);
("REAL_LT_ADD2",REAL_LT_ADD2);
("REAL_LT_ADD",REAL_LT_ADD);
("REAL_LT_ADDNEG",REAL_LT_ADDNEG);
("REAL_LT_ADDNEG2",REAL_LT_ADDNEG2);
("REAL_LT_ADD1",REAL_LT_ADD1);
("REAL_SUB_ADD",REAL_SUB_ADD);
("REAL_SUB_ADD2",REAL_SUB_ADD2);
("REAL_SUB_REFL",REAL_SUB_REFL);
("REAL_SUB_0",REAL_SUB_0);
("REAL_LE_DOUBLE",REAL_LE_DOUBLE);
("REAL_LE_NEGL",REAL_LE_NEGL);
("REAL_LE_NEGR",REAL_LE_NEGR);
("REAL_NEG_EQ0",REAL_NEG_EQ0);
("REAL_NEG_0",REAL_NEG_0);
("REAL_NEG_SUB",REAL_NEG_SUB);
("REAL_SUB_LT",REAL_SUB_LT);
("REAL_SUB_LE",REAL_SUB_LE);
("REAL_EQ_LMUL",REAL_EQ_LMUL);
("REAL_EQ_RMUL",REAL_EQ_RMUL);
("REAL_SUB_LDISTRIB",REAL_SUB_LDISTRIB);
("REAL_SUB_RDISTRIB",REAL_SUB_RDISTRIB);
("REAL_NEG_EQ",REAL_NEG_EQ);
("REAL_NEG_MINUS1",REAL_NEG_MINUS1);
("REAL_INV_NZ",REAL_INV_NZ);
("REAL_INVINV",REAL_INVINV);
("REAL_LT_IMP_NE",REAL_LT_IMP_NE);
("REAL_INV_POS",REAL_INV_POS);
("REAL_LT_LMUL_0",REAL_LT_LMUL_0);
("REAL_LT_RMUL_0",REAL_LT_RMUL_0);
("REAL_LT_LMUL_EQ",REAL_LT_LMUL_EQ);
("REAL_LT_RMUL_EQ",REAL_LT_RMUL_EQ);
("REAL_LT_RMUL_IMP",REAL_LT_RMUL_IMP);
("REAL_LT_LMUL_IMP",REAL_LT_LMUL_IMP);
("REAL_LINV_UNIQ",REAL_LINV_UNIQ);
("REAL_RINV_UNIQ",REAL_RINV_UNIQ);
("REAL_NEG_INV",REAL_NEG_INV);
("REAL_INV_1OVER",REAL_INV_1OVER);
("REAL",REAL);
("REAL_POS",REAL_POS);
("REAL_LE",REAL_LE);
("REAL_LT",REAL_LT);
("REAL_INJ",REAL_INJ);
("REAL_ADD",REAL_ADD);
("REAL_MUL",REAL_MUL);
("REAL_INV1",REAL_INV1);
("REAL_DIV_LZERO",REAL_DIV_LZERO);
("REAL_LT_NZ",REAL_LT_NZ);
("REAL_NZ_IMP_LT",REAL_NZ_IMP_LT);
("REAL_LT_RDIV_0",REAL_LT_RDIV_0);
("REAL_LT_RDIV",REAL_LT_RDIV);
("REAL_LT_FRACTION_0",REAL_LT_FRACTION_0);
("REAL_LT_MULTIPLE",REAL_LT_MULTIPLE);
("REAL_LT_FRACTION",REAL_LT_FRACTION);
("REAL_LT_HALF1",REAL_LT_HALF1);
("REAL_LT_HALF2",REAL_LT_HALF2);
("REAL_DOUBLE",REAL_DOUBLE);
("REAL_HALF_DOUBLE",REAL_HALF_DOUBLE);
("REAL_SUB_SUB",REAL_SUB_SUB);
("REAL_LT_ADD_SUB",REAL_LT_ADD_SUB);
("REAL_LT_SUB_RADD",REAL_LT_SUB_RADD);
("REAL_LT_SUB_LADD",REAL_LT_SUB_LADD);
("REAL_LE_SUB_LADD",REAL_LE_SUB_LADD);
("REAL_LE_SUB_RADD",REAL_LE_SUB_RADD);
("REAL_LT_NEG",REAL_LT_NEG);
("REAL_LE_NEG",REAL_LE_NEG);
("REAL_SUB_LZERO",REAL_SUB_LZERO);
("REAL_SUB_RZERO",REAL_SUB_RZERO);
("REAL_LTE_ADD2",REAL_LTE_ADD2);
("REAL_LTE_ADD",REAL_LTE_ADD);
("REAL_LT_MUL2_ALT",REAL_LT_MUL2_ALT);
("REAL_SUB_LNEG",REAL_SUB_LNEG);
("REAL_SUB_RNEG",REAL_SUB_RNEG);
("REAL_SUB_NEG2",REAL_SUB_NEG2);
("REAL_SUB_TRIANGLE",REAL_SUB_TRIANGLE);
("REAL_INV_MUL_WEAK",REAL_INV_MUL_WEAK);
("REAL_LE_LMUL_LOCAL",REAL_LE_LMUL_LOCAL);
("REAL_LE_RMUL_EQ",REAL_LE_RMUL_EQ);
("REAL_SUB_INV2",REAL_SUB_INV2);
("REAL_SUB_SUB2",REAL_SUB_SUB2);
("REAL_MEAN",REAL_MEAN);
("REAL_EQ_LMUL2",REAL_EQ_LMUL2);
("REAL_LE_MUL2V",REAL_LE_MUL2V);
("REAL_LE_LDIV",REAL_LE_LDIV);
("REAL_LE_RDIV",REAL_LE_RDIV);
("REAL_LT_1",REAL_LT_1);
("REAL_LE_LMUL_IMP",REAL_LE_LMUL_IMP);
("REAL_LE_RMUL_IMP",REAL_LE_RMUL_IMP);
("REAL_INV_LT1",REAL_INV_LT1);
("REAL_POS_NZ",REAL_POS_NZ);
("REAL_EQ_RMUL_IMP",REAL_EQ_RMUL_IMP);
("REAL_EQ_LMUL_IMP",REAL_EQ_LMUL_IMP);
("REAL_FACT_NZ",REAL_FACT_NZ);
("REAL_POSSQ",REAL_POSSQ);
("REAL_SUMSQ",REAL_SUMSQ);
("REAL_EQ_NEG",REAL_EQ_NEG);
("REAL_DIV_MUL2",REAL_DIV_MUL2);
("REAL_MIDDLE1",REAL_MIDDLE1);
("REAL_MIDDLE2",REAL_MIDDLE2);
("ABS_ZERO",ABS_ZERO);
("ABS_0",ABS_0);
("ABS_1",ABS_1);
("ABS_NEG",ABS_NEG);
("ABS_TRIANGLE",ABS_TRIANGLE);
("ABS_POS",ABS_POS);
("ABS_MUL",ABS_MUL);
("ABS_LT_MUL2",ABS_LT_MUL2);
("ABS_SUB",ABS_SUB);
("ABS_NZ",ABS_NZ);
("ABS_INV",ABS_INV);
("ABS_ABS",ABS_ABS);
("ABS_LE",ABS_LE);
("ABS_REFL",ABS_REFL);
("ABS_N",ABS_N);
("ABS_BETWEEN",ABS_BETWEEN);
("ABS_BOUND",ABS_BOUND);
("ABS_STILLNZ",ABS_STILLNZ);
("ABS_CASES",ABS_CASES);
("ABS_BETWEEN1",ABS_BETWEEN1);
("ABS_SIGN",ABS_SIGN);
("ABS_SIGN2",ABS_SIGN2);
("ABS_DIV",ABS_DIV);
("ABS_CIRCLE",ABS_CIRCLE);
("REAL_SUB_ABS",REAL_SUB_ABS);
("ABS_SUB_ABS",ABS_SUB_ABS);
("ABS_BETWEEN2",ABS_BETWEEN2);
("ABS_BOUNDS",ABS_BOUNDS);
("pow",pow);
("POW_0",POW_0);
("POW_NZ",POW_NZ);
("POW_INV",POW_INV);
("POW_ABS",POW_ABS);
("POW_PLUS1",POW_PLUS1);
("POW_ADD",POW_ADD);
("POW_1",POW_1);
("POW_2",POW_2);
("POW_POS",POW_POS);
("POW_LE",POW_LE);
("POW_M1",POW_M1);
("POW_MUL",POW_MUL);
("REAL_LE_SQUARE_POW",REAL_LE_SQUARE_POW);
("ABS_POW2",ABS_POW2);
("REAL_LE1_POW2",REAL_LE1_POW2);
("REAL_LT1_POW2",REAL_LT1_POW2);
("POW_POS_LT",POW_POS_LT);
("POW_2_LE1",POW_2_LE1);
("POW_2_LT",POW_2_LT);
("POW_MINUS1",POW_MINUS1);
("REAL_SUP_EXISTS",REAL_SUP_EXISTS);
("sup_def",sup_def);
("sup",sup);
("REAL_SUP",REAL_SUP);
("REAL_SUP_UBOUND",REAL_SUP_UBOUND);
("SETOK_LE_LT",SETOK_LE_LT);
("REAL_SUP_LE",REAL_SUP_LE);
("REAL_SUP_UBOUND_LE",REAL_SUP_UBOUND_LE);
("REAL_ARCH_SIMPLE",REAL_ARCH_SIMPLE);
("REAL_ARCH",REAL_ARCH);
("REAL_ARCH_LEAST",REAL_ARCH_LEAST);
("REAL_POW_LBOUND",REAL_POW_LBOUND);
("REAL_ARCH_POW",REAL_ARCH_POW);
("REAL_ARCH_POW2",REAL_ARCH_POW2);
("sum_EXISTS",sum_EXISTS);
("sum_DEF",sum_DEF);
("sum",sum);
("PSUM_SUM",PSUM_SUM);
("PSUM_SUM_NUMSEG",PSUM_SUM_NUMSEG);
("SUM_TWO",SUM_TWO);
("SUM_DIFF",SUM_DIFF);
("ABS_SUM",ABS_SUM);
("SUM_LE",SUM_LE);
("SUM_EQ",SUM_EQ);
("SUM_POS",SUM_POS);
("SUM_POS_GEN",SUM_POS_GEN);
("SUM_ABS",SUM_ABS);
("SUM_ABS_LE",SUM_ABS_LE);
("SUM_ZERO",SUM_ZERO);
("SUM_ADD",SUM_ADD);
("SUM_CMUL",SUM_CMUL);
("SUM_NEG",SUM_NEG);
("SUM_SUB",SUM_SUB);
("SUM_SUBST",SUM_SUBST);
("SUM_NSUB",SUM_NSUB);
("SUM_BOUND",SUM_BOUND);
("SUM_GROUP",SUM_GROUP);
("SUM_1",SUM_1);
("SUM_2",SUM_2);
("SUM_OFFSET",SUM_OFFSET);
("SUM_REINDEX",SUM_REINDEX);
("SUM_0",SUM_0);
("SUM_CANCEL",SUM_CANCEL);
("SUM_HORNER",SUM_HORNER);
("SUM_CONST",SUM_CONST);
("SUM_SPLIT",SUM_SPLIT);
("SUM_SWAP",SUM_SWAP);
("SUM_EQ_0",SUM_EQ_0);
("SUM_MORETERMS_EQ",SUM_MORETERMS_EQ);
("SUM_DIFFERENCES_EQ",SUM_DIFFERENCES_EQ);
("re_Union",re_Union);
("re_union",re_union);
("re_intersect",re_intersect);
("re_null",re_null);
("re_universe",re_universe);
("re_subset",re_subset);
("re_compl",re_compl);
("SUBSETA_REFL",SUBSETA_REFL);
("COMPL_MEM",COMPL_MEM);
("SUBSETA_ANTISYM",SUBSETA_ANTISYM);
("SUBSETA_TRANS",SUBSETA_TRANS);
("istopology",istopology);
("topology_tybij",topology_tybij);
("TOPOLOGY",TOPOLOGY);
("TOPOLOGY_UNION",TOPOLOGY_UNION);
("neigh",neigh);
("OPEN_OWN_NEIGH",OPEN_OWN_NEIGH);
("OPEN_UNOPEN",OPEN_UNOPEN);
("OPEN_SUBOPEN",OPEN_SUBOPEN);
("OPEN_NEIGH",OPEN_NEIGH);
("closed",closed);
("limpt",limpt);
("CLOSED_LIMPT",CLOSED_LIMPT);
("ismet",ismet);
("metric_tybij",metric_tybij);
("METRIC_ISMET",METRIC_ISMET);
("METRIC_ZERO",METRIC_ZERO);
("METRIC_SAME",METRIC_SAME);
("METRIC_POS",METRIC_POS);
("METRIC_SYM",METRIC_SYM);
("METRIC_TRIANGLE",METRIC_TRIANGLE);
("METRIC_NZ",METRIC_NZ);
("mtop",mtop);
("mtop_istopology",mtop_istopology);
("MTOP_OPEN",MTOP_OPEN);
("ball",ball);
("BALL_OPEN",BALL_OPEN);
("BALL_NEIGH",BALL_NEIGH);
("MTOP_LIMPT",MTOP_LIMPT);
("ISMET_R1",ISMET_R1);
("mr1",mr1);
("MR1_DEF",MR1_DEF);
("MR1_ADD",MR1_ADD);
("MR1_SUB",MR1_SUB);
("MR1_ADD_LE",MR1_ADD_LE);
("MR1_SUB_LE",MR1_SUB_LE);
("MR1_ADD_LT",MR1_ADD_LT);
("MR1_SUB_LT",MR1_SUB_LT);
("MR1_BETWEEN1",MR1_BETWEEN1);
("MR1_LIMPT",MR1_LIMPT);
("dorder",dorder);
("tends",tends);
("bounded",bounded);
("tendsto",tendsto);
("DORDER_LEMMA",DORDER_LEMMA);
("DORDER_NGE",DORDER_NGE);
("DORDER_TENDSTO",DORDER_TENDSTO);
("MTOP_TENDS",MTOP_TENDS);
("MTOP_TENDS_UNIQ",MTOP_TENDS_UNIQ);
("SEQ_TENDS",SEQ_TENDS);
("LIM_TENDS",LIM_TENDS);
("LIM_TENDS2",LIM_TENDS2);
("MR1_BOUNDED",MR1_BOUNDED);
("NET_NULL",NET_NULL);
("NET_CONV_BOUNDED",NET_CONV_BOUNDED);
("NET_CONV_NZ",NET_CONV_NZ);
("NET_CONV_IBOUNDED",NET_CONV_IBOUNDED);
("NET_NULL_ADD",NET_NULL_ADD);
("NET_NULL_MUL",NET_NULL_MUL);
("NET_NULL_CMUL",NET_NULL_CMUL);
("NET_ADD",NET_ADD);
("NET_NEG",NET_NEG);
("NET_SUB",NET_SUB);
("NET_MUL",NET_MUL);
("NET_INV",NET_INV);
("NET_DIV",NET_DIV);
("NET_ABS",NET_ABS);
("NET_SUM",NET_SUM);
("NET_LE",NET_LE);
("tends_num_real",tends_num_real);
("SEQ",SEQ);
("SEQ_CONST",SEQ_CONST);
("SEQ_ADD",SEQ_ADD);
("SEQ_MUL",SEQ_MUL);
("SEQ_NEG",SEQ_NEG);
("SEQ_INV",SEQ_INV);
("SEQ_SUB",SEQ_SUB);
("SEQ_DIV",SEQ_DIV);
("SEQ_UNIQ",SEQ_UNIQ);
("SEQ_NULL",SEQ_NULL);
("SEQ_SUM",SEQ_SUM);
("SEQ_TRANSFORM",SEQ_TRANSFORM);
("convergent",convergent);
("cauchy",cauchy);
("lim",lim);
("SEQ_LIM",SEQ_LIM);
("subseq",subseq);
("SUBSEQ_SUC",SUBSEQ_SUC);
("mono",mono);
("MONO_SUC",MONO_SUC);
("MAX_LEMMA",MAX_LEMMA);
("SEQ_BOUNDED",SEQ_BOUNDED);
("SEQ_BOUNDED_2",SEQ_BOUNDED_2);
("SEQ_CBOUNDED",SEQ_CBOUNDED);
("SEQ_ICONV",SEQ_ICONV);
("SEQ_NEG_CONV",SEQ_NEG_CONV);
("SEQ_NEG_BOUNDED",SEQ_NEG_BOUNDED);
("SEQ_BCONV",SEQ_BCONV);
("SEQ_MONOSUB",SEQ_MONOSUB);
("SEQ_SBOUNDED",SEQ_SBOUNDED);
("SEQ_SUBLE",SEQ_SUBLE);
("SEQ_DIRECT",SEQ_DIRECT);
("SEQ_CAUCHY",SEQ_CAUCHY);
("SEQ_LE",SEQ_LE);
("SEQ_LE_0",SEQ_LE_0);
("SEQ_SUC",SEQ_SUC);
("SEQ_ABS",SEQ_ABS);
("SEQ_ABS_IMP",SEQ_ABS_IMP);
("SEQ_INV0",SEQ_INV0);
("SEQ_POWER_ABS",SEQ_POWER_ABS);
("SEQ_POWER",SEQ_POWER);
("SEQ_HARMONIC",SEQ_HARMONIC);
("SEQ_SUBSEQ",SEQ_SUBSEQ);
("SEQ_POW",SEQ_POW);
("NEST_LEMMA",NEST_LEMMA);
("NEST_LEMMA_UNIQ",NEST_LEMMA_UNIQ);
("BOLZANO_LEMMA",BOLZANO_LEMMA);
("BOLZANO_LEMMA_ALT",BOLZANO_LEMMA_ALT);
("sums",sums);
("summable",summable);
("suminf",suminf);
("SUM_SUMMABLE",SUM_SUMMABLE);
("SUMMABLE_SUM",SUMMABLE_SUM);
("SUM_UNIQ",SUM_UNIQ);
("SER_UNIQ",SER_UNIQ);
("SER_0",SER_0);
("SER_POS_LE",SER_POS_LE);
("SER_POS_LT",SER_POS_LT);
("SER_GROUP",SER_GROUP);
("SER_PAIR",SER_PAIR);
("SER_OFFSET",SER_OFFSET);
("SER_OFFSET_REV",SER_OFFSET_REV);
("SER_POS_LT_PAIR",SER_POS_LT_PAIR);
("SER_ADD",SER_ADD);
("SER_CMUL",SER_CMUL);
("SER_NEG",SER_NEG);
("SER_SUB",SER_SUB);
("SER_CDIV",SER_CDIV);
("SER_CAUCHY",SER_CAUCHY);
("SER_ZERO",SER_ZERO);
("SER_COMPAR",SER_COMPAR);
("SER_COMPARA",SER_COMPARA);
("SER_LE",SER_LE);
("SER_LE2",SER_LE2);
("SER_ACONV",SER_ACONV);
("SER_ABS",SER_ABS);
("GP_FINITE",GP_FINITE);
("GP",GP);
("ABS_NEG_LEMMA",ABS_NEG_LEMMA);
("SER_RATIO",SER_RATIO);
("SEQ_TRUNCATION",SEQ_TRUNCATION);
("tends_real_real",tends_real_real);
("LIM",LIM);
("LIM_CONST",LIM_CONST);
("LIM_ADD",LIM_ADD);
("LIM_MUL",LIM_MUL);
("LIM_NEG",LIM_NEG);
("LIM_INV",LIM_INV);
("LIM_SUB",LIM_SUB);
("LIM_DIV",LIM_DIV);
("LIM_NULL",LIM_NULL);
("LIM_SUM",LIM_SUM);
("LIM_X",LIM_X);
("LIM_UNIQ",LIM_UNIQ);
("LIM_EQUAL",LIM_EQUAL);
("LIM_TRANSFORM",LIM_TRANSFORM);
("diffl",diffl);
("contl",contl);
("differentiable",differentiable);
("DIFF_UNIQ",DIFF_UNIQ);
("DIFF_CONT",DIFF_CONT);
("CONTL_LIM",CONTL_LIM);
("CONT_X",CONT_X);
("CONT_CONST",CONT_CONST);
("CONT_ADD",CONT_ADD);
("CONT_MUL",CONT_MUL);
("CONT_NEG",CONT_NEG);
("CONT_INV",CONT_INV);
("CONT_SUB",CONT_SUB);
("CONT_DIV",CONT_DIV);
("CONT_ABS",CONT_ABS);
("CONT_COMPOSE",CONT_COMPOSE);
("IVT",IVT);
("IVT2",IVT2);
("DIFF_CONST",DIFF_CONST);
("DIFF_ADD",DIFF_ADD);
("DIFF_MUL",DIFF_MUL);
("DIFF_CMUL",DIFF_CMUL);
("DIFF_NEG",DIFF_NEG);
("DIFF_SUB",DIFF_SUB);
("DIFF_CARAT",DIFF_CARAT);
("DIFF_CHAIN",DIFF_CHAIN);
("DIFF_X",DIFF_X);
("DIFF_POW",DIFF_POW);
("DIFF_XM1",DIFF_XM1);
("DIFF_INV",DIFF_INV);
("DIFF_DIV",DIFF_DIV);
("DIFF_SUM",DIFF_SUM);
("CONT_BOUNDED",CONT_BOUNDED);
("CONT_BOUNDED_ABS",CONT_BOUNDED_ABS);
("CONT_HASSUP",CONT_HASSUP);
("CONT_ATTAINS",CONT_ATTAINS);
("CONT_ATTAINS2",CONT_ATTAINS2);
("CONT_ATTAINS_ALL",CONT_ATTAINS_ALL);
("DIFF_LINC",DIFF_LINC);
("DIFF_LDEC",DIFF_LDEC);
("DIFF_LMAX",DIFF_LMAX);
("DIFF_LMIN",DIFF_LMIN);
("DIFF_LCONST",DIFF_LCONST);
("INTERVAL_LEMMA_LT",INTERVAL_LEMMA_LT);
("INTERVAL_LEMMA",INTERVAL_LEMMA);
("ROLLE",ROLLE);
("MVT_LEMMA",MVT_LEMMA);
("MVT",MVT);
("MVT_ALT",MVT_ALT);
("DIFF_ISCONST_END",DIFF_ISCONST_END);
("DIFF_ISCONST",DIFF_ISCONST);
("DIFF_ISCONST_END_SIMPLE",DIFF_ISCONST_END_SIMPLE);
("DIFF_ISCONST_ALL",DIFF_ISCONST_ALL);
("INTERVAL_ABS",INTERVAL_ABS);
("CONT_INJ_LEMMA",CONT_INJ_LEMMA);
("CONT_INJ_LEMMA2",CONT_INJ_LEMMA2);
("CONT_INJ_RANGE",CONT_INJ_RANGE);
("CONT_INVERSE",CONT_INVERSE);
("DIFF_INVERSE",DIFF_INVERSE);
("DIFF_INVERSE_LT",DIFF_INVERSE_LT);
("IVT_DERIVATIVE_0",IVT_DERIVATIVE_0);
("IVT_DERIVATIVE_POS",IVT_DERIVATIVE_POS);
("IVT_DERIVATIVE_NEG",IVT_DERIVATIVE_NEG);
("SEQ_CONT_UNIFORM",SEQ_CONT_UNIFORM);
("SER_COMPARA_UNIFORM",SER_COMPARA_UNIFORM);
("SER_COMPARA_UNIFORM_WEAK",SER_COMPARA_UNIFORM_WEAK);
("CONTL",CONTL);
("CONTL_SEQ",CONTL_SEQ);
("SUP_INTERVAL",SUP_INTERVAL);
("CONT_UNIFORM",CONT_UNIFORM);
("CONT_UNIFORM_STRONG",CONT_UNIFORM_STRONG);
("POWDIFF_LEMMA",POWDIFF_LEMMA);
("POWDIFF",POWDIFF);
("POWREV",POWREV);
("POWSER_INSIDEA",POWSER_INSIDEA);
("POWSER_INSIDE",POWSER_INSIDE);
("diffs",diffs);
("DIFFS_NEG",DIFFS_NEG);
("DIFFS_LEMMA",DIFFS_LEMMA);
("DIFFS_LEMMA2",DIFFS_LEMMA2);
("DIFFS_EQUIV",DIFFS_EQUIV);
("TERMDIFF_LEMMA1",TERMDIFF_LEMMA1);
("TERMDIFF_LEMMA2",TERMDIFF_LEMMA2);
("TERMDIFF_LEMMA3",TERMDIFF_LEMMA3);
("TERMDIFF_LEMMA4",TERMDIFF_LEMMA4);
("TERMDIFF_LEMMA5",TERMDIFF_LEMMA5);
("TERMDIFF",TERMDIFF);
("SEQ_NPOW",SEQ_NPOW);
("TERMDIFF_CONVERGES",TERMDIFF_CONVERGES);
("TERMDIFF_STRONG",TERMDIFF_STRONG);
("POWSER_0",POWSER_0);
("POWSER_LIMIT_0",POWSER_LIMIT_0);
("POWSER_LIMIT_0_STRONG",POWSER_LIMIT_0_STRONG);
("POWSER_EQUAL_0",POWSER_EQUAL_0);
("POWSER_EQUAL",POWSER_EQUAL);
("MULT_DIV_2",MULT_DIV_2);
("EVEN_DIV2",EVEN_DIV2);
("POW_ZERO",POW_ZERO);
("POW_ZERO_EQ",POW_ZERO_EQ);
("POW_LT",POW_LT);
("POW_EQ",POW_EQ);
("exp",exp);
("sin",sin);
("cos",cos);
("REAL_EXP_CONVERGES",REAL_EXP_CONVERGES);
("SIN_CONVERGES",SIN_CONVERGES);
("COS_CONVERGES",COS_CONVERGES);
("REAL_EXP_FDIFF",REAL_EXP_FDIFF);
("SIN_FDIFF",SIN_FDIFF);
("COS_FDIFF",COS_FDIFF);
("SIN_NEGLEMMA",SIN_NEGLEMMA);
("DIFF_EXP",DIFF_EXP);
("DIFF_SIN",DIFF_SIN);
("DIFF_COS",DIFF_COS);
("DIFF_COMPOSITE",DIFF_COMPOSITE);
("REAL_EXP_0",REAL_EXP_0);
("REAL_EXP_LE_X",REAL_EXP_LE_X);
("REAL_EXP_LT_1",REAL_EXP_LT_1);
("REAL_EXP_ADD_MUL",REAL_EXP_ADD_MUL);
("REAL_EXP_NEG_MUL",REAL_EXP_NEG_MUL);
("REAL_EXP_NEG_MUL2",REAL_EXP_NEG_MUL2);
("REAL_EXP_NEG",REAL_EXP_NEG);
("REAL_EXP_ADD",REAL_EXP_ADD);
("REAL_EXP_POS_LE",REAL_EXP_POS_LE);
("REAL_EXP_NZ",REAL_EXP_NZ);
("REAL_EXP_POS_LT",REAL_EXP_POS_LT);
("REAL_EXP_N",REAL_EXP_N);
("REAL_EXP_SUB",REAL_EXP_SUB);
("REAL_EXP_MONO_IMP",REAL_EXP_MONO_IMP);
("REAL_EXP_MONO_LT",REAL_EXP_MONO_LT);
("REAL_EXP_MONO_LE",REAL_EXP_MONO_LE);
("REAL_EXP_INJ",REAL_EXP_INJ);
("REAL_EXP_TOTAL_LEMMA",REAL_EXP_TOTAL_LEMMA);
("REAL_EXP_TOTAL",REAL_EXP_TOTAL);
("REAL_EXP_BOUND_LEMMA",REAL_EXP_BOUND_LEMMA);
("ln",ln);
("LN_EXP",LN_EXP);
("REAL_EXP_LN",REAL_EXP_LN);
("EXP_LN",EXP_LN);
("LN_MUL",LN_MUL);
("LN_INJ",LN_INJ);
("LN_1",LN_1);
("LN_INV",LN_INV);
("LN_DIV",LN_DIV);
("LN_MONO_LT",LN_MONO_LT);
("LN_MONO_LE",LN_MONO_LE);
("LN_POW",LN_POW);
("LN_LE",LN_LE);
("LN_LT_X",LN_LT_X);
("LN_POS",LN_POS);
("LN_POS_LT",LN_POS_LT);
("DIFF_LN",DIFF_LN);
("root",root);
("sqrt_def",sqrt_def);
("sqrt",sqrt);
("ROOT_LT_LEMMA",ROOT_LT_LEMMA);
("ROOT_LN",ROOT_LN);
("ROOT_0",ROOT_0);
("ROOT_1",ROOT_1);
("ROOT_POW_POS",ROOT_POW_POS);
("POW_ROOT_POS",POW_ROOT_POS);
("ROOT_POS_POSITIVE",ROOT_POS_POSITIVE);
("ROOT_POS_UNIQ",ROOT_POS_UNIQ);
("ROOT_MUL",ROOT_MUL);
("ROOT_INV",ROOT_INV);
("ROOT_DIV",ROOT_DIV);
("ROOT_MONO_LT",ROOT_MONO_LT);
("ROOT_MONO_LE",ROOT_MONO_LE);
("ROOT_MONO_LT_EQ",ROOT_MONO_LT_EQ);
("ROOT_MONO_LE_EQ",ROOT_MONO_LE_EQ);
("ROOT_INJ",ROOT_INJ);
("SQRT_0",SQRT_0);
("SQRT_1",SQRT_1);
("SQRT_POS_LT",SQRT_POS_LT);
("SQRT_POS_LE",SQRT_POS_LE);
("SQRT_POW2",SQRT_POW2);
("SQRT_POW_2",SQRT_POW_2);
("POW_2_SQRT",POW_2_SQRT);
("SQRT_POS_UNIQ",SQRT_POS_UNIQ);
("SQRT_MUL",SQRT_MUL);
("SQRT_INV",SQRT_INV);
("SQRT_DIV",SQRT_DIV);
("SQRT_MONO_LT",SQRT_MONO_LT);
("SQRT_MONO_LE",SQRT_MONO_LE);
("SQRT_MONO_LT_EQ",SQRT_MONO_LT_EQ);
("SQRT_MONO_LE_EQ",SQRT_MONO_LE_EQ);
("SQRT_INJ",SQRT_INJ);
("SQRT_EVEN_POW2",SQRT_EVEN_POW2);
("REAL_DIV_SQRT",REAL_DIV_SQRT);
("POW_2_SQRT_ABS",POW_2_SQRT_ABS);
("SQRT_EQ_0",SQRT_EQ_0);
("REAL_LE_LSQRT",REAL_LE_LSQRT);
("REAL_LE_POW_2",REAL_LE_POW_2);
("REAL_LE_RSQRT",REAL_LE_RSQRT);
("DIFF_SQRT",DIFF_SQRT);
("SIN_0",SIN_0);
("COS_0",COS_0);
("SIN_CIRCLE",SIN_CIRCLE);
("SIN_BOUND",SIN_BOUND);
("SIN_BOUNDS",SIN_BOUNDS);
("COS_BOUND",COS_BOUND);
("COS_BOUNDS",COS_BOUNDS);
("SIN_COS_ADD",SIN_COS_ADD);
("SIN_COS_NEG",SIN_COS_NEG);
("SIN_ADD",SIN_ADD);
("COS_ADD",COS_ADD);
("SIN_NEG",SIN_NEG);
("COS_NEG",COS_NEG);
("SIN_DOUBLE",SIN_DOUBLE);
("COS_DOUBLE",COS_DOUBLE);
("COS_ABS",COS_ABS);
("SIN_PAIRED",SIN_PAIRED);
("SIN_POS",SIN_POS);
("COS_PAIRED",COS_PAIRED);
("COS_2",COS_2);
("COS_ISZERO",COS_ISZERO);
("pi",pi);
("PI2",PI2);
("COS_PI2",COS_PI2);
("PI2_BOUNDS",PI2_BOUNDS);
("PI_POS",PI_POS);
("SIN_PI2",SIN_PI2);
("COS_PI",COS_PI);
("SIN_PI",SIN_PI);
("SIN_COS",SIN_COS);
("COS_SIN",COS_SIN);
("SIN_PERIODIC_PI",SIN_PERIODIC_PI);
("COS_PERIODIC_PI",COS_PERIODIC_PI);
("SIN_PERIODIC",SIN_PERIODIC);
("COS_PERIODIC",COS_PERIODIC);
("COS_NPI",COS_NPI);
("SIN_NPI",SIN_NPI);
("SIN_POS_PI2",SIN_POS_PI2);
("COS_POS_PI2",COS_POS_PI2);
("COS_POS_PI",COS_POS_PI);
("SIN_POS_PI",SIN_POS_PI);
("SIN_POS_PI_LE",SIN_POS_PI_LE);
("COS_TOTAL",COS_TOTAL);
("SIN_TOTAL",SIN_TOTAL);
("COS_ZERO_LEMMA",COS_ZERO_LEMMA);
("SIN_ZERO_LEMMA",SIN_ZERO_LEMMA);
("COS_ZERO",COS_ZERO);
("SIN_ZERO",SIN_ZERO);
("SIN_ZERO_PI",SIN_ZERO_PI);
("COS_ONE_2PI",COS_ONE_2PI);
("tan",tan);
("TAN_0",TAN_0);
("TAN_PI",TAN_PI);
("TAN_NPI",TAN_NPI);
("TAN_NEG",TAN_NEG);
("TAN_PERIODIC",TAN_PERIODIC);
("TAN_PERIODIC_PI",TAN_PERIODIC_PI);
("TAN_PERIODIC_NPI",TAN_PERIODIC_NPI);
("TAN_ADD",TAN_ADD);
("TAN_DOUBLE",TAN_DOUBLE);
("TAN_POS_PI2",TAN_POS_PI2);
("DIFF_TAN",DIFF_TAN);
("TAN_TOTAL_LEMMA",TAN_TOTAL_LEMMA);
("TAN_TOTAL_POS",TAN_TOTAL_POS);
("TAN_TOTAL",TAN_TOTAL);
("PI2_PI4",PI2_PI4);
("TAN_PI4",TAN_PI4);
("TAN_COT",TAN_COT);
("TAN_BOUND_PI2",TAN_BOUND_PI2);
("TAN_ABS_GE_X",TAN_ABS_GE_X);
("asn",asn);
("acs",acs);
("atn",atn);
("ASN",ASN);
("ASN_SIN",ASN_SIN);
("ASN_BOUNDS",ASN_BOUNDS);
("ASN_BOUNDS_LT",ASN_BOUNDS_LT);
("SIN_ASN",SIN_ASN);
("ACS",ACS);
("ACS_COS",ACS_COS);
("ACS_BOUNDS",ACS_BOUNDS);
("ACS_BOUNDS_LT",ACS_BOUNDS_LT);
("COS_ACS",COS_ACS);
("ATN",ATN);
("ATN_TAN",ATN_TAN);
("ATN_BOUNDS",ATN_BOUNDS);
("TAN_ATN",TAN_ATN);
("ATN_0",ATN_0);
("ATN_1",ATN_1);
("ATN_NEG",ATN_NEG);
("COS_ATN_NZ",COS_ATN_NZ);
("TAN_SEC",TAN_SEC);
("DIFF_ATN",DIFF_ATN);
("ATN_MONO_LT",ATN_MONO_LT);
("ATN_MONO_LT_EQ",ATN_MONO_LT_EQ);
("ATN_MONO_LE_EQ",ATN_MONO_LE_EQ);
("ATN_INJ",ATN_INJ);
("ATN_POS_LT",ATN_POS_LT);
("ATN_POS_LE",ATN_POS_LE);
("ATN_LT_PI4_POS",ATN_LT_PI4_POS);
("ATN_LT_PI4_NEG",ATN_LT_PI4_NEG);
("ATN_LT_PI4",ATN_LT_PI4);
("ATN_LE_PI4",ATN_LE_PI4);
("COS_SIN_SQRT",COS_SIN_SQRT);
("COS_ASN_NZ",COS_ASN_NZ);
("DIFF_ASN_COS",DIFF_ASN_COS);
("DIFF_ASN",DIFF_ASN);
("SIN_COS_SQRT",SIN_COS_SQRT);
("SIN_ACS_NZ",SIN_ACS_NZ);
("DIFF_ACS_SIN",DIFF_ACS_SIN);
("DIFF_ACS",DIFF_ACS);
("CIRCLE_SINCOS",CIRCLE_SINCOS);
("ACS_MONO_LT",ACS_MONO_LT);
("LESS_SUC_EQ",LESS_SUC_EQ);
("LESS_1",LESS_1);
("division",division);
("dsize",dsize);
("tdiv",tdiv);
("gauge",gauge);
("fine",fine);
("rsum",rsum);
("defint",defint);
("DIVISION_0",DIVISION_0);
("DIVISION_1",DIVISION_1);
("DIVISION_SINGLE",DIVISION_SINGLE);
("DIVISION_LHS",DIVISION_LHS);
("DIVISION_THM",DIVISION_THM);
("DIVISION_RHS",DIVISION_RHS);
("DIVISION_LT_GEN",DIVISION_LT_GEN);
("DIVISION_LT",DIVISION_LT);
("DIVISION_LE",DIVISION_LE);
("DIVISION_GT",DIVISION_GT);
("DIVISION_EQ",DIVISION_EQ);
("DIVISION_LBOUND",DIVISION_LBOUND);
("DIVISION_LBOUND_LT",DIVISION_LBOUND_LT);
("DIVISION_UBOUND",DIVISION_UBOUND);
("DIVISION_UBOUND_LT",DIVISION_UBOUND_LT);
("DIVISION_APPEND_LEMMA1",DIVISION_APPEND_LEMMA1);
("DIVISION_APPEND_LEMMA2",DIVISION_APPEND_LEMMA2);
("DIVISION_APPEND_EXPLICIT",DIVISION_APPEND_EXPLICIT);
("DIVISION_APPEND_STRONG",DIVISION_APPEND_STRONG);
("DIVISION_APPEND",DIVISION_APPEND);
("DIVISION_EXISTS",DIVISION_EXISTS);
("GAUGE_MIN",GAUGE_MIN);
("FINE_MIN",FINE_MIN);
("DINT_UNIQ",DINT_UNIQ);
("INTEGRAL_NULL",INTEGRAL_NULL);
("STRADDLE_LEMMA",STRADDLE_LEMMA);
("FTC1",FTC1);
("integrable",integrable);
("integral",integral);
("INTEGRABLE_DEFINT",INTEGRABLE_DEFINT);
("DIVISION_BOUNDS",DIVISION_BOUNDS);
("TDIV_BOUNDS",TDIV_BOUNDS);
("TDIV_LE",TDIV_LE);
("DEFINT_WRONG",DEFINT_WRONG);
("DEFINT_INTEGRAL",DEFINT_INTEGRAL);
("DEFINT_CONST",DEFINT_CONST);
("DEFINT_0",DEFINT_0);
("DEFINT_NEG",DEFINT_NEG);
("DEFINT_CMUL",DEFINT_CMUL);
("DEFINT_ADD",DEFINT_ADD);
("DEFINT_SUB",DEFINT_SUB);
("INTEGRAL_LE",INTEGRAL_LE);
("DEFINT_LE",DEFINT_LE);
("DEFINT_TRIANGLE",DEFINT_TRIANGLE);
("DEFINT_EQ",DEFINT_EQ);
("INTEGRAL_EQ",INTEGRAL_EQ);
("INTEGRATION_BY_PARTS",INTEGRATION_BY_PARTS);
("DIVISION_LE_SUC",DIVISION_LE_SUC);
("DIVISION_MONO_LE",DIVISION_MONO_LE);
("DIVISION_MONO_LE_SUC",DIVISION_MONO_LE_SUC);
("DIVISION_INTERMEDIATE",DIVISION_INTERMEDIATE);
("DIVISION_DSIZE_LE",DIVISION_DSIZE_LE);
("DIVISION_DSIZE_GE",DIVISION_DSIZE_GE);
("DIVISION_DSIZE_EQ",DIVISION_DSIZE_EQ);
("DIVISION_DSIZE_EQ_ALT",DIVISION_DSIZE_EQ_ALT);
("DEFINT_COMBINE",DEFINT_COMBINE);
("DEFINT_DELTA_LEFT",DEFINT_DELTA_LEFT);
("DEFINT_DELTA_RIGHT",DEFINT_DELTA_RIGHT);
("DEFINT_DELTA",DEFINT_DELTA);
("DEFINT_POINT_SPIKE",DEFINT_POINT_SPIKE);
("DEFINT_FINITE_SPIKE",DEFINT_FINITE_SPIKE);
("GAUGE_MIN_FINITE",GAUGE_MIN_FINITE);
("INTEGRABLE_CAUCHY",INTEGRABLE_CAUCHY);
("SUM_DIFFS",SUM_DIFFS);
("RSUM_BOUND",RSUM_BOUND);
("RSUM_DIFF_BOUND",RSUM_DIFF_BOUND);
("INTEGRABLE_LIMIT",INTEGRABLE_LIMIT);
("INTEGRABLE_CONST",INTEGRABLE_CONST);
("INTEGRABLE_COMBINE",INTEGRABLE_COMBINE);
("INTEGRABLE_POINT_SPIKE",INTEGRABLE_POINT_SPIKE);
("INTEGRABLE_CONTINUOUS",INTEGRABLE_CONTINUOUS);
("INTEGRABLE_SPLIT_SIDES",INTEGRABLE_SPLIT_SIDES);
("INTEGRABLE_SUBINTERVAL_LEFT",INTEGRABLE_SUBINTERVAL_LEFT);
("INTEGRABLE_SUBINTERVAL_RIGHT",INTEGRABLE_SUBINTERVAL_RIGHT);
("INTEGRABLE_SUBINTERVAL",INTEGRABLE_SUBINTERVAL);
("INTEGRAL_CONST",INTEGRAL_CONST);
("INTEGRAL_CMUL",INTEGRAL_CMUL);
("INTEGRAL_ADD",INTEGRAL_ADD);
("INTEGRAL_SUB",INTEGRAL_SUB);
("INTEGRAL_BY_PARTS",INTEGRAL_BY_PARTS);
("MCLAURIN",MCLAURIN);
("MCLAURIN_NEG",MCLAURIN_NEG);
("MCLAURIN_BI_LE",MCLAURIN_BI_LE);
("MCLAURIN_ALL_LT",MCLAURIN_ALL_LT);
("MCLAURIN_ZERO",MCLAURIN_ZERO);
("MCLAURIN_ALL_LE",MCLAURIN_ALL_LE);
("MCLAURIN_EXP_LEMMA",MCLAURIN_EXP_LEMMA);
("MCLAURIN_EXP_LT",MCLAURIN_EXP_LT);
("MCLAURIN_EXP_LE",MCLAURIN_EXP_LE);
("MCLAURIN_LN_POS",MCLAURIN_LN_POS);
("MCLAURIN_LN_NEG",MCLAURIN_LN_NEG);
("MCLAURIN_SIN",MCLAURIN_SIN);
("MCLAURIN_COS",MCLAURIN_COS);
("REAL_ATN_POWSER_SUMMABLE",REAL_ATN_POWSER_SUMMABLE);
("REAL_ATN_POWSER_DIFFS_SUMMABLE",REAL_ATN_POWSER_DIFFS_SUMMABLE);
("REAL_ATN_POWSER_DIFFS_SUM",REAL_ATN_POWSER_DIFFS_SUM);
("REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE",REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE);
("REAL_ATN_POWSER_DIFFL",REAL_ATN_POWSER_DIFFL);
("REAL_ATN_POWSER",REAL_ATN_POWSER);
("MCLAURIN_ATN",MCLAURIN_ATN);
("max_real",max_real);
("min_real",min_real);
("min_num",min_num);
("deriv",deriv);
("deriv2",deriv2);
("atn2",atn2);
("sqrt8",sqrt8);
("sqrt2",sqrt2);
("t0",t0);
("two_t0",two_t0);
("square_2t0",square_2t0);
("square_4t0",square_4t0);
("pt",pt);
("square",square);
("zeta",zeta);
("doct",doct);
("dtet",dtet);
("pi_rt18",pi_rt18);
("rogers",rogers);
("compression_cut",compression_cut);
("squander_target",squander_target);
("xiV",xiV);
("xi_gamma",xi_gamma);
("xi'_gamma",xi'_gamma);
("xi_kappa",xi_kappa);
("xi_kappa_gamma",xi_kappa_gamma);
("pi_max",pi_max);
("t4",t4);
("t5",t5);
("t6",t6);
("t7",t7);
("t8",t8);
("t9",t9);
("t10",t10);
("s5",s5);
("s6",s6);
("s7",s7);
("s8",s8);
("s9",s9);
("s10",s10);
("eps0",eps0);
("Z31",Z31);
("Z32",Z32);
("Z33",Z33);
("Z41",Z41);
("Z42",Z42);
("D31",D31);
("D32",D32);
("D33",D33);
("D41",D41);
("D42",D42);
("D51",D51);
("pp_a1",pp_a1);
("pp_a2",pp_a2);
("pp_d0",pp_d0);
("pp_m",pp_m);
("pp_b",pp_b);
("pp_a",pp_a);
("pp_bc",pp_bc);
("pp_c",pp_c);
("pp_d",pp_d);
("pp_solt0",pp_solt0);
("delta_x",delta_x);
("delta_x4",delta_x4);
("delta_x6",delta_x6);
("ups_x",ups_x);
("eta_x",eta_x);
("eta_y",eta_y);
("rho_x",rho_x);
("rad2_y",rad2_y);
("chi_x",chi_x);
("dih_x",dih_x);
("dih_y",dih_y);
("dih2_y",dih2_y);
("dih3_y",dih3_y);
("dih2_x",dih2_x);
("dih3_x",dih3_x);
("sol_x",sol_x);
("sol_y",sol_y);
("vol_x",vol_x);
("beta",beta);
("arclength",arclength);
("volR",volR);
("solR",solR);
("dihR",dihR);
("vorR",vorR);
("denR",denR);
("tauR",tauR);
("quoin",quoin);
("qy",qy);
("quo_x",quo_x);
("qn",qn);
("phi",phi);
("phi0",phi0);
("eta0",eta0);
("crown",crown);
("anc",anc);
("K0",K0);
("AH",AH);
("BHY",BHY);
("KY",KY);
("KX",KX);
("vor_analytic_x",vor_analytic_x);
("vor_analytic_x_flipped",vor_analytic_x_flipped);
("octavor_analytic_x",octavor_analytic_x);
("tau_analytic_x",tau_analytic_x);
("kappa",kappa);
("kappa_dih_y",kappa_dih_y);
("level_at",level_at);
("vorstar",vorstar);
("vort_y",vort_y);
("vor_0_y",vor_0_y);
("tau_0_y",tau_0_y);
("vor_0_x",vor_0_x);
("tau_0_x",tau_0_x);
("vort_x",vort_x);
("tauVt_x",tauVt_x);
("vorA_x",vorA_x);
("tauA_x",tauA_x);
("vorC0_x",vorC0_x);
("tauC0_x",tauC0_x);
("vorC_x",vorC_x);
("tauC_x",tauC_x);
("v0x",v0x);
("v1x",v1x);
("gamma_x",gamma_x);
("tau_gamma_x",tau_gamma_x);
("rad2_x",rad2_x);
("sigma_qrtet_x",sigma_qrtet_x);
("sigma1_qrtet_x",sigma1_qrtet_x);
("tau_sigma_x",tau_sigma_x);
("sigma32_qrtet_x",sigma32_qrtet_x);
("mu_flat_x",mu_flat_x);
("taumu_flat_x",taumu_flat_x);
("mu_upright_x",mu_upright_x);
("mu_flipped_x",mu_flipped_x);
("vor_0_x_flipped",vor_0_x_flipped);
("octavor0_x",octavor0_x);
("nu_x",nu_x);
("nu_gamma_x",nu_gamma_x);
("taunu_x",taunu_x);
("octa_x",octa_x);
("sigmahat_x",sigmahat_x);
("sigmahat_x'",sigmahat_x');
("sigmahatpi_x",sigmahatpi_x);
("tauhat_x",tauhat_x);
("tauhatpi_x",tauhatpi_x);
("pi_prime_tau",pi_prime_tau);
("pi_prime_sigma",pi_prime_sigma);
("findpoint",findpoint);
("enclosed",enclosed);
("cross_diag",cross_diag);
("cross_diag_x",cross_diag_x);
("affine",affine);
("convex",convex);
("aff",aff);
("conv",conv);
("conv0",conv0);
("cone",cone);
("cone0",cone0);
("voronoi",voronoi);
("line",line);
("collinear",collinear);
("plane",plane);
("closed_half_plane",closed_half_plane);
("open_half_plane",open_half_plane);
("coplanar",coplanar);
("closed_half_space",closed_half_space);
("open_half_space",open_half_space);
("arcV",arcV);
("cross",cross);
("dihV",dihV);
("ylist",ylist);
("xlist",xlist);
("euler_p",euler_p);
("radius",radius);
("polar_angle",polar_angle);
("polar_c",polar_c);
("less_polar",less_polar);
("min_polar",min_polar);
("polar_cycle",polar_cycle);
("iter_spec",iter_spec);
("iter",iter);
("orthonormal",orthonormal);
("cyclic_set",cyclic_set);
("azim_cycle_hyp_def",azim_cycle_hyp_def);
("azim_cycle_spec",azim_cycle_spec);
("azim_cycle_def",azim_cycle_def);
("ineq",ineq)


(* ==================== *)
(* ==== QUANG TRUONG ======= *)
(* ====== if you load geomdetail, you should load the following things
, so that you can find thm in geomdetail.ml 


("VC_DISJOINT", VC_DISJOINT );
("trg_sub_bo", trg_sub_bo);
("trg_sub_se", trg_sub_se);

("not_in_set3", not_in_set3);

("trg_d3_sym", trg_d3_sym);

("affine_hull_e", affine_hull_e);

("wlog", wlog );

("wlog_real", wlog_real);

("dkdx", dkdx);

("tarski_arith", tarski_arith);

("simp_def", simp_def);

("AFFINE_HULL_SINGLE", AFFINE_HULL_SINGLE);

("usefull", usefull );

("near", near);

("near2t0", near2t0);

("e_plane", e_plane);

("bis", bis);

("min_dist", min_dist);

("exists_min_dist", exists_min_dist);











("centered_pac", centered_pac);

("Q_SYS", Q_SYS);









("a_le_sub", a_le_sub);

("strict_qua_in_oct", strict_qua_in_oct);

("set_3elements", set_3elements);




("without_lost", without_lost );

("condi_of_wlofg", condi_of_wlofg);

("SET_OF_4", SET_OF_4);

("def_simplex", def_simplex);

("strict_qua2_interior_pos", strict_qua2_interior_pos);

("simplex_interior_pos", simplex_interior_pos);






("WHEN_IN_QSYS", WHEN_IN_Q_SYS);








("strict_qua2_imply_strict_qua", strict_qua2_imply_strict_qua);


("CASES_OF_Q_SYS", CASES_OF_Q_SYS);

("RELATE_Q_SYS", RELATE_Q_SYS);

("tarski_FFSXOWD", tarski_FFSXOWD);





("barrier'", barrier');
 
("lemma7_7_CXRHOVG", lemma7_7_CXRHOVG);

("tarski_UMMNOJN", tarski_UMMNOJN);

("CARD_SING", CARD_SING);

("FINITE6", FINITE6);

("CARD_SET2", CARD_SET2);

("CARD_EQUATION ", CARD_EQUATION);

(" CARD5", CARD5 );

(" CARD_DISJOINT", CARD_DISJOINT);

("QUA_TET_IMPLY_QUA_TRI", QUA_TET_IMPLY_QUA_TRI);

("PAIR_D3", PAIR_D3);

("PAIR_DIST", PAIR_DIST);

("TRIANGLE_IN_STRICT_QUA", TRIANGLE_IN_STRICT_QUA);

("TRIANGLE_IN_BARRIER", TRIANGLE_IN_BARRIER);

("DIA_OF_QUARTER", DIA_OF_QUARTER);

("SUB_PACKING", SUB_PACKING);

("D3_REFL", D3_REFL);

("db_t0_sq8", db_t0_sq8);

("db_t0", db_t0);

("TRIANGLE_IN_BARRIER'", TRIANGLE_IN_BARRIER');



("IN_AFF_GE_CON", IN_AFF_GE_CON );

("OCT23", OCT23);


(* ---------------
("OTHER_LEMMA", OTHER_LEMMA );

("quasi_reg_tet_case", quasi_reg_tet_case );

("in_VC", in_VC);

("MEETING_CONDITION", MEETING_CONDITION); 

("quasi_tri_case", quasi_tri_case);

("OCTOR23", OCTOR23);

("OCTO23", OCTO23);

("OCT24", OCT24);

("hard_case", hard_case );

("v_near2t0_v", v_near2t0_v);

("lemma_of_lemma82", lemma_of_lemma82);

("le1_82", le1_82);

("rhand_subset_lhand", rhand_subset_lhand);

("import_le", import_le);

("v1_in_convex3", v1_in_convex3);

("v1v2v3_in_convex3", v1v2v3_in_convex3);

("minconvex3", minconvex3);

("convex3_in_inters", convex3_in_inters) 
----------------- *)



("DIAGONAL_QUA", DIAGONAL_QUA);

("DIAGONAL_STRICT_QUA", DIAGONAL_STRICT_QUA);

("DIAGONAL_BARRIER", DIAGONAL_BARRIER);

("simp_def", simp_def);

("def_obstructed", def_obstructed );

("CARD_CLAUSES_IMP", CARD_CLAUSES_IMP);

("CARD2", CARD2);

("CARD3", CARD3);

(" CARD4", CARD4);

("PAIR_EQ_EXPAND", PAIR_EQ_EXPAND);

("IN_SET3", IN_SET3);

("IN_SET4", IN_SET4);

("SHORT_EDGES", SHORT_EDGES);

("CONV_EM", CONV_EM);

("CONV_SING", CONV_SING);

("IN_ACT_SING", IN_ACT_SING);

("IN_SET2", IN_SET2);

("VSUM_DIS2", VSUM_DIS2);

("SUM_DIS2", SUM_DIS2);

("CONV_SET2", CONV_SET2);

("CEWWWDQ", CEWWWDQ);

("QHSEWMI", QHSEWMI );

("TCQPONA", TCQPONA );

("CONV3_A_EQ", CONV3_A_EQ);

("VSUM_DIS3", VSUM_DIS3);

("SUM_DIS3", SUM_DIS3);

("EQ_EXPAND", EQ_EXPAND);

("CONV_SET3", CONV_SET3);
("SET3_SUBSET", SET3_SUBSET);




("convex3", convex3);
("INTERS_SUBSET", INTERS_SUBSET);

("SUM_TWO_RATIO ", SUM_TWO_RATIO);

("OTHER_CONVEX_CONDI ", OTHER_CONVEX_CONDI );

("CONV_BAR_EQ", CONV_BAR_EQ);

("CONV3_EQ", CONV3_EQ);

("DOT_SUB_ADD", DOT_SUB_ADD);

("DIST_LT_HALF_PLANE", DIST_LT_HALF_PLANE);

("OR_IMP_EX", OR_IMP_EX);

("HALF_PLANE_CONV", HALF_PLANE_CONV);

("HALF_PLANE_CONV_EP", HALF_PLANE_CONV_EP );
("VORONOI_CONV ", VORONOI_CONV );

("CONVEX_IM_CONV2_SU", CONVEX_IM_CONV2_SU );

("CONVEX_AS_CONV2", CONVEX_AS_CONV2 );

("CONV0_SING", CONV0_SING);

("CONV0_SET2", CONV0_SET2);

("CONV02_SU_CONV2", CONV02_SU_CONV2);

("CONVEX_IM_CONV02_SU ", CONVEX_IM_CONV02_SU );

("BAR_TRI", BAR_TRI);

("X_IN_VOR_X", X_IN_VOR_X);

("IN_VO2_EQ", IN_VO2_EQ);

("IN_VO_EQ", IN_VO_EQ);

("IN_BAR_DISTINCT", IN_BAR_DISTINCT);

("FOUR_POINTS", FOUR_POINTS);

("IN_Q_SYS_IMP4", IN_Q_SYS_IMP4 );

("D3_SYM", D3_SYM);

("SET2_SU_EX", SET2_SU_EX);

("QUARTER_EQ_EX_DIA", QUARTER_EQ_EX_DIA );

("IN_Q_IMP", IN_Q_IMP);

("EXISTS_DIA", EXISTS_DIA);

("COND_Q_SYS", COND_Q_SYS);

("SET4_SUB_EX", SET4_SUB_EX);

("IMP_QUA_RE_TE", IMP_QUA_RE_TE);

("SET3_U_SET1", SET3_U_SET1);

("IN_BA_IM_PA_SU ", IN_BA_IM_PA_SU );

("QUA_TRI_EDGE", QUA_TRI_EDGE);

("BAR_WI_LONG_ED", BAR_WI_LONG_ED)


========== *)

];;

theorems := !theorems @ !thm_region_array;;