HOL html

Files Index

Theorems Index

P (theorems)

PAIR
PAIRED_ETA_THM
PAIRED_EXT
PAIRSUP_COFUNCTIONAL
PAIRSUP_COMPOSE
PAIRSUP_CONVERSE
PAIRSUP_DOMRAN
PAIRSUP_EMPTY
PAIRSUP_EXPLICIT
PAIRSUP_FUNCTIONAL
PAIRSUP_ID
PAIRSUP_INSERT
PAIRWISE
PAIRWISE_DISJOINT_COMPONENTS
PAIRWISE_DISJOINT_HYPERPLANE_CELLS
PAIRWISE_EMPTY
PAIRWISE_IMAGE
PAIRWISE_INSERT
PAIRWISE_MONO
PAIRWISE_ORTHOGONAL_IMP_FINITE
PAIRWISE_ORTHOGONAL_INDEPENDENT
PAIRWISE_SING
PAIR_BETA_THM
PAIR_CLAUSES
PAIR_EQ
PAIR_EXISTS_THM
PAIR_INJ
PAIR_IN_LEVEL
PAIR_LEMMA
PAIR_LEMMAv2
PAIR_SPLIT
PAIR_SURJECTIVE
PARALLEL
PARALLEL_PROJL_HOMOL
PARALLEL_PROJP_HOMOP
PARALLEL_PROJP_HOMOP_EXPLICIT
PARDIR_EQUIV
PARITY_EXP
PARITY_LEMMA
PARITY_POW_LT
PARTIAL_DIVISION_EXTEND
PARTIAL_DIVISION_EXTEND_1
PARTIAL_DIVISION_EXTEND_INTERVAL
PARTIAL_DIVISION_OF_TAGGED_DIVISION
PARTIAL_SUMS_COMPONENT_LE_INFSUM
PARTIAL_SUMS_DROP_LE_INFSUM
PARTITIONS
PARTITIONS_BOUND
PARTITION_LINE_APPEND
PARTITION_LINE_LENGTH
PARTITION_LINE_LENGTH_TL
PARTITION_LINE_NOT_NIL
PAR_ATOM
PAR_INT
PAR_PAR
PAR_SEQ
PASCAL
PASCAL_AFFINE
PASCAL_AFFINE_CIRCLE
PASCAL_DIRECT
PASSOC_DEF
PASTECART_ADD
PASTECART_AS_ORTHOGONAL_SUM
PASTECART_CMUL
PASTECART_EQ
PASTECART_EQ_VEC
PASTECART_FST_SND
PASTECART_INJ
PASTECART_IN_INTERIOR_SUBTOPOLOGY
PASTECART_IN_PCROSS
PASTECART_NEG
PASTECART_SUB
PASTECART_VEC
PASTECART_VSUM
PASTING_LEMMA
PASTING_LEMMA_CLOSED
PASTING_LEMMA_EXISTS
PASTING_LEMMA_EXISTS_CLOSED
PATHFINISH_CIRCLEPATH
PATHFINISH_COMPOSE
PATHFINISH_IN_PATH_IMAGE
PATHFINISH_JOIN
PATHFINISH_LINEAR_IMAGE
PATHFINISH_LINEPATH
PATHFINISH_NEGATEPATH
PATHFINISH_PARTCIRCLEPATH
PATHFINISH_POLYGONAL_PATH
PATHFINISH_REVERSEPATH
PATHFINISH_SHIFTPATH
PATHFINISH_SUBPATH
PATHFINISH_TRANSLATION
PATHINTEGRAL_CONVEX_PRIMITIVE
PATHSTART_CIRCLEPATH
PATHSTART_COMPOSE
PATHSTART_IN_PATH_IMAGE
PATHSTART_JOIN
PATHSTART_LINEAR_IMAGE_EQ
PATHSTART_LINEPATH
PATHSTART_NEGATEPATH
PATHSTART_PARTCIRCLEPATH
PATHSTART_POLYGONAL_PATH
PATHSTART_REVERSEPATH
PATHSTART_SHIFTPATH
PATHSTART_SUBPATH
PATHSTART_TRANSLATION
PATHS_MONO
PATH_APPROX_VECTOR_POLYNOMIAL_FUNCTION
PATH_ASSOC
PATH_COMPONENT
PATH_COMPONENT_DISJOINT
PATH_COMPONENT_EMPTY
PATH_COMPONENT_EQ
PATH_COMPONENT_EQ_CONNECTED_COMPONENT
PATH_COMPONENT_EQ_EMPTY
PATH_COMPONENT_EQ_EQ
PATH_COMPONENT_IMP_HOMOTOPIC_POINTS
PATH_COMPONENT_IN
PATH_COMPONENT_LINEAR_IMAGE
PATH_COMPONENT_MAXIMAL
PATH_COMPONENT_MONO
PATH_COMPONENT_OF_SUBSET
PATH_COMPONENT_PATH_COMPONENT
PATH_COMPONENT_PATH_IMAGE_PATHSTART
PATH_COMPONENT_REFL
PATH_COMPONENT_REFL_EQ
PATH_COMPONENT_SET
PATH_COMPONENT_SUBSET
PATH_COMPONENT_SUBSET_CONNECTED_COMPONENT
PATH_COMPONENT_SYM
PATH_COMPONENT_SYM_EQ
PATH_COMPONENT_TRANS
PATH_COMPONENT_TRANSLATION
PATH_COMPONENT_UNIV
PATH_COMPOSE_JOIN
PATH_COMPOSE_REVERSEPATH
PATH_CONNECTED_ANNULUS
PATH_CONNECTED_ARCWISE
PATH_CONNECTED_ARC_COMPLEMENT
PATH_CONNECTED_COMPLEMENT_ABSOLUTE_RETRACT
PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX
PATH_CONNECTED_COMPLEMENT_CARD_LT
PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_CONVEX_COMPACT
PATH_CONNECTED_COMPONENT_SET
PATH_CONNECTED_CONTINUOUS_IMAGE
PATH_CONNECTED_CONVEX_DIFF_CARD_LT
PATH_CONNECTED_DIFF_BALL
PATH_CONNECTED_EMPTY
PATH_CONNECTED_EQ_CONNECTED
PATH_CONNECTED_EQ_CONNECTED_LPC
PATH_CONNECTED_EQ_HOMOTOPIC_POINTS
PATH_CONNECTED_IFF_PATH_COMPONENT
PATH_CONNECTED_IMP_CONNECTED
PATH_CONNECTED_INTERVAL
PATH_CONNECTED_LINEAR_IMAGE
PATH_CONNECTED_LINEAR_IMAGE_EQ
PATH_CONNECTED_LINEPATH
PATH_CONNECTED_NEGATIONS
PATH_CONNECTED_OPEN_DELETE
PATH_CONNECTED_OPEN_DIFF_CARD_LT
PATH_CONNECTED_OPEN_DIFF_COUNTABLE
PATH_CONNECTED_OPEN_IN_DIFF_CARD_LT
PATH_CONNECTED_PATH_COMPONENT
PATH_CONNECTED_PATH_IMAGE
PATH_CONNECTED_PCROSS
PATH_CONNECTED_PCROSS_EQ
PATH_CONNECTED_PUNCTURED_BALL
PATH_CONNECTED_PUNCTURED_UNIVERSE
PATH_CONNECTED_SCALING
PATH_CONNECTED_SEGMENT
PATH_CONNECTED_SEMIOPEN_SEGMENT
PATH_CONNECTED_SING
PATH_CONNECTED_SPHERE
PATH_CONNECTED_SPHERE_EQ
PATH_CONNECTED_SUMS
PATH_CONNECTED_TRANSLATION
PATH_CONNECTED_TRANSLATION_EQ
PATH_CONNECTED_UNION
PATH_CONNECTED_UNIV
PATH_CONTAINS_ARC
PATH_CONTINUOUS_IMAGE
PATH_EQ
PATH_IMAGE_CIRCLEPATH
PATH_IMAGE_COMPOSE
PATH_IMAGE_JOIN
PATH_IMAGE_JOIN_SUBSET
PATH_IMAGE_LINEAR_IMAGE
PATH_IMAGE_LINEPATH
PATH_IMAGE_NEGATEPATH
PATH_IMAGE_NONEMPTY
PATH_IMAGE_PARTCIRCLEPATH
PATH_IMAGE_PARTCIRCLEPATH_SUBSET
PATH_IMAGE_POLYGONAL_PATH_ROTATE
PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL
PATH_IMAGE_POLYGONAL_PATH_SUBSET_SEGMENTS
PATH_IMAGE_REVERSEPATH
PATH_IMAGE_SHIFTPATH
PATH_IMAGE_SUBPATH
PATH_IMAGE_SUBPATH_GEN
PATH_IMAGE_SUBPATH_SUBSET
PATH_IMAGE_SYM
PATH_IMAGE_TRANSLATION
PATH_INTEGRABLE_ADD
PATH_INTEGRABLE_COMPLEX_DIV
PATH_INTEGRABLE_COMPLEX_LMUL
PATH_INTEGRABLE_COMPLEX_RMUL
PATH_INTEGRABLE_CONTINUOUS_CIRCLEPATH
PATH_INTEGRABLE_CONTINUOUS_LINEPATH
PATH_INTEGRABLE_CONTINUOUS_PARTCIRCLEPATH
PATH_INTEGRABLE_EQ
PATH_INTEGRABLE_HOLOMORPHIC
PATH_INTEGRABLE_HOLOMORPHIC_SIMPLE
PATH_INTEGRABLE_INVERSEDIFF
PATH_INTEGRABLE_JOIN
PATH_INTEGRABLE_NEG
PATH_INTEGRABLE_NEGATEPATH
PATH_INTEGRABLE_ON
PATH_INTEGRABLE_REVERSEPATH
PATH_INTEGRABLE_REVERSEPATH_EQ
PATH_INTEGRABLE_SUB
PATH_INTEGRABLE_SUBPATH
PATH_INTEGRABLE_SUBPATH_REFL
PATH_INTEGRABLE_VSUM
PATH_INTEGRAL_0
PATH_INTEGRAL_ADD
PATH_INTEGRAL_BOUND_EXISTS
PATH_INTEGRAL_BOUND_LINEPATH
PATH_INTEGRAL_COMPLEX_DIV
PATH_INTEGRAL_COMPLEX_LMUL
PATH_INTEGRAL_COMPLEX_RMUL
PATH_INTEGRAL_CONST_LINEPATH
PATH_INTEGRAL_EQ
PATH_INTEGRAL_EQ_0
PATH_INTEGRAL_INTEGRAL
PATH_INTEGRAL_JOIN
PATH_INTEGRAL_LOCAL_PRIMITIVE
PATH_INTEGRAL_LOCAL_PRIMITIVE_ANY
PATH_INTEGRAL_LOCAL_PRIMITIVE_LEMMA
PATH_INTEGRAL_MIDPOINT
PATH_INTEGRAL_NEG
PATH_INTEGRAL_PRIMITIVE
PATH_INTEGRAL_PRIMITIVE_LEMMA
PATH_INTEGRAL_REVERSEPATH
PATH_INTEGRAL_REVERSE_LINEPATH
PATH_INTEGRAL_SHIFTPATH
PATH_INTEGRAL_SPLIT
PATH_INTEGRAL_SPLIT_LINEPATH
PATH_INTEGRAL_SUB
PATH_INTEGRAL_SUBPATH_COMBINE
PATH_INTEGRAL_SUBPATH_INTEGRAL
PATH_INTEGRAL_SUBPATH_REFL
PATH_INTEGRAL_SWAP
PATH_INTEGRAL_TRIVIAL
PATH_INTEGRAL_UNIFORM_LIMIT
PATH_INTEGRAL_UNIFORM_LIMIT_CIRCLEPATH
PATH_INTEGRAL_UNIQUE
PATH_INTEGRAL_VSUM
PATH_JOIN
PATH_JOIN_EQ
PATH_JOIN_IMP
PATH_JOIN_PATH_ENDS
PATH_LENGTH_DIFFERENTIABLE
PATH_LENGTH_JOIN
PATH_LENGTH_REVERSEPATH
PATH_LENGTH_VALID_PATH
PATH_LINEAR_IMAGE_EQ
PATH_LINEPATH
PATH_PARTCIRCLEPATH
PATH_POLYGONAL_PATH
PATH_REVERSEPATH
PATH_SHIFTPATH
PATH_SUBPATH
PATH_SYM
PATH_TRANSLATION_EQ
PATH_VECTOR_POLYNOMIAL_FUNCTION
PA_SOUND
PBR_LEMMA
PCROSS
PCROSS_AS_ORTHOGONAL_SUM
PCROSS_EMPTY
PCROSS_EQ
PCROSS_EQ_EMPTY
PCROSS_INTER
PCROSS_INTERVAL
PCROSS_MONO
PCROSS_UNION
PDA_LENGTH
PDIFF_NEG_LAST
PDIFF_POS_LAST
PDI_COEFF_FACT
PDI_DEF
PDI_LENGTH_AUX
PDI_LENGTH_NIL
PDI_LENGTH_THM
PDI_POLYDIFF_SUC_LEMMA
PDI_POLY_DIFF_COMM
PELL_INDUCTION
PERFECT_EUCLID
PERFECT_EULER
PERMUTATION
PERMUTATION_BIJECTIVE
PERMUTATION_COMPOSE
PERMUTATION_COMPOSE_EQ
PERMUTATION_COMPOSE_SWAP
PERMUTATION_COUNT
PERMUTATION_FINITE_SUPPORT
PERMUTATION_I
PERMUTATION_INVERSE
PERMUTATION_INVERSE_COMPOSE
PERMUTATION_INVERSE_WORKS
PERMUTATION_LEMMA
PERMUTATION_LIST_UNIQ
PERMUTATION_MEM
PERMUTATION_NIL
PERMUTATION_PERMUTES
PERMUTATION_SET_OF_LIST
PERMUTATION_SWAP
PERMUTATION_UNIQ_LT
PERMUTED_ALL
PERMUTED_APPEND_SWAP
PERMUTED_CONS_DELETE1
PERMUTED_COUNT
PERMUTED_DELETE1_L
PERMUTED_DELETE1_R
PERMUTED_IMP_PAIRWISE
PERMUTED_LENGTH
PERMUTED_LIST_UNIQ
PERMUTED_MAP
PERMUTED_MEM
PERMUTED_NIL_EQ_NIL
PERMUTED_PAIRWISE
PERMUTED_RFL
PERMUTED_SINGLETON
PERMUTED_SWAP_HEAD
PERMUTED_SYM
PERMUTED_TAIL
PERMUTED_TAIL_IMP
PERMUTED_TRS
PERMUTES_COFUNCTIONAL
PERMUTES_COMPOSE
PERMUTES_CONVERSE
PERMUTES_DOMRAN
PERMUTES_EMPTY
PERMUTES_EXPLICIT
PERMUTES_FINITE_INJECTIVE
PERMUTES_FINITE_SURJECTIVE
PERMUTES_FUNCTIONAL
PERMUTES_I
PERMUTES_ID
PERMUTES_IMAGE
PERMUTES_INDUCT
PERMUTES_INJECTIVE
PERMUTES_INSERT
PERMUTES_INSERT_LEMMA
PERMUTES_INVERSE
PERMUTES_INVERSES
PERMUTES_INVERSES_o
PERMUTES_INVERSE_EQ
PERMUTES_INVERSE_INVERSE
PERMUTES_IN_IMAGE
PERMUTES_IN_NUMSEG
PERMUTES_NUMSET_GE
PERMUTES_NUMSET_LE
PERMUTES_SING
PERMUTES_SUBSET
PERMUTES_SUPERSET
PERMUTES_SURJECTIVE
PERMUTES_SWAP
PERMUTES_UNIV
PERPDIR_WELLDEF
PHI
PHI_0
PHI_1
PHI_2
PHI_ALT
PHI_ANOTHER
PHI_DIFFERENTIABLE
PHI_DIVISORSUM
PHI_FINITE_LEMMA
PHI_LIMIT
PHI_LIMIT_STRONG
PHI_LOWERBOUND_1
PHI_LOWERBOUND_1_STRONG
PHI_LOWERBOUND_2
PHI_MULTIPLICATIVE
PHI_PRIME
PHI_PRIMEPOW
PHI_PRIMEPOW_SUC
PHI_PRIME_EQ
PHI_abs
PI
PI2
PI2_BOUNDS
PICK
PICK_ELEMENTARY_TRIANGLE
PICK_ELEMENTARY_TRIANGLE_0
PICK_TRIANGLE
PICK_TRIANGLE_ALT
PICK_TRIANGLE_FLAT
PIECEWISE_DIFFERENTIABLE_ADD
PIECEWISE_DIFFERENTIABLE_AFFINE
PIECEWISE_DIFFERENTIABLE_CASES
PIECEWISE_DIFFERENTIABLE_COMPOSE
PIECEWISE_DIFFERENTIABLE_NEG
PIECEWISE_DIFFERENTIABLE_ON_IMP_CONTINUOUS_ON
PIECEWISE_DIFFERENTIABLE_ON_SUBSET
PIECEWISE_DIFFERENTIABLE_SUB
PIGEONHOLE_LEMMA
PIGEONHOLE_LEMMA_P12
PII
PII_0
PII_CHANGE
PII_ISQRT_INDUCT
PII_LBOUND
PII_MONO
PII_POS
PII_UBOUND_5
PII_UBOUND_CASES_50
PI_APPROX_32
PI_EST
PI_EST2
PI_NZ
PI_POS
PI_POS_LE
PI_SER
PI_WORKS
PLANETMATH_DIVIDES_FACT_PRIME_1
PLANETMATH_EQN_1_1_1
PLANETMATH_EQN_1_1_2
PLANETMATH_EQN_1_1_3
PLANETMATH_EQN_3
PLANETMATH_EQN_4
PLANETMATH_EQN_5
PLANETMATH_EQN_5_2
PLANETMATH_LEMMA_1
PLANETMATH_LEMMA_2_A
PLANETMATH_LEMMA_2_B
PLANETMATH_THM_5_1
PLANET_MATH_alpha
PLANET_MATH_alpha_1
PLANET_MATH_alpha_2
PLANET_MATH_alpha_3
PLANET_MATH_beta
PLANET_MATH_gamma
PLANE_AFFINE_HULL_3
PLANE_LINEAR_IMAGE
PLANE_LINEAR_IMAGE_EQ
PLANE_TRANSLATION
PLANE_TRANSLATION_EQ
PLATONIC_SOLIDS
PLATONIC_SOLIDS_LIMITS
PLUSINF_MIRROR
PLUS_MOD_REFL
PL_ALL2_LENGTH
PL_BUTLAST
PL_LEM
PL_LEM2
PNEG_AUX_LENGTH
PNEG_AUX_NIL
PNEG_AUX_NORMALIZE_LENGTH
PNEG_CONS
PNEG_LAST
PNEG_LENGTH
PNEG_NIL
PNEG_NONCONSTANT
PNEG_NORMALIZE_LENGTH
PNEG_SING
PNT
PNT_PARTIAL_SUMMATION
POCKLINGTON
POCKLINGTON_ALT
POCKLINGTON_LEMMA
POCKLINGTON_PRIMEFACT
POINCARIFY_KLEINIFY
POINTS_IN_CONVEX_HULL
POINTWISE_ANTISYM
POINT_CLAUSES
POLE_LEMMA
POLE_LEMMA_OPEN
POLE_THEOREM
POLE_THEOREM_0
POLE_THEOREM_ANALYTIC
POLE_THEOREM_ANALYTIC_0
POLE_THEOREM_ANALYTIC_OPEN_SUPERSET
POLE_THEOREM_ANALYTIC_OPEN_SUPERSET_0
POLE_THEOREM_OPEN
POLE_THEOREM_OPEN_0
POLY
POLYDIFF_ADD
POLYFUN_N_ADD
POLYFUN_N_CMUL
POLYFUN_N_CONST
POLYFUN_N_PRODUCT
POLYFUN_N_SUM
POLYGONAL_PATH_CONS_CONS
POLYGONAL_PATH_LINEAR_IMAGE
POLYGONAL_PATH_TRANSLATION
POLYGON_CHOP_IN_TWO
POLYHEDRON_AFFINE_HULL
POLYHEDRON_AFF_GE
POLYHEDRON_AS_CONE_PLUS_CONV
POLYHEDRON_COLLINEAR_FACES
POLYHEDRON_COLLINEAR_FACES_STRONG
POLYHEDRON_CONVEX_CONE_HULL
POLYHEDRON_CONVEX_HULL
POLYHEDRON_EMPTY
POLYHEDRON_EQ_FINITE_EXPOSED_FACES
POLYHEDRON_EQ_FINITE_FACES
POLYHEDRON_HALFSPACE_GE
POLYHEDRON_HALFSPACE_LE
POLYHEDRON_HYPERPLANE
POLYHEDRON_IMP_CLOSED
POLYHEDRON_IMP_CONVEX
POLYHEDRON_INTER
POLYHEDRON_INTERS
POLYHEDRON_INTERVAL
POLYHEDRON_INTER_AFFINE
POLYHEDRON_INTER_AFFINE_MINIMAL
POLYHEDRON_INTER_AFFINE_PARALLEL
POLYHEDRON_INTER_AFFINE_PARALLEL_MINIMAL
POLYHEDRON_INTER_POLYTOPE
POLYHEDRON_LINEAR_IMAGE
POLYHEDRON_LINEAR_IMAGE_EQ
POLYHEDRON_NEGATIONS
POLYHEDRON_POLYTOPE_SUMS
POLYHEDRON_POSITIVE_ORTHANT
POLYHEDRON_RIDGE_TWO_FACETS
POLYHEDRON_SUMS
POLYHEDRON_TRANSLATION_EQ
POLYHEDRON_UNIV
POLYLOG_CONVERGES
POLYLOG_DERIVATIVE
POLYLOG_THM
POLYTOPE_3D_LEMMA
POLYTOPE_CONVEX_HULL
POLYTOPE_EMPTY
POLYTOPE_EQ_BOUNDED_POLYHEDRON
POLYTOPE_FACET_EXISTS
POLYTOPE_FACET_LOWER_BOUND
POLYTOPE_IMP_BOUNDED
POLYTOPE_IMP_CLOSED
POLYTOPE_IMP_COMPACT
POLYTOPE_IMP_CONVEX
POLYTOPE_IMP_POLYHEDRON
POLYTOPE_INTER
POLYTOPE_INTERVAL
POLYTOPE_INTER_POLYHEDRON
POLYTOPE_LINEAR_IMAGE
POLYTOPE_LINEAR_IMAGE_EQ
POLYTOPE_NEGATIONS
POLYTOPE_PCROSS
POLYTOPE_PCROSS_EQ
POLYTOPE_SCALING
POLYTOPE_SCALING_EQ
POLYTOPE_SING
POLYTOPE_SUMS
POLYTOPE_TRANSLATION_EQ
POLYTOPE_UNION_CONVEX_HULL_FACETS
POLYTOPE_VERTEX_LOWER_BOUND
POLY_0
POLY_0_THM
POLY_ADD
POLY_ADD_ASSOC
POLY_ADD_CLAUSES
POLY_ADD_IDENT
POLY_ADD_LENGTH
POLY_ADD_NEUTRAL
POLY_ADD_RZERO
POLY_ADD_SYM
POLY_AT_ZERO
POLY_BOUND_EXISTS
POLY_BOUND_INTERVAL
POLY_CMUL
POLY_CMUL_CLAUSES
POLY_CMUL_EL
POLY_CMUL_EQUALS
POLY_CMUL_HD
POLY_CMUL_LENGTH
POLY_CMUL_LID
POLY_CMUL_MAP
POLY_CMUL_NIL
POLY_CMUL_PDI
POLY_CMUL_POLY_DIFF
POLY_CONST
POLY_CONST_NO_ROOTS
POLY_CONS_EQ
POLY_CONT
POLY_DECOMPOSE
POLY_DECOMPOSE_LEMMA
POLY_DIFF
POLY_DIFFERENTIABLE
POLY_DIFF_ADD
POLY_DIFF_ADD_CONST_COMMUTE
POLY_DIFF_AUX_ADD
POLY_DIFF_AUX_ADD_LEMMA
POLY_DIFF_AUX_CMUL
POLY_DIFF_AUX_DEGREE
POLY_DIFF_AUX_ISZERO
POLY_DIFF_AUX_LEM1
POLY_DIFF_AUX_MUL_LEMMA
POLY_DIFF_AUX_NEG
POLY_DIFF_AUX_NORMAL
POLY_DIFF_AUX_NORMAL2
POLY_DIFF_AUX_POLY_CMUL
POLY_DIFF_CLAUSES
POLY_DIFF_CMUL
POLY_DIFF_DOWN_LEFT
POLY_DIFF_DOWN_LEFT2
POLY_DIFF_DOWN_LEFT3
POLY_DIFF_DOWN_LEFT4
POLY_DIFF_DOWN_LEFT5
POLY_DIFF_DOWN_RIGHT
POLY_DIFF_DOWN_RIGHT2
POLY_DIFF_DOWN_RIGHT3
POLY_DIFF_EXP
POLY_DIFF_EXP_PRIME
POLY_DIFF_ISZERO
POLY_DIFF_LAST_GT
POLY_DIFF_LAST_LEM
POLY_DIFF_LAST_LT
POLY_DIFF_LEMMA
POLY_DIFF_LENGTH
POLY_DIFF_LENGTH_LE_SUC
POLY_DIFF_LENGTH_LT
POLY_DIFF_MUL
POLY_DIFF_MUL_LEMMA
POLY_DIFF_NEG
POLY_DIFF_NORMAL
POLY_DIFF_SING
POLY_DIFF_UP_LEFT
POLY_DIFF_UP_LEFT2
POLY_DIFF_UP_LEFT3
POLY_DIFF_UP_LEFT4
POLY_DIFF_UP_LEFT5
POLY_DIFF_UP_RIGHT
POLY_DIFF_UP_RIGHT2
POLY_DIFF_UP_RIGHT3
POLY_DIFF_WELLDEF
POLY_DIFF_ZERO
POLY_DIVIDES_ADD
POLY_DIVIDES_EXP
POLY_DIVIDES_MUL
POLY_DIVIDES_MUL3
POLY_DIVIDES_PDI
POLY_DIVIDES_PDI2
POLY_DIVIDES_POLY_DIFF
POLY_DIVIDES_POLY_EXP2
POLY_DIVIDES_POLY_MUL_ITER
POLY_DIVIDES_REFL
POLY_DIVIDES_ROOT
POLY_DIVIDES_SUB
POLY_DIVIDES_SUB2
POLY_DIVIDES_TRANS
POLY_DIVIDES_ZERO
POLY_ENTIRE
POLY_ENTIRE_LEMMA
POLY_EXP
POLY_EXP_ADD
POLY_EXP_DIVIDES
POLY_EXP_EQ_0
POLY_EXP_ONE
POLY_EXP_PRIME_EQ_0
POLY_EXP_X_LENGTH
POLY_EXP_X_REC
POLY_INFINITY
POLY_IVT_NEG
POLY_IVT_POS
POLY_LAST_GT
POLY_LAST_LT
POLY_LENGTH_MUL
POLY_LINEAR_DIVIDES
POLY_LINEAR_REM
POLY_MCLAURIN
POLY_MINIMUM_MODULUS
POLY_MINIMUM_MODULUS_DISC
POLY_MONO
POLY_MUL
POLY_MULTIPLE_INTEGER
POLY_MUL_ASSOC
POLY_MUL_CLAUSES
POLY_MUL_HD
POLY_MUL_ITER
POLY_MUL_ITER_HD_FACTORIAL
POLY_MUL_LCANCEL
POLY_MUL_LENGTH
POLY_MUL_LENGTH2
POLY_MUL_LID
POLY_MUL_RID
POLY_MVT
POLY_MVT_ADD
POLY_NEG
POLY_NEG_CLAUSES
POLY_NEG_NEG
POLY_NEG_NIL
POLY_NORMALIZE
POLY_NORMALIZE_EQ
POLY_NORMALIZE_EQ_LEMMA
POLY_NORMALIZE_ZERO
POLY_NUKE
POLY_NUKE_HD_NONZERO
POLY_NUKE_ROOT
POLY_NUKE_ZERO
POLY_OFFSET
POLY_OFFSET_LEMMA
POLY_ORDER
POLY_ORDER_EXISTS
POLY_PNEG
POLY_PNEG_AUX
POLY_PNEG_AUX_SUC
POLY_PNEG_LAST
POLY_PNEG_LAST2
POLY_PNEG_NEG
POLY_PRIMES
POLY_PRIME_EQ_0
POLY_REPLICATE_APPEND
POLY_ROOTS_FINITE
POLY_ROOTS_FINITE_LEMMA
POLY_ROOTS_FINITE_SET
POLY_ROOTS_INDEX_LEMMA
POLY_ROOTS_INDEX_LENGTH
POLY_ROOT_SEPARATE_LE
POLY_ROOT_SEPARATE_LT
POLY_SHIFT
POLY_SHIFT_DEF
POLY_SHIFT_LENGTH
POLY_SING
POLY_SQUAREFREE_DECOMP
POLY_SQUAREFREE_DECOMP_ORDER
POLY_SUB
POLY_SUM_EQUIV
POLY_TAYLOR
POLY_UB
POLY_X
POLY_X_NOT_POLY_NIL
POLY_ZERO
POLY_ZERO_LEMMA
POSET_FLEQ
POSET_RESTRICTED_SUBSET
POSITIVE_DIFF_LEMMA
POS_NAT_POW
POS_POW
POWDIFF
POWDIFF_LEMMA
POWERSET
POWERSET_CLAUSES
POWERSET_EXISTS
POWER_REAL_SERIES_CONV_IMP_ABSCONV_WEAK
POWER_SERIES_ANALYTIC
POWER_SERIES_AND_DERIVATIVE
POWER_SERIES_AND_DERIVATIVE_0
POWER_SERIES_CONV_IMP_ABSCONV
POWER_SERIES_CONV_IMP_ABSCONV_WEAK
POWER_SERIES_HOLOMORPHIC
POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ
POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1
POWREV
POWSER_0
POWSER_EQUAL
POWSER_EQUAL_0
POWSER_INSIDE
POWSER_INSIDEA
POWSER_LIMIT_0
POWSER_LIMIT_0_STRONG
POW_0
POW_1
POW_2
POW_2_CSQRT
POW_2_LE1
POW_2_LT
POW_2_SQRT
POW_2_SQRT_ABS
POW_ABS
POW_ADD
POW_EQ
POW_INT_NEG_1
POW_INV
POW_LE
POW_LT
POW_M1
POW_MINUS1
POW_MUL
POW_NEG_1
POW_NZ
POW_PLUS1
POW_POS
POW_POS_LT
POW_PROD_SUM
POW_ROOT_POS
POW_UNB
POW_UNBB_CON
POW_UNB_CON
POW_ZERO
POW_ZERO_EQ
PRE
PRESERVES_LEBESGUE_MEASURABLE_IMP_PRESERVES_NEGLIGIBLE
PRESERVES_NORM_INJECTIVE
PRESERVES_NORM_PRESERVES_DOT
PRE_ELIM_THM
PRE_ELIM_THM'
PRE_LEM
PRE_def
PRIME
PRIMEPOW_0
PRIMEPOW_FACTOR
PRIMEPOW_GE_2
PRIMEPOW_ODD_EVEN
PRIMERECIP_DIVERGES
PRIMERECIP_DIVERGES_NUMSEG
PRIMERECIP_HARMONIC_LBOUND
PRIMERECIP_LBOUND
PRIMES_FINITE
PRIMES_INFINITE
PRIME_0
PRIME_1
PRIME_2
PRIME_4X
PRIME_ATMOST_ALT
PRIME_COPRIME
PRIME_COPRIME_CASES
PRIME_COPRIME_EQ
PRIME_COPRIME_LT
PRIME_COPRIME_STRONG
PRIME_DIVEXP
PRIME_DIVEXP_EQ
PRIME_DIVEXP_N
PRIME_DIVIDES_NPRODUCT
PRIME_DIVISOR_SQRT
PRIME_DIVPROD
PRIME_DIVPROD_EQ
PRIME_DIVPROD_POW
PRIME_EXP
PRIME_FACTOR
PRIME_FACTOR_INDUCT
PRIME_FACTOR_LT
PRIME_GE_2
PRIME_IMP_NZ
PRIME_ODD
PRIME_POWER_EXISTS
PRIME_POWER_EXP
PRIME_POWER_MULT
PRIME_PRIMEPOW
PRIME_PRIME_FACTOR
PRIME_PRIME_FACTOR_SQRT
PRIME_SQUARE
PRIME_XYZ_NONZERO
PRIMITIVE_ROOTS_MODULO_PRIME
PRIMITIVE_ROOT_DOUBLE_LEMMA
PRIMITIVE_ROOT_EXISTS
PRIMITIVE_ROOT_EXISTS_NONTRIVIAL
PRIMITIVE_ROOT_MODULO_0
PRIMITIVE_ROOT_MODULO_1
PRIMITIVE_ROOT_MODULO_2
PRIMITIVE_ROOT_MODULO_4
PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW
PRIMITIVE_ROOT_MODULO_PRIME
PRIMITIVE_ROOT_MODULO_PRIMEPOW
PRIMITIVE_ROOT_MODULO_PRIMEPOWS
PRIMREC_SIGMA
PRODUCT
PRODUCT_1
PRODUCT_2
PRODUCT_3
PRODUCT_4
PRODUCT_ABS
PRODUCT_ADD_SPLIT
PRODUCT_ASSOCIATIVE
PRODUCT_CLAUSES
PRODUCT_CLAUSES_LEFT
PRODUCT_CLAUSES_NUMSEG
PRODUCT_CLAUSES_RIGHT
PRODUCT_CLOSED
PRODUCT_CONST
PRODUCT_CONST_NUMSEG
PRODUCT_CONST_NUMSEG_1
PRODUCT_DIV
PRODUCT_DIV_NUMSEG
PRODUCT_EQ
PRODUCT_EQ_0
PRODUCT_EQ_0_NUMSEG
PRODUCT_EQ_1
PRODUCT_EQ_1_NUMSEG
PRODUCT_EQ_NUMSEG
PRODUCT_IMAGE
PRODUCT_INHABITED
PRODUCT_INV
PRODUCT_LE
PRODUCT_LE_1
PRODUCT_LE_NUMSEG
PRODUCT_MBASIS
PRODUCT_MBASIS_SING
PRODUCT_MUL
PRODUCT_MUL_NUMSEG
PRODUCT_NEG
PRODUCT_NEG_NUMSEG
PRODUCT_NEG_NUMSEG_1
PRODUCT_OFFSET
PRODUCT_ONE
PRODUCT_PAIRUP
PRODUCT_PAIRUP_INDUCT
PRODUCT_PERMUTE
PRODUCT_PERMUTE_NUMSEG
PRODUCT_POS_LE
PRODUCT_POS_LE_NUMSEG
PRODUCT_POS_LT
PRODUCT_POS_LT_NUMSEG
PRODUCT_POW_NSUM
PRODUCT_SING
PRODUCT_SING_NUMSEG
PRODUCT_SPECIAL
PRODUCT_SPLIT_2
PRODUCT_UNION
PROD_ABS
PROD_CMUL
PROD_EQ
PROD_MUL
PROD_POS
PROD_POS_GEN
PROD_TWO
PROD_ZERO
PROFORMA_BOTH
PROFORMA_LEFT
PROFORMA_RIGHT
PROJECTIVE_CONIC_BRACKET
PROJL_TOTAL
PROJP_TOTAL
PROPERTIES_POLYGONAL_PATH_SNOC
PROPERTY_EMPTY_INTERVAL
PROPER_MAP
PROPER_MAP_FROM_COMPACT
PROV
PROV1
PROVABLE_CLOSURE
PROVABLE_GENERALIZE
PROVE
PROVES_MONO
PROV_DEFINABLE
PROV_LEMMA1
PROV_LEMMA2
PROV_THM
PROV_THM_STRONG
PSEQ
PSEQ_1
PSEQ_BOUND
PSEQ_SPLIT
PSI_0
PSI_BOUND
PSI_BOUNDS_INDUCT
PSI_BOUNDS_LN_FACT
PSI_BOUNDS_SUSTAINED
PSI_BOUNDS_SUSTAINED_INDUCT
PSI_BOUND_EXP
PSI_BOUND_INDUCT
PSI_DOUBLE_LEMMA
PSI_EXPANSION_CUTOFF
PSI_LBOUND_3_5
PSI_MONO
PSI_POS
PSI_RESIDUES_COMPARE
PSI_RESIDUES_COMPARE_2
PSI_SPLIT
PSI_SQRT
PSI_THETA
PSI_UBOUND_128
PSI_UBOUND_128_LOG
PSI_UBOUND_30
PSI_UBOUND_3_2
PSI_UBOUND_LOG
PSUBSET
PSUBSET_ALT
PSUBSET_INSERT_SUBSET
PSUBSET_IRREFL
PSUBSET_MEMBER
PSUBSET_SUBSET_TRANS
PSUBSET_TRANS
PSUBSET_UNIV
PSUM_ITERATE
PSUM_SUM
PSUM_SUM_NUMSEG
PTOLEMY
PULL_CASES_THM
PULL_CASES_THM_NZ
PUSHIN_DROPOUT
PYTHAGORAS
P_AND_NOT_P_lemma
P_AND_Q_OR_Q_lemma
P_HULL
P_OR_NOT_P_lemma
P_OR_Q_AND_Q_lemma
Parallelogram_DEF
PlaneComplement_DEF
Point_INDUCT,Point_RECURSION
Product_DEF
p_connA
p_conn_ball
p_conn_conn
p_conn_diff
p_conn_euclid
p_conn_hv_finite
p_conn_open
p_conn_subset
pad2d3d
pair
pair_INDUCT
pair_RECURSION
pair_apply
pair_indistinct
pair_order_endpoint
pair_size_2
pair_swap
pair_swap_adj
pair_swap_invol
pair_swap_pair
pair_swap_unique
pairsup
pairwise
par_cell_cell
par_cell_cell_partition
par_cell_closure
par_cell_closure_cell
par_cell_comp
par_cell_curve_cell_disj
par_cell_curve_disj
par_cell_disjoint
par_cell_even_imp
par_cell_h
par_cell_h_in_rectangle
par_cell_h_rectangle
par_cell_h_squ
par_cell_nbd
par_cell_nonempty
par_cell_odd_imp
par_cell_open
par_cell_partition
par_cell_point
par_cell_pointI
par_cell_pointI_trichot
par_cell_point_h
par_cell_point_in_rectangle
par_cell_point_rectangle
par_cell_point_v
par_cell_simple_arc
par_cell_squ
par_cell_squ_neg
par_cell_squ_rectangle
par_cell_union_comp
par_cell_union_disjoint
par_cell_unions_nonempty
par_cell_v
par_cell_v_in_rectangle
par_cell_v_rectangle
par_cell_v_squ
parallel
pardir
parity
parity_even_cell
parity_h
parity_point
parity_squ
parity_union
parity_union_triple
parity_union_triple_even
parity_union_triple_odd
parity_unique
parity_v
part0
part1
part2
part3
part4
part5
part6
part7
part_below_finite
part_below_h
part_below_subset
part_below_v
partcirclepath
partition_DEF
partition_line
partitions
pastecart
path
path_component
path_component_in
path_component_subspace
path_connected
path_domain
path_eq_conn
path_image
path_integrable_on
path_integral
path_length
path_refl
path_symm
path_symm_eq
path_trans
pathfinish
pathstart
pbetween
pconn_refl
pconn_symm
pconn_trans
pdist
perfect
permutation
permutes
perpdir
perpendicular
phi
pi
pi_bounds
piecewise_differentiable_on
pii
planar_graph_hv
planar_graph_rectagonal
planar_is_graph
planar_iso
plane
plane_graph_contain
plane_graph_image_bij
plane_graph_image_e
plane_graph_image_i
plane_graph_image_iso
plane_graph_image_plane
plane_graph_image_v
plane_graph_mod
plane_planar
plus_e12
plusinf
pneg
pneg_aux
poincarify
pointI_col
pointI_inj
pointI_inter
pointI_row
point_INDUCT,point_RECURSION
point_add
point_closure
point_dest_pt
point_inj
point_onto
point_scale
point_split
point_x
point_xy
polar_cont
polar_curve_lemma
polar_distinct
polar_euclid
polar_exist
polar_fg_inj
polar_inj
polar_nz
poly
poly_add
poly_cmul
poly_diff
poly_diff_aux
poly_diff_aux_odd
poly_diff_parity
poly_diff_parity2
poly_exp
poly_mul
poly_neg
polygonal_path
polyhedron
polytope
pos_neg_neq_thm
pos_neg_neq_thm2
pos_pos_neq_thm
pos_pos_neq_thm2
pos_zero_pos_thm
poset
predn_RTCredn
predn_diamond
predn_diamond_lemma
preimage
preimage_closed
preimage_compact
preimage_compact_interval
preimage_disjoint
preimage_first
preimage_restrict
preimage_subset
preimage_union
preimage_union2
preimage_unions
prime
prime_DELTA
primefact
primepow
primepow_DELTA
primitive
prod
prod_DEF
prod_EXISTS
product
proj_cauchy
proj_contraction
proj_d_euclid
proj_euclid1
projective
projective_conic
projectivize
projl
projp
propform_INDUCT,propform_RECURSION
prove_thm((s:string),g,t)
psegment_cls
psegment_delete_end
psegment_edge
psegment_endpoint
psegment_order
psegment_order'
psegment_order_induct_lemma
psegment_subset_endpoint
psegment_triple2
psegment_triple3
psegment_triple_odd_even
psi
pt_thm
pth
pth0
pth1
pth2
pth_0
pth_1
pth_2
pth_2b
pth_3
pth_4
pth_abs
pth_atom
pth_base
pth_divides
pth_empty
pth_false
pth_lexleft
pth_lexright
pth_lt_neg
pth_measure
pth_nocancel
pth_nzg
pth_nzl
pth_refl
pth_relativize
pth_step
pth_triv
pth_trivial
pth_yes_l
pth_zero
pthm
pts_thm
pushin