Update from HH

[Flyspeck/.git] / legacy / general / database_more.ml

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