(* 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;;