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 _

S (theorems)

SATURATED_IMP_NONEMPTY
SATURATED_TRANS
SATURATE_BALL_ANNULUS
SCALING_LINEAR
SCHANGE
SCS_3M1_BASIC
SCS_3M1_IS_SCS
SCS_3M1_prime_ARROW_MM_3M1
SCS_3M1_prime_BASIC
SCS_3M1_prime_IS_SCS
SCS_3T1_BASIC
SCS_3T1_IS_SCS
SCS_3T1_prime_ARROW_MM_3T1
SCS_3T1_prime_BASIC
SCS_3T1_prime_IS_SCS
SCS_3T3_BASIC
SCS_3T3_IS_SCS
SCS_3T3_prime_ARROW_MM_3T3
SCS_3T3_prime_BASIC
SCS_3T3_prime_IS_SCS
SCS_3T4_BASIC
SCS_3T4_IS_SCS
SCS_3T4_prime2_ARROW_MM_3T4
SCS_3T4_prime2_BASIC
SCS_3T4_prime2_IS_SCS
SCS_3T4_prime_ARROW_MM_3T4
SCS_3T4_prime_BASIC
SCS_3T4_prime_IS_SCS
SCS_3T5_BASIC
SCS_3T5_IS_SCS
SCS_3T6_BASIC
SCS_3T6_IS_SCS
SCS_3T7_BASIC
SCS_3T7_IS_SCS
SCS_3T7_OPP_IS_SCS
SCS_3_IS_TRI_STABLE
SCS_4I1_ARROW_SCS_4I2_STAB_4I1
SCS_4I1_BASIC
SCS_4I1_IMP_SCS_4I2
SCS_4I1_IS_SCS
SCS_4I1_SLICE_02
SCS_4I1_STAB_DIAG
SCS_4I2_3_LE_A
SCS_4I2_BASIC
SCS_4I2_GENERIC
SCS_4I2_IMP_SCS_4T1
SCS_4I2_IS_SCS
SCS_4I2_STRAIGHT
SCS_4I2_STRAIGHT_ALL
SCS_4I3_ARROW_4T4
SCS_4I3_ARROW_SCS_4M6_STAB_4I3
SCS_4I3_BASIC
SCS_4I3_IS_SCS
SCS_4M2_ARROW_SCS_4M6_STAB_4M2
SCS_4M2_BASIC
SCS_4M2_IS_SCS
SCS_4M2_SLICE_13
SCS_4M3_ARROW_SCS_4M6_STAB_4M3
SCS_4M3_BASIC
SCS_4M3_IS_SCS
SCS_4M3_SLICE_13
SCS_4M4_ARROW_SCS_4M7_STAB_4M4
SCS_4M4_BASIC
SCS_4M4_IS_SCS
SCS_4M4_SLICE_02
SCS_4M4_SLICE_13
SCS_4M5_ARROW_SCS_4M8_STAB_4M5
SCS_4M5_BASIC
SCS_4M5_IS_SCS
SCS_4M5_SLICE_13
SCS_4M6_ARROW_SCS_4T3_STAB_4M6
SCS_4M6_BASIC
SCS_4M6_IS_SCS
SCS_4M6_OPP_IS_SCS
SCS_4M6_STAND
SCS_4M6_STAND_OR_PRO
SCS_4M6_prime_ARROW_MM_4M6
SCS_4M6_prime_BASIC
SCS_4M6_prime_IS_SCS
SCS_4M7_ARROW_STAB_4M7_4M6
SCS_4M7_BASIC
SCS_4M7_IS_SCS
SCS_4M7_SLICE_02
SCS_4M7_SLICE_02_ARROW_3T3_3M1
SCS_4M7_SLICE_13
SCS_4M7_SLICE_13_ARROW_3T4
SCS_4M7_STAND
SCS_4M7_STAND_OR_PRO
SCS_4M7_prime_ARROW_MM_4M7
SCS_4M7_prime_BASIC
SCS_4M7_prime_IS_SCS
SCS_4M8_02_ARROW_3T7
SCS_4M8_02_ARROW_4M8_13
SCS_4M8_02_BASIC
SCS_4M8_02_IS_SCS
SCS_4M8_02_SLICE_02
SCS_4M8_13_ARROW_3T7
SCS_4M8_13_ARROW_3T7_OPP
SCS_4M8_13_BASIC
SCS_4M8_13_IS_SCS
SCS_4M8_13_SLICE_13
SCS_4M8_ARROW_STEP_ONE
SCS_4M8_BASIC
SCS_4M8_IS_SCS
SCS_4M8_SLICE_02_ARROW_3T4
SCS_4M8_SLICE_13
SCS_4M8_SLICE_13_ARROW_3T4
SCS_4M8_STAND
SCS_4M8_STAND_OR_PRO
SCS_4M8_prime_ARROW_MM_4M8
SCS_4M8_prime_BASIC
SCS_4M8_prime_IS_SCS
SCS_4T1_BASIC
SCS_4T1_IS_SCS
SCS_4T2_BASIC
SCS_4T2_IS_SCS
SCS_4T3_BASIC
SCS_4T3_IS_SCS
SCS_4T4_BASIC
SCS_4T4_IS_SCS
SCS_4T5_BASIC
SCS_4T5_IS_SCS
SCS_4_3_IS_TRI_STABLE
SCS_4_IS_TRI_STABLE
SCS_4_sqrt8_IS_TRI_STABLE
SCS_5I1_BASIC
SCS_5I1_BERAK_BY_CSTAB
SCS_5I1_IS_SCS
SCS_5I1_SLICE_02
SCS_5I1_STAB_DIAG
SCS_5I1_STAB_DIAG_2h0
SCS_5I1_STAB_DIAG_2h0_sqrt8
SCS_5I1_STAB_DIAG_sqrt8
SCS_5I2_BASIC
SCS_5I2_BERAK_BY_CSTAB
SCS_5I2_IS_SCS
SCS_5I2_SLICE_02
SCS_5I2_STAB_DIAG
SCS_5I3_BASIC
SCS_5I3_BERAK_BY_CSTAB
SCS_5I3_IS_SCS
SCS_5I3_STAB_DIAG
SCS_5M1_BASIC
SCS_5M1_BERAK_BY_CSTAB
SCS_5M1_IS_SCS
SCS_5M1_SLICE_02
SCS_5M1_SLICE_03
SCS_5M1_SLICE_24
SCS_5M1_STAB_DIAG
SCS_5M2_BASIC
SCS_5M2_EDGE_LE_2H0
SCS_5M2_EDGE_LE_2H0_IMP_0
SCS_5M2_IMP_SCS_5T1
SCS_5M2_IS_SCS
SCS_5M3_02_ARROW_3T4_4M6
SCS_5M3_03_ARROW_3T1_4M7
SCS_5M3_24_ARROW_3T1_4M8
SCS_5M3_BASIC
SCS_5M3_IS_SCS
SCS_5M3_SLICE_02
SCS_5M3_SLICE_03
SCS_5M3_SLICE_24
SCS_5M3_STAB_DIAG_sqrt8
SCS_5T1_BASIC
SCS_5T1_IS_SCS
SCS_5_IS_TRI_STABLE
SCS_5_pro_cs_IS_TRI_STABLE
SCS_5_sqrt8_IS_TRI_STABLE
SCS_6I1_BASIC
SCS_6I1_BERAK_BY_CSTAB
SCS_6I1_IMP_SCS_6T1
SCS_6I1_IS_SCS
SCS_6M1_BASIC
SCS_6M1_IMP_SCS_6T1
SCS_6M1_IS_SCS
SCS_6T1_BASIC
SCS_6T1_IS_SCS
SCS_6_IS_TRI_STABLE
SCS_ARROW_TRANS_SING
SCS_A_2
SCS_A_B__EQ_MOD_3
SCS_A_B__EQ_MOD_4
SCS_A_B__EQ_MOD_4_3
SCS_A_B__EQ_MOD_4_sqrt8
SCS_A_B__EQ_MOD_5
SCS_A_B__EQ_MOD_5_pro_cs
SCS_A_B__EQ_MOD_5_sqrt8
SCS_A_B__EQ_MOD_6
SCS_A_SYM
SCS_BASIC_DSV
SCS_BASIC_TAUSTAR
SCS_B_LE_CSTAB
SCS_B_SYM
SCS_DIAG_2
SCS_DIAG_4_ADD0
SCS_DIAG_4_ADD2
SCS_DIAG_4_CASES
SCS_DIAG_ADD1
SCS_DIAG_A_LE_DIST
SCS_DIAG_SCS_4I1_02
SCS_DIAG_SCS_4I3_02
SCS_DIAG_SCS_4I3_13
SCS_DIAG_SCS_4M2_02
SCS_DIAG_SCS_4M2_13
SCS_DIAG_SCS_4M3_02
SCS_DIAG_SCS_4M3_13
SCS_DIAG_SCS_4M4_02
SCS_DIAG_SCS_4M4_13
SCS_DIAG_SCS_4M5_02
SCS_DIAG_SCS_4M5_13
SCS_DIAG_SCS_4M6_02
SCS_DIAG_SCS_4M6_13
SCS_DIAG_SCS_4M7_02
SCS_DIAG_SCS_4M7_13
SCS_DIAG_SCS_4M8_02
SCS_DIAG_SCS_4M8_02_02
SCS_DIAG_SCS_4M8_02_13
SCS_DIAG_SCS_4M8_13
SCS_DIAG_SCS_4M8_13_13
SCS_DIAG_SCS_5I1_02
SCS_DIAG_SCS_5I2_02
SCS_DIAG_SCS_5M1_02
SCS_DIAG_SCS_5M1_03
SCS_DIAG_SCS_5M1_24
SCS_DIAG_SCS_5M2_02
SCS_DIAG_SCS_5M2_03
SCS_DIAG_SCS_5M2_24
SCS_DIAG_SCS_5M3_02
SCS_DIAG_SCS_5M3_03
SCS_DIAG_SCS_5M3_24
SCS_DIAG_SCS_6I1_02
SCS_DIAG_SCS_6I1_03
SCS_GENERIC_SYM_0
SCS_HALF_SLICE_IS_A_SCS
SCS_HALF_SLICE_IS_SCS
SCS_HALF_SLICE_IS_SCS_4
SCS_HALF_SLICE_IS_SCS_4_PRIME
SCS_HALF_SLICE_IS_SCS_PRIME
SCS_J_DIAG_EQ
SCS_J_PRIME_SUBSET_SCS_J
SCS_K_D_A_STAB_EQ
SCS_K_LE_6
SCS_K_LT_2
SCS_K_PRIME_CASE_3
SCS_K_PRIME_CASE_4
SCS_K_PRIME_CASE_5
SCS_K_PRIME_CASE_6
SCS_K_PRIME_LE_GE
SCS_M_4I1
SCS_M_4I2
SCS_M_5I1
SCS_M_5M2
SCS_M_5T1
SCS_M_6I1_EQ_6M1
SCS_M_6M1
SCS_M_6T1
SCS_M_CASES_4_EQ
SCS_M_CASES_4_EQ1
SCS_M_CASES_4_LE_2
SCS_M_EQ_0
SCS_M_EQ_1
SCS_M_LE_1
SCS_M_LE_K
SCS_OPP_REFL
SCS_SLICE_SYM
SCS_STR_CASES_4
SDIFF
SDIFF_SUBSET
SDIFF_SYM
SDIFF_TRANS
SDIHJZK
SDIHJZK_INTERPRETE
SECOND_CHAIN_CONTINUOUS
SECOND_CHAIN_CRITICAL
SECOND_CHAIN_GENERAL
SECOND_DERIVATIVE_TEST
SECOND_DERIVATIVE_TEST_COMPOSE
SECOND_DERIVATIVE_TEST_TAUM
SEC_DOT
SEGMENT_CONNECTED
SEGMENT_EDGE_ONTO
SEGMENT_INTER_CBALL_LEMMA
SEGMENT_TO_ONE
SEGMENT_TO_TWO
SELECT_EXIST
SELECT_THM
SELF_CYCLIC_IMP_BIJ
SELF_CYCLIC_IMP_FINITE
SELF_PAIR_EMPTY_VV
SEPARATE_CLOSED_CONES
SEQUENCE_INFINITE_LEMMA_FAN
SEQUENCE_OF_RHO_NODE_IS_SUC
SEQUENCE_UNIQUE_LIMPT_FAN
SEQUENTIALLY_DIVH
SEQUENTIALLY_EQ_2POINT
SEQUENTIALLY_FAN
SER_APPROX
SER_APPROX1
SET2_DETER
SET2_HAS_SIZE2
SET2_INSERT1
SET2_INSERT2
SET_EQ
SET_EQ_DIAG_STAB_4I1
SET_EQ_DIAG_STAB_4I1_02
SET_EQ_DIAG_STAB_4I3
SET_EQ_DIAG_STAB_4M2
SET_EQ_DIAG_STAB_4M3
SET_EQ_DIAG_STAB_4M4
SET_EQ_DIAG_STAB_4M5
SET_EQ_DIAG_STAB_4M6
SET_EQ_DIAG_STAB_4M7
SET_EQ_DIAG_STAB_4M8
SET_EQ_DIAG_STAB_5I1
SET_EQ_DIAG_STAB_5I1_02
SET_EQ_DIAG_STAB_5I2
SET_EQ_DIAG_STAB_5I2_02
SET_EQ_DIAG_STAB_5M1
SET_EQ_DIAG_STAB_5M3
SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4
SET_EQ_DIAG_STAB_6I1
SET_EQ_DIAG_STAB_6I1_02
SET_EQ_DIAG_STAB_6I1_03
SET_EQ_SYM_0
SET_OF_0_TO_2
SET_OF_0_TO_3
SET_OF_4
SET_OF_EDGE_CARD_EQ2
SET_OF_EDGE_INVARIANT
SET_OF_EDGE_LINEAR_IMAGE_EQ
SET_OF_EDGE_TRANSLATION_EQ
SET_OF_EDGE_UNION_GRAPH
SET_OF_LIST_A_EMPTY
SET_OF_LIST_CC_UH
SET_OF_LIST_DELETE_EQ_DROP
SET_OF_LIST_DELETE_SUBSET_DROP
SET_OF_LIST_FILTER
SET_OF_LIST_FLATTEN
SET_OF_LIST_INITIAL_SUBLIST_SUBSET
SET_OF_LIST_LEFT_ACTION_LIST
SET_OF_LIST_LEFT_ACTION_LIST_2
SET_OF_LIST_LEFT_ACTION_LIST_3
SET_OF_LIST_REMOVE_DUPLICATES
SET_OF_LIST_TRUN2_LEFT_ACTION_LIST2
SET_OF_LIST_TRUNCATE_1
SET_OF_LIST_TRUNCATE_2
SET_OF_LIST_TRUNCATE_SIMPLEX_SUBSET
SET_STAB_4I1
SET_STAB_4I3
SET_STAB_4M2
SET_STAB_4M3
SET_STAB_4M4
SET_STAB_4M5
SET_STAB_4M6
SET_STAB_4M6_ARROW_4T5
SET_STAB_4M7
SET_STAB_4M8
SET_STAB_4M8_ARROW_3T4
SET_STAB_5I1
SET_STAB_5I2
SET_STAB_5I3
SET_STAB_5M1
SET_STAB_5M3
SET_STAB_6I1
SET_SUBSET_AFFINE_HULL
SGFCDZO
SGIN_POW_EQ
SGTRNAF
SHIFT_LEFT_RIGHT
SHIFT_LEFT_RIGHT_o_I
SHIFT_RIGHT
SHOGYBS
SHORT_EDGES
SIGMAHAT_EQ
SIGMA_FAN
SIGMA_FAN_OF_FANADD1
SIGMA_FAN_OF_FANADD_AT_POINT1
SIGMA_FAN_OF_FANADD_AT_POINT2
SIGMA_FAN_OF_FANADD_AT_POINT3
SIGMA_FAN_OF_FANADD_AT_POINT4
SIGMA_FAN_OF_FANADD_AT_POINT5
SIGMA_FAN_OF_FANADD_AT_POINT6
SIGMA_FAN_POWER
SIGMA_SY_LE1
SIG_AND_INVERSE1_SIG
SIMPLEX_FURTHEST_LT_2
SIMPLE_FACE_DISJOINT_NODE_MAP_2
SIMPLE_FACE_EDGE_INJ
SIMPLE_HYPERMAP_IMP_FACE_INJ
SIMPLE_HYPERMAP_lemma
SIMPLE_IMP_DISTINCT_FF_NODE_IMAGE
SIMPLIZE_COS_IF_OTHOR
SIMP_DOT_ALEM
SIMP_ORBITS_POINTS_FAN
SINCOS_PRINCIPAL_VALUE_FAN
SING_EQ
SING_GSPEC_APP
SING_J1_SY
SING_UNION_EQ_INSERT
SIN_ARCV_EQ_0
SIN_ARCV_EQ_0_EQ_LAP
SIN_AZIM_MUTUAL_CROSS
SIN_AZIM_MUTUAL_SROSS
SIN_AZIM_NEG_PI_LT
SIN_AZIM_POS_PI_LT
SIN_COMPLEMENTIVE
SIN_COS_IDEN_IFF_DIFFER_PERS
SIN_DI_HOC
SIN_EQ_SQRT_ONE_SUB
SIN_MUL_EXPAND
SIN_NEGPOS_PI
SIN_PERIODIC_IN_WHOLE
SIN_PERIODIC_N2PI
SIN_PI6
SIN_PI6_STRADDLE
SIN_POW2_EQ_1_SUB_COS_POW2
SIN_SUB_PERIODIC
SIN_TOTAL_PERIODIC
SKOLEM_EPSILON
SKOLEM_PERIODIC
SKOLEM_PERIODIC2
SKOLEM_TAG
SKOLEM_TAG2
SLICEE_EQ_E2_SY
SLICEE_EQ_E_SY
SLICEF_EQ_F2_SY
SLICEF_EQ_F_SY
SLICEV_BIJ
SLICEV_EQ_V2_SY
SLICEV_EQ_V_SY
SLICEV_IMAGE
SLICEW_BIJ
SLICEW_IMAGE
SLICE_IS_UNADORNED
SLICE_REPRENT
SLICE_REPRENT2
SLIDABLE_PROJECTION
SLTSTLO1
SLTSTLO2
SMALLEST_ANGLE_IN_CONVEX_HULL
SMALLEST_ANGLE_LINE_EXISTS
SMALLEST_ANGLE_LINE_PROPERTY
SMALL_BALL_ANNULUS_6
SMALL_BALL_ANNULUS_6_3
SMALL_BALL_ANNULUS_6_sqrt8
SNDCART_ADD
SNDCART_CMUL
SNDCART_NEG
SNDCART_SUB
SNDCART_VEC
SNDCART_VSUM
SND_BIJ
SND_IN_SET_OF_DART_OF_FRST
SOL0_POS
SOLID_ANGLE_YFAN
SOL_AFF_GT_2_1
SOL_DISJOINT_UNION
SOL_EMPTY
SOL_LOCAL_FAN_POS_CASE3
SOL_LOFA_EQ_SUM_INANGLE
SOL_NN
SOL_SOLID_TRIANGLE
SOL_SOLID_TRIANGLE_ALT
SOL_SOL_Y_EXPLICIT
SOL_SUBSET
SOL_UNIONS
SPACE3_EQ_UNION_3SET
SPANNING_SUBSET_INDEPENDENT
SPANNING_SURJECTIVE_IMAGE
SPANS_IMAGE
SPAN_0
SPAN_2
SPAN_3
SPAN_ADD
SPAN_ADD_EQ
SPAN_BREAKDOWN
SPAN_BREAKDOWN_EQ
SPAN_CARD_GE_DIM
SPAN_CLAUSES
SPAN_DELETE_0
SPAN_EMPTY
SPAN_EQ
SPAN_EQ_DIM
SPAN_EQ_SELF
SPAN_EXPLICIT
SPAN_FINITE
SPAN_IMAGE_SCALE
SPAN_INC
SPAN_INDUCT
SPAN_INDUCT_ALT
SPAN_INSERT_0
SPAN_LINEAR_IMAGE
SPAN_MONO
SPAN_MUL
SPAN_MUL_EQ
SPAN_NEG
SPAN_NEG_EQ
SPAN_NOT_UNIV_ORTHOGONAL
SPAN_NOT_UNIV_SUBSET_HYPERPLANE
SPAN_SING
SPAN_SPAN
SPAN_STDBASIS
SPAN_SUB
SPAN_SUBSET_SUBSPACE
SPAN_SUBSPACE
SPAN_SUPERSET
SPAN_TRANS
SPAN_UNION
SPAN_UNION_SUBSET
SPAN_UNIV
SPAN_VSUM
SPECIAL_HYPERPLANE_SPAN
SPEC_HY_ELEMS
SQRT2_LT_2
SQRT4_EQ2
SQRT8_LE_EQ_8_LESS_POW2
SQRT8_LT
SQRT8_LT_4_45
SQRT8_TWO_TWO
SQRT_DELTA_X_AFTER_RESCALE
SQRT_DIV
SQRT_DIV_R
SQRT_EQ_0
SQRT_EVEN_POW2
SQRT_INJ
SQRT_INV
SQRT_LT_0
SQRT_MONO_LE
SQRT_MONO_LE_EQ
SQRT_MONO_LT
SQRT_MONO_LT_EQ
SQRT_MUL
SQRT_MUL_L
SQRT_MUL_POW_2
SQRT_MUL_R
SQRT_OF_32_lemma
SQRT_OF_POW_2_LE
SQRT_POS_LE
SQRT_POS_LT
SQRT_POW2
SQRT_POW_2
SQRT_RULE_Euler_lemma
SQRT_SEPARATED
SQRT_WORKS
SQUARE_BOUND_LEMMA
SQUARE_CONTINUOUS
SQUARE_NORM_CAUCHY_SCHWARZ_POW2
SRGTIHY
SRPRNPL
STAB_4I1_SCS
STAB_4I3_02_ARROW_4I3_13
STAB_4I3_SCS
STAB_4M2_02_ARROW_4M2_13
STAB_4M2_SCS
STAB_4M3_02_ARROW_4M3_13
STAB_4M3_SCS
STAB_4M4_SCS
STAB_4M5_02_ARROW_4M5_13
STAB_4M5_SCS
STAB_4M6_02_ARROW_4M6_13
STAB_4M6_02_ARROW_4T5
STAB_4M6_13_ARROW_4T5
STAB_4M6_SCS
STAB_4M7_SCS
STAB_4M8_02_ARROW_4M8_13
STAB_4M8_02_SCS
STAB_4M8_13_SCS
STAB_4M8_SCS
STAB_5I1_SCS
STAB_5I2_SCS
STAB_5I3_ARROW_STAB_5M1
STAB_5I3_ARROW_STAB_5M1_DIAG
STAB_5I3_SCS
STAB_5M1_SCS
STAB_5M2_SCS
STAB_5M3_SCS
STAB_5T1_SCS
STAB_6I1_SCS
STAB_BB
STAB_IS_SCS
STAB_MOD
STAB_SCS_4M7_ARROW_3T3_3M1_3T4
STAB_SYM
STEM_EDGEX
STEM_OF_LEAF
STEP2_REDUCE_FAN
STEP3_REDUCE_FAN
STRICTLY_INCREASE_PRESERVING_CARD
STRICT_CYCLIC_FAN_PROPERTIES
STRICT_CYCLIC_IMP_FAN
STRICT_SORT_FINITE
STR_MOD_EQ
SUBCASE1
SUBCASE2
SUBCASE3
SUBCASE31
SUBCASE32
SUBCASE33
SUBCASE34
SUBCASE35
SUBCASE36
SUBCASE4
SUBCASE41
SUBCASE42
SUBCASE43
SUBCASE44
SUBCASE45
SUBCASE46
SUBCASE47
SUBCASE48
SUBCASE49
SUBCASE5
SUBCASE50
SUBCASE51
SUBCASE52
SUBCASE6
SUBCASE7
SUBCASE8
SUBCRITICAL_EDGEX_ALT
SUBDIVISION_CS1_DSV_EQ
SUBDIVISION_CS1_TAUSTAR_EQ
SUBDIVISION_IS_NOT_EAR
SUBSET1
SUBSET_AFF2_IMP_COLL
SUBSET_AFFINE_HULL3_EQ_SUB_PLANE
SUBSET_BALL_FAN
SUBSET_CBALL_FAN
SUBSET_CLOSURE_FAN
SUBSET_EDGES0_FAN
SUBSET_IMP_SO_DO_EE
SUBSET_IMP_SUBSET_HULL
SUBSET_INTER
SUBSET_INTERIOR_FAN
SUBSET_INTERS
SUBSET_INTERVAL_IMP
SUBSET_LE_DIM
SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ
SUBSET_PACKING
SUBSET_PREIMAGE
SUBSET_P_HULL
SUBSET_SUC
SUBSET_SUC2
SUBSET_SYM_0
SUBSET_aff
SUBSET_affcomb
SUBSET_hull
SUBSPACES_INTER_BALL_EQ_IMP_EQ
SUBSPACE_0
SUBSPACE_ADD
SUBSPACE_BOUNDED_EQ_TRIVIAL
SUBSPACE_HYPERPLANE
SUBSPACE_IMP_NONEMPTY
SUBSPACE_INTER
SUBSPACE_INTERS
SUBSPACE_ISOMORPHISM
SUBSPACE_KERNEL
SUBSPACE_LINEAR_IMAGE
SUBSPACE_LINEAR_IMAGE_EQ
SUBSPACE_LINEAR_PREIMAGE
SUBSPACE_MUL
SUBSPACE_NEG
SUBSPACE_ORTHOGONAL_TO_VECTOR
SUBSPACE_ORTHOGONAL_TO_VECTORS
SUBSPACE_SPAN
SUBSPACE_SPECIAL_HYPERPLANE
SUBSPACE_SUB
SUBSPACE_SUMS
SUBSPACE_TRANSLATION_SELF
SUBSPACE_TRANSLATION_SELF_EQ
SUBSPACE_TRIVIAL
SUBSPACE_UNION_CHAIN
SUBSPACE_UNIV
SUBSPACE_VSUM
SUB_CONST_o
SUB_DIST_POW2_INTERPRETE
SUB_DOT_EQ_0_INVERTALE
SUB_LUNAR_DEFORM_LEMMA
SUB_NUM
SUB_PACKING
SUCCESSIVE_RHO_NODE1_AFF_LT
SUC_0
SUC_ADD_RIGHT
SUC_EXPLICIT
SUC_LE_THM
SUC_LT_THM
SUC_MOD_EQ
SUC_MOD_EQ1
SUC_MOD_EQ_MOD_SUC
SUC_MOD_NOT_EQ
SUC_NOT
SUC_NUM
SUC_OPP_ID
SUC_POWER2_NOT
SUC_PRE_2
SUM1_IFAZIMS_FAN
SUM_1
SUM_2
SUM_3
SUM_4ANGLE_4POINT_EQ_2PI
SUM_AZIMS_EQ_2PI_FAN
SUM_AZIM_DART
SUM_AZIM_DART_FULLY_SURROUNDED
SUM_AZIM_EQ_ANGLE_EQ4
SUM_AZIM_EQ_ANGLE_LE4
SUM_AZIM_EQ_ANGLE_LE4_FUN
SUM_AZIM_FAN_OF_NODE_EQ_2PI_I_FAN
SUM_AZIM_FAN_OF_NODE_EQ_SUM_AZIM_I_FAN
SUM_AZIM_POWER_SIGMA_FAN
SUM_AZIM_SYM_0
SUM_BETA
SUM_BETA_BUMP_LEMMA
SUM_BOUND_LT_ALT
SUM_CARD_FACE_NODE_DART_FAN
SUM_CHI_EQ_2DELTA
SUM_CLAUSES_alt
SUM_CONST2
SUM_DIS2
SUM_DIS3
SUM_DIS4
SUM_EQ_IF_AZIMS_FAN
SUM_FACE_CONST
SUM_FACE_ISO
SUM_FACE_LIST
SUM_FACE_LIST_ALL
SUM_FACE_SUB
SUM_FACE_SUB_CONST
SUM_GAMMAX_LMFUN_ESTIMATE
SUM_HAS_SIZE
SUM_IF_AZIMS_FAN
SUM_INCREASE_ARG_DIFF
SUM_INTER
SUM_INTERIOR_AGL_LEMMA
SUM_ISOMORPHISM
SUM_LOWER_BOUND
SUM_NODE_CONST
SUM_NODE_ISO
SUM_NODE_LIST
SUM_NODE_LIST_ALL
SUM_NODE_SUB
SUM_NODE_SUB_CONST
SUM_NUMSEG2
SUM_NUMSEG3
SUM_NUMSEG4
SUM_ORBIT
SUM_OVER_W_EQUAL_AT_ANY_POINT
SUM_PAIR_0
SUM_PAIR_2_SET
SUM_PAIR_SYM_0
SUM_POS_LT_NUMSEG
SUM_POW2_EQ1_UNIQUE_TRIG
SUM_RMUL_BOUND
SUM_SET_OF_2_ELEMENTS
SUM_SET_OF_ORBITS
SUM_SOL_IN_FACE_SET_EQ_4PI
SUM_SOL_IN_TOPOLOGICAL_COMPONENET_EQ_IN_FACE_SET
SUM_SOL_TOPOLOGICAL_COMPONENT_YFAN_EQ_SOL_UNIONS
SUM_UPS_X_1
SUM_VSUM
SUM_lemma
SUPP
SUPSET_INTER
SUP_lt
SURJECTIVE_SCALING
SURJ_ALT
SURJ_FINITE
SURJ_IMAGE
SURJ_IMP_FINITE
SURJ_IMP_RES_INVERSE
SURJ_IMP_S2_EQ_IMAGE_S1
SURROUNDED_IMP_CARD_NODE_GE_3
SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3
SURROUNDED_IMP_IN_DART1_OF_FAN
SUR_E_FAN
SUR_F1_FAN
SUR_FCHANGED
SUR_MOD_FUN
SUR_N_FAN
SUR_SIGMA_FAN
SUR_TRANF_FACE_DELETE_DS
SWAP_EXISTS_THM
SWAP_FORALL_TAG
SYMMETRIC_LINEAR_IMAGE
SYM_AZIM_CYCLE_SYM_0
SYNQIWN
SZIPOAS
S_INIT_IS_UNADORNED
S_LEAF_BOUNDED
S_LEAF_CARD2
S_LEAF_FINITE
S_LEAF_IN_WEDGE_GE
S_LEAF_SET
S_LEAF_SUBSET_PACKING
S_LEAF_SYM
S_LEAF_TRUNCATE
S_SUBSET_IMP_AFF_S_TOO
s_extremal_edge
s_init_J_empty
s_init_list_alt
s_init_list_v39
s_leaf
s_leaf_collinear
s_leaf_leaf
s_minimal_edge
s_special
safesqrt
same_count1
same_projective_sphere_ge_fan
same_projective_sphere_gt_fan
samsara_formula
saturated
scalar6
scale
scale6
scale_aff_ge_fan
scale_aff_gt_fan
scale_in_edges_fan
scale_mul
scanl
scriptL
scriptL_lemma
scs_3I1
scs_3M1
scs_3M1_prime
scs_3T1
scs_3T1_prime
scs_4I1
scs_4I2
scs_4I3
scs_4M1
scs_4M2
scs_4M3
scs_4M4
scs_4M5
scs_4M6
scs_4M6_prime
scs_4M7
scs_4M7_prime
scs_4M8
scs_4M8_02
scs_4M8_13
scs_4M8_prime
scs_4T4
scs_4T5
scs_5I1
scs_5I2
scs_5I3
scs_5M1
scs_5M2
scs_5M3
scs_5T1
scs_5T1_generic
scs_5T1_props
scs_6I1
scs_6M1
scs_6T1
scs_6T1_generic
scs_6T1_props
scs_J_v39
scs_J_v39_explicit
scs_M
scs_a_v39
scs_a_v39_explicit
scs_am_v39
scs_am_v39_explicit
scs_arrow_sing_empty
scs_arrow_v39
scs_b_v39
scs_b_v39_explicit
scs_basic
scs_basic3
scs_basic4
scs_basic_unadorned
scs_bm_v39
scs_bm_v39_explicit
scs_components
scs_d_v39
scs_d_v39_explicit
scs_diag
scs_diag_2
scs_diag_cs_adj
scs_generic
scs_half_slice_v39
scs_hi_v39
scs_hi_v39_explicit
scs_inj
scs_is_str
scs_k_bounds
scs_k_le_3
scs_k_v39
scs_k_v39_explicit
scs_lb_2
scs_lo_v39
scs_lo_v39_explicit
scs_mk_unadorned_unadorned
scs_opp_v39
scs_prop_equ_v39
scs_slice_v39
scs_stab_diag_v39
scs_str_v39
scs_str_v39_explicit
scs_unadorned
scs_unadorned_explicit
scs_vv_MOD
second_bounded
second_glue_evaluation
second_join_evaluation
segment_in_segment
segment_inter_aff_ge_ends
segment_inter_conv
segment_intersects_aff_ge_lemma
segment_subset_aff_gt_union
segment_subset_yfan
segmentsubset_aff_gt
selectd
selectd_cases
selectd_exists
self_inverse
self_pairs
selling_homog
selling_surface_nn
selling_surface_nn01_23
selling_surface_nn2_013
selling_surface_num
selling_surface_num01_23_approx
selling_surface_num2_013_approx
selling_volume2
separate1_sphere_fan
separate1_sphere_not0_fan
separate_point_convex_fan
separation_plane_4_points
sequentially_fan
set_3elements
set_components
set_edges_is_finite_fan
set_nth
set_of_ccube
set_of_components
set_of_cube
set_of_edge
set_of_edge_subset_edges
set_of_edges
set_of_exceptional
set_of_exceptional_meeting_node
set_of_exterior_contour
set_of_face_meeting_node
set_of_interior_contour
set_of_iso
set_of_list2
set_of_list2_explicit
set_of_list3
set_of_list3_explicit
set_of_list4
set_of_list4_explicit
set_of_only_edge
set_of_only_edge1
set_of_orbits
set_of_orbits_points_fan
set_of_quadrilateral
set_of_quadrilaterals_meeting_node
set_of_triangle
set_of_triangles_meeting_node
set_one_point
set_op
set_op1
set_part_components
sgn_ge
sgn_gt
sgn_le
sgn_lt
shape
shift
shift_left
shift_left_empty'
shift_lemma
shift_path
shift_right
shift_right_empty'
shift_scalar6
sierpinski
sigma
sigma_fan
sigma_fan_in_set_of_edge
sigma_set1
sigma_sy
simp_def_ge
simp_inverse_sigma_fan_alt
simpl_conv3
simple_hypermap
simplex
simplex_exists
simplex_interior_pos
simplex_unique
sinV
sin_acs_t
sin_azim_pos
sin_of_u_fan
sincos1_of_u_fan
sincos_of_u_fan
six_point
size
skolem_epsilon_old
slicee
slicef
slicev
sloc2_ortho
small
smallest_angle_line
smallest_angle_set
sol
sol0
sol0_EQ_sol_y
sol0_POS
sol0_const1
sol0_linear
sol0_linear_r
sol0_over_pi_EQ_const1
solR
sol_euler156_x_div_sqrtdelta
sol_euler246_x_div_sqrtdelta
sol_euler345_x_div_sqrtdelta
sol_euler_x
sol_euler_x_div_sqrtdelta
sol_fan
sol_local
sol_local_azim
sol_spec
sol_x
sol_x'
sol_x_nn
sol_x_sol_euler_x
sol_x_sol_x_sqrtdelta
sol_x_sol_y
sol_x_sym
sol_x_sym2
sol_y
sol_y'
sol_y_123
sol_y_sol_x
sol_yu_large
solid
solid_of_dartset_leads_into_fan_triangle_fan
solid_triangle
solve_mod_k
sorted
sovo
span
span_run_edges_fan
special_datum
special_fan
special_feature_extreme_edge
sphere
split
split4_lemma
splitAt
splitAtRec
split_fan_face
split_interval
split_list_face
split_list_hyp_empty
split_list_list
sq_pow2
sql
sqn
sqp
sqrt01
sqrt2
sqrt20
sqrt2_lb
sqrt2_nn
sqrt2_sqrt2
sqrt2_sqrt8
sqrt3
sqrt3_nn
sqrt8
sqrt8_2
sqrt8_LE_6
sqrt8_LE_CSTAB
sqrt8_bounds
sqrt8_flyspeck
sqrt8_nn
sqrt8_sqrt2
sqrt_of_ge_root
sqrt_partial_lemma'
sqrt_pos_eq
sqrt_secant_approx
sqrt_second_lemma'
sqrt_sqrt
sqrt_squared
sqrt_x1
sqrt_x2
sqrt_x3
sqrt_x4
sqrt_x5
sqrt_x6
sqrtpow2
sqrtxx
square_add_neg_lemma
square_edge_convolution
square_edge_convolution2
square_le
ssqrt
ssqrt_sqrt
ssreflect_eq_def
stab
stable_sy_explicit
stable_sy_lemma
stable_system
start_glue_evaluation
stem
strict_lemma
strict_qua
strict_qua2
strict_qua2_imply_strict_qua
strict_qua2_interior_pos
strict_qua_in_oct
strip_le_lemma
strip_lt_lemma
sub6
sub_1
sub_aff
sub_partial_lemma'
sub_second_lemma'
sub_union
subcritical_edgeX
subdiv_v39
subgroup
subpred
subrel
subseq
subset_aff
subset_by_inequality_fan
subset_cyclic_set_fan
subset_d_fan
subset_inter
subspace
suc_eq_th
sum1_azim_fan
sum2_azim_fan
sum3_azim_fan
sum4_azim_fan
sum5_azim_fan
sum_even
sum_in_seg
sum_measure_ccube
sum_measure_voronoi_le_ball
sum_odd
sumn
sumsquaresnot0
sup_property1
supp
support_darts
support_list
support_loop_sub_dart
support_node
surfR
surfR126d
surfRdyc2
surfRy
surf_x
surfy
surj2_cube
surj2_map1
surj_cube
surj_map_to_ball
surj_map_to_nua_kg
surj_map_to_voronoi
surj_map_to_voronoi_db
surrounded_node
sv
sv0
svan
switch_lemma_le
switch_lemma_let
switch_lemma_lt
sym_line01_fan
sym_line02_fan
sym_line0_fan
sym_line1_fan
sym_line_fan
sym_line_fan0
sym_line_fan1
symmetric