HOL html

Files Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _
Theorems Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _

D (theorems)

D1
D2
D3_REFL
DART1_NOT_COLLINEAR
DART1_NOT_COLLINEAR_2
DART1_OF_FAN_EQ_DISJOINT_UNIONS
DART1_OF_FAN_SUBSET_DART_OF_FAN
DART3_LIST_ALL
DART4_LIST_ALL
DARTSET_FULLY_SURROUNDED_IS_NON_ISOLATED_FAN2
DARTSET_LEADS_INTO_FAN
DARTSET_LEADS_INTO_SUBSET_WDART_FAN
DARTS_E_PRIME_EQ_FF_UNION_SWITCH
DARTS_E_PRIME_GT1_SWITCH
DARTX_LIST_ALL
DART_EQ_UNIONS
DART_EQ_UNIONS_FACE_SET_NODE_SET_EDGE_SET
DART_EXISTS
DART_EXISTS_EQ
DART_FANADD_EQ_DART_FAN_ADD_2DART
DART_FANADD_EQ_HALFSPACE
DART_FANADD_SUBSET_HALFSPACE
DART_FANADD_SUBSET_HALFSPACE1
DART_FANADD_SUBSET_HALFSPACE2
DART_FANADD_SUBSET_HALFSPACE3
DART_FANADD_SUBSET_HALFSPACE4
DART_FAN_SY
DART_FAN_SY1
DART_IN_DARTS
DART_IN_FACE
DART_IN_FIND_PAIR_LIST
DART_IN_UNIQUE_EDGE
DART_IN_UNIQUE_FACE
DART_IN_UNIQUE_NODE
DART_LEADS_INTO
DART_LIST_ALL
DART_OF_FAN_SYM
DART_OF_HYP_EQ_FACE_SY
DART_OF_HYP_SY_EQ
DART_OF_HYP_SY_EQ1
DART_OF_HYP_VV
DART_SUM_lemma
DDZUPHJ
DECIMAL_EQ
DECIMAL_INT
DECREASING_CLOSED_NEST_FAN
DECREASING_CLOSED_NEST_SING_FAN
DEFORMATION_AZIM_V3_DEFOR_NOT_MK
DEFORMATION_AZIM_V3_DEFOR_NOT_MK_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_SUB_MK
DEFORMATION_AZIM_V3_DEFOR_SUB_MK_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_SUC_MK
DEFORMATION_AZIM_V3_DEFOR_SUC_MK_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_ALL
DEFORMATION_AZIM_V3_DEFOR_V1_AT_ALL_MK
DEFORMATION_AZIM_V3_DEFOR_V1_AT_ALL_MK_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_AT_ALL_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_ALL_V1_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V1_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V1_V1_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V_ANY
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V_ANY_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_V_ANY_V1_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_AT_W
DEFORMATION_AZIM_V3_DEFOR_V1_AT_W_V1
DEFORMATION_AZIM_V3_DEFOR_V1_AT_W_V1_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_MK
DEFORMATION_AZIM_V3_DEFOR_V1_MK_TWO_CASES
DEFORMATION_AZIM_V3_DEFOR_V1_V1
DEFORMATION_AZIM_V3_DEFOR_V1_V1_TWO_CASES
DEFORMATION_BB_WW_DEFOR_LE3
DEFORMATION_DIST_LE_2
DEFORMATION_DIST_LE_2_TWO_CASES
DEFORMATION_DIST_LE_A
DEFORMATION_DIST_LE_ALL
DEFORMATION_DIST_LE_ALL_COM
DEFORMATION_DIST_LE_ALL_COM_LE3
DEFORMATION_DIST_LE_ALL_LE3
DEFORMATION_DIST_LE_B
DEFORMATION_DIST_LE_BLL
DEFORMATION_DIST_LE_BLL_COM
DEFORMATION_DIST_LE_BLL_COM_LE3
DEFORMATION_DIST_LE_BLL_EDGE
DEFORMATION_DIST_LE_BLL_EDGE2
DEFORMATION_DIST_LE_BLL_EDGE2_LE3
DEFORMATION_DIST_LE_BLL_EDGE_LE3
DEFORMATION_DIST_LE_BLL_LE3
DEFORMATION_DIST_LE_BLL_PRIME
DEFORMATION_DIST_LE_BLL_PRIME_LE3
DEFORMATION_DIST_LE_BLL_V3_DEFOR_COM
DEFORMATION_DIST_LE_BLL_V3_DEFOR_COM_TWO_CASES
DEFORMATION_DIST_LE_MK_A
DEFORMATION_DIST_LE_MK_A_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A
DEFORMATION_DIST_LE_V3_DEFOR_AA_COM_MK
DEFORMATION_DIST_LE_V3_DEFOR_AA_COM_MK_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_COM
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_MK
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_MK1
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_MK1_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_MK_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_SUC
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_SUC_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_COM_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_SUC
DEFORMATION_DIST_LE_V3_DEFOR_A_SUC_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_A_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_B_COM_MK
DEFORMATION_DIST_LE_V3_DEFOR_B_COM_MK1
DEFORMATION_DIST_LE_V3_DEFOR_B_COM_MK1_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_B_COM_MK_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_B_MK
DEFORMATION_DIST_LE_V3_DEFOR_B_MK_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_B_SUC
DEFORMATION_DIST_LE_V3_DEFOR_B_SUC_TWO_CASES
DEFORMATION_DIST_LE_V3_DEFOR_EDGE_SUB
DEFORMATION_DIST_LE_V3_DEFOR_EDGE_SUB_TWO_CASES
DEFORMATION_INTERIOR_ANGLE1_EQ_V3_DEFOR_V1
DEFORMATION_INTERIOR_ANGLE1_EQ_V3_DEFOR_V1_TWO_CASES
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1_AT_ALL_MK
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1_AT_ALL_MK_TWO_CASES
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1_LE_PI_AT_ALL_MK
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1_LE_PI_AT_ALL_MK_TWO_CASES
DEFORMATION_INTERIOR_ANGLE1_V3_DEFOR_V1_TWO_CASES
DEFORMATION_IN_BALL_ANNULUS
DEFORMATION_LUNAR_AFFINE_HULL
DEFORMATION_LUNAR_AFFINE_HULL_MK
DEFORMATION_LUNAR_AFFINE_HULL_MK_TWO_CASES
DEFORMATION_LUNAR_AFFINE_HULL_V1
DEFORMATION_LUNAR_AFFINE_HULL_V1_TWO_CASES
DEFORMATION_MK_DEFOR_IN_BALL_ANNULUS
DEFORMATION_SMALL_INTERVAL
DEFORMATION_V3_DEFOR_EDGE
DEFORMATION_V3_DEFOR_EDGE_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V
DEFORMATION_V3_DEFOR_NOT_IN_V_COM
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_EQ
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_EQ_MK
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_EQ_MK_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_EQ_V1
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_EQ_V1_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_MK
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_MK_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_V1
DEFORMATION_V3_DEFOR_NOT_IN_V_COM_V1_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V_MK
DEFORMATION_V3_DEFOR_NOT_IN_V_MK_TWO_CASES
DEFORMATION_V3_DEFOR_NOT_IN_V_V1
DEFORMATION_V3_DEFOR_NOT_IN_V_V1_TWO_CASES
DELTA_COEFS
DELTA_EQ_DELTA_X
DELTA_POS_4POINTS
DELTA_RRR_INTERPRETE
DELTA_TRIPLE_SUB_H_EXPAND
DELTA_X14_RRR
DELTA_X1I_RRR
DELTA_X34
DELTA_X34_B
DELTA_X4_MONO_LE_4
DELTA_X4_MONO_LT_4
DELTA_X_AND_DELTA_X4
DELTA_X_DET_3
DELTA_X_LT_0_COLLINEAR
DELTA_Y_POS_4POINTS
DEPENDENT_BIGGERSET
DEPENDENT_BIGGERSET_GENERAL
DEPENDENT_EXPLICIT
DEPENDENT_FINITE
DEPENDENT_LINEAR_IMAGE
DEPENDENT_LINEAR_IMAGE_EQ
DEPENDENT_MONO
DERIVATIVE_WRT_A_Euler_lemma
DERIVATIVE_WRT_C1_Euler_lemma
DETERMINE_FV
DETERMINE_FV2
DETERMINE_WEDGE_IN_FAN
DETER_RHO_NODE
DET_0
DET_1
DET_2
DET_3
DET_COFACTOR_EXPANSION
DET_CROSS
DET_DEPENDENT_COLUMNS
DET_DEPENDENT_ROWS
DET_DIAGONAL
DET_EQ_0
DET_EQ_0_RANK
DET_I
DET_IDENTICAL_COLUMNS
DET_IDENTICAL_ROWS
DET_LINEAR_ROWS_VSUM
DET_LINEAR_ROWS_VSUM_LEMMA
DET_LINEAR_ROW_VSUM
DET_LOWERTRIANGULAR
DET_MATRIX_EQ_0
DET_MATRIX_EQ_0_LEFT
DET_MATRIX_EQ_0_RIGHT
DET_MUL
DET_ORTHOGONAL_MATRIX
DET_PERMUTE_COLUMNS
DET_PERMUTE_ROWS
DET_ROWS_MUL
DET_ROW_ADD
DET_ROW_MUL
DET_ROW_OPERATION
DET_ROW_SPAN
DET_TRANSP
DET_UPPERTRIANGULAR
DET_VEC3_AND_DELTA
DET_VEC3_AS_CROSS_DOT
DET_VEC3_EXPAND
DET_VECC3_AND_DELTA
DET_ZERO_COLUMN
DET_ZERO_ROW
DHVFGBC
DIAD_PSORT_IMP_DIAD
DIAGE_VAL_P_Q
DIAGONAL_BARRIER
DIAGONAL_QUA
DIAGONAL_STRICT_QUA
DIAGONAL_SY
DIAG_5_EQU_PSORT
DIAG_EQ_ADD
DIAG_EQ_ADD5
DIAG_IS_NOT_EAR
DIAG_MOD
DIAG_NOT_IN_EDGES
DIAG_NOT_IN_SCS_J
DIAG_NOT_PSORT
DIAG_OPP
DIAG_PSORT
DIAG_PSORT1
DIAG_PSORT2
DIAG_SCS_M_EQ
DIAMETER_BOUNDED_BOUND_FAN
DIAMETER_BOUNDED_FAN
DIAMETER_COMPACT_ATTAINED_FAN
DIA_OF_QUARTER
DIA_SY
DIFF2_DOMAIN_IMP_CONTINUOUS_ON
DIFFERENCE_IMP_LT_CARDV
DIFF_DIFF2
DIFF_EDGEX
DIFF_INTER
DIFF_LEMMA
DIH2K_FACE_SIMPLIZED
DIH2K_FAN_HYP_SY
DIH2K_HYP_ISO_LEMMA
DIH2K_IMP_NODE_MAP_X_DIFF_X
DIH2K_IMP_PRE_SIMPLE_HYP
DIH2K_IMP_SIMPLE_HYPERMAP
DIH2K_IMP_SIMPLE_HYPERMAP2
DIHV_ARCV
DIHV_DIH_X
DIHV_EQ_0_PI_EQ_COPLANAR_ALT
DIHV_EQ_DIH_Y
DIHV_FORMULAR
DIHV_GT_PI2
DIHV_LE_0
DIHV_LE_AZIM
DIHV_NOT_CHANGE
DIHV_RESCALE_UNCHANGED
DIHV_SPECIAL_SCALE1
DIHV_SPECIAL_SCALE2
DIHV_SYM
DIHV_SYM_2
DIHV_SYM_3
DIHV_TRASABLE
DIHX_DIH_Y_lemma
DIHX_LE_PI
DIHX_POS
DIHX_RANGE
DIHX_SYM
DIH_IMP_EULER_A_POS
DIH_IMP_EVERY_NODE_INTER_FACE
DIH_K_HYP_E_PRIME
DIH_X_LT_PI
DIH_X_MONO_LT_4
DIH_X_NN
DIH_Y_INEQ
DIH_Y_LT_PI
DIH_Y_LT_RHAZIM
DIH_Y_NN
DIJ_AFF_GE_PARTITION
DIMINDEX_4
DIMINDEX_5
DIMINDEX_6
DIMINDEX_FINITE_PRODUCT
DIMINDEX_HAS_SIZE_FINITE_PRODUCT
DIM_EMPTY
DIM_EQ_0
DIM_EQ_CARD
DIM_EQ_FULL
DIM_EQ_SPAN
DIM_IMAGE_KERNEL
DIM_IMAGE_KERNEL_GEN
DIM_INJECTIVE_LINEAR_IMAGE
DIM_INSERT
DIM_INSERT_0
DIM_KERNEL_COMPOSE
DIM_LE_CARD
DIM_LINEAR_IMAGE_LE
DIM_ORTHOGONAL_SUM
DIM_PSUBSET
DIM_ROWS_LE_DIM_COLUMNS
DIM_SING
DIM_SPAN
DIM_SPECIAL_HYPERPLANE
DIM_SUBSET
DIM_SUBSET_UNIV
DIM_SUMS_INTER
DIM_UNIQUE
DIM_UNIV
DISCRETE_BOUNDED_IMP_FINITE
DISCRETE_IMP_BOUNDED_EQ_COMPACT
DISCRETE_OPEN_COVER
DISCRETE_SUBSET
DISJOINT0_SCALE
DISJOINT_IMP_Z_IN_AFF_GT
DISJOINT_KY_LEMMA
DISJOINT_PAIR
DISJOINT_RW_DART_FAN_SAME_NODE_FAN
DISJTINCT_PROPERTY
DISTANCE_ATTAINS_INF_FAN
DISTANCE_ATTAINS_SUP_FAN
DIST_0
DIST_BETWEEN_FURTHEST_LT
DIST_DIAG_2_CASES
DIST_DIAG_2_CASES_3_LE
DIST_DIAG_2_CASES_3_LT
DIST_DIAG_2_CASES_EQ_3
DIST_DIAG_LE_CSTAB
DIST_EDGE_IN_BB_LE_2
DIST_EDGE_LE_CSTAB_CASE_LE3
DIST_EQ
DIST_EQ_0
DIST_EQ_2_IMP_A_EQ_2
DIST_EQ_HALF_PLANE
DIST_EQ_IMP_ORTHOGONAL
DIST_EQ_IMP_OTHORGONAL
DIST_EQ_IS_UNIQUE
DIST_FSTCART
DIST_IMP_COLLINEAR
DIST_IMP_UPS_X_POS
DIST_I_SUCI
DIST_LAW_OF_COS
DIST_LAW_OF_COS_ALT
DIST_LE2_BB_CASSE_4
DIST_LE2_BB_CASSE_5
DIST_LE_0
DIST_LE_2h0_IN_CASES_6
DIST_LE_HALF_PLANE
DIST_LE_IMP_A_LE
DIST_LIFT
DIST_LOWER_BOUND_lemma
DIST_LT_HALF_PLANE
DIST_L_ZERO
DIST_MIDPOINT
DIST_MUL
DIST_NZ
DIST_PAIR_LEMMA
DIST_POS
DIST_POS_LE
DIST_POS_LT
DIST_POW2_DOT
DIST_PROJECTION_LT_LEMMA
DIST_PSORT
DIST_REAL
DIST_REFL
DIST_ROOT_AND_DISCRIMINANT
DIST_SCALING
DIST_SNDCART
DIST_SQR
DIST_SYM
DIST_SYM_0
DIST_TRANSABLE
DIST_TRIANGLE
DIST_TRIANGLE_ADD
DIST_TRIANGLE_ADD_HALF
DIST_TRIANGLE_ALT
DIST_TRIANGLE_AS_ABS
DIST_TRIANGLE_DETAILS
DIST_TRIANGLE_EQ
DIST_TRIANGLE_HALF_L
DIST_TRIANGLE_HALF_R
DIST_TRIANGLE_LE
DIST_TRIANGLE_LT
DIST_UPS_X_POS
DIST_V3_DEFOR_EDGE_SUC
DIST_V3_DEFOR_EDGE_SUC_TWO_CASES
DIST_VECMAT
DIST_V_IN_BB_LE_C
DIV2_EVEN_lemma
DIVIDE
DIVIDE_DIVIDE
DIVIDE_EQ
DIVIDE_PROD
DIVIDE_PROD2
DIVIDE_SUM
DIVIDE_SUMMAND
DIV_NUM
DIV_lemma
DLWCHEM
DLWCHEM_VECTOR_sum
DLWCHEM_sum
DOMAIN_EMPTY
DOMAIN_INSERT
DOMAIN_TRANF_FACE_DELETE_DS
DOT_0_ARCV
DOT_1
DOT_2
DOT_3
DOT_BASIS
DOT_BASIS_BASIS
DOT_BASIS_BASIS_UNEQUAL
DOT_CAUCHY_SCHWARZ_EQUAL
DOT_COMPLEX
DOT_COS
DOT_EQ_0
DOT_EQ_IMP_INEQ
DOT_EQ_IMP_INEQ_LEMMA
DOT_ITSELF_2
DOT_LADD
DOT_LMUL
DOT_LMUL_MATRIX
DOT_LNEG
DOT_LSUB
DOT_LSUM
DOT_LZERO
DOT_MATRIX_PRODUCT
DOT_MATRIX_VECTOR_MUL
DOT_NORM
DOT_NORM_NEG
DOT_PASTECART
DOT_POS_LE
DOT_POS_LT
DOT_RADD
DOT_RE
DOT_RMUL
DOT_RNEG
DOT_ROWVECTOR_COLUMNVECTOR
DOT_RSUB
DOT_RSUM
DOT_RZERO
DOT_SCALING
DOT_SQUARE_NORM
DOT_SUB_ADD
DOT_SYM
DOT_VECMAT
DROP
DROP_ADD
DROP_CMUL
DROP_EQ
DROP_EQ_0
DROP_LAMBDA
DROP_NEG
DROP_SUB
DROP_VEC
DROP_VSUM
DROP_WLOG_LE
DRUQUFE
DS1_DS2_EQ_DS_FANADD
DS1_DS2_EQ_DS_FANADD1
DS1_DS2_EQ_DS_FANADD2
DSV_EQ_SYM_0
DSV_LE_DSV_TRANSFER
DSV_V3_DEFOR_EQ
DSV_V3_DEFOR_EQ_MK
DSV_WW_DEFOR_EQ
DUALNEG_PEROPP_BB
DUAL_EXISTS_MOD
DUAL_EXISTS_MOD0
DUAL_EXISTS_MOD_GE
DUAL_EXISTS_MOD_LE
DUAL_NEG_PEROPP
DUAL_PEROPP
DUAL_PEROPP2
DUUNHOR
DWFBRQY
DWWUTKW
D_6M1_EQ_6I1
D_FUN_COVER_SY
D_FUN_LE
D_HALF_SLICE
D_HALF_SLICE1
d1_fan
d20_fan
d2_fan
d2_special
d2_tame
d3
d_bn_eq
d_fan
d_fun
d_fun3
d_sy
d_tame
d_ts
dart
dart1_of_fan
dart2_of_fan
dart4_diag3
dart4_diag3_b
dartX
dartY
dart_Hll_n
dart_Hll_w
dart_degenerate
dart_face_walkup
dart_fan
dart_fan_character
dart_inside
dart_leads_into
dart_leads_into1
dart_leads_into_fan_in_topological_component_yfan
dart_mll_n
dart_mll_w
dart_node_walkup
dart_nondegenerate
dart_of
dart_of_fan
dart_of_fan_eq
dart_set
dart_std3
dart_std3_big
dart_std3_big_200_218
dart_std3_lw
dart_std3_mini
dart_std3_small
dart_std4
darts_k
darts_of_hyp
darts_of_hyp_elim
darts_of_list
dartset_fully_surrounded_is_non_isolated_fan
dartset_leads_in_fanadd_topological_component_yfan
dartset_leads_into
dartset_leads_into_ds_open_fanadd
dartset_leads_into_fan
dartset_leads_into_fan_SUBSET_U
dartset_leads_into_fan_eq_fanadd
dartset_leads_into_fan_eventually_radial_norm
dartset_leads_into_fan_radial
dartset_leads_into_fanadd1
dartset_leads_into_fanadd2
dartset_leads_into_is_topological_component_yfan
dartset_leads_into_subset_yfan
dat_th1
daumut_ccube
db_t0
decomposition_planar_by_angle_fan
def_obstructed
def_simplex
deform_684_pent_exists
deform_azim_sum
deform_pent_exists
deform_planar
deform_planar_exists
deform_planar_exists_second_version
deform_planar_second_version
deform_simplex_684_pent
deform_simplex_decrease_edge23
deform_simplex_edge_exists
deformation
deformation_BBs
deformation_BBs_ALT
deformation_ivs_rho_node1_equivariant1
deformation_restrict
deformation_rho_node1_equivariant
deformation_rho_node1_equivariant1
deformation_subset
degenerate_lemma
delta
delta4_hexall_x
delta4_squared_x
delta4_squared_y
delta4_y
delta4_y_imp_obtuse
delta_126_135
delta_126_x
delta_126_x_2h0_le_d
delta_135_x
delta_135_x_2h0_le_d
delta_234_x
delta_2_nn
delta_4680581274
delta_7697147739
delta_delta_x
delta_diff
delta_diff4
delta_func
delta_hexall_x
delta_mono
delta_oct
delta_pent_x
delta_quadratic
delta_sub1_x
delta_template_B_x
delta_template_B_x_alt
delta_tet
delta_top_x
delta_x
delta_x1
delta_x12
delta_x13
delta_x14
delta_x1_decreasing
delta_x1_sym
delta_x2
delta_x23
delta_x3
delta_x34
delta_x4
delta_x4_2
delta_x4_decreasing
delta_x4_delta4_y
delta_x4_dim_reduction
delta_x4_eq64
delta_x4_imp_obtuse
delta_x4_pos
delta_x4_rad2
delta_x5
delta_x5_delta_x6
delta_x6
delta_x_126_s2
delta_x_135_s2
delta_x_3_points
delta_x_eq0
delta_x_pos
delta_x_pos_apex
delta_x_root_exists
delta_x_rrr
delta_x_sym
delta_x_sym2
delta_x_xrr
delta_x_y
delta_xrrr_ups_x
delta_y
delta_y_LC
delta_y_continuous
delta_y_dim_reduction
delta_y_hex_cases
delta_y_pos_apex
delta_y_pos_xrr
delta_y_root_exists
delta_y_sym
delta_y_sym_cases2
dependent
deriv
deriv2
deriv_data6
deriv_form_taud
deriv_form_taud_D2
deriv_minus_pi
deriv_minus_pi_minus
deriv_pi
deriv_pi_minus
derivative
derived_form
derived_form2a
derived_form2b
derived_form_F
derived_form_acs
derived_form_add
derived_form_asn
derived_form_atn
derived_form_atn2curry
derived_form_b
derived_form_chain
derived_form_chain_old
derived_form_chain_simple
derived_form_const
derived_form_cos
derived_form_delta_x
derived_form_delta_x1
derived_form_delta_x4_wrt_x4
derived_form_delta_x4_wrt_x5
derived_form_delta_x4_wrt_x6
derived_form_delta_x_wrt_x4
derived_form_delta_x_wrt_x5
derived_form_delta_x_wrt_x6
derived_form_delta_y
derived_form_dih_x_wrt_x4
derived_form_dih_x_wrt_x5
derived_form_dih_x_wrt_x6
derived_form_div
derived_form_dnum1
derived_form_edge2_flatD_x1
derived_form_equivalence
derived_form_generic
derived_form_id
derived_form_inv
derived_form_local
derived_form_mul
derived_form_neg
derived_form_num1
derived_form_pow
derived_form_sin
derived_form_sqrt
derived_form_sub
derived_form_sum_dih
derived_form_sum_dih444
derived_form_sum_dih444sub
derived_form_tau2D
derived_form_taud_ALT
derived_form_taud_D3
derived_form_taum_d3_exists
derived_form_unique
derived_form_xrr
derived_form_xrr_D2
derived_form_xrr_D3
derived_form_xrr_wrt_y1
derived_imp_pos_open
derived_imp_pos_open_2
derived_imp_pos_open_3
det
det_vec3
determine_loop_index
dfdodec
diag
diag_trape
diag_trape1
diagonal
diameter_fan
diff2
diff2_domain
diff2c
diff2c_domain
diff2c_domain_pow
diff2c_pow
different_ccube
dih1_hexall_x
dih2_x
dih2_x_126_s2
dih2_x_135_s2
dih2_x_y
dih2_y
dih2_y_eq_dih3_y
dih2k
dih3_x
dih3_x_126_s2
dih3_x_135_s2
dih3_x_div_sqrtdelta_posbranch
dih3_x_y
dih3_y
dih3_y_eq_dih2_y
dih4_x
dih4_x_126_s2
dih4_x_135_s2
dih4_x_div_sqrtdelta_posbranch
dih4_y
dih5_x
dih5_x_126_s2
dih5_x_135_s2
dih5_x_div_sqrtdelta_posbranch
dih5_y
dih6_x
dih6_x_126_s2
dih6_x_135_s2
dih6_y
dihR
dihV
dihV_obtuse_mono
dihV_obtuse_mono_a
dihV_obtuse_mono_b
dihX
dihX3
dihX4
dih_dot
dih_gt_pi2
dih_hexall_x
dih_obtuse_mono
dih_obtuse_mono_b
dih_template_B_x
dih_template_B_x_alt
dih_x
dih_x'
dih_x5_mono
dih_x_126_s2
dih_x_135_s2
dih_x_alt
dih_x_dih_x_div_sqrtdelta_negbranch
dih_x_dih_x_div_sqrtdelta_posbranch
dih_x_dim_reduction
dih_x_div_sqrtdelta_pos
dih_x_div_sqrtdelta_posbranch
dih_x_interval
dih_x_nn
dih_x_pos_eq
dih_x_rad2
dih_x_sym
dih_x_sym2
dih_x_y
dih_y
dih_y'
dih_y_div_sqrtdelta_pos
dih_y_mono
dih_y_sym
dih_y_sym2
dihu2
dihu3
dihu4
dim
dirac_delta
directed_angle
discrete
disjiont1_cor6dot1
disjiont_union_fan
disjoint_cube
disjoint_ds1_and_ds2
disjoint_fan1
disjoint_fan2
disjoint_fan3
disjoint_line_interval
disjoint_loops
disjoint_set_fan
dist
dist3
dist_decreasing_ivt_lemma
dist_lemma
dist_lower_bound
distinct_nodes
distn
div6
div_th
dn1
dn10
dn11
dn111
dn112
dn12
dn2
dn3
dn4
dn5
dn51
dn6
dn61
dn62
dn63
dn7
dn8
dn9
dn91
dn92
dn93
dnax
dnay
dnum1
dodai
domain6
domain6_assum
dot
dot_coordinates
dot_coordinates_2
dot_e2_fan
dot_eq_0
dot_gt_0
dot_normalize
dot_pos_lemma
double
double_edge_walkup
double_edge_walkup_plain_hypermap
double_face_walkup
double_face_walkup_plain_hypermap
double_node_walkup
double_node_walkup_plain_hypermap
double_shift_lemma
drop
drop0
drop1
drop2
drop3
drop6_lift6
drop_6
drop_ant_tac_example
dropout_pad2d3d
ds1_in_face_set_fanadd
ds2_in_face_set_fanadd
dsv_F
dsv_J_empty
dsv_fun3
dsv_fun4
dsv_scs_init
dsv_unadorned
dsv_v39
dua
dummy6