HOL html

Files Index

Theorems Index

V (theorems)

VALID
VALID_COUNTINGS
VALID_COUNTINGS_0
VALID_COUNTINGS_SUC
VALID_PATH_CIRCLEPATH
VALID_PATH_COMPOSE
VALID_PATH_IMP_PATH
VALID_PATH_JOIN
VALID_PATH_JOIN_EQ
VALID_PATH_LINEPATH
VALID_PATH_NEGATEPATH
VALID_PATH_PARTCIRCLEPATH
VALID_PATH_REVERSEPATH
VALID_PATH_SHIFTPATH
VALID_PATH_SUBPATH
VALID_PATH_VECTOR_POLYNOMIAL_FUNCTION
VALMOD
VALMOD_BASIC
VALMOD_REPEAT
VALMOD_SWAP
VALMOD_TRIVIAL
VALMOD_VALMOD_BASIC
VANGLE
VANGLE_EQ_PI
VANGLE_RANGE
VARIANT
VARIANT_EXISTS
VARIANT_FINITE
VARIANT_THM
VARIATION_1
VARIATION_2
VARIATION_3
VARIATION_EQ
VARIATION_EQUAL_LEMMA
VARIATION_OFFSET
VARIATION_OPPOSITE_ENDS
VARIATION_POSITIVE_ROOT_FACTOR
VARIATION_POSITIVE_ROOT_MULTIPLE_FACTOR
VARIATION_POSITIVE_ROOT_MULTIPLICITY_FACTOR
VARIATION_SET_FINITE
VARIATION_SPLIT
VARIATION_SPLIT_NUMSEG
VARIATION_SUBSET
VARS
VARS_FINITE
VAR_ASG
VAR_EXP
VAR_FST_ASG
VAR_INDEXVAR
VAR_INDEX_ASG
VAR_INDEX_EXP
VAR_SND_ASG
VC_ABORT
VC_ADO_MEASURE
VC_ADO_VARIANT
VC_ASSERT
VC_ASSIGN
VC_AWHILE_MEASURE
VC_AWHILE_VARIANT
VC_IF
VC_ITE
VC_SEQ_ASSERT_LEFT
VC_SEQ_ASSERT_MIDDLE
VC_SEQ_ASSERT_RIGHT
VC_SEQ_ASSIGN_LEFT
VC_SEQ_ASSIGN_RIGHT
VC_SKIP
VECTOR_1
VECTOR_2
VECTOR_3
VECTOR_4
VECTOR_ADD_AC
VECTOR_ADD_ASSOC
VECTOR_ADD_COMPONENT
VECTOR_ADD_LDISTRIB
VECTOR_ADD_LID
VECTOR_ADD_LINV
VECTOR_ADD_RDISTRIB
VECTOR_ADD_RID
VECTOR_ADD_RINV
VECTOR_ADD_SUB
VECTOR_ADD_SYM
VECTOR_AFFINITY_EQ
VECTOR_ANGLE
VECTOR_ANGLE_1
VECTOR_ANGLE_ANGLE
VECTOR_ANGLE_ARG
VECTOR_ANGLE_COMPLEX_LMUL
VECTOR_ANGLE_EQ
VECTOR_ANGLE_EQ_0
VECTOR_ANGLE_EQ_0_DIST
VECTOR_ANGLE_EQ_0_LEFT
VECTOR_ANGLE_EQ_0_RIGHT
VECTOR_ANGLE_EQ_PI
VECTOR_ANGLE_EQ_PI_DIST
VECTOR_ANGLE_EQ_PI_LEFT
VECTOR_ANGLE_EQ_PI_RIGHT
VECTOR_ANGLE_LINEAR_IMAGE_EQ
VECTOR_ANGLE_LMUL
VECTOR_ANGLE_LNEG
VECTOR_ANGLE_NEG2
VECTOR_ANGLE_RANGE
VECTOR_ANGLE_REFL
VECTOR_ANGLE_RMUL
VECTOR_ANGLE_RNEG
VECTOR_ANGLE_SYM
VECTOR_CHOOSE_DIST
VECTOR_CHOOSE_SIZE
VECTOR_COMPONENTWISE
VECTOR_DERIVATIVE_AT
VECTOR_DERIVATIVE_CIRCLEPATH
VECTOR_DERIVATIVE_CONST_AT
VECTOR_DERIVATIVE_LINEPATH_AT
VECTOR_DERIVATIVE_LINEPATH_WITHIN
VECTOR_DERIVATIVE_PARTCIRCLEPATH
VECTOR_DERIVATIVE_UNIQUE_AT
VECTOR_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL
VECTOR_DERIVATIVE_WITHIN_CLOSED_INTERVAL
VECTOR_DERIVATIVE_WITHIN_INTERIOR
VECTOR_DERIVATIVE_WORKS
VECTOR_DIFF_CHAIN_AT
VECTOR_DIFF_CHAIN_WITHIN
VECTOR_EQ
VECTOR_EQ_ADDR
VECTOR_EQ_AFFINITY
VECTOR_EQ_DOT_SPAN
VECTOR_EQ_LDOT
VECTOR_EQ_NEG2
VECTOR_EQ_RDOT
VECTOR_EXPAND_1
VECTOR_EXPAND_2
VECTOR_EXPAND_3
VECTOR_EXPAND_4
VECTOR_IN_ORTHOGONAL_BASIS
VECTOR_IN_ORTHOGONAL_SPANNINGSET
VECTOR_IN_ORTHONORMAL_BASIS
VECTOR_MATRIX_MUL_TRANSP
VECTOR_MUL_ASSOC
VECTOR_MUL_COMPONENT
VECTOR_MUL_EQ_0
VECTOR_MUL_LCANCEL
VECTOR_MUL_LCANCEL_IMP
VECTOR_MUL_LID
VECTOR_MUL_LNEG
VECTOR_MUL_LZERO
VECTOR_MUL_RCANCEL
VECTOR_MUL_RCANCEL_IMP
VECTOR_MUL_RNEG
VECTOR_MUL_RZERO
VECTOR_NEG_0
VECTOR_NEG_COMPONENT
VECTOR_NEG_EQ_0
VECTOR_NEG_MINUS1
VECTOR_NEG_NEG
VECTOR_NEG_SUB
VECTOR_ONE
VECTOR_POLYNOMIAL_FUNCTION_ADD
VECTOR_POLYNOMIAL_FUNCTION_CMUL
VECTOR_POLYNOMIAL_FUNCTION_COMPONENT
VECTOR_POLYNOMIAL_FUNCTION_CONST
VECTOR_POLYNOMIAL_FUNCTION_ID
VECTOR_POLYNOMIAL_FUNCTION_LIFT
VECTOR_POLYNOMIAL_FUNCTION_MUL
VECTOR_POLYNOMIAL_FUNCTION_NEG
VECTOR_POLYNOMIAL_FUNCTION_SUB
VECTOR_POLYNOMIAL_FUNCTION_VSUM
VECTOR_POLYNOMIAL_FUNCTION_o
VECTOR_SUB
VECTOR_SUB_ADD
VECTOR_SUB_ADD2
VECTOR_SUB_COMPONENT
VECTOR_SUB_ELIM_THM
VECTOR_SUB_EQ
VECTOR_SUB_LDISTRIB
VECTOR_SUB_LZERO
VECTOR_SUB_PROJECT_ORTHOGONAL
VECTOR_SUB_RADD
VECTOR_SUB_RDISTRIB
VECTOR_SUB_REFL
VECTOR_SUB_RZERO
VECTOR_VARIATION_COMBINE
VECTOR_VARIATION_CONST
VECTOR_VARIATION_CONST_EQ
VECTOR_VARIATION_CONTINUOUS
VECTOR_VARIATION_CONTINUOUS_LEFT
VECTOR_VARIATION_CONTINUOUS_RIGHT
VECTOR_VARIATION_EQ
VECTOR_VARIATION_GE_DROP_FUNCTION
VECTOR_VARIATION_GE_NORM_FUNCTION
VECTOR_VARIATION_INTEGRAL_NORM_DERIVATIVE
VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE
VECTOR_VARIATION_MONOTONE
VECTOR_VARIATION_NEG
VECTOR_VARIATION_ON_DIVISION
VECTOR_VARIATION_ON_NULL
VECTOR_VARIATION_POS_LE
VECTOR_VARIATION_REFLECT
VECTOR_VARIATION_REFLECT_INTERVAL
VECTOR_VARIATION_TRIANGLE
VECTOR_ZERO
VEC_COMPONENT
VEC_EQ
VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH
VERTICES_LINEAR_IMAGE
VERTICES_TRANSLATION
VFREE_IN
VFREE_IN_ACONV
VFREE_IN_FINITE
VFREE_IN_FINITE_ALT
VFREE_IN_RACONV
VFREE_IN_VSUBST
VOLUME_BALL
VOLUME_BALL_WEDGE
VOLUME_CBALL
VOLUME_CONIC_CAP
VOLUME_CONIC_CAP_COMPL
VOLUME_CONIC_CAP_STRONG
VOLUME_CONIC_CAP_WEDGE
VOLUME_CONIC_CAP_WEDGE_MEDIUM
VOLUME_CONIC_CAP_WEDGE_WEAK
VOLUME_FRUSTT
VOLUME_FRUSTT_STRONG
VOLUME_FRUSTT_WEDGE
VOLUME_OF_CLOSED_TETRAHEDRON
VOLUME_OF_TETRAHEDRON
VOLUME_SOLID_TRIANGLE
VOTE_NOT_EQ
VSUBST
VSUBST_HAS_TYPE
VSUBST_WELLTYPED
VSUM
VSUM_0
VSUM_1
VSUM_2
VSUM_3
VSUM_4
VSUM_ADD
VSUM_ADD_GEN
VSUM_ADD_NUMSEG
VSUM_ADD_SPLIT
VSUM_BIJECTION
VSUM_CASES
VSUM_CASES_1
VSUM_CLAUSES
VSUM_CLAUSES_LEFT
VSUM_CLAUSES_NUMSEG
VSUM_CLAUSES_RIGHT
VSUM_CMUL_NUMSEG
VSUM_COMBINE_L
VSUM_COMBINE_R
VSUM_COMPLEX_LMUL
VSUM_COMPLEX_RMUL
VSUM_COMPONENT
VSUM_CONST
VSUM_CONST_NUMSEG
VSUM_CONTENT_NULL
VSUM_CX
VSUM_CX_NUMSEG
VSUM_DELETE
VSUM_DELETE_CASES
VSUM_DELTA
VSUM_DIFF
VSUM_DIFFS
VSUM_DIFFS_ALT
VSUM_DIFF_LEMMA
VSUM_EQ
VSUM_EQ_0
VSUM_EQ_GENERAL
VSUM_EQ_GENERAL_INVERSES
VSUM_EQ_NUMSEG
VSUM_EQ_SUPERSET
VSUM_GP
VSUM_GP_BASIC
VSUM_GP_MULTIPLIED
VSUM_GP_OFFSET
VSUM_GROUP
VSUM_IMAGE
VSUM_IMAGE_GEN
VSUM_IMAGE_NONZERO
VSUM_INCL_EXCL
VSUM_INJECTION
VSUM_LMUL
VSUM_LNORM
VSUM_NEG
VSUM_NONZERO_IMAGE_LEMMA
VSUM_NORM
VSUM_NORM_ALLSUBSETS_BOUND
VSUM_NORM_BOUND
VSUM_NORM_LE
VSUM_NORM_TRIANGLE
VSUM_OFFSET
VSUM_OFFSET_0
VSUM_OVER_TAGGED_DIVISION_LEMMA
VSUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA
VSUM_PAIR
VSUM_PAIR_0
VSUM_PARTIAL_PRE
VSUM_PARTIAL_SUC
VSUM_REAL
VSUM_RESTRICT
VSUM_RESTRICT_SET
VSUM_RMUL
VSUM_SING
VSUM_SING_NUMSEG
VSUM_SUB
VSUM_SUB_NUMSEG
VSUM_SUC
VSUM_SUPERSET
VSUM_SUPPORT
VSUM_SWAP
VSUM_SWAP_NUMSEG
VSUM_TRIV_NUMSEG
VSUM_UNION
VSUM_UNIONS_NONZERO
VSUM_UNION_LZERO
VSUM_UNION_NONZERO
VSUM_UNION_RZERO
VSUM_VMUL
VSUM_VSUM_DIVISORS
VSUM_VSUM_PRODUCT
V_TYBIJ
v_compat_bij2
v_edge_ball
v_edge_cases
v_edge_closed_ball
v_edge_closure
v_edge_col
v_edge_convex
v_edge_cpoint
v_edge_disj
v_edge_euclid
v_edge_floor
v_edge_inj
v_edge_inter
v_edge_pointI
v_edge_pointIv2
v_edge_subset
v_simple_polygonal
v_translate_bij
v_translate_cont
v_translate_h
v_translate_hom
v_translate_inv
v_translate_point
v_translate_v
v_tybij_th
valid
valid_countings
valid_path
valmod
value
vangle
variant_def
variation
vc_edge_closed
vc_edge_convex
vc_edge_inter
vc_edge_pointI
vec
vector
vector_add
vector_angle
vector_derivative
vector_matrix_mul
vector_mul
vector_neg
vector_norm
vector_polynomial_function
vector_sub
vector_variation
version1
version2
vertices
vol_ball_wedge
vol_conic_cap_wedge
vol_conv
vol_frustt_wedge
vol_rect
vol_solid_triangle
volume_props
vote_INDUCT,vote_RECURSION
vsum