HOL html
| Files Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Theorems Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
X (theorems)
XXFAN_EQ_UNIONS_AFF_GE_1_2
XFAN_INTER_BALL_UNIONS
XFAN_INTER_SET
XIN_BARV
XIVPHKS
XIVPHKS_SHIFT
XIV_DEFORMATION
XIV_ECAU
XIV_ECAU_BACK
XNHPWAB1
XNHPWAB2
XNHPWAB3
XNHPWAB4
XOHLED
XOR_DEF
XRECQNS
XRECQNS_UPDATE
XULJEPR
XULJEPR_VECTOR_sum
XULJEPR_sum
XWITCCN
XWITCCN2
XWITCCN_CASE_3
XWITCCN_CASE_3_IS_SCS
XWITCCN_CASE_4
XWITCCN_CASE_4_3
XWITCCN_CASE_4_IS_SCS
XWITCCN_CASE_4_sqrt8
XWITCCN_CASE_5
XWITCCN_CASE_5_IS_SCS
XWITCCN_CASE_5_pro_cs
XWITCCN_CASE_5_sqrt8
XWITCCN_CASE_6
XWITCCN_CASE_6_IS_SCS
XWITCCN_TYPE
XWNHLMD
XWNHLMD_MM
XXXXX
XX_SS_TT
XYOFCGX
XYOFCGX_1
XYOFCGX_2
XYOFCGX_3_0
XYOFCGX_4_0
XYOFCGX_lemma0
X_DOT_X_EQ
X_EQ_COS_T
X_IN_AFF_GE
X_IN_AFF_GE11
X_IN_AFF_GE_LEFT
X_IN_HYP_ORBITS
X_IN_ITS_ORBIT
X_IN_VOR_X
x1_delta_x
x1_delta_y
x1cube
x2notless0
x2notlesseq0
x_greater_lemma
x_in_xfan
xfan
xfan_closed_fan
xfan_inter_segment_closed_fan
xfan_notempty_fan
xlist
xrr
xrr_bounds
xrr_bounds_2
xrr_convert
xrr_decreasing
xrr_decreasing_lt
xrr_factor
xrr_factor_8
xrr_increasing
xrr_increasing_le
xrr_le_1553
xrr_le_1553_BB
xrr_le_16
xrr_lt_16
xrr_pos
xrr_simple_lower_bound
xrr_simple_upper_bound
xrr_sym