HOL THEORY BINDINGS
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
A
B
C
- C_ABS_L (value; combinTheory)
- C_BAG_INSERT_ONE_ONE (value; bagTheory)
- C_DEF (value; combinTheory)
- C_THM (value; combinTheory)
- C_UNCURRY_L (value; pairTheory)
- CANCEL_SUB (value; arithmeticTheory)
- canonical0_def (value; canonicalTheory)
- canonical1_def (value; canonicalTheory)
- canonical2_def (value; canonicalTheory)
- canonical3_def (value; canonicalTheory)
- canonical4_def (value; canonicalTheory)
- canonical5_def (value; canonicalTheory)
- canonical6_def (value; canonicalTheory)
- canonical_grammars (value; canonicalTheory)
- canonical_sum_11 (value; canonicalTheory)
- canonical_sum_Axiom (value; canonicalTheory)
- canonical_sum_case_cong (value; canonicalTheory)
- canonical_sum_case_def (value; canonicalTheory)
- canonical_sum_distinct (value; canonicalTheory)
- canonical_sum_induction (value; canonicalTheory)
- canonical_sum_merge_curried_def (value; canonicalTheory)
- canonical_sum_merge_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_merge_ind (value; canonicalTheory)
- canonical_sum_merge_ok (value; canonicalTheory)
- canonical_sum_merge_tupled_primitive_def (value; canonicalTheory)
- canonical_sum_nchotomy (value; canonicalTheory)
- canonical_sum_prod_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_prod_ok (value; canonicalTheory)
- canonical_sum_repfns (value; canonicalTheory)
- canonical_sum_scalar2_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_scalar2_ok (value; canonicalTheory)
- canonical_sum_scalar3_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_scalar3_ok (value; canonicalTheory)
- canonical_sum_scalar_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_scalar_ok (value; canonicalTheory)
- canonical_sum_simplify_def (value; canonicalTheory, ringNormTheory)
- canonical_sum_simplify_ok (value; canonicalTheory)
- canonical_sum_size_def (value; canonicalTheory)
- canonical_sum_TY_DEF (value; canonicalTheory)
- canonicalTheory (structure)
- CARD_COUNT (value; pred_setTheory)
- CARD_CROSS (value; pred_setTheory)
- CARD_DEF (value; pred_setTheory)
- CARD_DELETE (value; pred_setTheory)
- CARD_DIFF (value; pred_setTheory)
- CARD_EMPTY (value; pred_setTheory)
- CARD_EQ_0 (value; pred_setTheory)
- CARD_INSERT (value; pred_setTheory)
- CARD_INTER_LESS_EQ (value; pred_setTheory)
- CARD_POW (value; pred_setTheory)
- CARD_PSUBSET (value; pred_setTheory)
- CARD_SING (value; pred_setTheory)
- CARD_SING_CROSS (value; pred_setTheory)
- CARD_SUBSET (value; pred_setTheory)
- CARD_UNION (value; pred_setTheory)
- CART_EQ (value; fcpTheory)
- cart_TY_DEF (value; fcpTheory)
- cart_tybij (value; fcpTheory)
- cauchy (value; seqTheory)
- ccode2num_11 (value; ieeeTheory)
- ccode2num_num2ccode (value; ieeeTheory)
- ccode2num_ONTO (value; ieeeTheory)
- ccode2num_thm (value; ieeeTheory)
- ccode_Axiom (value; ieeeTheory)
- ccode_BIJ (value; ieeeTheory)
- ccode_case (value; ieeeTheory)
- ccode_case_cong (value; ieeeTheory)
- ccode_case_def (value; ieeeTheory)
- ccode_distinct (value; ieeeTheory)
- ccode_EQ_ccode (value; ieeeTheory)
- ccode_induction (value; ieeeTheory)
- ccode_nchotomy (value; ieeeTheory)
- ccode_size_def (value; ieeeTheory)
- ccode_TY_DEF (value; ieeeTheory)
- char_BIJ (value; stringTheory)
- CHAR_EQ_THM (value; stringTheory)
- CHAR_INDUCT_THM (value; stringTheory)
- char_TY_DEF (value; stringTheory)
- CHOICE_DEF (value; pred_setTheory)
- CHOICE_INSERT_REST (value; pred_setTheory)
- CHOICE_NOT_IN_REST (value; pred_setTheory)
- CHOICE_SING (value; pred_setTheory)
- ChoosePath_def (value; MachineTransitionTheory)
- CHR_11 (value; stringTheory)
- CHR_ONTO (value; stringTheory)
- CHR_ORD (value; stringTheory)
- Clip (value; fxpTheory)
- closed (value; topologyTheory)
- closed_def (value; fixedPointTheory)
- CLOSED_LIMPT (value; topologyTheory)
- CLOSED_PAIR_EQ (value; pairTheory)
- closest (value; ieeeTheory)
- CLOSEST_IN_SET (value; floatTheory)
- CLOSEST_IS_CLOSEST (value; floatTheory)
- CLOSEST_IS_EVERYTHING (value; floatTheory)
- CO_BUECHI_BEFORE_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_CONJ_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_DISJ_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_NEXT_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_SBEFORE_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_SUNTIL_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_SWHEN_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_UNTIL_CLOSURE (value; Omega_AutomataTheory)
- CO_BUECHI_WHEN_CLOSURE (value; Omega_AutomataTheory)
- Coder_grammars (value; CoderTheory)
- CoderTheory (structure)
- collision_free_def (value; EncodeTheory)
- combin_grammars (value; combinTheory)
- combinTheory (structure)
- COMM_ASSOC_FOLDL_REVERSE (value; rich_listTheory)
- COMM_ASSOC_FOLDR_REVERSE (value; rich_listTheory)
- COMM_BAG_UNION (value; bagTheory)
- COMM_DEF (value; operatorTheory)
- COMM_MONOID_FOLDL (value; rich_listTheory)
- COMM_MONOID_FOLDR (value; rich_listTheory)
- COMMA_DEF (value; pairTheory)
- comma_tm (value; pairTheory)
- COMMUTING_ITBAG_INSERT (value; bagTheory)
- COMMUTING_ITBAG_RECURSES (value; bagTheory)
- COMMUTING_ITSET_INSERT (value; pred_setTheory)
- COMMUTING_ITSET_RECURSES (value; pred_setTheory)
- compare_def (value; prelimTheory)
- compare_equal (value; prelimTheory)
- compare_index_equal (value; quoteTheory)
- compare_list_index (value; quoteTheory)
- COMPL_CLAUSES (value; pred_setTheory, prob_extraTheory)
- COMPL_COMPL (value; pred_setTheory, prob_extraTheory)
- COMPL_DEF (value; pred_setTheory)
- COMPL_def (value; prob_extraTheory)
- COMPL_EMPTY (value; pred_setTheory)
- COMPL_INTER (value; pred_setTheory)
- COMPL_MEM (value; topologyTheory)
- COMPL_SHD (value; prob_algebraTheory)
- COMPL_SPLITS (value; pred_setTheory, prob_extraTheory)
- COMPLETE_INDUCTION (value; arithmeticTheory)
- COMPONENT (value; pred_setTheory)
- CONCAT_EXTRACT (value; wordsTheory)
- COND_ABS (value; boolTheory)
- COND_CLAUSES (value; boolTheory)
- COND_CONG (value; boolTheory)
- COND_DEF (value; boolTheory)
- COND_EXPAND (value; boolTheory)
- COND_ID (value; boolTheory)
- COND_RAND (value; boolTheory)
- COND_RATOR (value; boolTheory)
- COND_SIMP (value; MachineTransitionTheory)
- CONJ_ASSOC (value; boolTheory)
- CONJ_COMM (value; boolTheory)
- CONJ_SYM (value; boolTheory)
- CONJUNCTIVE_NORMAL_FORM (value; Past_Temporal_LogicTheory)
- CONS (value; listTheory, rich_listTheory)
- CONS_11 (value; listTheory, rich_listTheory)
- CONS_ACYCLIC (value; listTheory)
- CONS_APPEND (value; rich_listTheory)
- CONS_def (value; listTheory)
- Cons_monom (value; canonicalTheory)
- CONS_PERM (value; sortingTheory)
- Cons_varlist (value; canonicalTheory)
- CONSISTENCY (value; defCNFTheory)
- CONSTR (value; ind_typeTheory)
- CONSTR_BOT (value; ind_typeTheory)
- CONSTR_IND (value; ind_typeTheory)
- CONSTR_INJ (value; ind_typeTheory)
- CONSTR_REC (value; ind_typeTheory)
- CONT_ADD (value; limTheory)
- CONT_ATTAINS (value; limTheory)
- CONT_ATTAINS2 (value; limTheory)
- CONT_ATTAINS_ALL (value; limTheory)
- CONT_BOUNDED (value; limTheory)
- CONT_COMPOSE (value; limTheory)
- CONT_CONST (value; limTheory)
- CONT_DIV (value; limTheory)
- CONT_HASSUP (value; limTheory)
- CONT_INJ_LEMMA (value; limTheory)
- CONT_INJ_LEMMA2 (value; limTheory)
- CONT_INJ_RANGE (value; limTheory)
- CONT_INV (value; limTheory)
- CONT_INVERSE (value; limTheory)
- CONT_MUL (value; limTheory)
- CONT_NEG (value; limTheory)
- CONT_SUB (value; limTheory)
- container_grammars (value; containerTheory)
- container_rwts (value; containerTheory)
- containerTheory (structure)
- contl (value; limTheory)
- CONTL_LIM (value; limTheory)
- conv (type; pairTheory)
- Convergent (value; fxpTheory)
- convergent (value; seqTheory)
- cos (value; transcTheory)
- COS_0 (value; transcTheory)
- COS_2 (value; transcTheory)
- COS_ACS (value; transcTheory)
- COS_ADD (value; transcTheory)
- COS_ASN_NZ (value; transcTheory)
- COS_ATN_NZ (value; transcTheory)
- COS_BOUND (value; transcTheory)
- COS_BOUNDS (value; transcTheory)
- COS_CONVERGES (value; transcTheory)
- COS_DOUBLE (value; transcTheory)
- COS_FDIFF (value; transcTheory)
- COS_ISZERO (value; transcTheory)
- COS_NEG (value; transcTheory)
- COS_NPI (value; transcTheory)
- COS_PAIRED (value; transcTheory)
- COS_PERIODIC (value; transcTheory)
- COS_PERIODIC_PI (value; transcTheory)
- COS_PI (value; transcTheory)
- COS_PI2 (value; transcTheory)
- COS_POS_PI (value; transcTheory)
- COS_POS_PI2 (value; transcTheory)
- COS_POS_PI2_LE (value; transcTheory)
- COS_POS_PI_LE (value; transcTheory)
- COS_SIN (value; transcTheory)
- COS_SIN_SQ (value; transcTheory)
- COS_SIN_SQRT (value; transcTheory)
- COS_TOTAL (value; transcTheory)
- COS_ZERO (value; transcTheory)
- COS_ZERO_LEMMA (value; transcTheory)
- count_def (value; pred_setTheory)
- count_EQN (value; pred_setTheory)
- COUNT_SUC (value; pred_setTheory)
- COUNT_ZERO (value; pred_setTheory)
- COUNTINDUCT (value; fxpTheory)
- CR_def (value; relationTheory)
- CROSS_DEF (value; pred_setTheory)
- CROSS_EMPTY (value; pred_setTheory)
- CROSS_EQNS (value; pred_setTheory)
- CROSS_INSERT_LEFT (value; pred_setTheory)
- CROSS_INSERT_RIGHT (value; pred_setTheory)
- CROSS_SINGS (value; pred_setTheory)
- CROSS_SUBSET (value; pred_setTheory)
- CURRY_DEF (value; pairTheory)
- CURRY_ONE_ONE_THM (value; pairTheory)
- CURRY_UNCURRY_THM (value; pairTheory)
- CUT_BOUNDED (value; hrealTheory)
- CUT_DOWN (value; hrealTheory)
- CUT_ISACUT (value; hrealTheory)
- CUT_NEARTOP_ADD (value; hrealTheory)
- CUT_NEARTOP_MUL (value; hrealTheory)
- CUT_NONEMPTY (value; hrealTheory)
- cut_of_hrat (value; hrealTheory)
- CUT_STRADDLE (value; hrealTheory)
- CUT_UBOUND (value; hrealTheory)
- CUT_UP (value; hrealTheory)
D
E
F
G
H
I
- i12_TY_DEF (value; wordsTheory)
- i16_TY_DEF (value; wordsTheory)
- i20_TY_DEF (value; wordsTheory)
- i24_TY_DEF (value; wordsTheory)
- i28_TY_DEF (value; wordsTheory)
- i2_TY_DEF (value; wordsTheory)
- i30_TY_DEF (value; wordsTheory)
- i32_TY_DEF (value; wordsTheory)
- i3_TY_DEF (value; wordsTheory)
- i4_TY_DEF (value; wordsTheory)
- i5_TY_DEF (value; wordsTheory)
- i64_TY_DEF (value; wordsTheory)
- i6_TY_DEF (value; wordsTheory)
- i7_TY_DEF (value; wordsTheory)
- i8_TY_DEF (value; wordsTheory)
- I_DEF (value; combinTheory)
- I_o_ID (value; combinTheory)
- I_THM (value; combinTheory)
- iBIT_cases (value; numeralTheory)
- ICARRY_DEF (value; bword_arithTheory)
- ICARRY_WSEG (value; bword_arithTheory)
- ics_aux_def (value; canonicalTheory, ringNormTheory)
- ics_aux_ok (value; canonicalTheory)
- Id_O (value; relationTheory)
- IDEM (value; relationTheory)
- IDEM_DEF (value; relationTheory)
- IDEM_RC (value; relationTheory)
- IDEM_RTC (value; relationTheory)
- IDEM_SC (value; relationTheory)
- IDEM_STRORD (value; relationTheory)
- IDEM_TC (value; relationTheory)
- iDUB (value; numeralTheory)
- iDUB_removal (value; numeralTheory)
- ieee_grammars (value; ieeeTheory)
- ieeeTheory (structure)
- iIsigned (value; fxpTheory)
- iiSUC (value; numeralTheory)
- IMAGE_11_INFINITE (value; pred_setTheory)
- IMAGE_COMPOSE (value; pred_setTheory)
- IMAGE_DEF (value; pred_setTheory)
- IMAGE_DELETE (value; pred_setTheory)
- IMAGE_EMPTY (value; pred_setTheory)
- IMAGE_EQ_EMPTY (value; pred_setTheory)
- IMAGE_FINITE (value; pred_setTheory)
- IMAGE_ID (value; pred_setTheory)
- IMAGE_IN (value; pred_setTheory)
- IMAGE_INSERT (value; pred_setTheory)
- IMAGE_INTER (value; pred_setTheory)
- IMAGE_SUBSET (value; pred_setTheory)
- IMAGE_SURJ (value; pred_setTheory)
- IMAGE_UNION (value; pred_setTheory)
- IMMEDIATE_EVENT (value; Past_Temporal_LogicTheory, Temporal_LogicTheory)
- iMOD_2EXP (value; numeralTheory)
- IMP_ANTISYM_AX (value; boolTheory)
- IMP_CLAUSES (value; boolTheory)
- IMP_CONG (value; boolTheory)
- IMP_CONJ_THM (value; boolTheory)
- IMP_DISJ_THM (value; boolTheory)
- IMP_F (value; boolTheory)
- IMP_F_EQ_F (value; boolTheory)
- IMP_NEXT (value; Temporal_LogicTheory)
- IMPLODE_11 (value; stringTheory)
- IMPLODE_EQ_EMPTYSTRING (value; stringTheory)
- IMPLODE_EQ_THM (value; stringTheory)
- IMPLODE_EQNS (value; stringTheory)
- IMPLODE_EXPLODE (value; stringTheory)
- IMPLODE_ONTO (value; stringTheory)
- IMPLODE_STRING (value; stringTheory)
- IMPORT (value; canonicalTheory, ringNormTheory, ringTheory, semi_ringTheory)
- IN_BIGINTER (value; pred_setTheory)
- IN_BIGUNION (value; pred_setTheory)
- IN_COMPL (value; pred_setTheory, prob_extraTheory)
- IN_COUNT (value; pred_setTheory)
- IN_CROSS (value; pred_setTheory)
- IN_DEF (value; boolTheory)
- IN_DELETE (value; pred_setTheory)
- IN_DELETE_EQ (value; pred_setTheory)
- IN_DIFF (value; pred_setTheory)
- IN_DISJOINT (value; pred_setTheory)
- IN_EMPTY (value; prob_extraTheory)
- IN_IMAGE (value; pred_setTheory)
- IN_INFINITE_NOT_FINITE (value; pred_setTheory)
- IN_INSERT (value; pred_setTheory)
- IN_INTER (value; pred_setTheory)
- IN_LIST_TO_SET (value; listTheory)
- IN_PBITBOP (value; word_bitopTheory)
- IN_PBITOP (value; word_bitopTheory)
- IN_PL_drop (value; pathTheory)
- IN_POW (value; pred_setTheory)
- IN_PWORDLEN (value; word_baseTheory)
- IN_RDOM (value; relationTheory)
- IN_RRANGE (value; relationTheory)
- IN_SET_OF_BAG (value; bagTheory)
- IN_SING (value; pred_setTheory)
- IN_UNION (value; pred_setTheory)
- IN_UNIV (value; pred_setTheory)
- ind_type_grammars (value; ind_typeTheory)
- ind_typeTheory (structure)
- INDEP_BIND (value; prob_indepTheory)
- INDEP_BIND_SDEST (value; prob_indepTheory)
- indep_def (value; prob_indepTheory)
- INDEP_INDEP_SET (value; prob_indepTheory)
- INDEP_INDEP_SET_LEMMA (value; prob_indepTheory)
- INDEP_MEASURABLE1 (value; prob_indepTheory)
- INDEP_MEASURABLE2 (value; prob_indepTheory)
- INDEP_PROB (value; prob_indepTheory)
- INDEP_SDEST (value; prob_indepTheory)
- INDEP_SET_BASIC (value; prob_indepTheory)
- indep_set_def (value; prob_indepTheory)
- INDEP_SET_DISJOINT_DECOMP (value; prob_indepTheory)
- INDEP_SET_LIST (value; prob_indepTheory)
- INDEP_SET_SYM (value; prob_indepTheory)
- INDEP_UNIF (value; prob_uniformTheory)
- INDEP_UNIFORM (value; prob_uniformTheory)
- INDEP_UNIT (value; prob_indepTheory)
- index (value; fcpTheory)
- index12_bij (value; wordsTheory)
- index16_bij (value; wordsTheory)
- index20_bij (value; wordsTheory)
- index24_bij (value; wordsTheory)
- index28_bij (value; wordsTheory)
- index2_bij (value; wordsTheory)
- index30_bij (value; wordsTheory)
- index32_bij (value; wordsTheory)
- index3_bij (value; wordsTheory)
- index4_bij (value; wordsTheory)
- index5_bij (value; wordsTheory)
- index64_bij (value; wordsTheory)
- index6_bij (value; wordsTheory)
- index7_bij (value; wordsTheory)
- index8_bij (value; wordsTheory)
- index_11 (value; quoteTheory)
- index_Axiom (value; quoteTheory)
- index_case_cong (value; quoteTheory)
- index_case_def (value; quoteTheory)
- index_compare_curried_def (value; quoteTheory)
- index_compare_def (value; quoteTheory)
- index_compare_ind (value; quoteTheory)
- index_compare_tupled_primitive_def (value; quoteTheory)
- index_distinct (value; quoteTheory)
- index_induction (value; quoteTheory)
- index_lt_def (value; quoteTheory)
- index_nchotomy (value; quoteTheory)
- index_repfns (value; quoteTheory)
- index_size (value; fcpTheory)
- index_size_def (value; quoteTheory)
- index_sum (value; fcpTheory)
- index_TY_DEF (value; quoteTheory)
- INDUCTION (value; numTheory)
- INDUCTION_WF_THM (value; relationTheory)
- INDUCTIVE_INVARIANT_DEF (value; relationTheory)
- INDUCTIVE_INVARIANT_ON_DEF (value; relationTheory)
- INDUCTIVE_INVARIANT_ON_WFREC (value; relationTheory)
- INDUCTIVE_INVARIANT_WFREC (value; relationTheory)
- inf_def (value; prob_extraTheory, realTheory)
- INF_DEF_ALT (value; prob_extraTheory)
- INFINITE_DEF (value; pred_setTheory)
- INFINITE_DIFF_FINITE (value; pred_setTheory)
- INFINITE_INHAB (value; pred_setTheory)
- infinite_PL (value; pathTheory)
- INFINITE_SUBSET (value; pred_setTheory)
- INFINITE_UNIV (value; pred_setTheory)
- Infinity (value; ieeeTheory)
- INFINITY_AX (value; boolTheory)
- INFINITY_IS_INFINITY (value; floatTheory)
- INFINITY_NOT_NAN (value; floatTheory)
- INITIALISATION (value; Past_Temporal_LogicTheory)
- InitPoint (value; Past_Temporal_LogicTheory)
- INJ_CARD (value; pred_setTheory)
- INJ_COMPOSE (value; pred_setTheory)
- INJ_DEF (value; pred_setTheory)
- INJ_DELETE (value; pred_setTheory)
- INJ_EMPTY (value; pred_setTheory)
- INJ_ID (value; pred_setTheory)
- INJ_INVERSE2 (value; ind_typeTheory)
- INJA (value; ind_typeTheory)
- INJA_INJ (value; ind_typeTheory)
- INJECTIVE_IMAGE_FINITE (value; pred_setTheory)
- INJF (value; ind_typeTheory)
- INJF_INJ (value; ind_typeTheory)
- INJN (value; ind_typeTheory)
- INJN_INJ (value; ind_typeTheory)
- INJP (value; ind_typeTheory)
- INJP_INJ (value; ind_typeTheory)
- INL (value; sumTheory)
- INL_DEF (value; sumTheory)
- INR (value; sumTheory)
- INR_DEF (value; sumTheory)
- INR_INL_11 (value; sumTheory)
- INR_neq_INL (value; sumTheory)
- INSERT_COMM (value; pred_setTheory)
- INSERT_DEF (value; pred_setTheory)
- INSERT_DELETE (value; pred_setTheory)
- INSERT_DIFF (value; pred_setTheory)
- INSERT_INSERT (value; pred_setTheory)
- INSERT_INTER (value; pred_setTheory)
- INSERT_SING_UNION (value; pred_setTheory)
- INSERT_SUBSET (value; pred_setTheory)
- INSERT_UNION (value; pred_setTheory)
- INSERT_UNION_EQ (value; pred_setTheory)
- INSERT_UNIV (value; pred_setTheory)
- INSTANCE (value; fxpTheory)
- INSTANCEFINITE (value; fxpTheory)
- INT (value; integerTheory)
- INT_0 (value; integerTheory)
- int_0 (value; integerTheory)
- INT_1 (value; integerTheory)
- int_1 (value; integerTheory)
- INT_10 (value; integerTheory)
- INT_ABS (value; integerTheory)
- INT_ABS_ABS (value; integerTheory)
- int_ABS_def (value; integerTheory)
- INT_ABS_EQ (value; integerTheory)
- INT_ABS_EQ0 (value; integerTheory)
- INT_ABS_EQ_ID (value; integerTheory)
- INT_ABS_LE (value; integerTheory)
- INT_ABS_LE0 (value; integerTheory)
- INT_ABS_LT (value; integerTheory)
- INT_ABS_LT0 (value; integerTheory)
- INT_ABS_MUL (value; integerTheory)
- INT_ABS_NEG (value; integerTheory)
- INT_ABS_NUM (value; integerTheory)
- INT_ABS_POS (value; integerTheory)
- INT_ABS_QUOT (value; integerTheory)
- int_ABS_REP_CLASS (value; integerTheory)
- INT_ADD (value; integerTheory)
- int_add (value; integerTheory)
- INT_ADD2_SUB2 (value; integerTheory)
- INT_ADD_ASSOC (value; integerTheory)
- INT_ADD_CALCULATE (value; integerTheory)
- INT_ADD_COMM (value; integerTheory)
- INT_ADD_DIV (value; integerTheory)
- INT_ADD_LID (value; integerTheory)
- INT_ADD_LID_UNIQ (value; integerTheory)
- INT_ADD_LINV (value; integerTheory)
- INT_ADD_REDUCE (value; integerTheory)
- INT_ADD_RID (value; integerTheory)
- INT_ADD_RID_UNIQ (value; integerTheory)
- INT_ADD_RINV (value; integerTheory)
- INT_ADD_SUB (value; integerTheory)
- INT_ADD_SUB2 (value; integerTheory)
- INT_ADD_SYM (value; integerTheory)
- int_bijections (value; integerTheory)
- int_calculate (value; integerRingTheory)
- INT_DIFFSQ (value; integerTheory)
- INT_DISCRETE (value; integerTheory)
- INT_DIV (value; integerTheory)
- int_div (value; integerTheory)
- INT_DIV_0 (value; integerTheory)
- INT_DIV_1 (value; integerTheory)
- INT_DIV_CALCULATE (value; integerTheory)
- INT_DIV_FORALL_P (value; integerTheory)
- INT_DIV_ID (value; integerTheory)
- INT_DIV_LMUL (value; integerTheory)
- INT_DIV_MUL_ID (value; integerTheory)
- INT_DIV_NEG (value; integerTheory)
- INT_DIV_P (value; integerTheory)
- INT_DIV_REDUCE (value; integerTheory)
- INT_DIV_RMUL (value; integerTheory)
- INT_DIV_UNIQUE (value; integerTheory)
- INT_DIVIDES (value; integerTheory)
- INT_DIVIDES_0 (value; integerTheory)
- INT_DIVIDES_1 (value; integerTheory)
- INT_DIVIDES_LADD (value; integerTheory)
- INT_DIVIDES_LMUL (value; integerTheory)
- INT_DIVIDES_LSUB (value; integerTheory)
- INT_DIVIDES_MOD0 (value; integerTheory)
- INT_DIVIDES_MUL (value; integerTheory)
- INT_DIVIDES_MUL_BOTH (value; integerTheory)
- INT_DIVIDES_NEG (value; integerTheory)
- INT_DIVIDES_RADD (value; integerTheory)
- INT_DIVIDES_REDUCE (value; integerTheory)
- INT_DIVIDES_REFL (value; integerTheory)
- INT_DIVIDES_RMUL (value; integerTheory)
- INT_DIVIDES_RSUB (value; integerTheory)
- INT_DIVIDES_TRANS (value; integerTheory)
- INT_DIVISION (value; integerTheory)
- INT_DOUBLE (value; integerTheory)
- INT_ENTIRE (value; integerTheory)
- INT_EQ_CALCULATE (value; integerTheory)
- INT_EQ_IMP_LE (value; integerTheory)
- INT_EQ_LADD (value; integerTheory)
- INT_EQ_LMUL (value; integerTheory)
- INT_EQ_LMUL2 (value; integerTheory)
- INT_EQ_LMUL_IMP (value; integerTheory)
- INT_EQ_NEG (value; integerTheory)
- INT_EQ_RADD (value; integerTheory)
- INT_EQ_REDUCE (value; integerTheory)
- INT_EQ_RMUL (value; integerTheory)
- INT_EQ_RMUL_IMP (value; integerTheory)
- INT_EQ_SUB_LADD (value; integerTheory)
- INT_EQ_SUB_RADD (value; integerTheory)
- INT_EXP (value; integerTheory)
- int_exp (value; integerTheory)
- INT_EXP_ADD_EXPONENTS (value; integerTheory)
- INT_EXP_CALCULATE (value; integerTheory)
- INT_EXP_EQ0 (value; integerTheory)
- INT_EXP_MOD (value; integerTheory)
- INT_EXP_MULTIPLY_EXPONENTS (value; integerTheory)
- INT_EXP_NEG (value; integerTheory)
- INT_EXP_REDUCE (value; integerTheory)
- INT_EXP_SUBTRACT_EXPONENTS (value; integerTheory)
- int_ge (value; integerTheory)
- INT_GE_CALCULATE (value; integerTheory)
- INT_GE_REDUCE (value; integerTheory)
- int_gt (value; integerTheory)
- INT_GT_CALCULATE (value; integerTheory)
- INT_GT_REDUCE (value; integerTheory)
- INT_INJ (value; integerTheory)
- int_interp_p_def (value; integerRingTheory)
- int_is_ring (value; integerRingTheory)
- INT_LDISTRIB (value; integerTheory)
- INT_LE (value; integerTheory)
- int_le (value; integerTheory)
- INT_LE_01 (value; integerTheory)
- INT_LE_ADD (value; integerTheory)
- INT_LE_ADD2 (value; integerTheory)
- INT_LE_ADDL (value; integerTheory)
- INT_LE_ADDR (value; integerTheory)
- INT_LE_ANTISYM (value; integerTheory)
- INT_LE_CALCULATE (value; integerTheory)
- INT_LE_DOUBLE (value; integerTheory)
- INT_LE_LADD (value; integerTheory)
- INT_LE_LT (value; integerTheory)
- INT_LE_MONO (value; integerTheory)
- INT_LE_MUL (value; integerTheory)
- INT_LE_NEG (value; integerTheory)
- INT_LE_NEGL (value; integerTheory)
- INT_LE_NEGR (value; integerTheory)
- INT_LE_NEGTOTAL (value; integerTheory)
- INT_LE_RADD (value; integerTheory)
- INT_LE_REDUCE (value; integerTheory)
- INT_LE_REFL (value; integerTheory)
- INT_LE_SQUARE (value; integerTheory)
- INT_LE_SUB_LADD (value; integerTheory)
- INT_LE_SUB_RADD (value; integerTheory)
- INT_LE_TOTAL (value; integerTheory)
- INT_LE_TRANS (value; integerTheory)
- INT_LET_ADD (value; integerTheory)
- INT_LET_ADD2 (value; integerTheory)
- INT_LET_ANTISYM (value; integerTheory)
- INT_LET_TOTAL (value; integerTheory)
- INT_LET_TRANS (value; integerTheory)
- INT_LNEG_UNIQ (value; integerTheory)
- INT_LT (value; integerTheory)
- int_lt (value; integerTheory)
- INT_LT_01 (value; integerTheory)
- INT_LT_ADD (value; integerTheory)
- INT_LT_ADD1 (value; integerTheory)
- INT_LT_ADD2 (value; integerTheory)
- INT_LT_ADD_SUB (value; integerTheory)
- INT_LT_ADDL (value; integerTheory)
- INT_LT_ADDNEG (value; integerTheory)
- INT_LT_ADDNEG2 (value; integerTheory)
- INT_LT_ADDR (value; integerTheory)
- INT_LT_ANTISYM (value; integerTheory)
- INT_LT_CALCULATE (value; integerTheory)
- INT_LT_GT (value; integerTheory)
- INT_LT_IMP_LE (value; integerTheory)
- INT_LT_IMP_NE (value; integerTheory)
- INT_LT_LADD (value; integerTheory)
- INT_LT_LADD_IMP (value; integerTheory)
- INT_LT_LE (value; integerTheory)
- INT_LT_MONO (value; integerTheory)
- INT_LT_MUL (value; integerTheory)
- INT_LT_MUL2 (value; integerTheory)
- INT_LT_NEG (value; integerTheory)
- INT_LT_NEGTOTAL (value; integerTheory)
- INT_LT_NZ (value; integerTheory)
- INT_LT_RADD (value; integerTheory)
- INT_LT_REDUCE (value; integerTheory)
- INT_LT_REFL (value; integerTheory)
- INT_LT_SUB_LADD (value; integerTheory)
- INT_LT_SUB_RADD (value; integerTheory)
- INT_LT_TOTAL (value; integerTheory)
- INT_LT_TRANS (value; integerTheory)
- INT_LTE_ADD (value; integerTheory)
- INT_LTE_ADD2 (value; integerTheory)
- INT_LTE_ANTSYM (value; integerTheory)
- INT_LTE_TOTAL (value; integerTheory)
- INT_LTE_TRANS (value; integerTheory)
- INT_MAX (value; integerTheory)
- INT_MAX_def (value; wordsTheory)
- INT_MAX_LT (value; integerTheory)
- INT_MAX_NUM (value; integerTheory)
- INT_MIN (value; integerTheory)
- INT_MIN_12 (value; wordsTheory)
- INT_MIN_16 (value; wordsTheory)
- INT_MIN_2 (value; wordsTheory)
- INT_MIN_20 (value; wordsTheory)
- INT_MIN_24 (value; wordsTheory)
- INT_MIN_28 (value; wordsTheory)
- INT_MIN_3 (value; wordsTheory)
- INT_MIN_30 (value; wordsTheory)
- INT_MIN_32 (value; wordsTheory)
- INT_MIN_4 (value; wordsTheory)
- INT_MIN_5 (value; wordsTheory)
- INT_MIN_6 (value; wordsTheory)
- INT_MIN_64 (value; wordsTheory)
- INT_MIN_7 (value; wordsTheory)
- INT_MIN_8 (value; wordsTheory)
- INT_MIN_def (value; wordsTheory)
- INT_MIN_LT (value; integerTheory)
- INT_MIN_NUM (value; integerTheory)
- INT_MOD (value; integerTheory)
- int_mod (value; integerTheory)
- INT_MOD0 (value; integerTheory)
- INT_MOD_ADD_MULTIPLES (value; integerTheory)
- INT_MOD_BOUNDS (value; integerTheory)
- INT_MOD_CALCULATE (value; integerTheory)
- INT_MOD_COMMON_FACTOR (value; integerTheory)
- INT_MOD_EQ0 (value; integerTheory)
- INT_MOD_FORALL_P (value; integerTheory)
- INT_MOD_ID (value; integerTheory)
- INT_MOD_MOD (value; integerTheory)
- INT_MOD_NEG (value; integerTheory)
- INT_MOD_NEG_NUMERATOR (value; integerTheory)
- INT_MOD_P (value; integerTheory)
- INT_MOD_PLUS (value; integerTheory)
- INT_MOD_REDUCE (value; integerTheory)
- INT_MOD_SUB (value; integerTheory)
- INT_MOD_UNIQUE (value; integerTheory)
- INT_MUL (value; integerTheory)
- int_mul (value; integerTheory)
- INT_MUL_ASSOC (value; integerTheory)
- INT_MUL_CALCULATE (value; integerTheory)
- INT_MUL_COMM (value; integerTheory)
- INT_MUL_DIV (value; integerTheory)
- INT_MUL_EQ_1 (value; integerTheory)
- INT_MUL_LID (value; integerTheory)
- INT_MUL_LZERO (value; integerTheory)
- INT_MUL_QUOT (value; integerTheory)
- INT_MUL_REDUCE (value; integerTheory)
- INT_MUL_RID (value; integerTheory)
- INT_MUL_RZERO (value; integerTheory)
- INT_MUL_SIGN_CASES (value; integerTheory)
- INT_MUL_SYM (value; integerTheory)
- int_neg (value; integerTheory)
- INT_NEG_0 (value; integerTheory)
- INT_NEG_ADD (value; integerTheory)
- INT_NEG_EQ (value; integerTheory)
- INT_NEG_EQ0 (value; integerTheory)
- INT_NEG_GE0 (value; integerTheory)
- INT_NEG_GT0 (value; integerTheory)
- INT_NEG_LE0 (value; integerTheory)
- INT_NEG_LMUL (value; integerTheory)
- INT_NEG_LT0 (value; integerTheory)
- INT_NEG_MINUS1 (value; integerTheory)
- INT_NEG_MUL2 (value; integerTheory)
- INT_NEG_RMUL (value; integerTheory)
- INT_NEG_SAME_EQ (value; integerTheory)
- INT_NEG_SUB (value; integerTheory)
- INT_NEGNEG (value; integerTheory)
- INT_NOT_LE (value; integerTheory)
- INT_NOT_LT (value; integerTheory)
- INT_NUM_CASES (value; integerTheory)
- INT_NZ_IMP_LT (value; integerTheory)
- INT_OF_NUM (value; integerTheory)
- int_of_num (value; integerTheory)
- INT_POASQ (value; integerTheory)
- int_polynom_normalize_def (value; integerRingTheory)
- int_polynom_simplify_def (value; integerRingTheory)
- INT_POS (value; integerTheory)
- INT_POS_NZ (value; integerTheory)
- INT_QUOT (value; integerTheory)
- int_quot (value; integerTheory)
- INT_QUOT_0 (value; integerTheory)
- INT_QUOT_1 (value; integerTheory)
- INT_QUOT_CALCULATE (value; integerTheory)
- INT_QUOT_ID (value; integerTheory)
- INT_QUOT_NEG (value; integerTheory)
- INT_QUOT_REDUCE (value; integerTheory)
- INT_QUOT_UNIQUE (value; integerTheory)
- int_QUOTIENT (value; integerTheory)
- int_r_canonical_sum_merge_def (value; integerRingTheory)
- int_r_canonical_sum_prod_def (value; integerRingTheory)
- int_r_canonical_sum_scalar2_def (value; integerRingTheory)
- int_r_canonical_sum_scalar3_def (value; integerRingTheory)
- int_r_canonical_sum_scalar_def (value; integerRingTheory)
- int_r_canonical_sum_simplify_def (value; integerRingTheory)
- int_r_ics_aux_def (value; integerRingTheory)
- int_r_interp_cs_def (value; integerRingTheory)
- int_r_interp_m_def (value; integerRingTheory)
- int_r_interp_sp_def (value; integerRingTheory)
- int_r_interp_vl_def (value; integerRingTheory)
- int_r_ivl_aux_def (value; integerRingTheory)
- int_r_monom_insert_def (value; integerRingTheory)
- int_r_spolynom_normalize_def (value; integerRingTheory)
- int_r_spolynom_simplify_def (value; integerRingTheory)
- int_r_varlist_insert_def (value; integerRingTheory)
- INT_RDISTRIB (value; integerTheory)
- INT_REM (value; integerTheory)
- int_rem (value; integerTheory)
- INT_REM0 (value; integerTheory)
- INT_REM_CALCULATE (value; integerTheory)
- INT_REM_COMMON_FACTOR (value; integerTheory)
- INT_REM_EQ0 (value; integerTheory)
- INT_REM_ID (value; integerTheory)
- INT_REM_NEG (value; integerTheory)
- INT_REM_REDUCE (value; integerTheory)
- INT_REM_UNIQUE (value; integerTheory)
- INT_REMQUOT (value; integerTheory)
- int_REP_def (value; integerTheory)
- int_rewrites (value; integerRingTheory)
- int_ring_thms (value; integerRingTheory)
- INT_RNEG_UNIQ (value; integerTheory)
- INT_SUB (value; integerTheory)
- int_sub (value; integerTheory)
- INT_SUB_0 (value; integerTheory)
- INT_SUB_ADD (value; integerTheory)
- INT_SUB_ADD2 (value; integerTheory)
- INT_SUB_CALCULATE (value; integerTheory)
- INT_SUB_LDISTRIB (value; integerTheory)
- INT_SUB_LE (value; integerTheory)
- INT_SUB_LNEG (value; integerTheory)
- INT_SUB_LT (value; integerTheory)
- INT_SUB_LZERO (value; integerTheory)
- INT_SUB_NEG2 (value; integerTheory)
- INT_SUB_RDISTRIB (value; integerTheory)
- INT_SUB_REDUCE (value; integerTheory)
- INT_SUB_REFL (value; integerTheory)
- INT_SUB_RNEG (value; integerTheory)
- INT_SUB_RZERO (value; integerTheory)
- INT_SUB_SUB (value; integerTheory)
- INT_SUB_SUB2 (value; integerTheory)
- INT_SUB_TRIANGLE (value; integerTheory)
- INT_SUMSQ (value; integerTheory)
- int_TY_DEF (value; integerTheory)
- INTBITS (value; fxpTheory)
- Intbits_def (value; fxpTheory)
- intbits_def (value; fxpTheory)
- integer_grammars (value; integerTheory)
- integer_rwts (value; integerTheory)
- integerRing_grammars (value; integerRingTheory)
- integerRingTheory (structure)
- integerTheory (structure)
- INTEGRAL_NULL (value; transcTheory)
- INTER_ASSOC (value; pred_setTheory)
- INTER_COMM (value; pred_setTheory)
- INTER_DEF (value; pred_setTheory)
- INTER_EMPTY (value; pred_setTheory)
- INTER_FINITE (value; pred_setTheory)
- INTER_IDEMPOT (value; pred_setTheory)
- INTER_IS_EMPTY (value; prob_extraTheory)
- INTER_OVER_UNION (value; pred_setTheory)
- INTER_STL (value; prob_algebraTheory)
- INTER_SUBSET (value; pred_setTheory)
- INTER_UNION_COMPL (value; pred_setTheory, prob_extraTheory)
- INTER_UNION_RDISTRIB (value; prob_extraTheory)
- INTER_UNIV (value; pred_setTheory)
- interp_cs_def (value; canonicalTheory, ringNormTheory)
- interp_m_def (value; canonicalTheory, ringNormTheory)
- interp_m_ok (value; canonicalTheory)
- interp_p_def (value; ringNormTheory)
- interp_sp_def (value; canonicalTheory, ringNormTheory)
- interp_vl_def (value; canonicalTheory, ringNormTheory)
- INTERVAL_ABS (value; limTheory)
- INTERVAL_CLEMMA (value; limTheory)
- INTERVAL_LEMMA (value; limTheory)
- intround_def (value; ieeeTheory)
- inv23gt0 (value; floatTheory)
- inv_DEF (value; relationTheory)
- inv_diag (value; relationTheory)
- inv_EQC (value; relationTheory)
- inv_Id (value; relationTheory)
- inv_image_def (value; relationTheory)
- inv_inv (value; relationTheory)
- inv_INVOL (value; relationTheory)
- inv_MOVES_OUT (value; relationTheory)
- inv_O (value; relationTheory)
- INV_PRE_EQ (value; arithmeticTheory)
- INV_PRE_LESS (value; arithmeticTheory)
- INV_PRE_LESS_EQ (value; arithmeticTheory)
- inv_RC (value; relationTheory)
- inv_SC (value; relationTheory)
- INV_SUC (value; numTheory, prob_extraTheory)
- INV_SUC_EQ (value; prim_recTheory)
- INV_SUC_MAX (value; prob_extraTheory)
- INV_SUC_POS (value; prob_extraTheory)
- inv_TC (value; relationTheory)
- invalid (value; fxpTheory)
- invfracge0 (value; fxpTheory)
- invfracgt0 (value; fxpTheory)
- INVOL (value; relationTheory)
- INVOL_DEF (value; relationTheory)
- INVOL_ONE_ENO (value; relationTheory)
- INVOL_ONE_ONE (value; relationTheory)
- irreflexive_def (value; relationTheory)
- irreflexive_inv (value; relationTheory)
- is_closest (value; ieeeTheory)
- IS_CLOSEST_EXISTS (value; floatTheory)
- is_denormal (value; ieeeTheory)
- is_double (value; ieeeTheory)
- is_double_extended (value; ieeeTheory)
- IS_EL (value; rich_listTheory)
- IS_EL_APPEND (value; rich_listTheory)
- IS_EL_BUTFIRSTN (value; rich_listTheory)
- IS_EL_BUTLASTN (value; rich_listTheory)
- IS_EL_DEF (value; rich_listTheory)
- IS_EL_FILTER (value; rich_listTheory)
- IS_EL_FIRSTN (value; rich_listTheory)
- IS_EL_FOLDL (value; rich_listTheory)
- IS_EL_FOLDL_MAP (value; rich_listTheory)
- IS_EL_FOLDR (value; rich_listTheory)
- IS_EL_FOLDR_MAP (value; rich_listTheory)
- IS_EL_LASTN (value; rich_listTheory)
- IS_EL_REPLICATE (value; rich_listTheory)
- IS_EL_REVERSE (value; rich_listTheory)
- IS_EL_SEG (value; rich_listTheory)
- IS_EL_SNOC (value; rich_listTheory)
- IS_EL_SOME_EL (value; rich_listTheory)
- is_finite (value; ieeeTheory)
- IS_FINITE_ALT (value; floatTheory)
- IS_FINITE_ALT1 (value; floatTheory)
- IS_FINITE_CLOSEST (value; floatTheory)
- IS_FINITE_EXPLICIT (value; floatTheory)
- IS_FINITE_FINITE (value; floatTheory)
- IS_FINITE_NONEMPTY (value; floatTheory)
- is_fmap (value; finite_mapTheory)
- is_fmap_cases (value; finite_mapTheory)
- is_fmap_ind (value; finite_mapTheory)
- is_fmap_rules (value; finite_mapTheory)
- is_fxp_closest_def (value; fxpTheory)
- IS_FXP_CLOSEST_EXISTS (value; fxpTheory)
- IS_GCD_0R (value; gcdTheory)
- is_gcd_def (value; gcdTheory)
- IS_GCD_MINUS_L (value; gcdTheory)
- IS_GCD_MINUS_R (value; gcdTheory)
- IS_GCD_REF (value; gcdTheory)
- IS_GCD_SYM (value; gcdTheory)
- IS_GCD_UNIQUE (value; gcdTheory)
- is_infinity (value; ieeeTheory)
- is_integral (value; ieeeTheory)
- is_nan (value; ieeeTheory)
- IS_NONE_DEF (value; optionTheory)
- IS_NONE_EQ_NONE (value; optionTheory)
- is_normal (value; ieeeTheory)
- IS_NUM_REP (value; numTheory)
- IS_PREFIX (value; rich_listTheory)
- IS_PREFIX_ANTISYM (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_APPEND (value; rich_listTheory)
- IS_PREFIX_APPEND1 (value; rich_listTheory)
- IS_PREFIX_APPEND2 (value; rich_listTheory)
- IS_PREFIX_APPENDS (value; rich_listTheory)
- IS_PREFIX_BUTLAST (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_IS_SUBLIST (value; rich_listTheory)
- IS_PREFIX_LENGTH (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_LENGTH_ANTI (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_NIL (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_PREFIX (value; rich_listTheory)
- IS_PREFIX_REFL (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_REVERSE (value; rich_listTheory)
- IS_PREFIX_SNOC (value; prob_extraTheory, rich_listTheory)
- IS_PREFIX_TRANS (value; prob_extraTheory, rich_listTheory)
- is_ring_def (value; ringTheory)
- is_semi_ring_def (value; semi_ringTheory)
- is_signed_def (value; fxpTheory)
- is_single (value; ieeeTheory)
- is_single_extended (value; ieeeTheory)
- IS_SOME_DEF (value; optionTheory)
- is_stopped_def (value; pathTheory)
- is_stopped_thm (value; pathTheory)
- IS_SUBLIST (value; rich_listTheory)
- IS_SUBLIST_APPEND (value; rich_listTheory)
- IS_SUBLIST_REVERSE (value; rich_listTheory)
- IS_SUFFIX (value; rich_listTheory)
- IS_SUFFIX_APPEND (value; rich_listTheory)
- IS_SUFFIX_IS_SUBLIST (value; rich_listTheory)
- IS_SUFFIX_REVERSE (value; rich_listTheory)
- IS_SUM_REP (value; sumTheory)
- is_unsigned_def (value; fxpTheory)
- IS_VALID (value; floatTheory)
- is_valid (value; ieeeTheory)
- IS_VALID_ATTRIB_NONEMPTY (value; fxpTheory)
- IS_VALID_CLOSEST (value; floatTheory)
- is_valid_def (value; fxpTheory)
- IS_VALID_DEFLOAT (value; floatTheory)
- IS_VALID_FINITE (value; floatTheory)
- IS_VALID_FXP_CLOSEST (value; fxpTheory)
- IS_VALID_NONEMPTY (value; floatTheory, fxpTheory)
- IS_VALID_ROUND (value; floatTheory)
- IS_VALID_ROUND_CONV_CLIP (value; fxpTheory)
- IS_VALID_SPECIAL (value; floatTheory)
- is_vstruct (value; pairTheory)
- is_zero (value; ieeeTheory)
- isacut (value; hrealTheory)
- ISACUT_HRAT (value; hrealTheory)
- Isdenormal (value; ieeeTheory)
- ISFINITE (value; floatTheory)
- ISFINITE_LEMMA (value; floatTheory)
- Isintegral (value; ieeeTheory)
- ISL (value; sumTheory)
- ISL_OR_ISR (value; sumTheory)
- ismet (value; topologyTheory)
- ISMET_R1 (value; topologyTheory)
- Isnan (value; ieeeTheory)
- Isnormal (value; ieeeTheory)
- ISO (value; ind_typeTheory)
- ISO_FUN (value; ind_typeTheory)
- ISO_REFL (value; ind_typeTheory)
- ISO_USAGE (value; ind_typeTheory)
- isPREFIX_curried_def (value; stringTheory)
- isPREFIX_DEF (value; stringTheory)
- isPREFIX_IND (value; stringTheory)
- isPREFIX_STRCAT (value; stringTheory)
- isPREFIX_tupled_primitive_def (value; stringTheory)
- iSQR (value; numeralTheory)
- ISR (value; sumTheory)
- Issigned_def (value; fxpTheory)
- istopology (value; topologyTheory)
- IsTrace_curried_def (value; MachineTransitionTheory)
- IsTrace_def (value; MachineTransitionTheory)
- IsTrace_ind (value; MachineTransitionTheory)
- IsTrace_tupled_primitive_def (value; MachineTransitionTheory)
- iSUB_DEF (value; numeralTheory)
- iSUB_THM (value; numeralTheory)
- Isunsigned_def (value; fxpTheory)
- ISVALID_ATTR_IMAGE (value; fxpTheory)
- ISVALID_ATTR_SUB (value; fxpTheory)
- Isvalid_def (value; fxpTheory)
- ISVALID_SUB (value; fxpTheory)
- ISVALID_WCAT (value; fxpTheory)
- ISVALID_WCATT (value; fxpTheory)
- ISVALIDNBWORD (value; fxpTheory)
- ISVALIDREPLICATE (value; fxpTheory)
- ISVALIDREPLICATEF (value; fxpTheory)
- ISVALIDWORDLEN (value; fxpTheory)
- ISVALISPECIAL (value; fxpTheory)
- Iszero (value; ieeeTheory)
- ITBAG_curried_def (value; bagTheory)
- ITBAG_EMPTY (value; bagTheory)
- ITBAG_IND (value; bagTheory)
- ITBAG_INSERT (value; bagTheory)
- ITBAG_THM (value; bagTheory)
- ITBAG_tupled_primitive_def (value; bagTheory)
- ITERATION (value; whileTheory)
- itself_Axiom (value; boolTheory)
- itself_case_thm (value; boolTheory)
- itself_induction (value; boolTheory)
- itself_TY_DEF (value; boolTheory)
- ITSELF_UNIQUE (value; boolTheory)
- ITSET_curried_def (value; pred_setTheory)
- ITSET_EMPTY (value; pred_setTheory)
- ITSET_IND (value; pred_setTheory)
- ITSET_INSERT (value; pred_setTheory)
- ITSET_THM (value; pred_setTheory)
- ITSET_tupled_primitive_def (value; pred_setTheory)
- ivl_aux_def (value; canonicalTheory, ringNormTheory)
- ivl_aux_ok (value; canonicalTheory)
- IVT (value; limTheory)
- IVT2 (value; limTheory)
- iZ (value; numeralTheory)
J
K
L
- L_EUCLIDES (value; gcdTheory)
- labels_def (value; pathTheory)
- LAMBDA_PROD (value; pairTheory)
- LAPPEND (value; llistTheory)
- LAPPEND_ASSOC (value; llistTheory)
- LAPPEND_EQ_LNIL (value; llistTheory)
- LAPPEND_NIL_2ND (value; llistTheory)
- largest (value; ieeeTheory)
- LAST (value; rich_listTheory)
- LAST_CONS (value; listTheory, rich_listTheory)
- LAST_DEF (value; listTheory)
- LAST_LASTN_LAST (value; rich_listTheory)
- LAST_MAP_CONS (value; prob_extraTheory)
- LAST_MEM (value; prob_extraTheory)
- last_plink (value; pathTheory)
- last_pmap (value; pathTheory)
- last_seg (value; pathTheory)
- last_take (value; pathTheory)
- last_thm (value; pathTheory)
- LASTN (value; rich_listTheory)
- LASTN1 (value; fxpTheory)
- LASTN_1 (value; rich_listTheory)
- LASTN_APPEND1 (value; rich_listTheory)
- LASTN_APPEND2 (value; rich_listTheory)
- LASTN_BUTFIRSTN (value; rich_listTheory)
- LASTN_BUTLASTN (value; rich_listTheory)
- LASTN_CONS (value; rich_listTheory)
- LASTN_LASTN (value; rich_listTheory)
- LASTN_LENGTH_APPEND (value; rich_listTheory)
- LASTN_LENGTH_ID (value; rich_listTheory)
- LASTN_MAP (value; rich_listTheory)
- LASTN_REVERSE (value; rich_listTheory)
- LASTN_SEG (value; rich_listTheory)
- LCOMM_THM (value; boolTheory)
- LCONS (value; llistTheory)
- LCONS_11 (value; llistTheory)
- LCONS_NOT_NIL (value; llistTheory)
- LDROP (value; llistTheory)
- LDROP1_THM (value; llistTheory)
- LDROP_THM (value; llistTheory)
- LE (value; arithmeticTheory)
- LE_ADD_LCANCEL (value; arithmeticTheory)
- LE_ADD_RCANCEL (value; arithmeticTheory)
- le_int (value; realTheory)
- LE_LT1 (value; arithmeticTheory)
- LE_MULT_LCANCEL (value; arithmeticTheory)
- LE_MULT_RCANCEL (value; arithmeticTheory)
- LE_NUM_CEILING (value; realTheory)
- LE_NUM_OF_INT (value; integerTheory)
- le_rat (value; realTheory)
- le_ratl (value; realTheory)
- le_ratr (value; realTheory)
- LE_SEQ_IMP_LE_LIM (value; seqTheory)
- LEAST_DEF (value; whileTheory)
- LEAST_ELIM (value; whileTheory)
- LEAST_EXISTS (value; whileTheory)
- LEAST_EXISTS_IMP (value; whileTheory)
- LEAST_INTRO (value; whileTheory)
- LEFT_ADD_DISTRIB (value; arithmeticTheory)
- LEFT_AND_FORALL_THM (value; boolTheory)
- LEFT_AND_OVER_OR (value; boolTheory)
- LEFT_EXISTS_AND_THM (value; boolTheory)
- LEFT_EXISTS_IMP_THM (value; boolTheory)
- LEFT_FORALL_IMP_THM (value; boolTheory)
- LEFT_FORALL_OR_THM (value; boolTheory)
- LEFT_ID_DEF (value; operatorTheory)
- Left_idx (value; quoteTheory)
- LEFT_OR_EXISTS_THM (value; boolTheory)
- LEFT_OR_OVER_AND (value; boolTheory)
- LEFT_SUB_DISTRIB (value; arithmeticTheory)
- LEN_DEF (value; listTheory)
- LEN_LENGTH_LEM (value; listTheory)
- LENGTH (value; listTheory, rich_listTheory)
- LENGTH_APPEND (value; listTheory, rich_listTheory)
- LENGTH_BUTFIRSTN (value; rich_listTheory)
- LENGTH_BUTLAST (value; rich_listTheory)
- LENGTH_BUTLASTN (value; rich_listTheory)
- LENGTH_CONS (value; listTheory, rich_listTheory)
- length_def (value; pathTheory)
- length_drop (value; pathTheory)
- LENGTH_EQ (value; rich_listTheory)
- LENGTH_EQ_CONS (value; listTheory)
- LENGTH_EQ_NIL (value; listTheory, rich_listTheory)
- LENGTH_FILTER (value; prob_extraTheory)
- LENGTH_FIRSTN (value; rich_listTheory)
- LENGTH_FLAT (value; rich_listTheory)
- LENGTH_FOLDL (value; rich_listTheory)
- LENGTH_FOLDR (value; rich_listTheory)
- LENGTH_GENLIST (value; rich_listTheory)
- LENGTH_LASTN (value; rich_listTheory)
- LENGTH_LEN (value; listTheory)
- LENGTH_MAP (value; listTheory, rich_listTheory)
- LENGTH_MAP2 (value; rich_listTheory)
- length_never_zero (value; pathTheory)
- LENGTH_NIL (value; listTheory, rich_listTheory)
- LENGTH_NOT_NULL (value; rich_listTheory)
- length_pmap (value; pathTheory)
- LENGTH_REPLICATE (value; rich_listTheory)
- LENGTH_REVERSE (value; rich_listTheory)
- LENGTH_SCANL (value; rich_listTheory)
- LENGTH_SCANR (value; rich_listTheory)
- LENGTH_SEG (value; rich_listTheory)
- LENGTH_SNOC (value; rich_listTheory)
- length_take (value; pathTheory)
- length_thm (value; pathTheory)
- LENGTH_UNZIP (value; listTheory)
- LENGTH_UNZIP_FST (value; rich_listTheory)
- LENGTH_UNZIP_SND (value; rich_listTheory)
- LENGTH_ZIP (value; listTheory, rich_listTheory)
- LESS_0 (value; prim_recTheory)
- LESS_0_0 (value; prim_recTheory)
- LESS_0_CASES (value; arithmeticTheory)
- LESS_ADD (value; arithmeticTheory)
- LESS_ADD_1 (value; arithmeticTheory)
- LESS_ADD_NONZERO (value; arithmeticTheory)
- LESS_ADD_SUC (value; arithmeticTheory)
- LESS_ANTISYM (value; arithmeticTheory)
- LESS_CARD_DIFF (value; pred_setTheory)
- LESS_CASES (value; arithmeticTheory)
- LESS_CASES_IMP (value; arithmeticTheory)
- LESS_DEF (value; prim_recTheory)
- LESS_def (value; prelimTheory)
- LESS_DIV_EQ_ZERO (value; arithmeticTheory)
- LESS_EQ (value; arithmeticTheory)
- LESS_EQ_0 (value; arithmeticTheory)
- LESS_EQ_ADD (value; arithmeticTheory)
- LESS_EQ_ADD_SUB (value; arithmeticTheory)
- LESS_EQ_ANTISYM (value; arithmeticTheory)
- LESS_EQ_CASES (value; arithmeticTheory)
- LESS_EQ_EXISTS (value; arithmeticTheory)
- LESS_EQ_EXP_MULT (value; bitTheory)
- LESS_EQ_IMP_LESS_SUC (value; arithmeticTheory)
- LESS_EQ_LESS_EQ_MONO (value; arithmeticTheory)
- LESS_EQ_LESS_TRANS (value; arithmeticTheory)
- LESS_EQ_MONO (value; arithmeticTheory)
- LESS_EQ_MONO_ADD_EQ (value; arithmeticTheory)
- LESS_EQ_REFL (value; arithmeticTheory)
- LESS_EQ_SUB_LESS (value; arithmeticTheory)
- LESS_EQ_SUC_REFL (value; arithmeticTheory)
- LESS_EQ_TRANS (value; arithmeticTheory)
- LESS_EQUAL_ADD (value; arithmeticTheory)
- LESS_EQUAL_ANTISYM (value; arithmeticTheory)
- LESS_EQUAL_DIFF (value; arithmeticTheory)
- LESS_EXP_SUC_MONO (value; arithmeticTheory)
- LESS_IMP_LESS_ADD (value; arithmeticTheory)
- LESS_IMP_LESS_OR_EQ (value; arithmeticTheory)
- LESS_LEAST (value; whileTheory)
- LESS_LEMMA1 (value; prim_recTheory)
- LESS_LEMMA2 (value; prim_recTheory)
- LESS_LESS_CASES (value; arithmeticTheory)
- LESS_LESS_EQ_TRANS (value; arithmeticTheory)
- LESS_LESS_SUC (value; arithmeticTheory)
- LESS_MOD (value; arithmeticTheory)
- LESS_MONO (value; prim_recTheory)
- LESS_MONO_ADD (value; arithmeticTheory)
- LESS_MONO_ADD_EQ (value; arithmeticTheory)
- LESS_MONO_ADD_INV (value; arithmeticTheory)
- LESS_MONO_EQ (value; arithmeticTheory)
- LESS_MONO_MULT (value; arithmeticTheory)
- LESS_MONO_MULT2 (value; arithmeticTheory)
- LESS_MONO_REV (value; arithmeticTheory)
- LESS_MULT2 (value; arithmeticTheory)
- LESS_MULT_MONO (value; arithmeticTheory)
- LESS_NOT_EQ (value; prim_recTheory)
- LESS_NOT_SUC (value; arithmeticTheory)
- LESS_OR (value; arithmeticTheory)
- LESS_OR_EQ (value; arithmeticTheory)
- LESS_OR_EQ_ADD (value; arithmeticTheory)
- LESS_REFL (value; prim_recTheory)
- LESS_SUB_ADD_LESS (value; arithmeticTheory)
- LESS_SUC (value; prim_recTheory)
- LESS_SUC_EQ_COR (value; arithmeticTheory)
- LESS_SUC_IMP (value; prim_recTheory)
- LESS_SUC_NOT (value; arithmeticTheory)
- LESS_SUC_REFL (value; prim_recTheory)
- LESS_SUC_SUC (value; prim_recTheory)
- LESS_THM (value; Omega_AutomataTheory, prim_recTheory)
- LESS_TRANS (value; arithmeticTheory)
- LET2_RAND (value; pairTheory)
- LET2_RATOR (value; pairTheory)
- LET_CONG (value; boolTheory)
- LET_DEF (value; boolTheory)
- LET_FORALL_ELIM (value; combinTheory)
- LET_RAND (value; boolTheory)
- LET_RATOR (value; boolTheory)
- LET_THM (value; boolTheory)
- LEX_DEF (value; pairTheory)
- LEX_DEF_THM (value; pairTheory)
- LFILTER (value; llistTheory)
- LFILTER_APPEND (value; llistTheory)
- LFILTER_EQ_NIL (value; llistTheory)
- LFILTER_NIL (value; llistTheory)
- LFILTER_THM (value; llistTheory)
- LFINITE (value; llistTheory)
- LFINITE_APPEND (value; llistTheory)
- LFINITE_cases (value; llistTheory)
- LFINITE_DROP (value; llistTheory)
- LFINITE_fromList (value; llistTheory)
- LFINITE_HAS_LENGTH (value; llistTheory)
- LFINITE_ind (value; llistTheory)
- LFINITE_INDUCTION (value; llistTheory)
- LFINITE_MAP (value; llistTheory)
- LFINITE_rules (value; llistTheory)
- LFINITE_STRONG_INDUCTION (value; llistTheory)
- LFINITE_TAKE (value; llistTheory)
- LFINITE_THM (value; llistTheory)
- LFINITE_toList (value; llistTheory)
- LFLATTEN (value; llistTheory)
- LFLATTEN_APPEND (value; llistTheory)
- LFLATTEN_EQ_NIL (value; llistTheory)
- LFLATTEN_SINGLETON (value; llistTheory)
- LFLATTEN_THM (value; llistTheory)
- lfp_def (value; fixedPointTheory)
- lfp_empty (value; fixedPointTheory)
- lfp_fixedpoint (value; fixedPointTheory)
- lfp_fnsum (value; fixedPointTheory)
- lfp_induction (value; fixedPointTheory)
- lfp_least_closed (value; fixedPointTheory)
- lfp_rule_applied (value; fixedPointTheory)
- lfp_strong_induction (value; fixedPointTheory)
- LHD (value; llistTheory)
- LHD_EQ_NONE (value; llistTheory)
- LHD_LCONS (value; llistTheory)
- LHD_THM (value; llistTheory)
- LHDTL_CONS_THM (value; llistTheory)
- LHDTL_EQ_SOME (value; llistTheory)
- lift_blist_def (value; EncodeTheory)
- lift_blist_suc (value; EncodeTheory)
- lift_option_def (value; EncodeTheory)
- lift_prod_def (value; EncodeTheory)
- lift_sum_def (value; EncodeTheory)
- lift_tree_curried_def (value; EncodeTheory)
- lift_tree_def (value; EncodeTheory)
- lift_tree_tupled_primitive_def (value; EncodeTheory)
- LIM (value; limTheory)
- lim (value; seqTheory)
- LIM_ADD (value; limTheory)
- LIM_CONST (value; limTheory)
- LIM_DIV (value; limTheory)
- LIM_EQUAL (value; limTheory)
- lim_grammars (value; limTheory)
- LIM_INV (value; limTheory)
- LIM_MUL (value; limTheory)
- LIM_NEG (value; limTheory)
- LIM_NULL (value; limTheory)
- LIM_SUB (value; limTheory)
- LIM_TENDS (value; netsTheory)
- LIM_TENDS2 (value; netsTheory)
- LIM_TRANSFORM (value; limTheory)
- LIM_UNIQ (value; limTheory)
- LIM_X (value; limTheory)
- limpt (value; topologyTheory)
- limTheory (structure)
- LINEAR_GCD (value; gcdTheory)
- LinearOrder (value; relationTheory)
- LINV_DEF (value; pred_setTheory)
- list0_def (value; listTheory)
- list1_def (value; listTheory)
- list_11 (value; listTheory)
- list_Axiom (value; listTheory)
- list_Axiom_old (value; listTheory)
- list_case_compute (value; listTheory)
- list_case_cong (value; listTheory)
- list_case_def (value; listTheory)
- list_CASES (value; listTheory, rich_listTheory)
- list_coder_def (value; CoderTheory)
- list_compare_curried_def (value; prelimTheory)
- list_compare_def (value; prelimTheory)
- list_compare_ind (value; prelimTheory)
- list_compare_tupled_primitive_def (value; prelimTheory)
- list_distinct (value; listTheory)
- list_grammars (value; listTheory)
- list_INDUCT (value; listTheory, rich_listTheory)
- list_induction (value; listTheory)
- list_merge_curried_def (value; prelimTheory)
- list_merge_def (value; prelimTheory)
- list_merge_ind (value; prelimTheory)
- list_merge_tupled_primitive_def (value; prelimTheory)
- list_nchotomy (value; listTheory)
- LIST_NOT_EQ (value; listTheory, rich_listTheory)
- list_repfns (value; listTheory)
- list_rwts (value; listTheory)
- list_size_cong (value; listTheory)
- list_size_def (value; listTheory)
- LIST_TO_BAG (value; containerTheory)
- LIST_TO_SET (value; listTheory)
- LIST_TO_SET_APPEND (value; containerTheory)
- LIST_TO_SET_THM (value; containerTheory)
- list_TY_DEF (value; listTheory)
- listEncode0_repfns (value; EncodeTheory)
- listEncode0_TY_DEF (value; EncodeTheory)
- listRel (value; listTheory)
- listRel_cases (value; listTheory)
- listRel_CONS (value; listTheory)
- listRel_ind (value; listTheory)
- listRel_LENGTH (value; listTheory)
- listRel_NIL (value; listTheory)
- listRel_rules (value; listTheory)
- listRel_strong_ind (value; listTheory)
- listTheory (structure)
- literal_case_CONG (value; boolTheory)
- literal_case_DEF (value; boolTheory)
- literal_case_FORALL_ELIM (value; combinTheory)
- literal_case_RAND (value; boolTheory)
- literal_case_RATOR (value; boolTheory)
- literal_case_THM (value; boolTheory)
- Live_def (value; MachineTransitionTheory)
- LL_ALL_THM (value; llistTheory)
- LLENGTH (value; llistTheory)
- LLENGTH_APPEND (value; llistTheory)
- LLENGTH_fromList (value; llistTheory)
- LLENGTH_MAP (value; llistTheory)
- llength_rel (value; llistTheory)
- llength_rel_cases (value; llistTheory)
- llength_rel_ind (value; llistTheory)
- llength_rel_rules (value; llistTheory)
- LLENGTH_THM (value; llistTheory)
- llist_absrep (value; llistTheory)
- llist_Axiom (value; llistTheory)
- llist_Axiom_1 (value; llistTheory)
- llist_Axiom_1ue (value; llistTheory)
- LLIST_BISIMULATION (value; llistTheory)
- LLIST_BISIMULATION0 (value; llistTheory)
- llist_CASES (value; llistTheory)
- llist_grammars (value; llistTheory)
- llist_rep_LCONS (value; llistTheory)
- llist_rwts (value; llistTheory)
- LLIST_STRONG_BISIMULATION (value; llistTheory)
- llist_TY_DEF (value; llistTheory)
- llist_ue_Axiom (value; llistTheory)
- llistTheory (structure)
- LMAP (value; llistTheory)
- LMAP_APPEND (value; llistTheory)
- LMAP_MAP (value; llistTheory)
- ln (value; transcTheory)
- LN_1 (value; transcTheory)
- LN_DIV (value; transcTheory)
- LN_EXP (value; transcTheory)
- LN_INJ (value; transcTheory)
- LN_INV (value; transcTheory)
- LN_LE (value; transcTheory)
- LN_LT_X (value; transcTheory)
- LN_MONO_LE (value; transcTheory)
- LN_MONO_LT (value; transcTheory)
- LN_MUL (value; transcTheory)
- LN_POS (value; transcTheory)
- LN_POW (value; transcTheory)
- LNIL (value; llistTheory)
- LNTH (value; llistTheory)
- LNTH_EQ (value; llistTheory)
- LNTH_THM (value; llistTheory)
- LOG2_def (value; bitTheory)
- LOG2_UNIQUE (value; bitTheory)
- loss_sign (value; fxpTheory)
- lrep_ok_def (value; llistTheory)
- LSB (value; word_baseTheory)
- LSB_DEF (value; word_baseTheory)
- LSB_def (value; bitTheory)
- LSB_ODD (value; bitTheory)
- LSL_ADD (value; wordsTheory)
- LSL_BITWISE (value; wordsTheory)
- LSL_LIMIT (value; wordsTheory)
- LSL_ONE (value; wordsTheory)
- LSL_UINT_MAX (value; wordsTheory)
- LSR_ADD (value; wordsTheory)
- LSR_BITWISE (value; wordsTheory)
- LSR_LIMIT (value; wordsTheory)
- Lt (value; ieeeTheory)
- lt1eqmul (value; floatTheory)
- LT_ADD2 (value; integerTheory)
- LT_ADD_LCANCEL (value; arithmeticTheory)
- LT_ADD_RCANCEL (value; arithmeticTheory)
- LT_ADDL (value; integerTheory)
- LT_ADDR (value; integerTheory)
- lt_int (value; realTheory)
- LT_LADD (value; integerTheory)
- LT_MULT_LCANCEL (value; arithmeticTheory)
- LT_MULT_RCANCEL (value; arithmeticTheory)
- lt_rat (value; realTheory)
- lt_ratl (value; realTheory)
- lt_ratr (value; realTheory)
- LT_SUC_LE (value; floatTheory)
- LT_THRESHOLD_LT_POW_INV (value; floatTheory)
- LTAKE (value; llistTheory)
- LTAKE_CONS_EQ_NONE (value; llistTheory)
- LTAKE_CONS_EQ_SOME (value; llistTheory)
- LTAKE_DROP (value; llistTheory)
- LTAKE_EQ (value; llistTheory)
- LTAKE_EQ_SOME_CONS (value; llistTheory)
- LTAKE_fromList (value; llistTheory)
- LTAKE_LNTH (value; llistTheory)
- LTAKE_NIL_EQ_NONE (value; llistTheory)
- LTAKE_NIL_EQ_SOME (value; llistTheory)
- LTAKE_SNOC_LNTH (value; llistTheory)
- LTAKE_THM (value; llistTheory)
- LTL (value; llistTheory)
- LTL_EQ_NONE (value; llistTheory)
- LTL_LCONS (value; llistTheory)
- LTL_THM (value; llistTheory)
- LUNFOLD (value; llistTheory)
- LUNZIP_THM (value; llistTheory)
- LVAL (value; word_numTheory)
- LVAL_DEF (value; word_numTheory)
- LVAL_MAX (value; word_numTheory)
- LVAL_SNOC (value; word_numTheory)
- LZIP_LUNZIP (value; llistTheory)
- LZIP_THM (value; llistTheory)
M
- MachineTransition_grammars (value; MachineTransitionTheory)
- MachineTransitionTheory (structure)
- MAINFINITE (value; fxpTheory)
- MAP (value; listTheory, rich_listTheory)
- MAP2 (value; listTheory, rich_listTheory)
- MAP2_ZIP (value; listTheory, rich_listTheory)
- MAP_APPEND (value; listTheory, rich_listTheory)
- MAP_CONG (value; listTheory)
- MAP_CONS_TL_FILTER (value; prob_indepTheory)
- MAP_EQ_NIL (value; listTheory)
- MAP_FILTER (value; rich_listTheory)
- MAP_FLAT (value; rich_listTheory)
- MAP_FOLDL (value; rich_listTheory)
- MAP_FOLDR (value; rich_listTheory)
- MAP_ID (value; prob_extraTheory)
- MAP_MAP_o (value; rich_listTheory)
- MAP_MEM (value; prob_extraTheory)
- MAP_o (value; rich_listTheory)
- MAP_REVERSE (value; rich_listTheory)
- MAP_SNOC (value; rich_listTheory)
- MATCH_FLOAT_FINITE (value; floatTheory)
- MATCHFINITE (value; fxpTheory)
- MATCHFINITEVALID (value; fxpTheory)
- MATCHFINITEVALIDATTR (value; fxpTheory)
- MAX_0 (value; arithmeticTheory)
- MAX_ASSOC (value; arithmeticTheory)
- MAX_COMM (value; arithmeticTheory)
- MAX_DEF (value; arithmeticTheory)
- MAX_def (value; fxpTheory)
- max_def (value; realTheory)
- MAX_IDEM (value; arithmeticTheory)
- MAX_LE (value; arithmeticTheory)
- MAX_LEMMA (value; seqTheory)
- MAX_LT (value; arithmeticTheory)
- MAX_SET_DEF (value; pred_setTheory)
- MAX_SET_THM (value; pred_setTheory)
- MAX_SET_UNION (value; pred_setTheory)
- maxmin (value; fxpTheory)
- MCLAURIN (value; transcTheory)
- MCLAURIN_ALL_LE (value; transcTheory)
- MCLAURIN_ALL_LT (value; transcTheory)
- MCLAURIN_EXP_LE (value; transcTheory)
- MCLAURIN_EXP_LT (value; transcTheory)
- MCLAURIN_NEG (value; transcTheory)
- MCLAURIN_ZERO (value; transcTheory)
- MEASURABLE_ALGEBRA (value; prob_algebraTheory)
- MEASURABLE_BASIC (value; prob_algebraTheory)
- MEASURABLE_COMPL (value; prob_algebraTheory)
- measurable_def (value; prob_algebraTheory)
- MEASURABLE_HALVES (value; prob_algebraTheory)
- MEASURABLE_INTER (value; prob_algebraTheory)
- MEASURABLE_INTER_HALVES (value; prob_algebraTheory)
- MEASURABLE_INTER_SHD (value; prob_algebraTheory)
- MEASURABLE_SDROP (value; prob_algebraTheory)
- MEASURABLE_SHD (value; prob_algebraTheory)
- MEASURABLE_STL (value; prob_algebraTheory)
- MEASURABLE_UNION (value; prob_algebraTheory)
- measure_def (value; prim_recTheory)
- measure_thm (value; prim_recTheory)
- MEM (value; listTheory)
- MEM_APPEND (value; listTheory)
- MEM_BAG_TO_LIST (value; containerTheory)
- mem_def (value; pathTheory)
- MEM_EL (value; listTheory)
- MEM_FILTER (value; listTheory, prob_extraTheory)
- MEM_MAP (value; listTheory)
- MEM_NIL (value; prob_extraTheory)
- MEM_NIL_MAP_CONS (value; prob_extraTheory)
- MEM_NIL_STEP (value; prob_canonTheory)
- MEM_REVERSE (value; listTheory)
- MEM_SET_TO_LIST (value; containerTheory)
- mem_thm (value; pathTheory)
- MEM_ZIP (value; listTheory)
- MEMBER_NOT_EMPTY (value; bagTheory, pred_setTheory)
- METRIC_ISMET (value; topologyTheory)
- METRIC_NZ (value; topologyTheory)
- METRIC_POS (value; topologyTheory)
- METRIC_SAME (value; topologyTheory)
- METRIC_SYM (value; topologyTheory)
- METRIC_TRIANGLE (value; topologyTheory)
- metric_TY_DEF (value; topologyTheory)
- metric_tybij (value; topologyTheory)
- METRIC_ZERO (value; topologyTheory)
- MIN_0 (value; arithmeticTheory)
- MIN_ASSOC (value; arithmeticTheory)
- MIN_COMM (value; arithmeticTheory)
- MIN_DEF (value; arithmeticTheory)
- MIN_def (value; fxpTheory)
- min_def (value; realTheory)
- MIN_IDEM (value; arithmeticTheory)
- MIN_LE (value; arithmeticTheory)
- MIN_LT (value; arithmeticTheory)
- MIN_MAX_EQ (value; arithmeticTheory)
- MIN_MAX_LE (value; arithmeticTheory)
- MIN_MAX_LT (value; arithmeticTheory)
- MIN_MAX_PRED (value; arithmeticTheory)
- MIN_SET_DEF (value; pred_setTheory)
- MIN_SET_ELIM (value; pred_setTheory)
- MIN_SET_LEM (value; pred_setTheory)
- MIN_SET_LEQ_MAX_SET (value; pred_setTheory)
- MIN_SET_THM (value; pred_setTheory)
- MIN_SET_UNION (value; pred_setTheory)
- minus (value; ieeeTheory)
- Minus_infinity (value; ieeeTheory)
- minus_infinity (value; ieeeTheory)
- Minus_zero (value; ieeeTheory)
- minus_zero (value; ieeeTheory)
- mk_pabs (value; pairTheory)
- MK_REC_INJ (value; ind_typeTheory)
- MMAP_COMP (value; state_transformerTheory)
- MMAP_DEF (value; state_transformerTheory)
- MMAP_ID (value; state_transformerTheory)
- MMAP_JOIN (value; state_transformerTheory)
- MMAP_UNIT (value; state_transformerTheory)
- MOD_1 (value; arithmeticTheory)
- MOD_2 (value; arithmeticTheory)
- MOD_2EXP (value; numeralTheory)
- MOD_2EXP_def (value; arithmeticTheory)
- MOD_2EXP_DIMINDEX (value; wordsTheory)
- MOD_2EXP_LT (value; bitTheory)
- MOD_2EXP_MONO (value; bitTheory)
- MOD_ADD_1 (value; bitTheory)
- MOD_COMMON_FACTOR (value; arithmeticTheory)
- MOD_DIMINDEX (value; wordsTheory)
- MOD_ELIM (value; arithmeticTheory)
- MOD_EQ_0 (value; arithmeticTheory)
- MOD_MOD (value; arithmeticTheory)
- MOD_MULT (value; arithmeticTheory)
- MOD_MULT_MOD (value; arithmeticTheory)
- MOD_ONE (value; arithmeticTheory)
- MOD_P (value; arithmeticTheory)
- MOD_P_UNIV (value; arithmeticTheory)
- MOD_PLUS (value; arithmeticTheory)
- MOD_PLUS_1 (value; bitTheory)
- MOD_PLUS_RIGHT (value; bitTheory)
- MOD_SUB (value; arithmeticTheory)
- MOD_TIMES (value; arithmeticTheory)
- MOD_TIMES2 (value; arithmeticTheory)
- MOD_TWO (value; prob_extraTheory)
- MOD_UNIQUE (value; arithmeticTheory)
- ModelCheckAlways (value; MachineTransitionTheory)
- ModelCheckAlwaysCor1 (value; MachineTransitionTheory)
- ModelCheckAlwaysCor2 (value; MachineTransitionTheory)
- mono (value; seqTheory)
- MONO_ALL (value; boolTheory)
- MONO_AND (value; boolTheory)
- MONO_COND (value; boolTheory)
- MONO_EVERY (value; listTheory)
- MONO_every (value; llistTheory)
- MONO_EXISTS (value; boolTheory, listTheory)
- MONO_exists (value; llistTheory)
- MONO_IMP (value; boolTheory)
- MONO_listRel (value; listTheory)
- MONO_NOT (value; boolTheory)
- MONO_OR (value; boolTheory)
- MONO_SUC (value; seqTheory)
- MONOID_APPEND_NIL (value; rich_listTheory)
- MONOID_CONJ_T (value; operatorTheory)
- MONOID_DEF (value; operatorTheory)
- MONOID_DISJ_F (value; operatorTheory)
- monom_insert_curried_def (value; canonicalTheory)
- monom_insert_def (value; canonicalTheory, ringNormTheory)
- monom_insert_ind (value; canonicalTheory)
- monom_insert_ok (value; canonicalTheory)
- monom_insert_tupled_primitive_def (value; canonicalTheory)
- monotone_def (value; fixedPointTheory)
- Moore_def (value; MachineTransitionTheory)
- MoorePath (value; MachineTransitionTheory)
- MooreReachable (value; MachineTransitionTheory)
- MooreReachable1 (value; MachineTransitionTheory)
- MooreReachable2 (value; MachineTransitionTheory)
- MooreReachableCor1 (value; MachineTransitionTheory)
- MooreReachableExists (value; MachineTransitionTheory)
- MooreTrans_def (value; MachineTransitionTheory)
- MooreTransEq (value; MachineTransitionTheory)
- MORE_EVENT (value; Past_Temporal_LogicTheory, Temporal_LogicTheory)
- move_BAG_UNION_over_eq (value; bagTheory)
- mr1 (value; topologyTheory)
- MR1_ADD (value; topologyTheory)
- MR1_ADD_LT (value; topologyTheory)
- MR1_ADD_POS (value; topologyTheory)
- MR1_BETWEEN1 (value; topologyTheory)
- MR1_BOUNDED (value; netsTheory)
- MR1_DEF (value; topologyTheory)
- MR1_LIMPT (value; topologyTheory)
- MR1_SUB (value; topologyTheory)
- MR1_SUB_LE (value; topologyTheory)
- MR1_SUB_LT (value; topologyTheory)
- MSB (value; word_baseTheory)
- MSB_DEF (value; word_baseTheory)
- MSB_NBWORD (value; bword_numTheory)
- mtop (value; topologyTheory)
- mtop_istopology (value; topologyTheory)
- MTOP_LIMPT (value; topologyTheory)
- MTOP_OPEN (value; topologyTheory)
- MTOP_TENDS (value; netsTheory)
- MTOP_TENDS_UNIQ (value; netsTheory)
- MULT (value; arithmeticTheory)
- MULT_0 (value; arithmeticTheory)
- MULT_ASSOC (value; arithmeticTheory)
- mult_assoc (value; ringTheory, semi_ringTheory)
- MULT_CLAUSES (value; arithmeticTheory)
- MULT_COMM (value; arithmeticTheory)
- MULT_DIV (value; arithmeticTheory)
- MULT_EQ_0 (value; arithmeticTheory)
- MULT_EQ_1 (value; arithmeticTheory)
- MULT_EQ_DIV (value; arithmeticTheory)
- MULT_EXP_MONO (value; arithmeticTheory)
- MULT_INCREASES (value; arithmeticTheory)
- mult_ints (value; realTheory)
- MULT_LEFT_1 (value; arithmeticTheory)
- MULT_LESS_EQ_SUC (value; arithmeticTheory)
- MULT_MONO_EQ (value; arithmeticTheory)
- mult_one_left (value; ringTheory, semi_ringTheory)
- mult_one_right (value; ringTheory, semi_ringTheory)
- mult_permute (value; semi_ringTheory)
- mult_rat (value; realTheory)
- mult_ratl (value; realTheory)
- mult_ratr (value; realTheory)
- MULT_RIGHT_1 (value; arithmeticTheory)
- mult_rotate (value; semi_ringTheory)
- MULT_SUC (value; arithmeticTheory)
- MULT_SUC_EQ (value; arithmeticTheory)
- MULT_SYM (value; arithmeticTheory)
- mult_sym (value; ringTheory, semi_ringTheory)
- mult_zero_left (value; ringTheory, semi_ringTheory)
- mult_zero_right (value; ringTheory, semi_ringTheory)
- MVT (value; limTheory)
- MVT_LEMMA (value; limTheory)
N
O
P
Q
R
- r_canonical_sum_merge_def (value; ringNormTheory)
- r_canonical_sum_prod_def (value; ringNormTheory)
- r_canonical_sum_scalar2_def (value; ringNormTheory)
- r_canonical_sum_scalar3_def (value; ringNormTheory)
- r_canonical_sum_scalar_def (value; ringNormTheory)
- r_canonical_sum_simplify_def (value; ringNormTheory)
- r_ics_aux_def (value; ringNormTheory)
- r_interp_cs_def (value; ringNormTheory)
- r_interp_m_def (value; ringNormTheory)
- r_interp_sp_def (value; ringNormTheory)
- r_interp_vl_def (value; ringNormTheory)
- r_ivl_aux_def (value; ringNormTheory)
- r_monom_insert_def (value; ringNormTheory)
- r_spolynom_normalize_def (value; ringNormTheory)
- r_spolynom_simplify_def (value; ringNormTheory)
- r_varlist_insert_def (value; ringNormTheory)
- RAND_THM (value; prob_extraTheory)
- ranged_word_nchotomy (value; wordsTheory)
- RAT (value; ratTheory)
- RAT_0 (value; ratTheory)
- rat_0 (value; ratTheory)
- rat_0_def (value; ratTheory)
- RAT_0LEQ_NMR (value; ratTheory)
- RAT_0LES_0LEQ_ADD (value; ratTheory)
- RAT_0LES_0LES_ADD (value; ratTheory)
- RAT_0LES_NMR (value; ratTheory)
- RAT_1 (value; ratTheory)
- rat_1 (value; ratTheory)
- rat_1_def (value; ratTheory)
- RAT_1_NOT_0 (value; ratTheory)
- RAT_ABS_EQUIV (value; ratTheory)
- rat_ABS_REP_CLASS (value; ratTheory)
- RAT_ADD_ASSOC (value; ratTheory)
- RAT_ADD_CALCULATE (value; ratTheory)
- RAT_ADD_COMM (value; ratTheory)
- RAT_ADD_CONG (value; ratTheory)
- RAT_ADD_CONG1 (value; ratTheory)
- RAT_ADD_CONG2 (value; ratTheory)
- rat_add_def (value; ratTheory)
- RAT_ADD_LID (value; ratTheory)
- RAT_ADD_LINV (value; ratTheory)
- RAT_ADD_NUM_CALCULATE (value; ratTheory)
- RAT_ADD_ONE_ONE (value; ratTheory)
- RAT_ADD_RID (value; ratTheory)
- RAT_ADD_RINV (value; ratTheory)
- RAT_AINV_0 (value; ratTheory)
- RAT_AINV_ADD (value; ratTheory)
- RAT_AINV_AINV (value; ratTheory)
- RAT_AINV_CALCULATE (value; ratTheory)
- RAT_AINV_CONG (value; ratTheory)
- rat_ainv_def (value; ratTheory)
- RAT_AINV_EQ (value; ratTheory)
- RAT_AINV_LES (value; ratTheory)
- RAT_AINV_LMUL (value; ratTheory)
- RAT_AINV_MINV (value; ratTheory)
- RAT_AINV_ONE_ONE (value; ratTheory)
- RAT_AINV_RMUL (value; ratTheory)
- RAT_AINV_SUB (value; ratTheory)
- rat_bijections (value; ratTheory)
- rat_cons_def (value; ratTheory)
- RAT_CONS_TO_NUM (value; ratTheory)
- rat_def (value; ratTheory)
- RAT_DENSE_THM (value; ratTheory)
- RAT_DIV_CALCULATE (value; ratTheory)
- RAT_DIV_CONG (value; ratTheory)
- RAT_DIV_CONG1 (value; ratTheory)
- RAT_DIV_CONG2 (value; ratTheory)
- rat_div_def (value; ratTheory)
- RAT_DIV_MULMINV (value; ratTheory)
- rat_dnm_def (value; ratTheory)
- RAT_EQ (value; ratTheory)
- RAT_EQ0_NMR (value; ratTheory)
- RAT_EQ_0SUB (value; ratTheory)
- RAT_EQ_AINV (value; ratTheory)
- RAT_EQ_ALT (value; ratTheory)
- RAT_EQ_CALCULATE (value; ratTheory)
- RAT_EQ_LADD (value; ratTheory)
- RAT_EQ_LMUL (value; ratTheory)
- RAT_EQ_NUM_CALCULATE (value; ratTheory)
- RAT_EQ_RADD (value; ratTheory)
- RAT_EQ_RMUL (value; ratTheory)
- RAT_EQ_SUB0 (value; ratTheory)
- RAT_EQUIV (value; ratTheory)
- RAT_EQUIV_ALT (value; ratTheory)
- rat_equiv_def (value; ratTheory)
- RAT_EQUIV_REF (value; ratTheory)
- RAT_EQUIV_SYM (value; ratTheory)
- RAT_EQUIV_TRANS (value; ratTheory)
- rat_geq_def (value; ratTheory)
- rat_grammars (value; ratTheory)
- rat_gre_def (value; ratTheory)
- RAT_LDISTRIB (value; ratTheory)
- RAT_LDIV_EQ (value; ratTheory)
- RAT_LDIV_LES_NEG (value; ratTheory)
- RAT_LDIV_LES_POS (value; ratTheory)
- RAT_LEQ0_NMR (value; ratTheory)
- RAT_LEQ_ANTISYM (value; ratTheory)
- rat_leq_def (value; ratTheory)
- RAT_LEQ_LES (value; ratTheory)
- RAT_LEQ_LES_TRANS (value; ratTheory)
- RAT_LEQ_REF (value; ratTheory)
- RAT_LEQ_TRANS (value; ratTheory)
- RAT_LES0_LEQ0_ADD (value; ratTheory)
- RAT_LES0_LES0_ADD (value; ratTheory)
- RAT_LES0_NMR (value; ratTheory)
- RAT_LES_01 (value; ratTheory)
- RAT_LES_0SUB (value; ratTheory)
- RAT_LES_AINV (value; ratTheory)
- RAT_LES_ANTISYM (value; ratTheory)
- RAT_LES_CALCULATE (value; ratTheory)
- rat_les_def (value; ratTheory)
- RAT_LES_IMP_LEQ (value; ratTheory)
- RAT_LES_IMP_NEQ (value; ratTheory)
- RAT_LES_LADD (value; ratTheory)
- RAT_LES_LEQ (value; ratTheory)
- RAT_LES_LEQ2 (value; ratTheory)
- RAT_LES_LEQ_TRANS (value; ratTheory)
- RAT_LES_LMUL_NEG (value; ratTheory)
- RAT_LES_LMUL_POS (value; ratTheory)
- RAT_LES_RADD (value; ratTheory)
- RAT_LES_REF (value; ratTheory)
- RAT_LES_RMUL_NEG (value; ratTheory)
- RAT_LES_RMUL_POS (value; ratTheory)
- RAT_LES_SUB0 (value; ratTheory)
- RAT_LES_TOTAL (value; ratTheory)
- RAT_LES_TRANS (value; ratTheory)
- RAT_LSUB_EQ (value; ratTheory)
- RAT_LSUB_LES (value; ratTheory)
- RAT_MINV_CALCULATE (value; ratTheory)
- RAT_MINV_CONG (value; ratTheory)
- rat_minv_def (value; ratTheory)
- RAT_MINV_LES (value; ratTheory)
- RAT_MUL_ASSOC (value; ratTheory)
- RAT_MUL_CALCULATE (value; ratTheory)
- RAT_MUL_COMM (value; ratTheory)
- RAT_MUL_CONG (value; ratTheory)
- RAT_MUL_CONG1 (value; ratTheory)
- RAT_MUL_CONG2 (value; ratTheory)
- rat_mul_def (value; ratTheory)
- RAT_MUL_LID (value; ratTheory)
- RAT_MUL_LINV (value; ratTheory)
- RAT_MUL_LZERO (value; ratTheory)
- RAT_MUL_NUM_CALCULATE (value; ratTheory)
- RAT_MUL_ONE_ONE (value; ratTheory)
- RAT_MUL_RID (value; ratTheory)
- RAT_MUL_RINV (value; ratTheory)
- RAT_MUL_RZERO (value; ratTheory)
- RAT_MUL_SIGN_CASES (value; ratTheory)
- rat_nmr_def (value; ratTheory)
- RAT_NMRDNM_EQ (value; ratTheory)
- RAT_NMREQ0_CONG (value; ratTheory)
- RAT_NMRGT0_CONG (value; ratTheory)
- RAT_NMRLT0_CONG (value; ratTheory)
- RAT_NO_IDDIV (value; ratTheory)
- RAT_NO_ZERODIV (value; ratTheory)
- RAT_NO_ZERODIV_NEG (value; ratTheory)
- RAT_OF_NUM (value; ratTheory)
- RAT_OF_NUM_CALCULATE (value; ratTheory)
- rat_of_num_def (value; ratTheory)
- rat_of_num_ind (value; ratTheory)
- rat_of_num_primitive_def (value; ratTheory)
- rat_QUOTIENT (value; ratTheory)
- RAT_RDISTRIB (value; ratTheory)
- RAT_RDIV_EQ (value; ratTheory)
- RAT_RDIV_LES_NEG (value; ratTheory)
- RAT_RDIV_LES_POS (value; ratTheory)
- RAT_RSUB_EQ (value; ratTheory)
- RAT_RSUB_LES (value; ratTheory)
- RAT_SAVE (value; ratTheory)
- RAT_SAVE_MINV (value; ratTheory)
- RAT_SAVE_NUM (value; ratTheory)
- RAT_SAVE_TO_CONS (value; ratTheory)
- RAT_SGN_0 (value; ratTheory)
- RAT_SGN_AINV (value; ratTheory)
- RAT_SGN_CALCULATE (value; ratTheory)
- RAT_SGN_CLAUSES (value; ratTheory)
- RAT_SGN_COMPLEMENT (value; ratTheory)
- RAT_SGN_CONG (value; ratTheory)
- rat_sgn_def (value; ratTheory)
- RAT_SGN_MINV (value; ratTheory)
- RAT_SGN_MUL (value; ratTheory)
- RAT_SGN_TOTAL (value; ratTheory)
- RAT_SUB_ADDAINV (value; ratTheory)
- RAT_SUB_CALCULATE (value; ratTheory)
- RAT_SUB_CONG (value; ratTheory)
- RAT_SUB_CONG1 (value; ratTheory)
- RAT_SUB_CONG2 (value; ratTheory)
- rat_sub_def (value; ratTheory)
- RAT_SUB_ID (value; ratTheory)
- RAT_SUB_LDISTRIB (value; ratTheory)
- RAT_SUB_LID (value; ratTheory)
- RAT_SUB_RDISTRIB (value; ratTheory)
- RAT_SUB_RID (value; ratTheory)
- rat_TY_DEF (value; ratTheory)
- ratTheory (structure)
- RC_DEF (value; relationTheory)
- RC_IDEM (value; relationTheory)
- RC_lifts_equalities (value; relationTheory)
- RC_lifts_invariants (value; relationTheory)
- RC_lifts_monotonicities (value; relationTheory)
- RC_MOVES_OUT (value; relationTheory)
- RC_OR_Id (value; relationTheory)
- RC_REFLEXIVE (value; relationTheory)
- RC_RTC (value; relationTheory)
- RC_STRORD (value; relationTheory)
- RC_SUBSET (value; relationTheory)
- RC_Weak (value; relationTheory)
- rcdiamond_def (value; relationTheory)
- rcdiamond_diamond (value; relationTheory)
- RCOMPL (value; relationTheory)
- RDOM_DEF (value; relationTheory)
- re_compl (value; topologyTheory)
- re_intersect (value; topologyTheory)
- re_null (value; topologyTheory)
- re_subset (value; topologyTheory)
- re_Union (value; topologyTheory)
- re_union (value; topologyTheory)
- re_universe (value; topologyTheory)
- Reachable_def (value; MachineTransitionTheory)
- Reachable_ReachBy (value; MachineTransitionTheory)
- Reachable_Stable (value; MachineTransitionTheory)
- ReachableFinPath (value; MachineTransitionTheory)
- ReachableMooreTrans (value; MachineTransitionTheory)
- ReachablePath (value; MachineTransitionTheory)
- ReachablePathThm (value; MachineTransitionTheory)
- ReachableTotalise (value; MachineTransitionTheory)
- ReachBy_def (value; MachineTransitionTheory)
- ReachBy_fixedpoint (value; MachineTransitionTheory)
- ReachBy_ReachIn (value; MachineTransitionTheory)
- ReachBy_rec (value; MachineTransitionTheory)
- ReachIn_def (value; MachineTransitionTheory)
- ReachIn_rec (value; MachineTransitionTheory)
- ReachIn_revrec (value; MachineTransitionTheory)
- ReachInFinPath (value; MachineTransitionTheory)
- ReachInPath (value; MachineTransitionTheory)
- REAL (value; realTheory)
- REAL_0 (value; realTheory)
- real_0 (value; realaxTheory)
- REAL_1 (value; realTheory)
- real_1 (value; realaxTheory)
- REAL_10 (value; realTheory, realaxTheory)
- REAL_ABS_0 (value; realTheory)
- real_ABS_def (value; realaxTheory)
- REAL_ABS_DIV (value; floatTheory)
- REAL_ABS_INV (value; floatTheory)
- REAL_ABS_MUL (value; realTheory)
- REAL_ABS_NUM (value; floatTheory)
- REAL_ABS_POS (value; realTheory)
- REAL_ABS_POW (value; floatTheory)
- real_ABS_REP_CLASS (value; realaxTheory)
- REAL_ABS_TRIANGLE (value; realTheory)
- REAL_ADD (value; realTheory)
- real_add (value; realaxTheory)
- REAL_ADD2_SUB2 (value; realTheory)
- REAL_ADD_ASSOC (value; realTheory, realaxTheory)
- REAL_ADD_COMM (value; realTheory)
- REAL_ADD_LDISTRIB (value; realTheory)
- REAL_ADD_LID (value; realTheory, realaxTheory)
- REAL_ADD_LID_UNIQ (value; realTheory)
- REAL_ADD_LINV (value; realTheory, realaxTheory)
- REAL_ADD_RAT (value; realTheory)
- REAL_ADD_RDISTRIB (value; realTheory)
- REAL_ADD_RID (value; realTheory)
- REAL_ADD_RID_UNIQ (value; realTheory)
- REAL_ADD_RINV (value; realTheory)
- REAL_ADD_SUB (value; realTheory)
- REAL_ADD_SUB2 (value; realTheory)
- REAL_ADD_SUB_ALT (value; realTheory)
- REAL_ADD_SYM (value; realTheory, realaxTheory)
- REAL_ARCH (value; realTheory)
- REAL_ARCH_LEAST (value; realTheory)
- REAL_BIGNUM (value; realTheory)
- real_bijections (value; realaxTheory)
- REAL_BNVAL_NBWORD (value; fxpTheory)
- REAL_DIFFSQ (value; realTheory)
- real_div (value; realTheory)
- REAL_DIV_ADD (value; realTheory)
- REAL_DIV_DENOM_CANCEL (value; realTheory)
- REAL_DIV_DENOM_CANCEL2 (value; realTheory)
- REAL_DIV_DENOM_CANCEL3 (value; realTheory)
- REAL_DIV_INNER_CANCEL (value; realTheory)
- REAL_DIV_INNER_CANCEL2 (value; realTheory)
- REAL_DIV_INNER_CANCEL3 (value; realTheory)
- REAL_DIV_LMUL (value; realTheory)
- REAL_DIV_LMUL_CANCEL (value; realTheory)
- REAL_DIV_LZERO (value; realTheory)
- REAL_DIV_MUL2 (value; realTheory)
- REAL_DIV_OUTER_CANCEL (value; realTheory)
- REAL_DIV_OUTER_CANCEL2 (value; realTheory)
- REAL_DIV_OUTER_CANCEL3 (value; realTheory)
- REAL_DIV_REFL (value; realTheory)
- REAL_DIV_REFL2 (value; realTheory)
- REAL_DIV_REFL3 (value; realTheory)
- REAL_DIV_RMUL (value; realTheory)
- REAL_DIV_RMUL_CANCEL (value; realTheory)
- REAL_DIV_SQRT (value; transcTheory)
- REAL_DOUBLE (value; realTheory)
- REAL_DOWN (value; realTheory)
- REAL_DOWN2 (value; realTheory)
- REAL_ENTIRE (value; realTheory)
- REAL_EQ_IMP_LE (value; realTheory)
- REAL_EQ_LADD (value; realTheory)
- REAL_EQ_LDIV_EQ (value; realTheory)
- REAL_EQ_LMUL (value; realTheory)
- REAL_EQ_LMUL2 (value; realTheory)
- REAL_EQ_LMUL_IMP (value; realTheory)
- REAL_EQ_MUL_LCANCEL (value; realTheory)
- REAL_EQ_NEG (value; realTheory)
- REAL_EQ_RADD (value; realTheory)
- REAL_EQ_RDIV_EQ (value; realTheory)
- REAL_EQ_RMUL (value; realTheory)
- REAL_EQ_RMUL_IMP (value; realTheory)
- REAL_EQ_SUB_LADD (value; realTheory)
- REAL_EQ_SUB_RADD (value; realTheory)
- REAL_FACT_NZ (value; realTheory)
- real_ge (value; realTheory)
- real_grammars (value; realTheory)
- real_gt (value; realTheory)
- REAL_HALF_BETWEEN (value; realTheory)
- REAL_HALF_DOUBLE (value; realTheory)
- REAL_IMP_INF_LE (value; realTheory)
- REAL_IMP_LE_INF (value; realTheory)
- REAL_IMP_LE_SUP (value; realTheory)
- REAL_IMP_MAX_LE2 (value; realTheory)
- REAL_IMP_MIN_LE2 (value; realTheory)
- REAL_IMP_SUP_LE (value; realTheory)
- REAL_IN_BINADE (value; floatTheory)
- REAL_INF_CLOSE (value; realTheory)
- REAL_INF_LE (value; realTheory)
- REAL_INF_LT (value; realTheory)
- REAL_INF_MIN (value; prob_extraTheory, realTheory)
- REAL_INJ (value; realTheory)
- real_inv (value; realaxTheory)
- REAL_INV1 (value; realTheory)
- REAL_INV_0 (value; realTheory, realaxTheory)
- REAL_INV_1OVER (value; realTheory)
- REAL_INV_EQ_0 (value; realTheory)
- REAL_INV_INJ (value; realTheory)
- REAL_INV_INV (value; realTheory)
- REAL_INV_LT1 (value; realTheory)
- REAL_INV_LT_ANTIMONO (value; realTheory)
- REAL_INV_MUL (value; realTheory)
- REAL_INV_NZ (value; realTheory)
- REAL_INV_POS (value; realTheory)
- REAL_INVINV (value; realTheory)
- REAL_INVINV_ALL (value; prob_extraTheory)
- REAL_ISO_EQ (value; realaxTheory)
- REAL_LDISTRIB (value; realTheory, realaxTheory)
- REAL_LE (value; realTheory)
- REAL_LE1_POW2 (value; realTheory)
- REAL_LE_01 (value; realTheory)
- REAL_LE_ADD (value; realTheory)
- REAL_LE_ADD2 (value; realTheory)
- REAL_LE_ADDL (value; realTheory)
- REAL_LE_ADDR (value; realTheory)
- REAL_LE_ANTISYM (value; realTheory)
- REAL_LE_DIV (value; realTheory)
- REAL_LE_DOUBLE (value; realTheory)
- REAL_LE_EPSILON (value; realTheory)
- REAL_LE_EQ (value; prob_extraTheory)
- REAL_LE_INV (value; realTheory)
- REAL_LE_INV2 (value; floatTheory)
- REAL_LE_INV_EQ (value; realTheory)
- REAL_LE_INV_LE (value; prob_extraTheory)
- REAL_LE_LADD (value; realTheory)
- REAL_LE_LADD_IMP (value; realTheory)
- REAL_LE_LCANCEL_IMP (value; floatTheory)
- REAL_LE_LDIV (value; realTheory)
- REAL_LE_LDIV_EQ (value; realTheory)
- REAL_LE_LMUL (value; realTheory)
- REAL_LE_LMUL_IMP (value; realTheory)
- REAL_LE_LNEG (value; realTheory)
- REAL_LE_LT (value; realTheory)
- REAL_LE_MAX (value; realTheory)
- REAL_LE_MAX1 (value; realTheory)
- REAL_LE_MAX2 (value; realTheory)
- REAL_LE_MIN (value; realTheory)
- REAL_LE_MUL (value; realTheory)
- REAL_LE_MUL2 (value; realTheory)
- REAL_LE_NEG (value; realTheory)
- REAL_LE_NEG2 (value; realTheory)
- REAL_LE_NEGL (value; realTheory)
- REAL_LE_NEGR (value; realTheory)
- REAL_LE_NEGTOTAL (value; realTheory)
- REAL_LE_POW2 (value; realTheory)
- REAL_LE_RADD (value; realTheory)
- REAL_LE_RCANCEL_IMP (value; floatTheory)
- REAL_LE_RDIV (value; realTheory)
- REAL_LE_RDIV_EQ (value; realTheory)
- REAL_LE_REFL (value; realTheory)
- REAL_LE_RMUL (value; realTheory)
- REAL_LE_RMUL_IMP (value; realTheory)
- REAL_LE_RNEG (value; realTheory)
- REAL_LE_SQUARE (value; realTheory)
- REAL_LE_SUB_CANCEL2 (value; realTheory)
- REAL_LE_SUB_LADD (value; realTheory)
- REAL_LE_SUB_RADD (value; realTheory)
- REAL_LE_SUP (value; realTheory)
- REAL_LE_TOTAL (value; realTheory)
- REAL_LE_TRANS (value; realTheory)
- REAL_LET_ADD (value; realTheory)
- REAL_LET_ADD2 (value; realTheory)
- REAL_LET_ANTISYM (value; realTheory)
- REAL_LET_TOTAL (value; realTheory)
- REAL_LET_TRANS (value; realTheory)
- REAL_LIN_LE_MAX (value; realTheory)
- REAL_LINV_UNIQ (value; realTheory)
- REAL_LNEG_UNIQ (value; realTheory)
- REAL_LT (value; realTheory)
- real_lt (value; realTheory, realaxTheory)
- REAL_LT1_POW2 (value; realTheory)
- REAL_LT_01 (value; realTheory)
- REAL_LT_1 (value; realTheory)
- REAL_LT_ADD (value; realTheory)
- REAL_LT_ADD1 (value; realTheory)
- REAL_LT_ADD2 (value; realTheory)
- REAL_LT_ADD_SUB (value; realTheory)
- REAL_LT_ADDL (value; realTheory)
- REAL_LT_ADDNEG (value; realTheory)
- REAL_LT_ADDNEG2 (value; realTheory)
- REAL_LT_ADDR (value; realTheory)
- REAL_LT_ANTISYM (value; realTheory)
- REAL_LT_DIV (value; realTheory)
- REAL_LT_FRACTION (value; realTheory)
- REAL_LT_FRACTION_0 (value; realTheory)
- REAL_LT_GT (value; realTheory)
- REAL_LT_HALF1 (value; realTheory)
- REAL_LT_HALF2 (value; realTheory)
- REAL_LT_IADD (value; realTheory, realaxTheory)
- REAL_LT_IMP_LE (value; realTheory)
- REAL_LT_IMP_NE (value; realTheory)
- REAL_LT_INV (value; realTheory)
- REAL_LT_INV_EQ (value; realTheory)
- REAL_LT_LADD (value; realTheory)
- REAL_LT_LCANCEL_IMP (value; floatTheory)
- REAL_LT_LDIV_EQ (value; realTheory)
- REAL_LT_LE (value; realTheory)
- REAL_LT_LMUL (value; realTheory)
- REAL_LT_LMUL_0 (value; realTheory)
- REAL_LT_LMUL_IMP (value; realTheory)
- REAL_LT_MUL (value; realTheory, realaxTheory)
- REAL_LT_MUL2 (value; realTheory)
- REAL_LT_MULTIPLE (value; realTheory)
- REAL_LT_NEG (value; realTheory)
- REAL_LT_NEGTOTAL (value; realTheory)
- REAL_LT_NZ (value; realTheory)
- REAL_LT_RADD (value; realTheory)
- REAL_LT_RCANCEL_IMP (value; floatTheory)
- REAL_LT_RDIV (value; realTheory)
- REAL_LT_RDIV_0 (value; realTheory)
- REAL_LT_RDIV_EQ (value; realTheory)
- REAL_LT_REFL (value; realTheory, realaxTheory)
- REAL_LT_RMUL (value; realTheory)
- REAL_LT_RMUL_0 (value; realTheory)
- REAL_LT_RMUL_IMP (value; realTheory)
- REAL_LT_SUB_LADD (value; realTheory)
- REAL_LT_SUB_RADD (value; realTheory)
- REAL_LT_TOTAL (value; realTheory, realaxTheory)
- REAL_LT_TRANS (value; realTheory, realaxTheory)
- real_lte (value; realTheory)
- REAL_LTE_ADD (value; realTheory)
- REAL_LTE_ADD2 (value; realTheory)
- REAL_LTE_ANTSYM (value; realTheory)
- REAL_LTE_TOTAL (value; realTheory)
- REAL_LTE_TRANS (value; realTheory)
- REAL_MAX_ADD (value; realTheory)
- REAL_MAX_ALT (value; realTheory)
- REAL_MAX_LE (value; realTheory)
- REAL_MAX_MIN (value; realTheory)
- REAL_MAX_REFL (value; realTheory)
- REAL_MAX_SUB (value; realTheory)
- REAL_MEAN (value; realTheory)
- REAL_MIDDLE1 (value; realTheory)
- REAL_MIDDLE2 (value; realTheory)
- REAL_MIN_ADD (value; realTheory)
- REAL_MIN_ALT (value; realTheory)
- REAL_MIN_LE (value; realTheory)
- REAL_MIN_LE1 (value; realTheory)
- REAL_MIN_LE2 (value; realTheory)
- REAL_MIN_LE_LIN (value; realTheory)
- REAL_MIN_MAX (value; realTheory)
- REAL_MIN_REFL (value; realTheory)
- REAL_MIN_SUB (value; realTheory)
- REAL_MUL (value; realTheory)
- real_mul (value; realaxTheory)
- REAL_MUL_AC (value; floatTheory)
- REAL_MUL_ASSOC (value; realTheory, realaxTheory)
- REAL_MUL_COMM (value; realTheory)
- REAL_MUL_LID (value; realTheory, realaxTheory)
- REAL_MUL_LINV (value; realTheory, realaxTheory)
- REAL_MUL_LNEG (value; realTheory)
- REAL_MUL_LZERO (value; realTheory)
- REAL_MUL_RID (value; realTheory)
- REAL_MUL_RINV (value; realTheory)
- REAL_MUL_RNEG (value; realTheory)
- REAL_MUL_RZERO (value; realTheory)
- REAL_MUL_SUB1_CANCEL (value; realTheory)
- REAL_MUL_SUB2_CANCEL (value; realTheory)
- REAL_MUL_SYM (value; realTheory, realaxTheory)
- real_neg (value; realaxTheory)
- REAL_NEG_0 (value; realTheory)
- REAL_NEG_ADD (value; realTheory)
- REAL_NEG_EQ (value; realTheory)
- REAL_NEG_EQ0 (value; realTheory)
- REAL_NEG_GE0 (value; realTheory)
- REAL_NEG_GT0 (value; realTheory)
- REAL_NEG_HALF (value; realTheory)
- REAL_NEG_IN_BINADE (value; floatTheory)
- REAL_NEG_INV (value; realTheory)
- REAL_NEG_LE0 (value; realTheory)
- REAL_NEG_LMUL (value; realTheory)
- REAL_NEG_LT0 (value; realTheory)
- REAL_NEG_MINUS1 (value; realTheory)
- REAL_NEG_MUL2 (value; realTheory)
- REAL_NEG_NEG (value; realTheory)
- REAL_NEG_RMUL (value; realTheory)
- REAL_NEG_SUB (value; realTheory)
- REAL_NEG_THIRD (value; realTheory)
- REAL_NEGNEG (value; realTheory)
- REAL_NOT_LE (value; realTheory)
- REAL_NOT_LT (value; realTheory)
- REAL_NZ_IMP_LT (value; realTheory)
- real_of_hreal (value; realaxTheory)
- real_of_num (value; realTheory)
- REAL_OF_NUM_ADD (value; realTheory)
- REAL_OF_NUM_EQ (value; realTheory)
- REAL_OF_NUM_GT (value; fxpTheory)
- REAL_OF_NUM_LE (value; realTheory)
- REAL_OF_NUM_LT (value; floatTheory)
- REAL_OF_NUM_MUL (value; realTheory)
- REAL_OF_NUM_POW (value; floatTheory, realTheory)
- REAL_OF_NUM_SUB (value; floatTheory, fxpTheory)
- REAL_OF_NUM_SUC (value; realTheory)
- REAL_OVER1 (value; realTheory)
- REAL_POASQ (value; realTheory)
- REAL_POS (value; realTheory, realaxTheory)
- REAL_POS_EQ_ZERO (value; realTheory)
- REAL_POS_ID (value; realTheory)
- REAL_POS_IN_BINADE (value; floatTheory)
- REAL_POS_INFLATE (value; realTheory)
- REAL_POS_LE_ZERO (value; realTheory)
- REAL_POS_MONO (value; realTheory)
- REAL_POS_NZ (value; realTheory)
- REAL_POS_POS (value; realTheory)
- REAL_POW (value; prob_extraTheory)
- REAL_POW2_ABS (value; realTheory)
- REAL_POW_ADD (value; realTheory)
- REAL_POW_DIV (value; realTheory)
- REAL_POW_EQ_0 (value; floatTheory)
- REAL_POW_INV (value; realTheory)
- REAL_POW_LE_1 (value; floatTheory)
- REAL_POW_LT (value; realTheory)
- REAL_POW_LT2 (value; realTheory)
- REAL_POW_MONO (value; floatTheory)
- REAL_POW_MONO_LT (value; realTheory)
- REAL_POW_POW (value; realTheory)
- real_QUOTIENT (value; realaxTheory)
- REAL_RDISTRIB (value; realTheory)
- real_REP_def (value; realaxTheory)
- REAL_RINV_UNIQ (value; realTheory)
- REAL_RNEG_UNIQ (value; realTheory)
- real_rwts (value; realTheory)
- REAL_SUB (value; realTheory)
- real_sub (value; realTheory)
- REAL_SUB_0 (value; realTheory)
- REAL_SUB_ABS (value; realTheory)
- REAL_SUB_ADD (value; realTheory)
- REAL_SUB_ADD2 (value; realTheory)
- REAL_SUB_INV2 (value; realTheory)
- REAL_SUB_LDISTRIB (value; realTheory)
- REAL_SUB_LE (value; realTheory)
- REAL_SUB_LNEG (value; realTheory)
- REAL_SUB_LT (value; realTheory)
- REAL_SUB_LZERO (value; realTheory)
- REAL_SUB_NEG2 (value; realTheory)
- REAL_SUB_RAT (value; realTheory)
- REAL_SUB_RDISTRIB (value; realTheory)
- REAL_SUB_REFL (value; realTheory)
- REAL_SUB_RNEG (value; realTheory)
- REAL_SUB_RZERO (value; realTheory)
- REAL_SUB_SUB (value; realTheory)
- REAL_SUB_SUB2 (value; realTheory)
- REAL_SUB_TRIANGLE (value; realTheory)
- REAL_SUMSQ (value; realTheory)
- REAL_SUP (value; realTheory)
- REAL_SUP_ALLPOS (value; realTheory, realaxTheory)
- REAL_SUP_CONST (value; realTheory)
- REAL_SUP_EXISTS (value; realTheory)
- REAL_SUP_EXISTS_UNIQUE (value; prob_extraTheory, realTheory)
- REAL_SUP_LE (value; realTheory)
- REAL_SUP_LE_X (value; prob_extraTheory)
- REAL_SUP_MAX (value; prob_extraTheory, realTheory)
- REAL_SUP_SOMEPOS (value; realTheory)
- REAL_SUP_UBOUND (value; realTheory)
- REAL_SUP_UBOUND_LE (value; realTheory)
- REAL_THIRDS_BETWEEN (value; realTheory)
- real_TY_DEF (value; realaxTheory)
- REAL_X_LE_SUP (value; prob_extraTheory)
- realax_grammars (value; realaxTheory)
- realaxTheory (structure)
- realTheory (structure)
- recspace_repfns (value; ind_typeTheory)
- recspace_TY_DEF (value; ind_typeTheory)
- RECURSION (value; Past_Temporal_LogicTheory)
- recursive_seg (value; pathTheory)
- REFL_CLAUSE (value; boolTheory)
- reflexive_def (value; relationTheory)
- reflexive_Id_RSUBSET (value; relationTheory)
- reflexive_inv (value; relationTheory)
- reflexive_RC (value; relationTheory)
- reflexive_RC_identity (value; relationTheory)
- reflexive_RTC (value; relationTheory)
- relation_grammars (value; relationTheory)
- relation_rwts (value; relationTheory)
- relationTheory (structure)
- RELATIVE_ERROR (value; floatTheory)
- RELATIVE_ERROR_NEG (value; floatTheory)
- RELATIVE_ERROR_POS (value; floatTheory)
- RELATIVE_ERROR_ZERO (value; floatTheory)
- rem (value; ieeeTheory)
- REMPTY_SUBSET (value; relationTheory)
- rep_rat_def (value; ratTheory)
- REPLICATE (value; rich_listTheory)
- REPLICATELENGTH (value; fxpTheory)
- REPLICATELENGTHF (value; fxpTheory)
- representable (value; fxpTheory)
- RES_ABSTRACT (value; res_quanTheory)
- RES_ABSTRACT_DEF (value; boolTheory)
- RES_ABSTRACT_EQUAL (value; res_quanTheory)
- RES_ABSTRACT_EQUAL_EQ (value; res_quanTheory)
- RES_ABSTRACT_IDEMPOT (value; res_quanTheory)
- RES_DISJ_EXISTS_DIST (value; res_quanTheory)
- RES_EXISTS (value; res_quanTheory)
- RES_EXISTS_ALT (value; res_quanTheory)
- RES_EXISTS_CONG (value; boolTheory)
- RES_EXISTS_DEF (value; boolTheory)
- RES_EXISTS_DISJ_DIST (value; res_quanTheory)
- RES_EXISTS_EMPTY (value; res_quanTheory)
- RES_EXISTS_EQUAL (value; res_quanTheory)
- RES_EXISTS_FALSE (value; boolTheory)
- RES_EXISTS_NULL (value; res_quanTheory)
- RES_EXISTS_REORDER (value; res_quanTheory)
- RES_EXISTS_THM (value; boolTheory)
- RES_EXISTS_UNIQUE (value; res_quanTheory)
- RES_EXISTS_UNIQUE_ALT (value; res_quanTheory)
- RES_EXISTS_UNIQUE_DEF (value; boolTheory)
- RES_EXISTS_UNIQUE_EMPTY (value; res_quanTheory)
- RES_EXISTS_UNIQUE_NULL (value; res_quanTheory)
- RES_EXISTS_UNIQUE_THM (value; boolTheory)
- RES_EXISTS_UNIQUE_UNIV (value; res_quanTheory)
- RES_EXISTS_UNIV (value; res_quanTheory)
- RES_FORALL (value; res_quanTheory)
- RES_FORALL_CONG (value; boolTheory)
- RES_FORALL_CONJ_DIST (value; res_quanTheory)
- RES_FORALL_DEF (value; boolTheory)
- RES_FORALL_DISJ_DIST (value; res_quanTheory)
- RES_FORALL_EMPTY (value; res_quanTheory)
- RES_FORALL_FORALL (value; res_quanTheory)
- RES_FORALL_NULL (value; res_quanTheory)
- RES_FORALL_REORDER (value; res_quanTheory)
- RES_FORALL_THM (value; boolTheory)
- RES_FORALL_TRUE (value; boolTheory)
- RES_FORALL_UNIQUE (value; res_quanTheory)
- RES_FORALL_UNIV (value; res_quanTheory)
- res_quan_grammars (value; res_quanTheory)
- res_quanTheory (structure)
- RES_SELECT (value; res_quanTheory)
- RES_SELECT_DEF (value; boolTheory)
- RES_SELECT_EMPTY (value; res_quanTheory)
- RES_SELECT_THM (value; boolTheory)
- RES_SELECT_UNIV (value; res_quanTheory)
- REST_DEF (value; pred_setTheory)
- REST_PSUBSET (value; pred_setTheory)
- REST_SING (value; pred_setTheory)
- REST_SUBSET (value; pred_setTheory)
- RESTRICT_DEF (value; relationTheory)
- RESTRICT_LEMMA (value; relationTheory)
- REV_DEF (value; listTheory)
- REV_REVERSE_LEM (value; listTheory)
- REVERSE (value; rich_listTheory)
- REVERSE_APPEND (value; listTheory, rich_listTheory)
- REVERSE_DEF (value; listTheory)
- REVERSE_EQ_NIL (value; rich_listTheory)
- REVERSE_FLAT (value; rich_listTheory)
- REVERSE_FOLDL (value; rich_listTheory)
- REVERSE_FOLDR (value; rich_listTheory)
- REVERSE_REV (value; listTheory)
- REVERSE_REVERSE (value; listTheory, rich_listTheory)
- REVERSE_SNOC (value; rich_listTheory)
- rich_list_grammars (value; rich_listTheory)
- rich_listTheory (structure)
- RIGHT_ADD_DISTRIB (value; arithmeticTheory)
- RIGHT_AND_FORALL_THM (value; boolTheory)
- RIGHT_AND_OVER_OR (value; boolTheory)
- RIGHT_EXISTS_AND_THM (value; boolTheory)
- RIGHT_EXISTS_IMP_THM (value; boolTheory)
- RIGHT_FORALL_IMP_THM (value; boolTheory)
- RIGHT_FORALL_OR_THM (value; boolTheory)
- RIGHT_ID_DEF (value; operatorTheory)
- Right_idx (value; quoteTheory)
- RIGHT_OR_EXISTS_THM (value; boolTheory)
- RIGHT_OR_OVER_AND (value; boolTheory)
- RIGHT_SUB_DISTRIB (value; arithmeticTheory)
- ring (value; ringTheory)
- ring0_def (value; ringTheory)
- ring_11 (value; ringTheory)
- ring_accessors (value; ringTheory)
- ring_accfupds (value; ringTheory)
- ring_Axiom (value; ringTheory)
- ring_case_cong (value; ringTheory)
- ring_case_def (value; ringTheory)
- ring_component_equality (value; ringTheory)
- ring_fn_updates (value; ringTheory)
- ring_fupdcanon (value; ringTheory)
- ring_fupdcanon_comp (value; ringTheory)
- ring_fupdfupds (value; ringTheory)
- ring_fupdfupds_comp (value; ringTheory)
- ring_grammars (value; ringTheory)
- ring_induction (value; ringTheory)
- ring_is_semi_ring (value; ringTheory)
- ring_literal_11 (value; ringTheory)
- ring_literal_nchotomy (value; ringTheory)
- ring_nchotomy (value; ringTheory)
- ring_R0 (value; ringTheory)
- ring_R0_fupd (value; ringTheory)
- ring_R1 (value; ringTheory)
- ring_R1_fupd (value; ringTheory)
- ring_repfns (value; ringTheory)
- ring_RM (value; ringTheory)
- ring_RM_fupd (value; ringTheory)
- ring_RN (value; ringTheory)
- ring_RN_fupd (value; ringTheory)
- ring_RP (value; ringTheory)
- ring_RP_fupd (value; ringTheory)
- ring_size_def (value; ringTheory)
- ring_TY_DEF (value; ringTheory)
- ring_updates_eq_literal (value; ringTheory)
- ringNorm0_def (value; ringNormTheory)
- ringNorm1_def (value; ringNormTheory)
- ringNorm2_def (value; ringNormTheory)
- ringNorm3_def (value; ringNormTheory)
- ringNorm4_def (value; ringNormTheory)
- ringNorm_grammars (value; ringNormTheory)
- ringNormTheory (structure)
- ringTheory (structure)
- RINTER (value; relationTheory)
- RINTER_ASSOC (value; relationTheory)
- RINTER_COMM (value; relationTheory)
- RINV_DEF (value; pred_setTheory)
- ROLLE (value; limTheory)
- root (value; transcTheory)
- ROOT_0 (value; transcTheory)
- ROOT_1 (value; transcTheory)
- ROOT_DIV (value; transcTheory)
- ROOT_INV (value; transcTheory)
- ROOT_LN (value; transcTheory)
- ROOT_LT_LEMMA (value; transcTheory)
- ROOT_MONO_LE (value; transcTheory)
- ROOT_MUL (value; transcTheory)
- ROOT_POS (value; transcTheory)
- ROOT_POS_LT (value; transcTheory)
- ROOT_POS_UNIQ (value; transcTheory)
- ROOT_POW_POS (value; transcTheory)
- ROR_ADD (value; wordsTheory)
- ROR_BITWISE (value; wordsTheory)
- ROR_CYCLE (value; wordsTheory)
- ROR_MOD (value; wordsTheory)
- ROR_ROL (value; wordsTheory)
- ROR_UINT_MAX (value; wordsTheory)
- Round (value; fxpTheory)
- round_def (value; ieeeTheory)
- ROUNDFLOAT (value; ieeeTheory)
- roundmode2num_11 (value; ieeeTheory)
- roundmode2num_num2roundmode (value; ieeeTheory)
- roundmode2num_ONTO (value; ieeeTheory)
- roundmode2num_thm (value; ieeeTheory)
- roundmode_Axiom (value; ieeeTheory)
- roundmode_BIJ (value; ieeeTheory)
- roundmode_case (value; ieeeTheory)
- roundmode_case_cong (value; ieeeTheory)
- roundmode_case_def (value; ieeeTheory)
- roundmode_distinct (value; ieeeTheory)
- roundmode_EQ_roundmode (value; ieeeTheory)
- roundmode_induction (value; ieeeTheory)
- roundmode_nchotomy (value; ieeeTheory)
- roundmode_size_def (value; ieeeTheory)
- roundmode_TY_DEF (value; ieeeTheory)
- RPROD_DEF (value; pairTheory)
- RRANGE (value; relationTheory)
- RRESTRICT_DEF (value; finite_mapTheory)
- RRESTRICT_FEMPTY (value; finite_mapTheory)
- RRESTRICT_FUPDATE (value; finite_mapTheory)
- RRRC1 (value; floatTheory)
- RRRC10 (value; floatTheory)
- RRRC11 (value; floatTheory)
- RRRC2 (value; floatTheory)
- RRRC3 (value; floatTheory)
- RRRC4 (value; floatTheory)
- RRRC5 (value; floatTheory)
- RRRC6 (value; floatTheory)
- RRRC7 (value; floatTheory)
- RRRC8 (value; floatTheory)
- RRRC9 (value; floatTheory)
- rsquarefree (value; polyTheory)
- RSQUAREFREE_DECOMP (value; polyTheory)
- RSQUAREFREE_ROOTS (value; polyTheory)
- RSUBSET (value; relationTheory)
- RSUBSET_ANTISYM (value; relationTheory)
- RSUBSET_antisymmetric (value; relationTheory)
- RSUBSET_WeakOrder (value; relationTheory)
- rsum (value; transcTheory)
- RTC_CASES1 (value; relationTheory)
- RTC_CASES2 (value; relationTheory)
- RTC_CASES_RTC_TWICE (value; relationTheory)
- RTC_DEF (value; relationTheory)
- RTC_IDEM (value; relationTheory)
- RTC_INDUCT (value; relationTheory)
- RTC_INDUCT_RIGHT1 (value; relationTheory)
- RTC_MONOTONE (value; relationTheory)
- RTC_REFLEXIVE (value; relationTheory)
- RTC_RTC (value; relationTheory)
- RTC_RULES (value; relationTheory)
- RTC_RULES_RIGHT1 (value; relationTheory)
- RTC_STRONG_INDUCT (value; relationTheory)
- RTC_STRONG_INDUCT_RIGHT1 (value; relationTheory)
- RTC_SUBSET (value; relationTheory)
- RTC_TC_RC (value; relationTheory)
- RTC_TRANSITIVE (value; relationTheory)
- RUNION (value; relationTheory)
- RUNION_ASSOC (value; relationTheory)
- RUNION_COMM (value; relationTheory)
- RUNIV (value; relationTheory)
- RUNIV_SUBSET (value; relationTheory)
S
T
- T_DEF (value; boolTheory)
- tail_def (value; pathTheory)
- tail_drop (value; pathTheory)
- take_def (value; pathTheory)
- tan (value; transcTheory)
- TAN_0 (value; transcTheory)
- TAN_ADD (value; transcTheory)
- TAN_ATN (value; transcTheory)
- TAN_DOUBLE (value; transcTheory)
- TAN_NEG (value; transcTheory)
- TAN_NPI (value; transcTheory)
- TAN_PERIODIC (value; transcTheory)
- TAN_PI (value; transcTheory)
- TAN_POS_PI2 (value; transcTheory)
- TAN_SEC (value; transcTheory)
- TAN_TOTAL (value; transcTheory)
- TAN_TOTAL_LEMMA (value; transcTheory)
- TAN_TOTAL_POS (value; transcTheory)
- TC_CASES1 (value; relationTheory)
- TC_CASES2 (value; relationTheory)
- TC_DEF (value; relationTheory)
- TC_IDEM (value; relationTheory)
- TC_INDUCT (value; relationTheory)
- TC_INDUCT_LEFT1 (value; relationTheory)
- TC_INDUCT_RIGHT1 (value; relationTheory)
- TC_lifts_equalities (value; relationTheory)
- TC_lifts_invariants (value; relationTheory)
- TC_lifts_monotonicities (value; relationTheory)
- TC_lifts_transitive_relations (value; relationTheory)
- TC_MONOTONE (value; relationTheory)
- TC_RC_EQNS (value; relationTheory)
- TC_RTC (value; relationTheory)
- TC_RULES (value; relationTheory)
- TC_STRONG_INDUCT (value; relationTheory)
- TC_STRONG_INDUCT_LEFT1 (value; relationTheory)
- TC_STRONG_INDUCT_RIGHT1 (value; relationTheory)
- TC_SUBSET (value; relationTheory)
- TC_TRANSITIVE (value; relationTheory)
- tdiv (value; transcTheory)
- temonz (value; floatTheory)
- TEMP_OPS_DEFS_TO_OMEGA (value; Omega_AutomataTheory)
- Temporal_Logic_grammars (value; Temporal_LogicTheory)
- Temporal_LogicTheory (structure)
- tends (value; netsTheory)
- tends_num_real (value; seqTheory)
- tends_real_real (value; limTheory)
- tendsto (value; netsTheory)
- term (type; pairTheory)
- TERMDIFF (value; powserTheory)
- TERMDIFF_LEMMA1 (value; powserTheory)
- TERMDIFF_LEMMA2 (value; powserTheory)
- TERMDIFF_LEMMA3 (value; powserTheory)
- TERMDIFF_LEMMA4 (value; powserTheory)
- TERMDIFF_LEMMA5 (value; powserTheory)
- tfflttfs (value; floatTheory)
- TFL_INDUCTIVE_INVARIANT_ON_WFREC (value; relationTheory)
- TFL_INDUCTIVE_INVARIANT_WFREC (value; relationTheory)
- THE_DEF (value; optionTheory)
- the_fun_def (value; relationTheory)
- thm (type; CoderTheory, DecodeTheory, EncodeTheory, EncodeVarTheory, MachineTransitionTheory, Omega_AutomataTheory, Past_Temporal_LogicTheory, Temporal_LogicTheory, arithmeticTheory, bagTheory, bitTheory, boolTheory, boolean_sequenceTheory, bword_arithTheory, bword_bitopTheory, bword_numTheory, canonicalTheory, combinTheory, containerTheory, defCNFTheory, dividesTheory, fcpTheory, finite_mapTheory, fixedPointTheory, floatTheory, fxpTheory, gcdTheory, hratTheory, hrealTheory, ieeeTheory, ind_typeTheory, integerRingTheory, integerTheory, limTheory, listTheory, llistTheory, netsTheory, numRingTheory, numTheory, numeralTheory, oneTheory, operatorTheory, optionTheory, pairTheory, pathTheory, polyTheory, powserTheory, pred_setTheory, prelimTheory, prim_recTheory, probTheory, prob_algebraTheory, prob_canonTheory, prob_extraTheory, prob_indepTheory, prob_pseudoTheory, prob_uniformTheory, quoteTheory, ratTheory, realTheory, realaxTheory, relationTheory, res_quanTheory, rich_listTheory, ringNormTheory, ringTheory, semi_ringTheory, seqTheory, sortingTheory, state_transformerTheory, stringTheory, sumTheory, topologyTheory, transcTheory, whileTheory, wordTheory, word_baseTheory, word_bitopTheory, word_numTheory, wordsTheory)
- threshold (value; ieeeTheory)
- THRESHOLD_LT_POW_INV (value; floatTheory)
- THRESHOLD_MUL_LT (value; floatTheory)
- TIMES2 (value; arithmeticTheory)
- TIMES_2EXP_def (value; bitTheory)
- tint_0 (value; integerTheory)
- tint_1 (value; integerTheory)
- TINT_10 (value; integerTheory)
- tint_add (value; integerTheory)
- TINT_ADD_ASSOC (value; integerTheory)
- TINT_ADD_LID (value; integerTheory)
- TINT_ADD_LINV (value; integerTheory)
- TINT_ADD_SYM (value; integerTheory)
- TINT_ADD_WELLDEF (value; integerTheory)
- TINT_ADD_WELLDEFR (value; integerTheory)
- tint_eq (value; integerTheory)
- TINT_EQ_AP (value; integerTheory)
- TINT_EQ_EQUIV (value; integerTheory)
- TINT_EQ_REFL (value; integerTheory)
- TINT_EQ_SYM (value; integerTheory)
- TINT_EQ_TRANS (value; integerTheory)
- TINT_INJ (value; integerTheory)
- TINT_LDISTRIB (value; integerTheory)
- tint_lt (value; integerTheory)
- TINT_LT_ADD (value; integerTheory)
- TINT_LT_MUL (value; integerTheory)
- TINT_LT_REFL (value; integerTheory)
- TINT_LT_TOTAL (value; integerTheory)
- TINT_LT_TRANS (value; integerTheory)
- TINT_LT_WELLDEF (value; integerTheory)
- TINT_LT_WELLDEFL (value; integerTheory)
- TINT_LT_WELLDEFR (value; integerTheory)
- tint_mul (value; integerTheory)
- TINT_MUL_ASSOC (value; integerTheory)
- TINT_MUL_LID (value; integerTheory)
- TINT_MUL_SYM (value; integerTheory)
- TINT_MUL_WELLDEF (value; integerTheory)
- TINT_MUL_WELLDEFR (value; integerTheory)
- tint_neg (value; integerTheory)
- TINT_NEG_WELLDEF (value; integerTheory)
- tint_of_num (value; integerTheory)
- tint_of_num_eq (value; integerTheory)
- tittfittt (value; floatTheory)
- TL (value; listTheory, rich_listTheory)
- TL_SNOC (value; rich_listTheory)
- to_fromList (value; llistTheory)
- To_nearest (value; ieeeTheory)
- To_ninfinity (value; ieeeTheory)
- To_pinfinity (value; ieeeTheory)
- To_plus_infinity (value; fxpTheory)
- To_zero (value; fxpTheory)
- toList (value; llistTheory)
- toList_THM (value; llistTheory)
- toPath_11 (value; pathTheory)
- toPath_onto (value; pathTheory)
- topfloat (value; ieeeTheory)
- topfxp_def (value; fxpTheory)
- TOPOLOGY (value; topologyTheory)
- topology_grammars (value; topologyTheory)
- topology_TY_DEF (value; topologyTheory)
- topology_tybij (value; topologyTheory)
- TOPOLOGY_UNION (value; topologyTheory)
- topologyTheory (structure)
- Total_def (value; MachineTransitionTheory)
- total_def (value; relationTheory)
- TotalImpTotalise (value; MachineTransitionTheory)
- TotalImpTotaliseLemma (value; MachineTransitionTheory)
- Totalise_def (value; MachineTransitionTheory)
- TotaliseReachBy (value; MachineTransitionTheory)
- TotalMooreTrans (value; MachineTransitionTheory)
- TotalPathExists (value; MachineTransitionTheory)
- TotalTotalise (value; MachineTransitionTheory)
- tpetfs (value; floatTheory)
- tptteteesze (value; floatTheory)
- TraceReachIn (value; MachineTransitionTheory)
- transc_grammars (value; transcTheory)
- transcTheory (structure)
- transitive_def (value; relationTheory)
- transitive_inv (value; relationTheory)
- transitive_O_RSUBSET (value; relationTheory)
- transitive_RC (value; relationTheory)
- transitive_RTC (value; relationTheory)
- transitive_TC_identity (value; relationTheory)
- trat_1 (value; hratTheory)
- trat_add (value; hratTheory)
- TRAT_ADD_ASSOC (value; hratTheory)
- TRAT_ADD_SYM (value; hratTheory)
- TRAT_ADD_SYM_EQ (value; hratTheory)
- TRAT_ADD_TOTAL (value; hratTheory)
- TRAT_ADD_WELLDEFINED (value; hratTheory)
- TRAT_ADD_WELLDEFINED2 (value; hratTheory)
- TRAT_ARCH (value; hratTheory)
- trat_eq (value; hratTheory)
- TRAT_EQ_AP (value; hratTheory)
- TRAT_EQ_EQUIV (value; hratTheory)
- TRAT_EQ_REFL (value; hratTheory)
- TRAT_EQ_SYM (value; hratTheory)
- TRAT_EQ_TRANS (value; hratTheory)
- trat_inv (value; hratTheory)
- TRAT_INV_WELLDEFINED (value; hratTheory)
- TRAT_LDISTRIB (value; hratTheory)
- trat_mul (value; hratTheory)
- TRAT_MUL_ASSOC (value; hratTheory)
- TRAT_MUL_LID (value; hratTheory)
- TRAT_MUL_LINV (value; hratTheory)
- TRAT_MUL_SYM (value; hratTheory)
- TRAT_MUL_SYM_EQ (value; hratTheory)
- TRAT_MUL_WELLDEFINED (value; hratTheory)
- TRAT_MUL_WELLDEFINED2 (value; hratTheory)
- TRAT_NOZERO (value; hratTheory)
- TRAT_SUCINT (value; hratTheory)
- trat_sucint (value; hratTheory)
- TRAT_SUCINT_0 (value; hratTheory)
- treal_0 (value; realaxTheory)
- treal_1 (value; realaxTheory)
- TREAL_10 (value; realaxTheory)
- treal_add (value; realaxTheory)
- TREAL_ADD_ASSOC (value; realaxTheory)
- TREAL_ADD_LID (value; realaxTheory)
- TREAL_ADD_LINV (value; realaxTheory)
- TREAL_ADD_SYM (value; realaxTheory)
- TREAL_ADD_WELLDEF (value; realaxTheory)
- TREAL_ADD_WELLDEFR (value; realaxTheory)
- TREAL_BIJ (value; realaxTheory)
- TREAL_BIJ_WELLDEF (value; realaxTheory)
- treal_eq (value; realaxTheory)
- TREAL_EQ_AP (value; realaxTheory)
- TREAL_EQ_EQUIV (value; realaxTheory)
- TREAL_EQ_REFL (value; realaxTheory)
- TREAL_EQ_SYM (value; realaxTheory)
- TREAL_EQ_TRANS (value; realaxTheory)
- treal_inv (value; realaxTheory)
- TREAL_INV_0 (value; realaxTheory)
- TREAL_INV_WELLDEF (value; realaxTheory)
- TREAL_ISO (value; realaxTheory)
- TREAL_LDISTRIB (value; realaxTheory)
- treal_lt (value; realaxTheory)
- TREAL_LT_ADD (value; realaxTheory)
- TREAL_LT_MUL (value; realaxTheory)
- TREAL_LT_REFL (value; realaxTheory)
- TREAL_LT_TOTAL (value; realaxTheory)
- TREAL_LT_TRANS (value; realaxTheory)
- TREAL_LT_WELLDEF (value; realaxTheory)
- TREAL_LT_WELLDEFL (value; realaxTheory)
- TREAL_LT_WELLDEFR (value; realaxTheory)
- treal_mul (value; realaxTheory)
- TREAL_MUL_ASSOC (value; realaxTheory)
- TREAL_MUL_LID (value; realaxTheory)
- TREAL_MUL_LINV (value; realaxTheory)
- TREAL_MUL_SYM (value; realaxTheory)
- TREAL_MUL_WELLDEF (value; realaxTheory)
- TREAL_MUL_WELLDEFR (value; realaxTheory)
- treal_neg (value; realaxTheory)
- TREAL_NEG_WELLDEF (value; realaxTheory)
- treal_of_hreal (value; realaxTheory)
- tree_11 (value; EncodeTheory)
- tree_Axiom (value; EncodeTheory)
- tree_case_cong (value; EncodeTheory)
- tree_case_def (value; EncodeTheory)
- tree_coder_def (value; CoderTheory)
- tree_ind (value; EncodeTheory)
- tree_induction (value; EncodeTheory)
- tree_nchotomy (value; EncodeTheory)
- tree_repfns (value; EncodeTheory)
- tree_size_def (value; EncodeTheory)
- tree_TY_DEF (value; EncodeTheory)
- trichotomous (value; relationTheory)
- Truncate (value; fxpTheory)
- TRUTH (value; boolTheory)
- tteettto (value; floatTheory)
- ttpinv (value; floatTheory)
- TWO (value; arithmeticTheory)
- TWO_COMP_NEG (value; wordsTheory)
- TWO_COMP_POS (value; wordsTheory)
- TWO_COMP_POS_NEG (value; wordsTheory)
- TWO_EXP_GE_1 (value; floatTheory)
- TWOEXP (value; fxpTheory)
- TWOEXP_DIVISION (value; bitTheory)
- TWOEXP_MONO (value; bitTheory)
- TWOEXP_MONO2 (value; bitTheory)
- TWOEXP_NOT_ZERO (value; bitTheory)
- TWOEXPGE1 (value; fxpTheory)
- TWOEXPONENT_def (value; fxpTheory)
- twoexpsl (value; fxpTheory)
- twogz (value; floatTheory)
- twoone (value; fxpTheory)
- TYPE_DEFINITION (value; boolTheory)
- TYPE_DEFINITION_THM (value; boolTheory)
U
V
W
X
Z
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
HOL 4, Kananaskis-3