• Package Name: hol_stdlib
• Author: John Harrison
• Sub Packages
• Verification Results
• Date Retrieved: 25/06/2015
• Comment: Standard HOL library retrieved from OpenTheory
• Total number of proofs: 1209
• Among them, there are 541 constructive proofs and 668 classical proofs, which means 44.75% of them are constructive proofs.
• Classical proofs have an average size of 283253.97 (up to lemma). Constructive proofs have an average size of 11719.28 (up to lemma).

Name	Conclusion	Link	Package
ABSORPTION	!x s. x IN s <=> x INSERT s = s	link to proof	set-thm
ABS_SIMP	!t1 t2. (\x. t1) t2 = t1	link to proof	bool-int
ADD1	!m. SUC m = m + 1	link to proof	natural-add-thm
ADD_0	!m. m + 0 = m	link to proof	natural-add-thm
ADD_ASSOC	!m n p. m + n + p = (m + n) + p	link to proof	natural-add-thm
ADD_EQ_0	!m n. m + n = 0 <=> m = 0 /\ n = 0	link to proof	natural-add-thm
ADD_SUB	!m n. (m + n) - n = m	link to proof	natural-add-sub-def
ADD_SUB2	!m n. (m + n) - m = n	link to proof	natural-add-sub-thm
ADD_SUC	!m n. m + SUC n = SUC (m + n)	link to proof	natural-add-thm
ADD_SYM	!m n. m + n = n + m	link to proof	natural-add-thm
ALL_APPEND	!p l1 l2. ALL p (APPEND l1 l2) <=> ALL p l1 /\ ALL p l2	link to proof	list-append-thm
ALL_CONS	!p h t. ALL p (CONS h t) <=> p h /\ ALL p t	link to proof	list-set-def
ALL_F	!l. ALL (\x. F) l <=> NULL l	link to proof	list-set-thm
ALL_FILTER	!p q l. ALL p (FILTER q l) <=> ALL (\x. q x ==> p x) l	link to proof	list-filter-thm
ALL_IMP	!p q l. (!x. MEM x l /\ p x ==> q x) /\ ALL p l ==> ALL q l	link to proof	list-set-thm
ALL_MAP	!p f l. ALL p (MAP f l) <=> ALL (p o f) l	link to proof	list-map-thm
ALL_MEM	!p l. (!x. MEM x l ==> p x) <=> ALL p l	link to proof	list-set-thm
ALL_MP	!p q l. ALL (\x. p x ==> q x) l /\ ALL p l ==> ALL q l	link to proof	list-set-thm
ALL_NIL	!p. ALL p []	link to proof	list-set-def
ALL_SET_OF_LIST	!p l. ALL p l <=> (!x. x IN set_of_list l ==> p x)	link to proof	list-set-thm
ALL_T	!l. ALL (\x. T) l	link to proof	list-set-thm
AND_ALL	!p q l. ALL (\x. p x /\ q x) l <=> ALL p l /\ ALL q l	link to proof	list-set-thm
AND_DEF	(/\) = (\p q. (\f. f p q) = (\f. f T T))	link to proof	bool-def
AND_FALSE_THM	!t. t /\ F <=> F	link to proof	bool-int
AND_FORALL_THM	!p q. (!x. p x) /\ (!x. q x) <=> (!x. p x /\ q x)	link to proof	bool-int
AND_TRUE_THM	!t. t /\ T <=> t	link to proof	bool-int
APPEND_ASSOC	!l1 l2 l3. APPEND l1 (APPEND l2 l3) = APPEND (APPEND l1 l2) l3	link to proof	list-append-thm
APPEND_EQ_NIL	!l1 l2. APPEND l1 l2 = [] <=> l1 = [] /\ l2 = []	link to proof	list-append-thm
APPEND_EQ_REPLICATE	!x n l1 l2. APPEND l1 l2 = REPLICATE x n <=> REPLICATE x (LENGTH l1) = l1 /\ REPLICATE x (LENGTH l2) = l2 /\ LENGTH l1 + LENGTH l2 = n	link to proof	list-replicate-thm
APPEND_LCANCEL	!l l1 l2. APPEND l l1 = APPEND l l2 <=> l1 = l2	link to proof	list-append-thm
APPEND_LCANCEL_IMP	!l l1 l2. APPEND l l1 = APPEND l l2 ==> l1 = l2	link to proof	list-append-thm
APPEND_LINJ	!l1 l1' l2 l2'. LENGTH l1 = LENGTH l1' /\ APPEND l1 l2 = APPEND l1' l2' ==> l1 = l1'	link to proof	list-append-thm
APPEND_NIL	!l. APPEND l [] = l	link to proof	list-append-thm
APPEND_RCANCEL	!l l1 l2. APPEND l1 l = APPEND l2 l <=> l1 = l2	link to proof	list-append-thm
APPEND_RCANCEL_IMP	!l l1 l2. APPEND l1 l = APPEND l2 l ==> l1 = l2	link to proof	list-append-thm
APPEND_RINJ	!l1 l1' l2 l2'. LENGTH l2 = LENGTH l2' /\ APPEND l1 l2 = APPEND l1' l2' ==> l2 = l2'	link to proof	list-append-thm
APPEND_SING	!h t. APPEND [h] t = CONS h t	link to proof	list-append-thm
BETA_THM	!f y. (\x. f x) y = f y	link to proof	bool-int
BIJ	!s t. BIJ s t = INJ s t INTER SURJ s t	link to proof	set-def
BIJECTIONS_CARD_EQ	!s t f g. (FINITE s \/ FINITE t) /\ (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) ==> CARD s = CARD t	link to proof	set-size-thm
BIJECTIONS_HAS_SIZE	!s t f g n. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) /\ s HAS_SIZE n ==> t HAS_SIZE n	link to proof	set-size-thm
BIJECTIONS_HAS_SIZE_EQ	!s t f g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y) ==> (!n. s HAS_SIZE n <=> t HAS_SIZE n)	link to proof	set-size-thm
BIJECTIVE_LEFT_RIGHT_INVERSE	!f. (!x y. f x = f y ==> x = y) /\ (!y. ?x. f x = y) <=> (?g. (!y. f (g y) = y) /\ (!x. g (f x) = x))	link to proof	set-thm
BIJECTIVE_ON_LEFT_RIGHT_INVERSE	!f s t. (!x. x IN s ==> f x IN t) ==> ((!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ (!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (?g. (!y. y IN t ==> g y IN s) /\ (!y. y IN t ==> f (g y) = y) /\ (!x. x IN s ==> g (f x) = x)))	link to proof	set-thm
BIT0_SUC	!n. BIT0 (SUC n) = SUC (SUC (BIT0 n))	link to proof	natural-numeral-def
BIT0_ZERO	BIT0 0 = 0	link to proof	natural-numeral-def
BIT1_DEF	!n. BIT1 n = SUC (BIT0 n)	link to proof	natural-numeral-def
BOOL_CASES_AX	!t. (t <=> T) \/ (t <=> F)	link to proof	bool-class
BOUNDS_DIVIDED	!p. (?b. !n. p n <= b) <=> (?a b. !n. n * p n <= a * n + b)	link to proof	natural-mult-thm
BOUNDS_IGNORE	!p q. (?b. !i. p i <= q i + b) <=> (?b n. !i. n <= i ==> p i <= q i + b)	link to proof	natural-add-thm
BOUNDS_LINEAR	!a b c. (!n. a * n <= b * n + c) <=> a <= b	link to proof	natural-mult-thm
BOUNDS_LINEAR_0	!a b. (!n. a * n <= b) <=> a = 0	link to proof	natural-mult-thm
BOUNDS_NOTZERO	!p a b. p 0 0 = 0 /\ (!m n. p m n <= a * (m + n) + b) ==> (?c. !m n. p m n <= c * (m + n))	link to proof	natural-mult-thm
CARD	CARD = ITSET (\x n. SUC n) 0	link to proof	set-size-def
CARD_CROSS	!s t. FINITE s /\ FINITE t ==> CARD (s CROSS t) = CARD s * CARD t	link to proof	set-size-thm
CARD_DELETE	!x s. FINITE s ==> CARD (s DELETE x) = (if x IN s then CARD s - 1 else CARD s)	link to proof	set-size-thm
CARD_DIFF	!s t. FINITE s /\ t SUBSET s ==> CARD (s DIFF t) = CARD s - CARD t	link to proof	set-size-thm
CARD_EMPTY	CARD {} = 0	link to proof	set-size-thm
CARD_EQ_0	!s. FINITE s ==> (CARD s = 0 <=> s = {})	link to proof	set-size-thm
CARD_EQ_BIJECTION	!s t. FINITE s /\ FINITE t /\ CARD s = CARD t ==> (?f. (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> (?x. x IN s /\ f x = y)) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))	link to proof	set-size-thm
CARD_EQ_BIJECTIONS	!s t. FINITE s /\ FINITE t /\ CARD s = CARD t ==> (?f g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\ (!y. y IN t ==> g y IN s /\ f (g y) = y))	link to proof	set-size-thm
CARD_FUNSPACE	!d s t. FINITE s /\ FINITE t ==> CARD {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)} = CARD t EXP CARD s	link to proof	set-size-thm
CARD_FUNSPACE_UNIV	FINITE UNIV /\ FINITE UNIV ==> CARD UNIV = CARD UNIV EXP CARD UNIV	link to proof	set-size-thm
CARD_IMAGE_EQ_INJ	!f s. FINITE s ==> (CARD (IMAGE f s) = CARD s <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))	link to proof	set-size-thm
CARD_IMAGE_INJ	!f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ FINITE s ==> CARD (IMAGE f s) = CARD s	link to proof	set-size-thm
CARD_IMAGE_INJ_EQ	!f s t. FINITE s /\ (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> (?!x. x IN s /\ f x = y)) ==> CARD t = CARD s	link to proof	set-size-thm
CARD_IMAGE_LE	!f s. FINITE s ==> CARD (IMAGE f s) <= CARD s	link to proof	set-size-thm
CARD_INSERT	!x s. FINITE s ==> CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s))	link to proof	set-size-thm
CARD_LE_INJ	!s t. FINITE s /\ FINITE t /\ CARD s <= CARD t ==> (?f. IMAGE f s SUBSET t /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))	link to proof	set-size-thm
CARD_NUMSEG_LE	!n. CARD {m | m <= n} = n + 1	link to proof	set-size-thm
CARD_NUMSEG_LT	!n. CARD {m | m < n} = n	link to proof	set-size-thm
CARD_POWERSET	!s. FINITE s ==> CARD {t | t SUBSET s} = 2 EXP CARD s	link to proof	set-size-thm
CARD_PRODUCT	!s t. FINITE s /\ FINITE t ==> CARD {x,y | x IN s /\ y IN t} = CARD s * CARD t	link to proof	set-size-thm
CARD_PSUBSET	!a b. a PSUBSET b /\ FINITE b ==> CARD a < CARD b	link to proof	set-size-thm
CARD_SET_OF_LIST_LE	!l. CARD (set_of_list l) <= LENGTH l	link to proof	list-set-thm
CARD_SING	!x. CARD {x} = 1	link to proof	set-size-thm
CARD_SUBSET	!a b. a SUBSET b /\ FINITE b ==> CARD a <= CARD b	link to proof	set-size-thm
CARD_SUBSET_EQ	!a b. FINITE b /\ a SUBSET b /\ CARD a = CARD b ==> a = b	link to proof	set-size-thm
CARD_SUBSET_IMAGE	!f s t. FINITE t /\ s SUBSET IMAGE f t ==> CARD s <= CARD t	link to proof	set-size-thm
CARD_SUBSET_LE	!a b. FINITE b /\ a SUBSET b /\ CARD b <= CARD a ==> a = b	link to proof	set-size-thm
CARD_UNION	!s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> CARD (s UNION t) = CARD s + CARD t	link to proof	set-size-thm
CARD_UNIONS_LE	!s t m n. s HAS_SIZE m /\ (!x. x IN s ==> FINITE (t x) /\ CARD (t x) <= n) ==> CARD (UNIONS {t x | x IN s}) <= m * n	link to proof	set-size-thm
CARD_UNION_DIFF	!s t. FINITE s /\ FINITE t ==> CARD (s UNION t) = CARD s + CARD (t DIFF s)	link to proof	set-size-thm
CARD_UNION_EQ	!s t u. FINITE u /\ DISJOINT s t /\ s UNION t = u ==> CARD s + CARD t = CARD u	link to proof	set-size-thm
CARD_UNION_GEN	!s t. FINITE s /\ FINITE t ==> CARD (s UNION t) = (CARD s + CARD t) - CARD (s INTER t)	link to proof	set-size-thm
CARD_UNION_INTER	!s t. FINITE s /\ FINITE t ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t	link to proof	set-size-thm
CARD_UNION_LE	!s t. FINITE s /\ FINITE t ==> CARD (s UNION t) <= CARD s + CARD t	link to proof	set-size-thm
CARD_UNION_OVERLAP	!s t. FINITE s /\ FINITE t /\ CARD (s UNION t) < CARD s + CARD t ==> ~DISJOINT s t	link to proof	set-size-thm
CARD_UNION_OVERLAP_EQ	!s t. FINITE s /\ FINITE t ==> (CARD (s UNION t) = CARD s + CARD t <=> DISJOINT s t)	link to proof	set-size-thm
CC_EQ_I	!f. C (C f) = f	link to proof	function-thm
CHOICE	!s. ~(s = {}) ==> CHOICE s IN s	link to proof	set-def
CHOICE_PAIRED_THM	!p q. (?a b. p a b) /\ (!a b. p a b ==> q (a,b)) ==> q (@(a,b). p a b)	link to proof	pair-thm
CHOICE_UNPAIR_THM	!p. (@(a,b). p a b) = (@x. p (FST x) (SND x))	link to proof	pair-thm
CHOOSE_SUBSET	!s n. FINITE s /\ n <= CARD s ==> (?t. t SUBSET s /\ t HAS_SIZE n)	link to proof	set-size-thm
CHOOSE_SUBSET_BETWEEN	!n s u. s SUBSET u /\ FINITE s /\ CARD s <= n /\ (FINITE u ==> n <= CARD u) ==> (?t. s SUBSET t /\ t SUBSET u /\ t HAS_SIZE n)	link to proof	set-size-thm
CHOOSE_SUBSET_STRONG	!s n. (FINITE s ==> n <= CARD s) ==> (?t. t SUBSET s /\ t HAS_SIZE n)	link to proof	set-size-thm
COMPONENT	!x s. x IN x INSERT s	link to proof	set-thm
COND_ABS	!b f g. (\x. if b then f x else g x) = (if b then f else g)	link to proof	bool-class
COND_DEF	COND = (\t t1 t2. @x. ((t <=> T) ==> x = t1) /\ ((t <=> F) ==> x = t2))	link to proof	bool-def
COND_ELIM_THM	!p c x y. p (if c then x else y) <=> (c ==> p x) /\ (~c ==> p y)	link to proof	bool-class
COND_EXPAND	!b t1 t2. (if b then t1 else t2) <=> (~b \/ t1) /\ (b \/ t2)	link to proof	bool-class
COND_FALSE	!t1 t2. (if F then t1 else t2) = t2	link to proof	bool-class
COND_ID	!b t. (if b then t else t) = t	link to proof	bool-class
COND_NOT	!c x y. (if ~c then x else y) = (if c then y else x)	link to proof	bool-class
COND_RAND	!b f x y. f (if b then x else y) = (if b then f x else f y)	link to proof	bool-class
COND_RATOR	!b f g x. (if b then f else g) x = (if b then f x else g x)	link to proof	bool-class
COND_TRUE	!t1 t2. (if T then t1 else t2) = t1	link to proof	bool-class
CONJ_ASSOC'	!t1 t2 t3. (t1 /\ t2) /\ t3 <=> t1 /\ t2 /\ t3	link to proof	bool-int
CONJ_REFL	!t. t /\ t <=> t	link to proof	bool-int
CONJ_SYM	!t1 t2. t1 /\ t2 <=> t2 /\ t1	link to proof	bool-int
CONS_11	!h1 h2 t1 t2. CONS h1 t1 = CONS h2 t2 <=> h1 = h2 /\ t1 = t2	link to proof	list-thm
CONS_APPEND	!l h t. APPEND (CONS h t) l = CONS h (APPEND t l)	link to proof	list-append-def
CONS_HD_TL	!l. ~NULL l ==> CONS (HD l) (TL l) = l	link to proof	list-dest-thm
CONTRAPOS_THM	!t1 t2. ~t1 ==> ~t2 <=> t2 ==> t1	link to proof	bool-class
CROSS	!s t. s CROSS t = {x,y | x IN s /\ y IN t}	link to proof	set-def
CROSS_EMPTY	!s. s CROSS {} = {}	link to proof	set-thm
CROSS_EQ_EMPTY	!s t. s CROSS t = {} <=> s = {} \/ t = {}	link to proof	set-thm
CROSS_UNIV	UNIV CROSS UNIV = UNIV	link to proof	set-thm
C_DEF	C = (\f x y. f y x)	link to proof	function-def
C_THM	!f x y. C f x y = f y x	link to proof	function-thm
DECOMPOSITION	!s x. x IN s <=> (?t. s = x INSERT t /\ ~(x IN t))	link to proof	set-thm
DELETE	!s x. s DELETE x = {y | y IN s /\ ~(y = x)}	link to proof	set-def
DELETE_COMM	!x y s. s DELETE x DELETE y = s DELETE y DELETE x	link to proof	set-thm
DELETE_DELETE	!x s. s DELETE x DELETE x = s DELETE x	link to proof	set-thm
DELETE_DIFF_SING	!x s. s DIFF {x} = s DELETE x	link to proof	set-thm
DELETE_INSERT	!x y s. (x INSERT s) DELETE y = (if x = y then s DELETE y else x INSERT (s DELETE y))	link to proof	set-thm
DELETE_INSERT_NON_ELEMENT	!x s. (x INSERT s) DELETE x = s <=> ~(x IN s)	link to proof	set-thm
DELETE_INTER	!s t x. s DELETE x INTER t = (s INTER t) DELETE x	link to proof	set-thm
DELETE_NON_ELEMENT	!x s. s DELETE x = s <=> ~(x IN s)	link to proof	set-thm
DELETE_SUBSET	!x s. s DELETE x SUBSET s	link to proof	set-thm
DIFF	!s t. s DIFF t = {x | x IN s /\ ~(x IN t)}	link to proof	set-def
DIFF_COMM	!t u s. s DIFF t DIFF u = s DIFF u DIFF t	link to proof	set-thm
DIFF_DIFF	!s t. s DIFF t DIFF t = s DIFF t	link to proof	set-thm
DIFF_EMPTY	!s. s DIFF {} = s	link to proof	set-thm
DIFF_EMPTY_SUBSET	!s t. s DIFF t = {} <=> s SUBSET t	link to proof	set-thm
DIFF_EQ_EMPTY	!s. s DIFF s = {}	link to proof	set-thm
DIFF_INSERT	!s t x. s DIFF x INSERT t = s DELETE x DIFF t	link to proof	set-thm
DIFF_INTERS	!u s. u DIFF INTERS s = UNIONS {u DIFF t | t IN s}	link to proof	set-thm
DIFF_SUBSET	!s t. s DIFF t SUBSET s	link to proof	set-thm
DIFF_UNION	!t u s. s DIFF t DIFF u = s DIFF (t UNION u)	link to proof	set-thm
DIFF_UNIONS	!u s. u DIFF UNIONS s = u INTER INTERS {u DIFF t | t IN s}	link to proof	set-thm
DIFF_UNION_CANCEL	!s t. s DIFF t UNION t = s UNION t	link to proof	set-thm
DIFF_UNION_SUBSET	!s t. t DIFF s UNION s = t <=> s SUBSET t	link to proof	set-thm
DIFF_UNIV	!s. s DIFF UNIV = {}	link to proof	set-thm
DISJOINT	!s t. DISJOINT s t <=> s INTER t = {}	link to proof	set-def
DISJOINT_DELETE_SYM	!s t x. DISJOINT (s DELETE x) t <=> DISJOINT (t DELETE x) s	link to proof	set-thm
DISJOINT_DIFF	!s t. s DIFF t = s <=> DISJOINT s t	link to proof	set-thm
DISJOINT_DIFF1	!s t. DISJOINT (t DIFF s) s	link to proof	set-thm
DISJOINT_DIFF2	!s t. DISJOINT s (t DIFF s)	link to proof	set-thm
DISJOINT_EMPTY	!s. DISJOINT s {}	link to proof	set-thm
DISJOINT_EMPTY_REFL	!s. DISJOINT s s <=> s = {}	link to proof	set-thm
DISJOINT_INSERT	!x s t. DISJOINT (x INSERT s) t <=> ~(x IN t) /\ DISJOINT s t	link to proof	set-thm
DISJOINT_SING	!x s. DISJOINT s {x} <=> ~(x IN s)	link to proof	set-thm
DISJOINT_SYM	!s t. DISJOINT s t <=> DISJOINT t s	link to proof	set-thm
DISJOINT_UNION	!s t u. DISJOINT (s UNION t) u <=> DISJOINT s u /\ DISJOINT t u	link to proof	set-thm
DISJOINT_UNIONS	!s t. DISJOINT s (UNIONS t) <=> (!x. x IN t ==> DISJOINT s x)	link to proof	set-thm
DISJ_ASSOC'	!t1 t2 t3. (t1 \/ t2) \/ t3 <=> t1 \/ t2 \/ t3	link to proof	bool-int
DISJ_REFL	!t. t \/ t <=> t	link to proof	bool-int
DISJ_SYM	!t1 t2. t1 \/ t2 <=> t2 \/ t1	link to proof	bool-int
DIST_ADD2	!m n p q. dist (m + n) (p + q) <= dist m p + dist n q	link to proof	natural-distance-thm
DIST_ADD2_REV	!m n p q. dist m p <= dist (m + n) (p + q) + dist n q	link to proof	natural-distance-thm
DIST_ADDBOUND	!m n. dist m n <= m + n	link to proof	natural-distance-thm
DIST_CASES	!m n p. dist m n = p <=> m + p = n \/ n + p = m	link to proof	natural-distance-thm
DIST_DIST_SUC	!m n. dist (dist m n) (dist m (n + 1)) = 1	link to proof	natural-distance-thm
DIST_ELIM_THM	!p x y. p (dist x y) <=> (!d. (x = y + d ==> p d) /\ (y = x + d ==> p d))	link to proof	natural-distance-thm
DIST_EQ_0	!m n. dist m n = 0 <=> m = n	link to proof	natural-distance-thm
DIST_LADD	!m n p. dist (m + n) (m + p) = dist n p	link to proof	natural-distance-thm
DIST_LADD_0	!m n. dist (m + n) m = n	link to proof	natural-distance-thm
DIST_LE_CASES	!m n p. dist m n <= p <=> m <= n + p /\ n <= m + p	link to proof	natural-distance-thm
DIST_LMUL	!m n p. m * dist n p = dist (m * n) (m * p)	link to proof	natural-distance-thm
DIST_LZERO	!n. dist 0 n = n	link to proof	natural-distance-thm
DIST_RADD	!p m n. dist (m + p) (n + p) = dist m n	link to proof	natural-distance-thm
DIST_RADD_0	!m n. dist m (m + n) = n	link to proof	natural-distance-thm
DIST_REFL	!n. dist n n = 0	link to proof	natural-distance-thm
DIST_RMUL	!p m n. dist m n * p = dist (m * p) (n * p)	link to proof	natural-distance-thm
DIST_RZERO	!n. dist n 0 = n	link to proof	natural-distance-thm
DIST_SUC	!m n. dist (SUC m) (SUC n) = dist m n	link to proof	natural-distance-thm
DIST_SYM	!m n. dist m n = dist n m	link to proof	natural-distance-thm
DIST_TRIANGLE	!m n p. dist m p <= dist m n + dist n p	link to proof	natural-distance-thm
DIST_TRIANGLES_LE	!m n p q r s. dist m n <= r /\ dist p q <= s ==> dist m p <= dist n q + r + s	link to proof	natural-distance-thm
DIST_TRIANGLE_LE	!m n p q. dist m n + dist n p <= q ==> dist m p <= q	link to proof	natural-distance-thm
DIVISION_DEF_DIV	!m n. ~(n = 0) ==> m DIV n * n + m MOD n = m	link to proof	natural-div-def
DIVISION_DEF_MOD	!m n. ~(n = 0) ==> m MOD n < n	link to proof	natural-div-def
DIV_0	!n. ~(n = 0) ==> 0 DIV n = 0	link to proof	natural-div-thm
DIV_1	!n. n DIV 1 = n	link to proof	natural-div-thm
DIV_ADD_MOD	!a b n. ~(n = 0) ==> ((a + b) MOD n = a MOD n + b MOD n <=> (a + b) DIV n = a DIV n + b DIV n)	link to proof	natural-div-thm
DIV_DIV	!m n p. ~(n * p = 0) ==> m DIV n DIV p = m DIV (n * p)	link to proof	natural-div-thm
DIV_EQ_0	!m n. ~(n = 0) ==> (m DIV n = 0 <=> m < n)	link to proof	natural-div-thm
DIV_EQ_EXCLUSION	!a b c d. b * c < (a + 1) * d /\ a * d < (c + 1) * b ==> a DIV b = c DIV d	link to proof	natural-div-thm
DIV_LE	!m n. ~(n = 0) ==> m DIV n <= m	link to proof	natural-div-thm
DIV_LE_EXCLUSION	!a b c d. ~(b = 0) /\ b * c < (a + 1) * d ==> c DIV d <= a DIV b	link to proof	natural-div-thm
DIV_LT	!m n. m < n ==> m DIV n = 0	link to proof	natural-div-thm
DIV_MOD	!m n p. ~(n * p = 0) ==> (m DIV n) MOD p = (m MOD (n * p)) DIV n	link to proof	natural-div-thm
DIV_MONO	!m n p. ~(p = 0) /\ m <= n ==> m DIV p <= n DIV p	link to proof	natural-div-thm
DIV_MONO2	!m n p. ~(p = 0) /\ p <= m ==> n DIV m <= n DIV p	link to proof	natural-div-thm
DIV_MONO_LT	!m n p. ~(p = 0) /\ m + p <= n ==> m DIV p < n DIV p	link to proof	natural-div-thm
DIV_MULT	!m n. ~(m = 0) ==> (m * n) DIV m = n	link to proof	natural-div-thm
DIV_MULT2	!m n p. ~(m * p = 0) ==> (m * n) DIV (m * p) = n DIV p	link to proof	natural-div-thm
DIV_MULT_ADD	!a b n. ~(n = 0) ==> (a * n + b) DIV n = a + b DIV n	link to proof	natural-div-thm
DIV_MUL_LE	!m n. n * m DIV n <= m	link to proof	natural-div-thm
DIV_REFL	!n. ~(n = 0) ==> n DIV n = 1	link to proof	natural-div-thm
DIV_UNIQ	!m n q r. m = q * n + r /\ r < n ==> m DIV n = q	link to proof	natural-div-thm
EMPTY	{} = {x | F}	link to proof	set-def
EMPTY_CROSS	!s. {} CROSS s = {}	link to proof	set-thm
EMPTY_DELETE	!x. {} DELETE x = {}	link to proof	set-thm
EMPTY_DIFF	!s. {} DIFF s = {}	link to proof	set-thm
EMPTY_DISJOINT	!s. DISJOINT {} s	link to proof	set-thm
EMPTY_FUNSPACE	!d t. {f | (!x. x IN {} ==> f x IN t) /\ (!x. ~(x IN {}) ==> f x = d)} = {(\x. d)}	link to proof	set-thm
EMPTY_GSPEC	GSPEC (\x. F) = {}	link to proof	set-thm
EMPTY_NUMSEG_LT	{m | m < 0} = {}	link to proof	set-thm
EMPTY_POWERSET	{s | s SUBSET {}} = {{}}	link to proof	set-thm
EMPTY_PRODUCT_DEPENDENT	!t. {x,y | x IN {} /\ y IN t x} = {}	link to proof	set-thm
EMPTY_SUBSET	!s. {} SUBSET s	link to proof	set-thm
EMPTY_UNION	!s t. s UNION t = {} <=> s = {} /\ t = {}	link to proof	set-thm
EMPTY_UNIONS	!s. UNIONS s = {} <=> (!t. t IN s ==> t = {})	link to proof	set-thm
EQ_ADD_LCANCEL	!m n p. m + n = m + p <=> n = p	link to proof	natural-add-thm
EQ_ADD_LCANCEL_0	!m n. m + n = m <=> n = 0	link to proof	natural-add-thm
EQ_ADD_RCANCEL	!p m n. m + p = n + p <=> m = n	link to proof	natural-add-thm
EQ_ADD_RCANCEL_0	!m n. m + n = n <=> m = 0	link to proof	natural-add-thm
EQ_EXP	!x m n. x EXP m = x EXP n <=> (if x = 0 then m = 0 <=> n = 0 else x = 1 \/ m = n)	link to proof	natural-exp-thm
EQ_EXT	!f g. (!x. f x = g x) ==> f = g	link to proof	bool-ext
EQ_FALSE_THM	!t. (t <=> F) <=> ~t	link to proof	bool-int
EQ_IMP	!a b. (a <=> b) ==> a ==> b	link to proof	bool-int
EQ_IMP_LE	!m n. m = n ==> m <= n	link to proof	natural-order-thm
EQ_MULTL	!m n. m = m * n <=> m = 0 \/ n = 1	link to proof	natural-mult-thm
EQ_MULTR	!m n. m = n * m <=> m = 0 \/ n = 1	link to proof	natural-mult-thm
EQ_MULT_LCANCEL	!m n p. m * n = m * p <=> m = 0 \/ n = p	link to proof	natural-mult-thm
EQ_MULT_RCANCEL	!m n p. m * p = n * p <=> m = n \/ p = 0	link to proof	natural-mult-thm
EQ_REFL	!x. x = x	link to proof	bool-int
EQ_SYM	!x y. x = y ==> y = x	link to proof	bool-int
EQ_SYM_EQ	!x y. x = y <=> y = x	link to proof	bool-int
EQ_TRANS	!x y z. x = y /\ y = z ==> x = z	link to proof	bool-int
EQ_TRUE_THM	!t. (t <=> T) <=> t	link to proof	bool-int
EQ_UNIV	!s. (!x. x IN s) <=> s = UNIV	link to proof	set-thm
ETA_AX	!t. (\x. t x) = t	link to proof	axiom-extensionality
EVEN_ADD	!m n. EVEN (m + n) <=> EVEN m <=> EVEN n	link to proof	natural-div-thm
EVEN_AND_ODD	!n. ~(EVEN n /\ ODD n)	link to proof	natural-div-thm
EVEN_DOUBLE	!n. EVEN (2 * n)	link to proof	natural-div-thm
EVEN_EXISTS	!n. EVEN n <=> (?m. n = 2 * m)	link to proof	natural-div-thm
EVEN_EXP	!m n. EVEN (m EXP n) <=> EVEN m /\ ~(n = 0)	link to proof	natural-exp-thm
EVEN_MOD	!n. EVEN n <=> n MOD 2 = 0	link to proof	natural-div-thm
EVEN_MULT	!m n. EVEN (m * n) <=> EVEN m \/ EVEN n	link to proof	natural-div-thm
EVEN_ODD_DECOMPOSITION	!n. (?k m. ODD m /\ n = 2 EXP k * m) <=> ~(n = 0)	link to proof	natural-exp-thm
EVEN_OR_ODD	!n. EVEN n \/ ODD n	link to proof	natural-div-thm
EVEN_SUB	!m n. n <= m ==> (EVEN (m - n) <=> EVEN m <=> EVEN n)	link to proof	natural-div-thm
EVEN_SUC	!n. EVEN (SUC n) <=> ~EVEN n	link to proof	natural-div-def
EVEN_ZERO	EVEN 0	link to proof	natural-div-def
EXCLUDED_MIDDLE	!t. t \/ ~t	link to proof	bool-class
EXISTS_BOOL_THM	!p. (?b. p b) <=> p T \/ p F	link to proof	bool-class
EXISTS_CURRY	!p. (?f. p f) <=> (?f. p (\(a,b). f a b))	link to proof	pair-thm
EXISTS_DEF	(?) = (\p. !q. (!x. p x ==> q) ==> q)	link to proof	bool-def
EXISTS_EX	!p l. (?x. EX (p x) l) <=> EX (\y. ?x. p x y) l	link to proof	list-set-thm
EXISTS_FINITE_SUBSET_IMAGE	!p f s. (?t. FINITE t /\ t SUBSET IMAGE f s /\ p t) <=> (?t. FINITE t /\ t SUBSET s /\ p (IMAGE f t))	link to proof	set-finite-thm
EXISTS_FINITE_SUBSET_IMAGE_INJ	!p f s. (?t. FINITE t /\ t SUBSET IMAGE f s /\ p t) <=> (?t. FINITE t /\ t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) /\ p (IMAGE f t))	link to proof	set-finite-thm
EXISTS_IN_GSPEC1	!p f q. (?z. z IN {f x | p x} /\ q z) <=> (?x. p x /\ q (f x))	link to proof	set-thm
EXISTS_IN_GSPEC2	!p f q. (?z. z IN {f x y | p x y} /\ q z) <=> (?x y. p x y /\ q (f x y))	link to proof	set-thm
EXISTS_IN_GSPEC3	!p f q. (?z. z IN {f w x y | p w x y} /\ q z) <=> (?w x y. p w x y /\ q (f w x y))	link to proof	set-thm
EXISTS_IN_IMAGE	!p f s. (?y. y IN IMAGE f s /\ p y) <=> (?x. x IN s /\ p (f x))	link to proof	set-thm
EXISTS_IN_INSERT	!p a s. (?x. x IN a INSERT s /\ p x) <=> p a \/ (?x. x IN s /\ p x)	link to proof	set-thm
EXISTS_IN_UNION	!p s t. (?x. x IN s UNION t /\ p x) <=> (?x. x IN s /\ p x) \/ (?x. x IN t /\ p x)	link to proof	set-thm
EXISTS_IN_UNIONS	!p s. (?x. x IN UNIONS s /\ p x) <=> (?t x. t IN s /\ x IN t /\ p x)	link to proof	set-thm
EXISTS_NOT_THM	!p. (?x. ~p x) <=> ~(!x. p x)	link to proof	bool-class
EXISTS_OR_THM	!p q. (?x. p x \/ q x) <=> (?x. p x) \/ (?x. q x)	link to proof	bool-int
EXISTS_PAIRED_THM	!p. (?(a,b). p a b) <=> (?a b. p a b)	link to proof	pair-thm
EXISTS_PAIR_THM	!p. (?x. p x) <=> (?a b. p (a,b))	link to proof	pair-thm
EXISTS_REFL	!a. ?x. x = a	link to proof	bool-int
EXISTS_SIMP	!t. (?x. t) <=> t	link to proof	bool-int
EXISTS_SUBSET_IMAGE	!p f s. (?t. t SUBSET IMAGE f s /\ p t) <=> (?t. t SUBSET s /\ p (IMAGE f t))	link to proof	set-thm
EXISTS_SUBSET_IMAGE_INJ	!p f s. (?t. t SUBSET IMAGE f s /\ p t) <=> (?t. t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) /\ p (IMAGE f t))	link to proof	set-thm
EXISTS_SUBSET_INSERT	!p x t. (?s. s SUBSET x INSERT t /\ p s) <=> (?s. s SUBSET t /\ (p s \/ p (x INSERT s)))	link to proof	set-thm
EXISTS_SUBSET_UNION	!p t u. (?s. s SUBSET t UNION u /\ p s) <=> (?t' u'. t' SUBSET t /\ u' SUBSET u /\ p (t' UNION u'))	link to proof	set-thm
EXISTS_THM	(?) = (\p. p ((@) p))	link to proof	bool-class
EXISTS_TRIPLED_THM	!p. (?(a,b,c). p a b c) <=> (?a b c. p a b c)	link to proof	pair-thm
EXISTS_UNCURRY	!p. (?f. p f) <=> (?f. p (\a b. f (a,b)))	link to proof	pair-thm
EXISTS_UNIQUE	!p. (?!x. p x) <=> (?x. p x /\ (!y. p y ==> y = x))	link to proof	bool-int
EXISTS_UNIQUE_ALT	!p. (?!x. p x) <=> (?x. !y. p y <=> x = y)	link to proof	bool-int
EXISTS_UNIQUE_DEF	(?!) = (\p. (?) p /\ (!x y. p x /\ p y ==> x = y))	link to proof	bool-def
EXISTS_UNIQUE_REFL	!a. ?!x. x = a	link to proof	bool-int
EXISTS_UNIQUE_THM	!p. (?!x. p x) <=> (?x. p x) /\ (!x x'. p x /\ p x' ==> x = x')	link to proof	bool-int
EXISTS_UNPAIR_THM	!p. (?x y. p x y) <=> (?z. p (FST z) (SND z))	link to proof	pair-thm
EXP_0	!m. m EXP 0 = 1	link to proof	natural-exp-def
EXP_1	!n. n EXP 1 = n	link to proof	natural-exp-thm
EXP_2	!n. n EXP 2 = n * n	link to proof	natural-exp-thm
EXP_ADD	!m n p. m EXP (n + p) = m EXP n * m EXP p	link to proof	natural-exp-thm
EXP_EQ_0	!m n. m EXP n = 0 <=> m = 0 /\ ~(n = 0)	link to proof	natural-exp-thm
EXP_EQ_1	!x n. x EXP n = 1 <=> x = 1 \/ n = 0	link to proof	natural-exp-thm
EXP_LT_0	!n x. 0 < x EXP n <=> ~(x = 0) \/ n = 0	link to proof	natural-exp-thm
EXP_MONO_EQ	!x y n. x EXP n = y EXP n <=> x = y \/ n = 0	link to proof	natural-exp-thm
EXP_MONO_LE	!x y n. x EXP n <= y EXP n <=> x <= y \/ n = 0	link to proof	natural-exp-thm
EXP_MONO_LE_IMP	!x y n. x <= y ==> x EXP n <= y EXP n	link to proof	natural-exp-thm
EXP_MONO_LT	!x y n. x EXP n < y EXP n <=> x < y /\ ~(n = 0)	link to proof	natural-exp-thm
EXP_MONO_LT_IMP	!x y n. x < y /\ ~(n = 0) ==> x EXP n < y EXP n	link to proof	natural-exp-thm
EXP_MULT	!m n p. m EXP (n * p) = m EXP n EXP p	link to proof	natural-exp-thm
EXP_ONE	!n. 1 EXP n = 1	link to proof	natural-exp-thm
EXP_SUC	!m n. m EXP SUC n = m * m EXP n	link to proof	natural-exp-def
EXP_ZERO	!n. 0 EXP n = (if n = 0 then 1 else 0)	link to proof	natural-exp-thm
EXTENSION'	!s t. (!x. x IN s <=> x IN t) <=> s = t	link to proof	set-thm
EXTENSION_IMP	!s t. (!x. x IN s <=> x IN t) ==> s = t	link to proof	set-def
EX_APPEND	!p l1 l2. EX p (APPEND l1 l2) <=> EX p l1 \/ EX p l2	link to proof	list-append-thm
EX_CONS	!p h t. EX p (CONS h t) <=> p h \/ EX p t	link to proof	list-set-def
EX_FILTER	!p q l. EX p (FILTER q l) <=> EX (\x. q x /\ p x) l	link to proof	list-filter-thm
EX_IMP	!p q l. (!x. MEM x l /\ p x ==> q x) /\ EX p l ==> EX q l	link to proof	list-set-thm
EX_MAP	!p f l. EX p (MAP f l) <=> EX (p o f) l	link to proof	list-map-thm
EX_MEM	!p l. (?x. MEM x l /\ p x) <=> EX p l	link to proof	list-set-thm
EX_NIL	!p. ~EX p []	link to proof	list-set-def
EX_SET_OF_LIST	!p l. EX p l <=> (?x. x IN set_of_list l /\ p x)	link to proof	list-set-thm
FACT_MONO	!m n. m <= n ==> FACT m <= FACT n	link to proof	natural-factorial-thm
FACT_NZ	!n. ~(FACT n = 0)	link to proof	natural-factorial-thm
FACT_SUC	!n. FACT (SUC n) = SUC n * FACT n	link to proof	natural-factorial-def
FACT_ZERO	FACT 0 = 1	link to proof	natural-factorial-def
FALSE_AND_THM	!t. F /\ t <=> F	link to proof	bool-int
FALSE_EQ_THM	!t. (F <=> t) <=> ~t	link to proof	bool-int
FALSE_IMP_THM	!t. F ==> t <=> T	link to proof	bool-int
FALSE_OR_THM	!t. F \/ t <=> t	link to proof	bool-int
FILTER_APPEND	!p l1 l2. FILTER p (APPEND l1 l2) = APPEND (FILTER p l1) (FILTER p l2)	link to proof	list-filter-thm
FILTER_CONS	!p h t. FILTER p (CONS h t) = (if p h then CONS h (FILTER p t) else FILTER p t)	link to proof	list-filter-def
FILTER_MAP	!p f l. FILTER p (MAP f l) = MAP f (FILTER (p o f) l)	link to proof	list-filter-thm
FILTER_NIL	!p. FILTER p [] = []	link to proof	list-filter-def
FINITE_BOOL	FINITE UNIV	link to proof	set-finite-thm
FINITE_CASES	!a. FINITE a <=> a = {} \/ (?x s. a = x INSERT s /\ FINITE s)	link to proof	set-finite-def
FINITE_CROSS	!s t. FINITE s /\ FINITE t ==> FINITE (s CROSS t)	link to proof	set-finite-thm
FINITE_CROSS_EQ	!s t. FINITE (s CROSS t) <=> s = {} \/ t = {} \/ FINITE s /\ FINITE t	link to proof	set-finite-thm
FINITE_DELETE	!s x. FINITE (s DELETE x) <=> FINITE s	link to proof	set-finite-thm
FINITE_DELETE_IMP	!s x. FINITE s ==> FINITE (s DELETE x)	link to proof	set-finite-thm
FINITE_DIFF	!s t. FINITE s ==> FINITE (s DIFF t)	link to proof	set-finite-thm
FINITE_EMPTY	FINITE {}	link to proof	set-finite-def
FINITE_FINITE_PREIMAGE	!f t. FINITE t /\ (!y. y IN t ==> FINITE {x | f x = y}) ==> FINITE {x | f x IN t}	link to proof	set-finite-thm
FINITE_FINITE_PREIMAGE_GENERAL	!f s t. FINITE t /\ (!y. y IN t ==> FINITE {x | x IN s /\ f x = y}) ==> FINITE {x | x IN s /\ f x IN t}	link to proof	set-finite-thm
FINITE_FINITE_UNIONS	!s. FINITE s ==> (FINITE (UNIONS s) <=> (!t. t IN s ==> FINITE t))	link to proof	set-finite-thm
FINITE_FUNSPACE	!d s t. FINITE s /\ FINITE t ==> FINITE {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)}	link to proof	set-finite-thm
FINITE_FUNSPACE_UNIV	FINITE UNIV /\ FINITE UNIV ==> FINITE UNIV	link to proof	set-size-thm
FINITE_HAS_SIZE	!s. FINITE s <=> s HAS_SIZE CARD s	link to proof	set-size-thm
FINITE_IMAGE	!f s. FINITE s ==> FINITE (IMAGE f s)	link to proof	set-finite-thm
FINITE_IMAGE_EXPAND	!f s. FINITE s ==> FINITE {y | ?x. x IN s /\ y = f x}	link to proof	set-finite-thm
FINITE_IMAGE_INJ	!f A. (!x y. f x = f y ==> x = y) /\ FINITE A ==> FINITE {x | f x IN A}	link to proof	set-finite-thm
FINITE_IMAGE_INJ_EQ	!f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> (FINITE (IMAGE f s) <=> FINITE s)	link to proof	set-finite-thm
FINITE_IMAGE_INJ_GENERAL	!f t s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ FINITE t ==> FINITE {x | x IN s /\ f x IN t}	link to proof	set-finite-thm
FINITE_INDUCT	!p. p {} /\ (!x s. p s ==> p (x INSERT s)) ==> (!a. FINITE a ==> p a)	link to proof	set-finite-def
FINITE_INDUCT_DELETE	!p. p {} /\ (!s. FINITE s /\ ~(s = {}) ==> (?x. x IN s /\ (p (s DELETE x) ==> p s))) ==> (!s. FINITE s ==> p s)	link to proof	set-size-thm
FINITE_INDUCT_STRONG	!p. p {} /\ (!x s. p s /\ ~(x IN s) /\ FINITE s ==> p (x INSERT s)) ==> (!s. FINITE s ==> p s)	link to proof	set-finite-thm
FINITE_INSERT	!s x. FINITE (x INSERT s) <=> FINITE s	link to proof	set-finite-thm
FINITE_INSERT_IMP	!x s. FINITE s ==> FINITE (x INSERT s)	link to proof	set-finite-def
FINITE_INTER	!s t. FINITE s \/ FINITE t ==> FINITE (s INTER t)	link to proof	set-finite-thm
FINITE_NUMSEG_LE	!n. FINITE {m | m <= n}	link to proof	set-finite-thm
FINITE_NUMSEG_LT	!n. FINITE {m | m < n}	link to proof	set-finite-thm
FINITE_POWERSET	!s. FINITE s ==> FINITE {t | t SUBSET s}	link to proof	set-finite-thm
FINITE_PRODUCT	!s t. FINITE s /\ FINITE t ==> FINITE {x,y | x IN s /\ y IN t}	link to proof	set-finite-thm
FINITE_PRODUCT_DEPENDENT	!f s t. FINITE s /\ (!x. x IN s ==> FINITE (t x)) ==> FINITE {f x y | x IN s /\ y IN t x}	link to proof	set-finite-thm
FINITE_RECURSION	!f b. (!x y s. ~(x = y) ==> f x (f y s) = f y (f x s)) ==> ITSET f b {} = b /\ (!x s. FINITE s ==> ITSET f b (x INSERT s) = (if x IN s then ITSET f b s else f x (ITSET f b s)))	link to proof	set-fold-def
FINITE_RECURSION_DELETE	!f b. (!x y s. ~(x = y) ==> f x (f y s) = f y (f x s)) ==> ITSET f b {} = b /\ (!x s. FINITE s ==> ITSET f b s = (if x IN s then f x (ITSET f b (s DELETE x)) else ITSET f b (s DELETE x)))	link to proof	set-fold-thm
FINITE_RESTRICT	!s p. FINITE s ==> FINITE {x | x IN s /\ p x}	link to proof	set-finite-thm
FINITE_SET_OF_LIST	!l. FINITE (set_of_list l)	link to proof	list-set-thm
FINITE_SING	!a. FINITE {a}	link to proof	set-finite-thm
FINITE_SUBSET	!s t. FINITE t /\ s SUBSET t ==> FINITE s	link to proof	set-finite-thm
FINITE_SUBSET_IMAGE	!f s t. FINITE t /\ t SUBSET IMAGE f s <=> (?s'. FINITE s' /\ s' SUBSET s /\ t = IMAGE f s')	link to proof	set-finite-thm
FINITE_SUBSET_IMAGE_IMP	!f s t. FINITE t /\ t SUBSET IMAGE f s ==> (?s'. FINITE s' /\ s' SUBSET s /\ t SUBSET IMAGE f s')	link to proof	set-finite-thm
FINITE_TRANSITIVITY_CHAIN	!r s. FINITE s /\ (!x. ~r x x) /\ (!x y z. r x y /\ r y z ==> r x z) /\ (!x. x IN s ==> (?y. y IN s /\ r x y)) ==> s = {}	link to proof	set-finite-thm
FINITE_UNION	!s t. FINITE (s UNION t) <=> FINITE s /\ FINITE t	link to proof	set-finite-thm
FINITE_UNIONS	!s. FINITE (UNIONS s) <=> FINITE s /\ (!t. t IN s ==> FINITE t)	link to proof	set-finite-thm
FINITE_UNION_IMP	!s t. FINITE s /\ FINITE t ==> FINITE (s UNION t)	link to proof	set-finite-thm
FORALL_ALL	!p l. (!x. ALL (p x) l) <=> ALL (\y. !x. p x y) l	link to proof	list-set-thm
FORALL_AND_THM	!p q. (!x. p x /\ q x) <=> (!x. p x) /\ (!x. q x)	link to proof	bool-int
FORALL_BOOL_THM	!p. (!b. p b) <=> p T /\ p F	link to proof	bool-class
FORALL_CURRY	!p. (!f. p f) <=> (!f. p (\(a,b). f a b))	link to proof	pair-thm
FORALL_DEF	(!) = (\p. p = (\x. T))	link to proof	bool-def
FORALL_FINITE_SUBSET_IMAGE	!p f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> p t) <=> (!t. FINITE t /\ t SUBSET s ==> p (IMAGE f t))	link to proof	set-finite-thm
FORALL_FINITE_SUBSET_IMAGE_INJ	!p f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> p t) <=> (!t. FINITE t /\ t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) ==> p (IMAGE f t))	link to proof	set-finite-thm
FORALL_IN_GSPEC1	!p f q. (!z. z IN {f x | p x} ==> q z) <=> (!x. p x ==> q (f x))	link to proof	set-thm
FORALL_IN_GSPEC2	!p f q. (!z. z IN {f x y | p x y} ==> q z) <=> (!x y. p x y ==> q (f x y))	link to proof	set-thm
FORALL_IN_GSPEC3	!p f q. (!z. z IN {f w x y | p w x y} ==> q z) <=> (!w x y. p w x y ==> q (f w x y))	link to proof	set-thm
FORALL_IN_IMAGE	!p f s. (!y. y IN IMAGE f s ==> p y) <=> (!x. x IN s ==> p (f x))	link to proof	set-thm
FORALL_IN_IMAGE_2	!p f s. (!x y. x IN IMAGE f s /\ y IN IMAGE f s ==> p x y) <=> (!x y. x IN s /\ y IN s ==> p (f x) (f y))	link to proof	set-thm
FORALL_IN_INSERT	!p a s. (!x. x IN a INSERT s ==> p x) <=> p a /\ (!x. x IN s ==> p x)	link to proof	set-thm
FORALL_IN_UNION	!p s t. (!x. x IN s UNION t ==> p x) <=> (!x. x IN s ==> p x) /\ (!x. x IN t ==> p x)	link to proof	set-thm
FORALL_IN_UNIONS	!p s. (!x. x IN UNIONS s ==> p x) <=> (!t x. t IN s /\ x IN t ==> p x)	link to proof	set-thm
FORALL_NOT_THM	!p. (!x. ~p x) <=> ~(?x. p x)	link to proof	bool-class
FORALL_PAIRED_THM	!p. (!(a,b). p a b) <=> (!a b. p a b)	link to proof	pair-thm
FORALL_PAIR_THM	!p. (!x. p x) <=> (!a b. p (a,b))	link to proof	pair-thm
FORALL_SIMP	!t. (!x. t) <=> t	link to proof	bool-int
FORALL_SUBSET_IMAGE	!p f s. (!t. t SUBSET IMAGE f s ==> p t) <=> (!t. t SUBSET s ==> p (IMAGE f t))	link to proof	set-thm
FORALL_SUBSET_IMAGE_INJ	!p f s. (!t. t SUBSET IMAGE f s ==> p t) <=> (!t. t SUBSET s /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y) ==> p (IMAGE f t))	link to proof	set-thm
FORALL_SUBSET_INSERT	!p x t. (!s. s SUBSET x INSERT t ==> p s) <=> (!s. s SUBSET t ==> p s /\ p (x INSERT s))	link to proof	set-thm
FORALL_SUBSET_UNION	!p t u. (!s. s SUBSET t UNION u ==> p s) <=> (!t' u'. t' SUBSET t /\ u' SUBSET u ==> p (t' UNION u'))	link to proof	set-thm
FORALL_TRIPLED_THM	!p. (!(a,b,c). p a b c) <=> (!a b c. p a b c)	link to proof	pair-thm
FORALL_UNCURRY	!p. (!f. p f) <=> (!f. p (\a b. f (a,b)))	link to proof	pair-thm
FORALL_UNPAIR_THM	!p. (!x y. p x y) <=> (!z. p (FST z) (SND z))	link to proof	pair-thm
FORALL_UNWIND_THM1	!p a. (!x. a = x ==> p x) <=> p a	link to proof	bool-int
FORALL_UNWIND_THM2	!p a. (!x. x = a ==> p x) <=> p a	link to proof	bool-int
FST	!a b. FST (a,b) = a	link to proof	pair-def
FUNCTION_FACTORS_LEFT	!f g. (!x y. g x = g y ==> f x = f y) <=> (?h. f = h o g)	link to proof	function-thm
FUNCTION_FACTORS_LEFT_GEN	!p f g. (!x y. p x /\ p y /\ g x = g y ==> f x = f y) <=> (?h. !x. p x ==> f x = h (g x))	link to proof	function-thm
FUNCTION_FACTORS_RIGHT	!f g. (!x. ?y. g y = f x) <=> (?h. f = g o h)	link to proof	function-thm
FUNCTION_FACTORS_RIGHT_GEN	!p f g. (!x. p x ==> (?y. g y = f x)) <=> (?h. !x. p x ==> f x = g (h x))	link to proof	function-thm
FUN_EQ_THM'	!f g. (!x. f x = g x) <=> f = g	link to proof	bool-ext
FUN_IN_IMAGE	!f s x. x IN s ==> f x IN IMAGE f s	link to proof	set-thm
F_DEF	F <=> (!p. p)	link to proof	bool-def
GE	!m n. m >= n <=> n <= m	link to proof	natural-order-def
GT	!m n. m > n <=> n < m	link to proof	natural-order-def
HAS_SIZE	!s n. s HAS_SIZE n <=> FINITE s /\ CARD s = n	link to proof	set-size-def
HAS_SIZE_0	!s. s HAS_SIZE 0 <=> s = {}	link to proof	set-size-thm
HAS_SIZE_BOOL	UNIV HAS_SIZE 2	link to proof	set-size-thm
HAS_SIZE_CARD	!s n. s HAS_SIZE n ==> CARD s = n	link to proof	set-size-thm
HAS_SIZE_CROSS	!s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> s CROSS t HAS_SIZE m * n	link to proof	set-size-thm
HAS_SIZE_DIFF	!s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ t SUBSET s ==> s DIFF t HAS_SIZE m - n	link to proof	set-size-thm
HAS_SIZE_FUNSPACE	!d s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)} HAS_SIZE n EXP m	link to proof	set-size-thm
HAS_SIZE_FUNSPACE_UNIV	!m n. UNIV HAS_SIZE m /\ UNIV HAS_SIZE n ==> UNIV HAS_SIZE n EXP m	link to proof	set-size-thm
HAS_SIZE_IMAGE_INJ	!f s n. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\ s HAS_SIZE n ==> IMAGE f s HAS_SIZE n	link to proof	set-size-thm
HAS_SIZE_IMAGE_INJ_EQ	!f s n. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> (IMAGE f s HAS_SIZE n <=> s HAS_SIZE n)	link to proof	set-size-thm
HAS_SIZE_INDEX	!s n. s HAS_SIZE n ==> (?f. (!m. m < n ==> f m IN s) /\ (!x. x IN s ==> (?!m. m < n /\ f m = x)))	link to proof	set-size-thm
HAS_SIZE_INSERT	!s n. s HAS_SIZE SUC n <=> (?a t. t HAS_SIZE n /\ ~(a IN t) /\ s = a INSERT t)	link to proof	set-size-thm
HAS_SIZE_NUMSEG_LE	!n. {m | m <= n} HAS_SIZE n + 1	link to proof	set-size-thm
HAS_SIZE_NUMSEG_LT	!n. {m | m < n} HAS_SIZE n	link to proof	set-size-thm
HAS_SIZE_POWERSET	!s n. s HAS_SIZE n ==> {t | t SUBSET s} HAS_SIZE 2 EXP n	link to proof	set-size-thm
HAS_SIZE_PRODUCT	!s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> {x,y | x IN s /\ y IN t} HAS_SIZE m * n	link to proof	set-size-thm
HAS_SIZE_PRODUCT_DEPENDENT	!s t m n. s HAS_SIZE m /\ (!x. x IN s ==> t x HAS_SIZE n) ==> {x,y | x IN s /\ y IN t x} HAS_SIZE m * n	link to proof	set-size-thm
HAS_SIZE_SING	!x. {x} HAS_SIZE 1	link to proof	set-size-thm
HAS_SIZE_SUC	!s n. s HAS_SIZE SUC n <=> ~(s = {}) /\ (!a. a IN s ==> s DELETE a HAS_SIZE n)	link to proof	set-size-thm
HAS_SIZE_UNION	!s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ DISJOINT s t ==> s UNION t HAS_SIZE m + n	link to proof	set-size-thm
HAS_SIZE_UNIONS	!s t m n. s HAS_SIZE m /\ (!x. x IN s ==> t x HAS_SIZE n) /\ (!x y. x IN s /\ y IN s /\ ~(x = y) ==> DISJOINT (t x) (t y)) ==> UNIONS {t x | x IN s} HAS_SIZE m * n	link to proof	set-size-thm
HD	!h t. HD (CONS h t) = h	link to proof	list-dest-def
IMAGE	!f s. IMAGE f s = {y | ?x. x IN s /\ y = f x}	link to proof	set-def
IMAGE_CONST	!s c. IMAGE (\x. c) s = (if s = {} then {} else {c})	link to proof	set-thm
IMAGE_DELETE_INJ	!f s a. (!x. f x = f a ==> x = a) ==> IMAGE f (s DELETE a) = IMAGE f s DELETE f a	link to proof	set-thm
IMAGE_DIFF_INJ	!f s t. (!x y. f x = f y ==> x = y) ==> IMAGE f (s DIFF t) = IMAGE f s DIFF IMAGE f t	link to proof	set-thm
IMAGE_EMPTY	!f. IMAGE f {} = {}	link to proof	set-thm
IMAGE_EQ_EMPTY	!f s. IMAGE f s = {} <=> s = {}	link to proof	set-thm
IMAGE_I	!s. IMAGE I s = s	link to proof	set-thm
IMAGE_ID	!s. IMAGE (\x. x) s = s	link to proof	set-thm
IMAGE_IMP_INJECTIVE	!s f. FINITE s /\ IMAGE f s = s ==> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)	link to proof	set-size-thm
IMAGE_IMP_INJECTIVE_GEN	!s t f. FINITE s /\ CARD s = CARD t /\ IMAGE f s = t ==> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)	link to proof	set-size-thm
IMAGE_INJECTIVE_IMAGE_OF_SUBSET	!f s. ?t. t SUBSET s /\ IMAGE f s = IMAGE f t /\ (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y)	link to proof	set-thm
IMAGE_INSERT	!f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s	link to proof	set-thm
IMAGE_INTERS	!f s. ~(s = {}) /\ (!x y. x IN UNIONS s /\ y IN UNIONS s /\ f x = f y ==> x = y) ==> IMAGE f (INTERS s) = INTERS (IMAGE (IMAGE f) s)	link to proof	set-thm
IMAGE_INTER_INJ	!f s t. (!x y. f x = f y ==> x = y) ==> IMAGE f (s INTER t) = IMAGE f s INTER IMAGE f t	link to proof	set-thm
IMAGE_POWERSET	!s. {t | t SUBSET s} = IMAGE (\p. {x | p x}) {p | (!x. x IN s ==> p x IN UNIV) /\ (!x. ~(x IN s) ==> (p x <=> F))}	link to proof	set-thm
IMAGE_SING	!f x. IMAGE f {x} = {f x}	link to proof	set-thm
IMAGE_SUBSET	!f s t. s SUBSET t ==> IMAGE f s SUBSET IMAGE f t	link to proof	set-thm
IMAGE_UNION	!f s t. IMAGE f (s UNION t) = IMAGE f s UNION IMAGE f t	link to proof	set-thm
IMAGE_UNIONS	!f s. IMAGE f (UNIONS s) = UNIONS (IMAGE (IMAGE f) s)	link to proof	set-thm
IMAGE_o	!f g s. IMAGE (f o g) s = IMAGE f (IMAGE g s)	link to proof	set-thm
IMP_AND_DISTRIB	!p q r. p ==> q /\ r <=> (p ==> q) /\ (p ==> r)	link to proof	bool-int
IMP_DEF	(==>) = (\p q. p /\ q <=> p)	link to proof	bool-def
IMP_FALSE_THM	!t. t ==> F <=> ~t	link to proof	bool-int
IMP_IMP	!p q r. p ==> q ==> r <=> p /\ q ==> r	link to proof	bool-int
IMP_REFL	!t. t ==> t	link to proof	bool-int
IMP_TRUE_THM	!t. t ==> T <=> T	link to proof	bool-int
INFINITE	!s. INFINITE s <=> ~FINITE s	link to proof	set-finite-def
INFINITE_DIFF_FINITE	!s t. INFINITE s /\ FINITE t ==> INFINITE (s DIFF t)	link to proof	set-finite-thm
INFINITE_ENUMERATE	!s. INFINITE s ==> (?r. (!m n. m < n ==> r m < r n) /\ IMAGE r UNIV = s)	link to proof	set-finite-thm
INFINITE_IMAGE_INJ	!f s. INFINITE s /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==> INFINITE (IMAGE f s)	link to proof	set-finite-thm
INFINITE_IMAGE_INJ_EQ	!f. (!x y. f x = f y ==> x = y) ==> (!s. INFINITE (IMAGE f s) <=> INFINITE s)	link to proof	set-finite-thm
INFINITE_NONEMPTY	!s. INFINITE s ==> ~(s = {})	link to proof	set-finite-thm
INFINITE_SUPERSET	!s t. INFINITE s /\ s SUBSET t ==> INFINITE t	link to proof	set-finite-thm
INFINITY_AX	?f. ONE_ONE f /\ ~ONTO f	link to proof	axiom-infinity
INJ	!s t. INJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}	link to proof	set-def
INJECTIVE_IMAGE	!f. (!s t. IMAGE f s = IMAGE f t ==> s = t) <=> (!x y. f x = f y ==> x = y)	link to proof	set-thm
INJECTIVE_LEFT_INVERSE	!f. (!x y. f x = f y ==> x = y) <=> (?g. !x. g (f x) = x)	link to proof	set-thm
INJECTIVE_MAP	!f. (!l1 l2. MAP f l1 = MAP f l2 ==> l1 = l2) <=> (!x y. f x = f y ==> x = y)	link to proof	list-map-thm
INJECTIVE_ON_IMAGE	!f u. (!s t. s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t ==> s = t) <=> (!x y. x IN u /\ y IN u /\ f x = f y ==> x = y)	link to proof	set-thm
INJECTIVE_ON_LEFT_INVERSE	!f s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) <=> (?g. !x. x IN s ==> g (f x) = x)	link to proof	set-thm
INSERT	!x s. x INSERT s = {y | y = x \/ y IN s}	link to proof	set-def
INSERT_AC	!x y s. x INSERT y INSERT s = y INSERT x INSERT s /\ x INSERT x INSERT s = x INSERT s	link to proof	set-thm
INSERT_BOOL	UNIV = {T, F}	link to proof	set-thm
INSERT_COMM	!x y s. x INSERT y INSERT s = y INSERT x INSERT s	link to proof	set-thm
INSERT_DELETE	!x s. x IN s ==> x INSERT (s DELETE x) = s	link to proof	set-thm
INSERT_DIFF	!s t x. x INSERT s DIFF t = (if x IN t then s DIFF t else x INSERT (s DIFF t))	link to proof	set-thm
INSERT_FUNSPACE	!d a s t. {f | (!x. x IN a INSERT s ==> f x IN t) /\ (!x. ~(x IN a INSERT s) ==> f x = d)} = IMAGE (\(b,g) x. if x = a then b else g x) (t CROSS {f | (!x. x IN s ==> f x IN t) /\ (!x. ~(x IN s) ==> f x = d)})	link to proof	set-thm
INSERT_INSERT	!x s. x INSERT x INSERT s = x INSERT s	link to proof	set-thm
INSERT_INTER	!x s t. x INSERT s INTER t = (if x IN t then x INSERT (s INTER t) else s INTER t)	link to proof	set-thm
INSERT_NUMSEG_LT	!n. {m | m < SUC n} = n INSERT {m | m < n}	link to proof	set-thm
INSERT_NUMSEG_LT'	!n. {m | m < SUC n} = 0 INSERT {SUC m | m < n}	link to proof	set-thm
INSERT_POWERSET	!a t. {s | s SUBSET a INSERT t} = {s | s SUBSET t} UNION IMAGE (\s. a INSERT s) {s | s SUBSET t}	link to proof	set-thm
INSERT_PRODUCT_DEPENDENT	!s t a. {x,y | x IN a INSERT s /\ y IN t x} = IMAGE ((,) a) (t a) UNION {x,y | x IN s /\ y IN t x}	link to proof	set-thm
INSERT_SUBSET	!x s t. x INSERT s SUBSET t <=> x IN t /\ s SUBSET t	link to proof	set-thm
INSERT_UNION	!x s t. x INSERT s UNION t = (if x IN t then s UNION t else x INSERT (s UNION t))	link to proof	set-thm
INSERT_UNION_EQ	!x s t. x INSERT s UNION t = x INSERT (s UNION t)	link to proof	set-thm
INSERT_UNION_SING	!x s. {x} UNION s = x INSERT s	link to proof	set-thm
INSERT_UNIV	!x. x INSERT UNIV = UNIV	link to proof	set-thm
INTER	!s t. s INTER t = {x | x IN s /\ x IN t}	link to proof	set-def
INTERS	!s. INTERS s = {x | !u. u IN s ==> x IN u}	link to proof	set-def
INTERS_0	INTERS {} = UNIV	link to proof	set-thm
INTERS_1	!s. INTERS {s} = s	link to proof	set-thm
INTERS_2	!s t. INTERS {s, t} = s INTER t	link to proof	set-thm
INTERS_GSPEC1	!p f. INTERS {f x | p x} = {a | !x. p x ==> a IN f x}	link to proof	set-thm
INTERS_GSPEC2	!p f. INTERS {f x y | p x y} = {a | !x y. p x y ==> a IN f x y}	link to proof	set-thm
INTERS_GSPEC3	!p f. INTERS {f x y z | p x y z} = {a | !x y z. p x y z ==> a IN f x y z}	link to proof	set-thm
INTERS_IMAGE	!f s. INTERS (IMAGE f s) = {y | !x. x IN s ==> y IN f x}	link to proof	set-thm
INTERS_INSERT	!s u. INTERS (s INSERT u) = s INTER INTERS u	link to proof	set-thm
INTERS_OVER_UNIONS	!f s. INTERS {UNIONS (f x) | x IN s} = UNIONS {INTERS {g x | x IN s} | g | !x. x IN s ==> g x IN f x}	link to proof	set-thm
INTERS_SUBSET	!u s. ~(u = {}) /\ (!t. t IN u ==> t SUBSET s) ==> INTERS u SUBSET s	link to proof	set-thm
INTERS_SUBSET_INTERS	!s t. s SUBSET t ==> INTERS t SUBSET INTERS s	link to proof	set-thm
INTERS_UNION	!s t. INTERS (s UNION t) = INTERS s INTER INTERS t	link to proof	set-thm
INTERS_UNIONS	!s. INTERS s = UNIV DIFF UNIONS {UNIV DIFF t | t IN s}	link to proof	set-thm
INTER_ACI	!p q r. p INTER q = q INTER p /\ (p INTER q) INTER r = p INTER q INTER r /\ p INTER q INTER r = q INTER p INTER r /\ p INTER p = p /\ p INTER p INTER q = p INTER q	link to proof	set-thm
INTER_ASSOC	!s t u. (s INTER t) INTER u = s INTER t INTER u	link to proof	set-thm
INTER_COMM	!s t. s INTER t = t INTER s	link to proof	set-thm
INTER_IDEMPOT	!s. s INTER s = s	link to proof	set-thm
INTER_LEFT_EMPTY	!s. {} INTER s = {}	link to proof	set-thm
INTER_LEFT_UNIV	!s. UNIV INTER s = s	link to proof	set-thm
INTER_RIGHT_EMPTY	!s. s INTER {} = {}	link to proof	set-thm
INTER_RIGHT_UNIV	!s. s INTER UNIV = s	link to proof	set-thm
INTER_UNIONS	!s t. t INTER UNIONS s = UNIONS {t INTER x | x IN s}	link to proof	set-thm
IN_CROSS	!x y s t. x,y IN s CROSS t <=> x IN s /\ y IN t	link to proof	set-thm
IN_DELETE	!s x y. x IN s DELETE y <=> x IN s /\ ~(x = y)	link to proof	set-thm
IN_DELETE_EQ	!s x x'. (x IN s DELETE x' <=> x' IN s DELETE x) <=> x IN s <=> x' IN s	link to proof	set-thm
IN_DELETE_SWAP	!s x x'. (x IN s <=> x' IN s) ==> (x IN s DELETE x' <=> x' IN s DELETE x)	link to proof	set-thm
IN_DIFF	!s t x. x IN s DIFF t <=> x IN s /\ ~(x IN t)	link to proof	set-thm
IN_DISJOINT	!s t. DISJOINT s t <=> ~(?x. x IN s /\ x IN t)	link to proof	set-thm
IN_ELIM	!p x. x IN {y | p y} <=> p x	link to proof	set-thm
IN_ELIM_PAIR_THM	!p a b. a,b IN {x,y | p x y} <=> p a b	link to proof	set-thm
IN_ELIM_THM	!p x. x IN GSPEC p <=> p x	link to proof	set-def
IN_IMAGE	!y s f. y IN IMAGE f s <=> (?x. y = f x /\ x IN s)	link to proof	set-thm
IN_INSERT	!x y s. x IN y INSERT s <=> x = y \/ x IN s	link to proof	set-thm
IN_INTER	!s t x. x IN s INTER t <=> x IN s /\ x IN t	link to proof	set-thm
IN_INTERS	!s x. x IN INTERS s <=> (!t. t IN s ==> x IN t)	link to proof	set-thm
IN_REST	!x s. x IN REST s <=> x IN s /\ ~(x = CHOICE s)	link to proof	set-thm
IN_SING	!x y. x IN {y} <=> x = y	link to proof	set-thm
IN_UNION	!s t x. x IN s UNION t <=> x IN s \/ x IN t	link to proof	set-thm
IN_UNIONS	!s x. x IN UNIONS s <=> (?t. t IN s /\ x IN t)	link to proof	set-thm
IN_UNIV	!x. x IN UNIV	link to proof	set-thm
ISL_INL	!a. ISL (INL a)	link to proof	sum-def
ISL_INR	!b. ~ISL (INR b)	link to proof	sum-def
ISL_case_sum	!f g x. ISL x ==> case_sum f g x = f (OUTL x)	link to proof	sum-thm
ISR_INL	!a. ~ISR (INL a)	link to proof	sum-def
ISR_INR	!b. ISR (INR b)	link to proof	sum-def
ISR_case_sum	!f g x. ISR x ==> case_sum f g x = g (OUTR x)	link to proof	sum-thm
ITSET_EQ	!f g b s. FINITE s /\ (!x. x IN s ==> f x = g x) /\ (!x y s. ~(x = y) ==> f x (f y s) = f y (f x s)) /\ (!x y s. ~(x = y) ==> g x (g y s) = g y (g x s)) ==> ITSET f b s = ITSET g b s	link to proof	set-fold-thm
I_DEF	I = (\x. x)	link to proof	function-def
I_O	!f. I o f = f	link to proof	function-thm
I_THM	!x. I x = x	link to proof	function-thm
K_DEF	K = (\x y. x)	link to proof	function-def
K_THM	!x y. K x y = x	link to proof	function-thm
LAMBDA_PAIR_THM	!f. (\x. f x) = (\(a,b). f (a,b))	link to proof	pair-thm
LAMBDA_UNPAIR_THM	!f. (\(x,y). f x y) = (\p. f (FST p) (SND p))	link to proof	pair-thm
LAST	!h t. LAST (CONS h t) = (if NULL t then h else LAST t)	link to proof	list-last-def
LAST_MULTIPLE	!x1 x2 l. LAST (CONS x1 (CONS x2 l)) = LAST (CONS x2 l)	link to proof	list-last-thm
LAST_SING	!x. LAST [x] = x	link to proof	list-last-thm
LEFT_ADD_DISTRIB	!m n p. m * (n + p) = m * n + m * p	link to proof	natural-mult-thm
LEFT_AND_DISTRIB	!p q r. p \/ q /\ r <=> (p \/ q) /\ (p \/ r)	link to proof	bool-int
LEFT_AND_EXISTS_THM	!p q. (?x. p x) /\ q <=> (?x. p x /\ q)	link to proof	bool-int
LEFT_AND_FORALL_THM	!p q. (!x. p x) /\ q <=> (!x. p x /\ q)	link to proof	bool-int
LEFT_EXISTS_AND_THM	!p q. (?x. p x /\ q) <=> (?x. p x) /\ q	link to proof	bool-int
LEFT_EXISTS_IMP_THM	!p q. (?x. p x ==> q) <=> (!x. p x) ==> q	link to proof	bool-class
LEFT_FORALL_IMP_THM	!p q. (!x. p x ==> q) <=> (?x. p x) ==> q	link to proof	bool-int
LEFT_FORALL_OR_THM	!p q. (!x. p x \/ q) <=> (!x. p x) \/ q	link to proof	bool-class
LEFT_IMP_EXISTS_THM	!p q. (?x. p x) ==> q <=> (!x. p x ==> q)	link to proof	bool-int
LEFT_IMP_FORALL_THM	!p q. (!x. p x) ==> q <=> (?x. p x ==> q)	link to proof	bool-class
LEFT_INTER_DISTRIB	!s t u. s UNION t INTER u = (s UNION t) INTER (s UNION u)	link to proof	set-thm
LEFT_INTER_SUBSET	!s t. s INTER t SUBSET s	link to proof	set-thm
LEFT_OR_DISTRIB	!p q r. p /\ (q \/ r) <=> p /\ q \/ p /\ r	link to proof	bool-int
LEFT_OR_EXISTS_THM	!p q. (?x. p x) \/ q <=> (?x. p x \/ q)	link to proof	bool-int
LEFT_OR_FORALL_THM	!p q. (!x. p x) \/ q <=> (!x. p x \/ q)	link to proof	bool-class
LEFT_SUB_DISTRIB	!m n p. p <= n ==> m * (n - p) = m * n - m * p	link to proof	natural-mult-thm
LEFT_UNION_DISTRIB	!s t u. s INTER (t UNION u) = s INTER t UNION s INTER u	link to proof	set-thm
LEFT_UNION_INTERS	!s t. t UNION INTERS s = INTERS {t UNION x | x IN s}	link to proof	set-thm
LENGTH_APPEND	!l1 l2. LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2	link to proof	list-append-thm
LENGTH_CONS	!h t. LENGTH (CONS h t) = SUC (LENGTH t)	link to proof	list-length-def
LENGTH_EQ_CONS	!l n. LENGTH l = SUC n <=> (?h t. l = CONS h t /\ LENGTH t = n)	link to proof	list-length-thm
LENGTH_EQ_NIL	!l. LENGTH l = 0 <=> l = []	link to proof	list-length-thm
LENGTH_FILTER	!p l. LENGTH (FILTER p l) <= LENGTH l	link to proof	list-filter-thm
LENGTH_LIST_OF_SET	!s. FINITE s ==> LENGTH (list_of_set s) = CARD s	link to proof	list-set-thm
LENGTH_MAP	!f l. LENGTH (MAP f l) = LENGTH l	link to proof	list-map-thm
LENGTH_NIL	LENGTH [] = 0	link to proof	list-length-def
LENGTH_REPLICATE	!x n. LENGTH (REPLICATE x n) = n	link to proof	list-replicate-thm
LENGTH_REVERSE	!l. LENGTH (REVERSE l) = LENGTH l	link to proof	list-reverse-thm
LENGTH_TL	!l. ~NULL l ==> LENGTH (TL l) = LENGTH l - 1	link to proof	list-length-thm
LET_ADD2	!m n p q. m <= p /\ n < q ==> m + n < p + q	link to proof	natural-add-thm
LET_ANTISYM	!m n. ~(m <= n /\ n < m)	link to proof	natural-order-thm
LET_CASES	!m n. m <= n \/ n < m	link to proof	natural-order-thm
LET_TRANS	!m n p. m <= n /\ n < p ==> m < p	link to proof	natural-order-thm
LE_0	!n. 0 <= n	link to proof	natural-order-thm
LE_ADD	!m n. m <= m + n	link to proof	natural-add-thm
LE_ADD2	!m n p q. m <= p /\ n <= q ==> m + n <= p + q	link to proof	natural-add-thm
LE_ADDR	!m n. n <= m + n	link to proof	natural-add-thm
LE_ADD_LCANCEL	!m n p. m + n <= m + p <=> n <= p	link to proof	natural-add-thm
LE_ADD_LCANCEL_0	!m n. m + n <= m <=> n = 0	link to proof	natural-add-thm
LE_ADD_RCANCEL	!m n p. n + m <= p + m <=> n <= p	link to proof	natural-add-thm
LE_ADD_RCANCEL_0	!m n. n + m <= m <=> n = 0	link to proof	natural-add-thm
LE_ANTISYM	!m n. m <= n /\ n <= m <=> m = n	link to proof	natural-order-thm
LE_CASES	!m n. m <= n \/ n <= m	link to proof	natural-order-thm
LE_EXISTS	!m n. m <= n <=> (?d. n = m + d)	link to proof	natural-add-thm
LE_EXP	!x m n. x EXP m <= x EXP n <=> (if x = 0 then m = 0 ==> n = 0 else x = 1 \/ m <= n)	link to proof	natural-exp-thm
LE_INDUCT	!p. (!m. p m m) /\ (!m n. m <= n /\ p m n ==> p m (SUC n)) ==> (!m n. m <= n ==> p m n)	link to proof	natural-add-thm
LE_LDIV	!a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n	link to proof	natural-div-thm
LE_LDIV_EQ	!a b n. ~(a = 0) ==> (b DIV a <= n <=> b < a * (n + 1))	link to proof	natural-div-thm
LE_LT	!m n. m <= n <=> m < n \/ m = n	link to proof	natural-order-thm
LE_MAX	!m n p. m <= MAX n p <=> m <= n \/ m <= p	link to proof	natural-order-min-max-thm
LE_MAX1	!m n. m <= MAX m n	link to proof	natural-order-min-max-thm
LE_MAX2	!m n. n <= MAX m n	link to proof	natural-order-min-max-thm
LE_MIN	!m n p. m <= MIN n p <=> m <= n /\ m <= p	link to proof	natural-order-min-max-thm
LE_MULT2	!m n p q. m <= n /\ p <= q ==> m * p <= n * q	link to proof	natural-mult-thm
LE_MULT_LCANCEL	!m n p. m * n <= m * p <=> m = 0 \/ n <= p	link to proof	natural-mult-thm
LE_MULT_RCANCEL	!m n p. m * p <= n * p <=> m <= n \/ p = 0	link to proof	natural-mult-thm
LE_RDIV_EQ	!a b n. ~(a = 0) ==> (n <= b DIV a <=> a * n <= b)	link to proof	natural-div-thm
LE_REFL	!n. n <= n	link to proof	natural-order-thm
LE_SQUARE_REFL	!n. n <= n * n	link to proof	natural-mult-thm
LE_SUC	!m n. SUC m <= SUC n <=> m <= n	link to proof	natural-order-thm
LE_SUC_LT	!m n. SUC m <= n <=> m < n	link to proof	natural-order-thm
LE_TRANS	!m n p. m <= n /\ n <= p ==> m <= p	link to proof	natural-order-thm
LE_ZERO	!m. m <= 0 <=> m = 0	link to proof	natural-order-def
LIST_OF_SET_PROPERTIES	!s. FINITE s ==> set_of_list (list_of_set s) = s /\ LENGTH (list_of_set s) = CARD s	link to proof	list-set-def
LTE_ADD2	!m n p q. m < p /\ n <= q ==> m + n < p + q	link to proof	natural-add-thm
LTE_ANTISYM	!m n. ~(m < n /\ n <= m)	link to proof	natural-order-thm
LTE_CASES	!m n. m < n \/ n <= m	link to proof	natural-order-thm
LTE_TRANS	!m n p. m < n /\ n <= p ==> m < p	link to proof	natural-order-thm
LT_0	!n. 0 < SUC n	link to proof	natural-order-thm
LT_ADD	!m n. m < m + n <=> 0 < n	link to proof	natural-add-thm
LT_ADD2	!m n p q. m < p /\ n < q ==> m + n < p + q	link to proof	natural-add-thm
LT_ADDR	!m n. n < m + n <=> 0 < m	link to proof	natural-add-thm
LT_ADD_LCANCEL	!m n p. m + n < m + p <=> n < p	link to proof	natural-add-thm
LT_ADD_LCANCEL_0	!m n. ~(m + n < m)	link to proof	natural-add-thm
LT_ADD_RCANCEL	!m n p. n + m < p + m <=> n < p	link to proof	natural-add-thm
LT_ADD_RCANCEL_0	!m n. ~(n + m < m)	link to proof	natural-add-thm
LT_ANTISYM	!m n. ~(m < n /\ n < m)	link to proof	natural-order-thm
LT_CASES	!m n. m < n \/ n < m \/ m = n	link to proof	natural-order-thm
LT_EXISTS	!m n. m < n <=> (?d. n = m + SUC d)	link to proof	natural-add-thm
LT_EXP	!x m n. x EXP m < x EXP n <=> 2 <= x /\ m < n \/ x = 0 /\ ~(m = 0) /\ n = 0	link to proof	natural-exp-thm
LT_IMP_LE	!m n. m < n ==> m <= n	link to proof	natural-order-thm
LT_IMP_NEQ	!m n. m < n ==> ~(m = n)	link to proof	natural-order-thm
LT_LDIV	!a b n. b < a * n ==> b DIV a < n	link to proof	natural-div-thm
LT_LDIV_EQ	!a b n. ~(a = 0) ==> (b DIV a < n <=> b < a * n)	link to proof	natural-div-thm
LT_LE	!m n. m < n <=> m <= n /\ ~(m = n)	link to proof	natural-order-thm
LT_LMULT	!m n p. ~(m = 0) /\ n < p ==> m * n < m * p	link to proof	natural-mult-thm
LT_MAX	!m n p. m < MAX n p <=> m < n \/ m < p	link to proof	natural-order-min-max-thm
LT_MIN	!m n p. m < MIN n p <=> m < n /\ m < p	link to proof	natural-order-min-max-thm
LT_MULT	!m n. 0 < m * n <=> 0 < m /\ 0 < n	link to proof	natural-mult-thm
LT_MULT2	!m n p q. m < n /\ p < q ==> m * p < n * q	link to proof	natural-mult-thm
LT_MULT_LCANCEL	!m n p. m * n < m * p <=> ~(m = 0) /\ n < p	link to proof	natural-mult-thm
LT_MULT_RCANCEL	!m n p. m * p < n * p <=> m < n /\ ~(p = 0)	link to proof	natural-mult-thm
LT_NZ	!n. 0 < n <=> ~(n = 0)	link to proof	natural-order-thm
LT_POW2_REFL	!n. n < 2 EXP n	link to proof	natural-exp-thm
LT_REFL	!n. ~(n < n)	link to proof	natural-order-thm
LT_SUC	!m n. SUC m < SUC n <=> m < n	link to proof	natural-order-thm
LT_SUC_LE	!m n. m < SUC n <=> m <= n	link to proof	natural-order-thm
LT_TRANS	!m n p. m < n /\ n < p ==> m < p	link to proof	natural-order-thm
LT_ZERO	!m. ~(m < 0)	link to proof	natural-order-def
MAP_APPEND	!f l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)	link to proof	list-map-thm
MAP_CONS	!f h t. MAP f (CONS h t) = CONS (f h) (MAP f t)	link to proof	list-map-def
MAP_EQ	!f g l. ALL (\x. f x = g x) l ==> MAP f l = MAP g l	link to proof	list-map-thm
MAP_EQ_NIL	!f l. MAP f l = [] <=> l = []	link to proof	list-map-thm
MAP_I	MAP I = I	link to proof	list-map-thm
MAP_ID	!l. MAP (\x. x) l = l	link to proof	list-map-thm
MAP_NIL	!f. MAP f [] = []	link to proof	list-map-def
MAP_REPLICATE	!f x n. MAP f (REPLICATE x n) = REPLICATE (f x) n	link to proof	list-replicate-thm
MAP_REVERSE	!f l. REVERSE (MAP f l) = MAP f (REVERSE l)	link to proof	list-reverse-thm
MAP_o	!f g l. MAP (f o g) l = MAP f (MAP g l)	link to proof	list-map-thm
MAP_o'	!f g. MAP f o MAP g = MAP (f o g)	link to proof	list-map-thm
MAX	!m n. MAX m n = (if m <= n then n else m)	link to proof	natural-order-min-max-def
MAX_ADD_LCANCEL	!m n p. MAX (m + n) (m + p) = m + MAX n p	link to proof	natural-add-thm
MAX_ADD_RCANCEL	!m n p. MAX (n + m) (p + m) = MAX n p + m	link to proof	natural-add-thm
MAX_COMM	!m n. MAX m n = MAX n m	link to proof	natural-order-min-max-thm
MAX_EQ_ZERO	!m n. MAX m n = 0 <=> m = 0 /\ n = 0	link to proof	natural-order-min-max-thm
MAX_L0	!n. MAX 0 n = n	link to proof	natural-order-min-max-thm
MAX_LE	!m n p. MAX n p <= m <=> n <= m /\ p <= m	link to proof	natural-order-min-max-thm
MAX_LT	!m n p. MAX n p < m <=> n < m /\ p < m	link to proof	natural-order-min-max-thm
MAX_R0	!n. MAX n 0 = n	link to proof	natural-order-min-max-thm
MAX_REFL	!n. MAX n n = n	link to proof	natural-order-min-max-thm
MAX_SUC	!m n. MAX (SUC m) (SUC n) = SUC (MAX m n)	link to proof	natural-order-min-max-thm
MEASURE	!m x y. MEASURE m x y <=> m x < m y	link to proof	relation-natural-def
MEASURE_LE	!m a b. (!y. MEASURE m y a ==> MEASURE m y b) <=> m a <= m b	link to proof	relation-natural-thm
MEMBER_NOT_EMPTY	!s. (?x. x IN s) <=> ~(s = {})	link to proof	set-thm
MEM_APPEND	!l1 l2 x. MEM x (APPEND l1 l2) <=> MEM x l1 \/ MEM x l2	link to proof	list-append-thm
MEM_APPEND_DECOMPOSE_LEFT	!x l. MEM x l <=> (?l1 l2. ~MEM x l1 /\ l = APPEND l1 (CONS x l2))	link to proof	list-append-thm
MEM_CONS	!x h t. MEM x (CONS h t) <=> x = h \/ MEM x t	link to proof	list-set-def
MEM_FILTER	!p l x. MEM x (FILTER p l) <=> MEM x l /\ p x	link to proof	list-filter-thm
MEM_LIST_OF_SET	!s. FINITE s ==> (!x. MEM x (list_of_set s) <=> x IN s)	link to proof	list-set-thm
MEM_MAP	!f l y. MEM y (MAP f l) <=> (?x. y = f x /\ MEM x l)	link to proof	list-map-thm
MEM_NIL	!x. ~MEM x []	link to proof	list-set-def
MEM_REPLICATE	!x n y. MEM y (REPLICATE x n) <=> y = x /\ ~(n = 0)	link to proof	list-replicate-thm
MEM_REVERSE	!l x. MEM x (REVERSE l) <=> MEM x l	link to proof	list-reverse-thm
MEM_SET_OF_LIST	!l x. MEM x l <=> x IN set_of_list l	link to proof	list-set-thm
MIN	!m n. MIN m n = (if m <= n then m else n)	link to proof	natural-order-min-max-def
MINIMAL	!p. (?n. p n) <=> p ((minimal) p) /\ (!m. m < (minimal) p ==> ~p m)	link to proof	natural-order-min-max-def
MINIMAL_EQ	!p n. p n /\ (!m. m < n ==> ~p m) ==> (minimal) p = n	link to proof	natural-order-min-max-thm
MINIMAL_T	(minimal n. T) = 0	link to proof	natural-order-min-max-thm
MIN_ADD_LCANCEL	!m n p. MIN (m + n) (m + p) = m + MIN n p	link to proof	natural-add-thm
MIN_ADD_RCANCEL	!m n p. MIN (n + m) (p + m) = MIN n p + m	link to proof	natural-add-thm
MIN_COMM	!m n. MIN m n = MIN n m	link to proof	natural-order-min-max-thm
MIN_L0	!n. MIN 0 n = 0	link to proof	natural-order-min-max-thm
MIN_LE	!m n p. MIN n p <= m <=> n <= m \/ p <= m	link to proof	natural-order-min-max-thm
MIN_LE1	!m n. MIN m n <= m	link to proof	natural-order-min-max-thm
MIN_LE2	!m n. MIN m n <= n	link to proof	natural-order-min-max-thm
MIN_LT	!m n p. MIN n p < m <=> n < m \/ p < m	link to proof	natural-order-min-max-thm
MIN_R0	!n. MIN n 0 = 0	link to proof	natural-order-min-max-thm
MIN_REFL	!n. MIN n n = n	link to proof	natural-order-min-max-thm
MIN_SUC	!m n. MIN (SUC m) (SUC n) = SUC (MIN m n)	link to proof	natural-order-min-max-thm
MOD_0	!n. ~(n = 0) ==> 0 MOD n = 0	link to proof	natural-div-thm
MOD_1	!n. n MOD 1 = 0	link to proof	natural-div-thm
MOD_ADD_MOD'	!n a b. ~(n = 0) ==> (a MOD n + b MOD n) MOD n = (a + b) MOD n	link to proof	natural-div-thm
MOD_EQ	!m n p q. m = n + q * p ==> m MOD p = n MOD p	link to proof	natural-div-thm
MOD_EQ_0	!m n. ~(n = 0) ==> (m MOD n = 0 <=> (?q. m = q * n))	link to proof	natural-div-thm
MOD_EXISTS	!m n. (?q. m = n * q) <=> (if n = 0 then m = 0 else m MOD n = 0)	link to proof	natural-div-thm
MOD_EXP_MOD'	!n m p. ~(n = 0) ==> (m MOD n) EXP p MOD n = m EXP p MOD n	link to proof	natural-exp-thm
MOD_LE	!m n. ~(n = 0) ==> m MOD n <= m	link to proof	natural-div-thm
MOD_LT	!m n. m < n ==> m MOD n = m	link to proof	natural-div-thm
MOD_MOD	!m n p. ~(n * p = 0) ==> m MOD (n * p) MOD n = m MOD n	link to proof	natural-div-thm
MOD_MOD_EXP_MIN	!x p m n. ~(p = 0) ==> x MOD p EXP m MOD p EXP n = x MOD p EXP MIN m n	link to proof	natural-exp-thm
MOD_MOD_REFL'	!n m. ~(n = 0) ==> m MOD n MOD n = m MOD n	link to proof	natural-div-thm
MOD_MULT	!m n. ~(m = 0) ==> (m * n) MOD m = 0	link to proof	natural-div-thm
MOD_MULT2	!m n p. ~(m * p = 0) ==> (m * n) MOD (m * p) = m * n MOD p	link to proof	natural-div-thm
MOD_MULT_ADD	!m n p. (m * n + p) MOD n = p MOD n	link to proof	natural-div-thm
MOD_MULT_LMOD'	!n m p. ~(n = 0) ==> (m MOD n * p) MOD n = (m * p) MOD n	link to proof	natural-div-thm
MOD_MULT_MOD2'	!n m p. ~(n = 0) ==> (m MOD n * p MOD n) MOD n = (m * p) MOD n	link to proof	natural-div-thm
MOD_MULT_RMOD'	!n m p. ~(n = 0) ==> (m * p MOD n) MOD n = (m * p) MOD n	link to proof	natural-div-thm
MOD_REFL	!n. ~(n = 0) ==> n MOD n = 0	link to proof	natural-div-thm
MOD_UNIQ	!m n q r. m = q * n + r /\ r < n ==> m MOD n = r	link to proof	natural-div-thm
MONO_AND	!p1 p2 q1 q2. (p1 ==> p2) /\ (q1 ==> q2) ==> p1 /\ q1 ==> p2 /\ q2	link to proof	bool-int
MONO_COND	!b p q r s. (p ==> q) /\ (r ==> s) ==> (if b then p else r) ==> (if b then q else s)	link to proof	bool-class
MONO_EXISTS	!p q. (!x. p x ==> q x) ==> (?x. p x) ==> (?x. q x)	link to proof	bool-int
MONO_FORALL	!p q. (!x. p x ==> q x) ==> (!x. p x) ==> (!x. q x)	link to proof	bool-int
MONO_IMP	!p1 p2 q1 q2. (p2 ==> p1) /\ (q1 ==> q2) ==> (p1 ==> q1) ==> p2 ==> q2	link to proof	bool-int
MONO_NOT	!p q. (q ==> p) ==> ~p ==> ~q	link to proof	bool-int
MONO_OR	!p1 p2 q1 q2. (p1 ==> p2) /\ (q1 ==> q2) ==> p1 \/ q1 ==> p2 \/ q2	link to proof	bool-int
MULTL_EQ	!m n. m * n = m <=> m = 0 \/ n = 1	link to proof	natural-mult-thm
MULTR_EQ	!m n. n * m = m <=> m = 0 \/ n = 1	link to proof	natural-mult-thm
MULT_0	!m. m * 0 = 0	link to proof	natural-mult-thm
MULT_1	!m. m * 1 = m	link to proof	natural-mult-thm
MULT_2	!n. 2 * n = n + n	link to proof	natural-mult-thm
MULT_ASSOC	!m n p. m * n * p = (m * n) * p	link to proof	natural-mult-thm
MULT_DIV_LE	!m n p. ~(p = 0) ==> m * n DIV p <= (m * n) DIV p	link to proof	natural-div-thm
MULT_EQ_0	!m n. m * n = 0 <=> m = 0 \/ n = 0	link to proof	natural-mult-thm
MULT_EQ_1	!m n. m * n = 1 <=> m = 1 /\ n = 1	link to proof	natural-mult-thm
MULT_EXP	!p m n. (m * n) EXP p = m EXP p * n EXP p	link to proof	natural-exp-thm
MULT_LASSOC	!m n p. m * n * p = n * m * p	link to proof	natural-mult-thm
MULT_SUC	!m n. m * SUC n = m + m * n	link to proof	natural-mult-thm
MULT_SYM	!m n. m * n = n * m	link to proof	natural-mult-thm
NIL_APPEND	!l. APPEND [] l = l	link to proof	list-append-def
NOT_ALL	!p l. ~ALL p l <=> EX (\x. ~p x) l	link to proof	list-set-thm
NOT_ALL_NOT	!p l. ~ALL (\x. ~p x) l <=> EX p l	link to proof	list-set-thm
NOT_AND_THM	!t1 t2. ~(t1 /\ t2) <=> ~t1 \/ ~t2	link to proof	bool-class
NOT_CONS_NIL	!h t. ~(CONS h t = [])	link to proof	list-thm
NOT_DEF	(~) = (\p. p ==> F)	link to proof	bool-def
NOT_EQUAL_SETS	!s t. ~(s = t) <=> (?x. x IN t <=> ~(x IN s))	link to proof	set-thm
NOT_EVEN	!n. ~EVEN n <=> ODD n	link to proof	natural-div-thm
NOT_EX	!p l. ~EX p l <=> ALL (\x. ~p x) l	link to proof	list-set-thm
NOT_EXISTS_THM	!p. ~(?x. p x) <=> (!x. ~p x)	link to proof	bool-class
NOT_EX_NOT	!p l. ~EX (\x. ~p x) l <=> ALL p l	link to proof	list-set-thm
NOT_FALSE_THM	~F <=> T	link to proof	bool-int
NOT_FORALL_THM	!p. ~(!x. p x) <=> (?x. ~p x)	link to proof	bool-class
NOT_IFF_THM	!t1 t2. (~t1 <=> ~t2) <=> t1 <=> t2	link to proof	bool-class
NOT_IMP	!t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2	link to proof	bool-class
NOT_INSERT_EMPTY	!x s. ~(x INSERT s = {})	link to proof	set-thm
NOT_IN_EMPTY	!x. ~(x IN {})	link to proof	set-thm
NOT_LE	!m n. ~(m <= n) <=> n < m	link to proof	natural-order-thm
NOT_LT	!m n. ~(m < n) <=> n <= m	link to proof	natural-order-thm
NOT_NOT_THM	!t. ~ ~t <=> t	link to proof	bool-class
NOT_ODD	!n. ~ODD n <=> EVEN n	link to proof	natural-div-thm
NOT_OR_THM	!t1 t2. ~(t1 \/ t2) <=> ~t1 /\ ~t2	link to proof	bool-class
NOT_PSUBSET_EMPTY	!s. ~(s PSUBSET {})	link to proof	set-thm
NOT_TRUE_THM	~T <=> F	link to proof	bool-int
NOT_UNIV_PSUBSET	!s. ~(UNIV PSUBSET s)	link to proof	set-thm
NO_NAME	!e f. ?!fn. fn _0 = e /\ (!n. fn (SUC n) = f (fn n) n)	link to proof	natural-thm
NO_NAME	!p. p _0 /\ (!n. p n ==> p (SUC n)) ==> (!n. p n)	link to proof	natural-def
NO_NAME	!m n. m < SUC n <=> m = n \/ m < n	link to proof	natural-order-def
NO_NAME	!m n. m <= SUC n <=> m = SUC n \/ m <= n	link to proof	natural-order-def
NO_NAME	!n. ~(SUC n = _0)	link to proof	natural-def
NULL_APPEND	!l1 l2. NULL (APPEND l1 l2) <=> NULL l1 /\ NULL l2	link to proof	list-append-thm
NULL_CONS	!h t. ~NULL (CONS h t)	link to proof	list-dest-def
NULL_EQ_NIL	!l. NULL l <=> l = []	link to proof	list-dest-thm
NULL_LENGTH	!l. LENGTH l = 0 <=> NULL l	link to proof	list-length-thm
NULL_MAP	!f l. NULL (MAP f l) <=> NULL l	link to proof	list-map-thm
NULL_NIL	NULL []	link to proof	list-dest-def
NULL_REPLICATE	!x n. NULL (REPLICATE x n) <=> n = 0	link to proof	list-replicate-thm
NULL_SET_OF_LIST	!l. set_of_list l = {} <=> NULL l	link to proof	list-set-thm
ODD_ADD	!m n. ODD (m + n) <=> ~(ODD m <=> ODD n)	link to proof	natural-div-thm
ODD_DOUBLE	!n. ODD (SUC (2 * n))	link to proof	natural-div-thm
ODD_EXISTS	!n. ODD n <=> (?m. n = SUC (2 * m))	link to proof	natural-div-thm
ODD_EXP	!m n. ODD (m EXP n) <=> ODD m \/ n = 0	link to proof	natural-exp-thm
ODD_MOD	!n. ODD n <=> n MOD 2 = 1	link to proof	natural-div-thm
ODD_MULT	!m n. ODD (m * n) <=> ODD m /\ ODD n	link to proof	natural-div-thm
ODD_SUB	!m n. n <= m ==> (ODD (m - n) <=> ~(ODD m <=> ODD n))	link to proof	natural-div-thm
ODD_SUC	!n. ODD (SUC n) <=> ~ODD n	link to proof	natural-div-def
ODD_ZERO	~ODD 0	link to proof	natural-div-def
ONE_MULT	!m. 1 * m = m	link to proof	natural-mult-thm
ONE_ONE	!f. ONE_ONE f <=> (!x1 x2. f x1 = f x2 ==> x1 = x2)	link to proof	function-def
ONTO	!f. ONTO f <=> (!y. ?x. y = f x)	link to proof	function-def
OR_DEF	(\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r)	link to proof	bool-def
OR_EXISTS_THM	!p q. (?x. p x) \/ (?x. q x) <=> (?x. p x \/ q x)	link to proof	bool-int
OR_FALSE_THM	!t. t \/ F <=> t	link to proof	bool-int
OR_IMP_DISTRIB	!p q r. p \/ q ==> r <=> (p ==> r) /\ (q ==> r)	link to proof	bool-int
OR_TRUE_THM	!t. t \/ T <=> T	link to proof	bool-int
OUTL	!a. OUTL (INL a) = a	link to proof	sum-def
OUTR	!b. OUTR (INR b) = b	link to proof	sum-def
O_I	!f. f o I = f	link to proof	function-thm
PAIR	!x. FST x,SND x = x	link to proof	pair-thm
PAIRED_ETA_THM	(!f. (\(a,b). f (a,b)) = f) /\ (!f. (\(a,b,c). f (a,b,c)) = f) /\ (!f. (\(a,b,c,d). f (a,b,c,d)) = f)	link to proof	pair-thm
PAIR_EQ	!a b a' b'. a,b = a',b' <=> a = a' /\ b = b'	link to proof	pair-def
PAIR_SURJECTIVE	!x. ?a b. x = a,b	link to proof	pair-def
PRE	!n. PRE (SUC n) = n	link to proof	natural-dest-def
PSUBSET	!s t. s PSUBSET t <=> s SUBSET t /\ ~(s = t)	link to proof	set-def
PSUBSET_ALT	!s t. s PSUBSET t <=> s SUBSET t /\ (?a. a IN t /\ ~(a IN s))	link to proof	set-thm
PSUBSET_INSERT_SUBSET	!s t. s PSUBSET t <=> (?x. ~(x IN s) /\ x INSERT s SUBSET t)	link to proof	set-thm
PSUBSET_IRREFL	!s. ~(s PSUBSET s)	link to proof	set-thm
PSUBSET_NOT_SUBSET	!s t. s PSUBSET t <=> s SUBSET t /\ ~(t SUBSET s)	link to proof	set-thm
PSUBSET_SUBSET	!s t. s PSUBSET t ==> s SUBSET t	link to proof	set-thm
PSUBSET_SUBSET_TRANS	!s t u. s PSUBSET t /\ t SUBSET u ==> s PSUBSET u	link to proof	set-thm
PSUBSET_TRANS	!s t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u	link to proof	set-thm
PSUBSET_UNIV	!s. s PSUBSET UNIV <=> (?x. ~(x IN s))	link to proof	set-thm
REPLICATE_0	!x. REPLICATE x 0 = []	link to proof	list-replicate-def
REPLICATE_ADD	!x m n. REPLICATE x (m + n) = APPEND (REPLICATE x m) (REPLICATE x n)	link to proof	list-replicate-thm
REPLICATE_SUC	!x n. REPLICATE x (SUC n) = CONS x (REPLICATE x n)	link to proof	list-replicate-def
REST	!s. REST s = s DELETE CHOICE s	link to proof	set-def
REVERSE_APPEND	!l1 l2. REVERSE (APPEND l1 l2) = APPEND (REVERSE l2) (REVERSE l1)	link to proof	list-reverse-thm
REVERSE_CONS	!h t. REVERSE (CONS h t) = APPEND (REVERSE t) [h]	link to proof	list-reverse-def
REVERSE_NIL	REVERSE [] = []	link to proof	list-reverse-def
REVERSE_REVERSE	!l. REVERSE (REVERSE l) = l	link to proof	list-reverse-thm
RIGHT_ADD_DISTRIB	!m n p. (m + n) * p = m * p + n * p	link to proof	natural-mult-thm
RIGHT_AND_DISTRIB	!p q r. p /\ q \/ r <=> (p \/ r) /\ (q \/ r)	link to proof	bool-int
RIGHT_AND_EXISTS_THM	!p q. p /\ (?x. q x) <=> (?x. p /\ q x)	link to proof	bool-int
RIGHT_AND_FORALL_THM	!p q. p /\ (!x. q x) <=> (!x. p /\ q x)	link to proof	bool-int
RIGHT_EXISTS_AND_THM	!p q. (?x. p /\ q x) <=> p /\ (?x. q x)	link to proof	bool-int
RIGHT_EXISTS_IMP_THM	!p q. (?x. p ==> q x) <=> p ==> (?x. q x)	link to proof	bool-class
RIGHT_FORALL_IMP_THM	!p q. (!x. p ==> q x) <=> p ==> (!x. q x)	link to proof	bool-int
RIGHT_FORALL_OR_THM	!p q. (!x. p \/ q x) <=> p \/ (!x. q x)	link to proof	bool-class
RIGHT_IMP_EXISTS_THM	!p q. p ==> (?x. q x) <=> (?x. p ==> q x)	link to proof	bool-class
RIGHT_IMP_FORALL_THM	!p q. p ==> (!x. q x) <=> (!x. p ==> q x)	link to proof	bool-int
RIGHT_INTER_DISTRIB	!s t u. s INTER t UNION u = (s UNION u) INTER (t UNION u)	link to proof	set-thm
RIGHT_INTER_SUBSET	!s t. t INTER s SUBSET s	link to proof	set-thm
RIGHT_OR_DISTRIB	!p q r. (p \/ q) /\ r <=> p /\ r \/ q /\ r	link to proof	bool-int
RIGHT_OR_EXISTS_THM	!p q. p \/ (?x. q x) <=> (?x. p \/ q x)	link to proof	bool-int
RIGHT_OR_FORALL_THM	!p q. p \/ (!x. q x) <=> (!x. p \/ q x)	link to proof	bool-class
RIGHT_SUB_DISTRIB	!m n p. n <= m ==> (m - n) * p = m * p - n * p	link to proof	natural-mult-thm
RIGHT_UNION_DISTRIB	!s t u. (s UNION t) INTER u = s INTER u UNION t INTER u	link to proof	set-thm
RIGHT_UNION_INTERS	!s t. INTERS s UNION t = INTERS {x UNION t | x IN s}	link to proof	set-thm
SELECT_AX	!p x. p x ==> p ((@) p)	link to proof	axiom-choice
SELECT_REFL	!x. (@y. y = x) = x	link to proof	bool-class
SELECT_UNIQUE	!p x. (!y. p y <=> y = x) ==> (@) p = x	link to proof	bool-class
SET_CASES	!s. s = {} \/ (?x t. s = x INSERT t /\ ~(x IN t))	link to proof	set-thm
SET_OF_LIST_APPEND	!l1 l2. set_of_list (APPEND l1 l2) = set_of_list l1 UNION set_of_list l2	link to proof	list-append-thm
SET_OF_LIST_EQ_EMPTY	!l. set_of_list l = {} <=> l = []	link to proof	list-set-thm
SET_OF_LIST_FILTER	!p l. set_of_list (FILTER p l) = set_of_list l DIFF {x | ~p x}	link to proof	list-filter-thm
SET_OF_LIST_MAP	!f l. set_of_list (MAP f l) = IMAGE f (set_of_list l)	link to proof	list-map-thm
SET_OF_LIST_OF_SET	!s. FINITE s ==> set_of_list (list_of_set s) = s	link to proof	list-set-thm
SET_OF_LIST_REPLICATE	!x n. set_of_list (REPLICATE x n) = (if n = 0 then {} else {x})	link to proof	list-replicate-thm
SET_OF_LIST_REVERSE	!l. set_of_list (REVERSE l) = set_of_list l	link to proof	list-reverse-thm
SET_PAIR_THM	!p. {x | p x} = {a,b | p (a,b)}	link to proof	set-thm
SET_PROVE_CASES	!p. p {} /\ (!a s. ~(a IN s) ==> p (a INSERT s)) ==> (!s. p s)	link to proof	set-thm
SIMPLE_IMAGE	!f s. {f x | x IN s} = IMAGE f s	link to proof	set-thm
SIMPLE_IMAGE_GEN	!p f. {f x | p x} = IMAGE f {x | p x}	link to proof	set-thm
SING	!s. SING s <=> (?x. s = {x})	link to proof	set-def
SING_DISJOINT	!x s. DISJOINT {x} s <=> ~(x IN s)	link to proof	set-thm
SING_GSPEC1	!a. {x | x = a} = {a}	link to proof	set-thm
SING_SUBSET	!s x. {x} SUBSET s <=> x IN s	link to proof	set-thm
SKOLEM_THM	!r. (!x. ?y. r x y) <=> (?f. !x. r x (f x))	link to proof	bool-class
SKOLEM_THM_GEN	!p r. (!x. p x ==> (?y. r x y)) <=> (?f. !x. p x ==> r x (f x))	link to proof	bool-class
SKX_EQ_I	!x. S K x = I	link to proof	function-thm
SND	!a b. SND (a,b) = b	link to proof	pair-def
SUB1	!n. ~(n = 0) ==> PRE n = n - 1	link to proof	natural-add-sub-thm
SUBSET	!s t. s SUBSET t <=> (!x. x IN s ==> x IN t)	link to proof	set-def
SUBSET_ANTISYM	!s t. s SUBSET t /\ t SUBSET s ==> s = t	link to proof	set-thm
SUBSET_ANTISYM_EQ	!s t. s SUBSET t /\ t SUBSET s <=> s = t	link to proof	set-thm
SUBSET_CARD_EQ	!s t. FINITE t /\ s SUBSET t ==> (CARD s = CARD t <=> s = t)	link to proof	set-size-thm
SUBSET_DELETE	!x s t. s SUBSET t DELETE x <=> s SUBSET t /\ ~(x IN s)	link to proof	set-thm
SUBSET_DIFF	!s t u. s SUBSET t DIFF u <=> s SUBSET t /\ DISJOINT s u	link to proof	set-thm
SUBSET_DIFF_UNION	!s t u. s SUBSET t UNION u <=> s DIFF t SUBSET u	link to proof	set-thm
SUBSET_EMPTY	!s. s SUBSET {} <=> s = {}	link to proof	set-thm
SUBSET_IMAGE	!f s t. s SUBSET IMAGE f t <=> (?u. u SUBSET t /\ s = IMAGE f u)	link to proof	set-thm
SUBSET_IMAGE_INJ	!f s t. s SUBSET IMAGE f t <=> (?u. u SUBSET t /\ (!x y. x IN u /\ y IN u /\ f x = f y ==> x = y) /\ s = IMAGE f u)	link to proof	set-thm
SUBSET_INSERT	!x s. ~(x IN s) ==> (!t. s SUBSET x INSERT t <=> s SUBSET t)	link to proof	set-thm
SUBSET_INSERT_DELETE	!x s t. s SUBSET x INSERT t <=> s DELETE x SUBSET t	link to proof	set-thm
SUBSET_INSERT_IMP	!s t x. s SUBSET t ==> s SUBSET x INSERT t	link to proof	set-thm
SUBSET_INTER	!s t u. s SUBSET t INTER u <=> s SUBSET t /\ s SUBSET u	link to proof	set-thm
SUBSET_INTERS	!t u. t SUBSET INTERS u <=> (!s. s IN u ==> t SUBSET s)	link to proof	set-thm
SUBSET_INTER_ABSORPTION	!s t. s SUBSET t <=> s INTER t = s	link to proof	set-thm
SUBSET_LEFT_UNION	!s t. s SUBSET s UNION t	link to proof	set-thm
SUBSET_PSUBSET_TRANS	!s t u. s SUBSET t /\ t PSUBSET u ==> s PSUBSET u	link to proof	set-thm
SUBSET_REFL	!s. s SUBSET s	link to proof	set-thm
SUBSET_RESTRICT	!s p. {x | x IN s /\ p x} SUBSET s	link to proof	set-thm
SUBSET_RIGHT_UNION	!s t. s SUBSET t UNION s	link to proof	set-thm
SUBSET_SING	!s x. s SUBSET {x} <=> s = {} \/ s = {x}	link to proof	set-thm
SUBSET_TRANS	!s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u	link to proof	set-thm
SUBSET_UNIONS	!f g. f SUBSET g ==> UNIONS f SUBSET UNIONS g	link to proof	set-thm
SUBSET_UNION_ABSORPTION	!s t. s SUBSET t <=> s UNION t = t	link to proof	set-thm
SUBSET_UNION_DIFF	!s t u. s SUBSET t UNION u <=> s DIFF u SUBSET t	link to proof	set-thm
SUBSET_UNIV	!s. s SUBSET UNIV	link to proof	set-thm
SUB_0	!m. m - 0 = m	link to proof	natural-add-sub-thm
SUB_ADD	!m n. n <= m ==> m - n + n = m	link to proof	natural-add-sub-thm
SUB_ADD2	!m n. n <= m ==> n + m - n = m	link to proof	natural-add-sub-thm
SUB_ADD_LCANCEL	!m n p. p <= n ==> (m + n) - (m + p) = n - p	link to proof	natural-add-sub-thm
SUB_ADD_RCANCEL	!m n p. n <= m ==> (m + p) - (n + p) = m - n	link to proof	natural-add-sub-thm
SUB_EQ_0	!m n. n <= m ==> (m - n = 0 <=> m = n)	link to proof	natural-add-sub-thm
SUB_PRESUC	!m n. n <= m ==> PRE (SUC m - n) = m - n	link to proof	natural-add-sub-thm
SUB_REFL	!n. n - n = 0	link to proof	natural-add-sub-thm
SUB_SUB	!m n p. n + p <= m ==> m - (n + p) = m - n - p	link to proof	natural-add-sub-thm
SUB_SUC	!m n. n <= m ==> SUC m - SUC n = m - n	link to proof	natural-add-sub-thm
SUB_SUC_CANCEL	!m n. n < m ==> SUC (m - SUC n) = m - n	link to proof	natural-add-sub-thm
SUB_SUC_PRE	!m n. n < m ==> m - SUC n = PRE (m - n)	link to proof	natural-add-sub-thm
SUC_ADD	!m n. SUC m + n = SUC (m + n)	link to proof	natural-add-def
SUC_INJ	!m n. SUC m = SUC n <=> m = n	link to proof	natural-def
SUC_INJ_MOD	!n a b. ~(n = 0) ==> (SUC a MOD n = SUC b MOD n <=> a MOD n = b MOD n)	link to proof	natural-div-thm
SUC_LE	!n. n <= SUC n	link to proof	natural-order-thm
SUC_LT	!n. n < SUC n	link to proof	natural-order-thm
SUC_MULT	!m n. SUC m * n = m * n + n	link to proof	natural-mult-def
SUC_SUB	!m n. n <= m ==> SUC (m - n) = SUC m - n	link to proof	natural-add-sub-thm
SUC_SUB1	!n. SUC n - 1 = n	link to proof	natural-add-sub-thm
SURJ	!s t. SURJ s t = {f | (!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> (?y. y IN s /\ f y = x))}	link to proof	set-def
SURJECTIVE_EXISTS_THM	!f. (!y. ?x. f x = y) <=> (!p. (?x. p (f x)) <=> (?y. p y))	link to proof	function-thm
SURJECTIVE_FORALL_THM	!f. (!y. ?x. f x = y) <=> (!p. (!x. p (f x)) <=> (!y. p y))	link to proof	function-thm
SURJECTIVE_IFF_INJECTIVE	!s f. FINITE s /\ IMAGE f s SUBSET s ==> ((!y. y IN s ==> (?x. x IN s /\ f x = y)) <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))	link to proof	set-size-thm
SURJECTIVE_IFF_INJECTIVE_GEN	!s t f. FINITE s /\ FINITE t /\ CARD s = CARD t /\ IMAGE f s SUBSET t ==> ((!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y))	link to proof	set-size-thm
SURJECTIVE_IMAGE	!f. (!t. ?s. IMAGE f s = t) <=> (!y. ?x. f x = y)	link to proof	set-thm
SURJECTIVE_IMAGE_EQ	!f s t. (!y. y IN t ==> (?x. f x = y)) /\ (!x. f x IN t <=> x IN s) ==> IMAGE f s = t	link to proof	set-thm
SURJECTIVE_IMAGE_THM	!f. (!y. ?x. f x = y) <=> (!p. IMAGE f {x | p (f x)} = {x | p x})	link to proof	set-thm
SURJECTIVE_MAP	!f. (!ys. ?xs. MAP f xs = ys) <=> (!y. ?x. f x = y)	link to proof	list-map-thm
SURJECTIVE_ON_IMAGE	!f u v. (!t. t SUBSET v ==> (?s. s SUBSET u /\ IMAGE f s = t)) <=> (!y. y IN v ==> (?x. x IN u /\ f x = y))	link to proof	set-thm
SURJECTIVE_ON_RIGHT_INVERSE	!f s t. (!y. y IN t ==> (?x. x IN s /\ f x = y)) <=> (?g. !y. y IN t ==> g y IN s /\ f (g y) = y)	link to proof	set-thm
SURJECTIVE_RIGHT_INVERSE	!f. (!y. ?x. f x = y) <=> (?g. !y. f (g y) = y)	link to proof	set-thm
SWAP_EXISTS_THM	!p. (?x y. p x y) <=> (?y x. p x y)	link to proof	bool-int
SWAP_FORALL_THM	!p. (!x y. p x y) <=> (!y x. p x y)	link to proof	bool-int
S_DEF	S = (\f g x. f x (g x))	link to proof	function-def
S_THM	!f g x. S f g x = f x (g x)	link to proof	function-thm
TL	!h t. TL (CONS h t) = t	link to proof	list-dest-def
TRIV_AND_EXISTS_THM	!p q. (?x. p) /\ (?x. q) <=> (?x. p /\ q)	link to proof	bool-int
TRIV_EXISTS_AND_THM	!p q. (?x. p /\ q) <=> (?x. p) /\ (?x. q)	link to proof	bool-int
TRIV_EXISTS_IMP_THM	!p q. (?x. p ==> q) <=> (!x. p) ==> (?x. q)	link to proof	bool-int
TRIV_FORALL_IMP_THM	!p q. (!x. p ==> q) <=> (?x. p) ==> (!x. q)	link to proof	bool-int
TRIV_FORALL_OR_THM	!p q. (!x. p \/ q) <=> (!x. p) \/ (!x. q)	link to proof	bool-int
TRIV_OR_FORALL_THM	!p q. (!x. p) \/ (!x. q) <=> (!x. p \/ q)	link to proof	bool-int
TRUE_AND_THM	!t. T /\ t <=> t	link to proof	bool-int
TRUE_EQ_THM	!t. (T <=> t) <=> t	link to proof	bool-int
TRUE_IMP_THM	!t. T ==> t <=> t	link to proof	bool-int
TRUE_OR_THM	!t. T \/ t <=> T	link to proof	bool-int
TRUTH	T	link to proof	bool-int
T_DEF	T <=> (\p. p) = (\p. p)	link to proof	bool-def
UNION	!s t. s UNION t = {x | x IN s \/ x IN t}	link to proof	set-def
UNIONS	!s. UNIONS s = {x | ?u. u IN s /\ x IN u}	link to proof	set-def
UNIONS_0	UNIONS {} = {}	link to proof	set-thm
UNIONS_1	!s. UNIONS {s} = s	link to proof	set-thm
UNIONS_2	!s t. UNIONS {s, t} = s UNION t	link to proof	set-thm
UNIONS_DIFF	!s t. UNIONS s DIFF t = UNIONS {x DIFF t | x IN s}	link to proof	set-thm
UNIONS_GSPEC1	!p f. UNIONS {f x | p x} = {a | ?x. p x /\ a IN f x}	link to proof	set-thm
UNIONS_GSPEC2	!p f. UNIONS {f x y | p x y} = {a | ?x y. p x y /\ a IN f x y}	link to proof	set-thm
UNIONS_GSPEC3	!p f. UNIONS {f x y z | p x y z} = {a | ?x y z. p x y z /\ a IN f x y z}	link to proof	set-thm
UNIONS_IMAGE	!f s. UNIONS (IMAGE f s) = {y | ?x. x IN s /\ y IN f x}	link to proof	set-thm
UNIONS_INSERT	!s u. UNIONS (s INSERT u) = s UNION UNIONS u	link to proof	set-thm
UNIONS_INTER	!s t. UNIONS s INTER t = UNIONS {x INTER t | x IN s}	link to proof	set-thm
UNIONS_INTERS	!s. UNIONS s = UNIV DIFF INTERS {UNIV DIFF t | t IN s}	link to proof	set-thm
UNIONS_MAXIMAL_SETS	!f. FINITE f ==> UNIONS {t | t IN f /\ (!u. u IN f ==> ~(t PSUBSET u))} = UNIONS f	link to proof	set-finite-thm
UNIONS_MONO	!s t. (!x. x IN s ==> (?y. y IN t /\ x SUBSET y)) ==> UNIONS s SUBSET UNIONS t	link to proof	set-thm
UNIONS_OVER_INTERS	!f s. UNIONS {INTERS (f x) | x IN s} = INTERS {UNIONS {g x | x IN s} | g | !x. x IN s ==> g x IN f x}	link to proof	set-thm
UNIONS_SUBSET	!f t. UNIONS f SUBSET t <=> (!s. s IN f ==> s SUBSET t)	link to proof	set-thm
UNIONS_UNION	!s t. UNIONS (s UNION t) = UNIONS s UNION UNIONS t	link to proof	set-thm
UNION_ACI	!p q r. p UNION q = q UNION p /\ (p UNION q) UNION r = p UNION q UNION r /\ p UNION q UNION r = q UNION p UNION r /\ p UNION p = p /\ p UNION p UNION q = p UNION q	link to proof	set-thm
UNION_ASSOC	!s t u. (s UNION t) UNION u = s UNION t UNION u	link to proof	set-thm
UNION_COMM	!s t. s UNION t = t UNION s	link to proof	set-thm
UNION_DIFF_CANCEL	!s t. t UNION s DIFF t = t UNION s	link to proof	set-thm
UNION_DIFF_SUBSET	!s t. s UNION t DIFF s = t <=> s SUBSET t	link to proof	set-thm
UNION_IDEMPOT	!s. s UNION s = s	link to proof	set-thm
UNION_LEFT_EMPTY	!s. {} UNION s = s	link to proof	set-thm
UNION_LEFT_UNIV	!s. UNIV UNION s = UNIV	link to proof	set-thm
UNION_RIGHT_EMPTY	!s. s UNION {} = s	link to proof	set-thm
UNION_RIGHT_UNIV	!s. s UNION UNIV = UNIV	link to proof	set-thm
UNION_SUBSET	!s t u. s UNION t SUBSET u <=> s SUBSET u /\ t SUBSET u	link to proof	set-thm
UNIQUE_SKOLEM_ALT	!p. (!x. ?!y. p x y) <=> (?f. !x y. p x y <=> f x = y)	link to proof	bool-class
UNIQUE_SKOLEM_THM	!p. (!x. ?!y. p x y) <=> (?!f. !x. p x (f x))	link to proof	bool-class
UNIV	UNIV = {x | T}	link to proof	set-def
UNIV_GSPEC	GSPEC (\x. T) = UNIV	link to proof	set-thm
UNIV_INTERS	!s. INTERS s = UNIV <=> (!t. t IN s ==> t = UNIV)	link to proof	set-thm
UNIV_NOT_EMPTY	~(UNIV = {})	link to proof	set-thm
UNIV_SUBSET	!s. UNIV SUBSET s <=> s = UNIV	link to proof	set-thm
UNWIND_THM1	!p a. (?x. a = x /\ p x) <=> p a	link to proof	bool-int
UNWIND_THM2	!p a. (?x. x = a /\ p x) <=> p a	link to proof	bool-int
WF	!r. WF r <=> (!p. (?x. p x) ==> (?x. p x /\ (!y. r y x ==> ~p y)))	link to proof	relation-well-founded-def
WF_DCHAIN	!r. WF r <=> ~(?f. !n. r (f (SUC n)) (f n))	link to proof	relation-natural-thm
WF_EQ	!r. WF r <=> (!p. (?x. p x) <=> (?x. p x /\ (!y. r y x ==> ~p y)))	link to proof	relation-well-founded-thm
WF_EREC	!r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?!f. !x. f x = h f x))	link to proof	relation-natural-thm
WF_FINITE	!r. (!x. ~r x x) /\ (!x y z. r x y /\ r y z ==> r x z) /\ (!x. FINITE {y | r y x}) ==> WF r	link to proof	relation-natural-thm
WF_IND	!r. WF r <=> (!p. (!x. (!y. r y x ==> p y) ==> p x) ==> (!x. p x))	link to proof	relation-well-founded-thm
WF_LEX	!r s. WF r /\ WF s ==> WF (\(x1,y1) (x2,y2). r x1 x2 \/ x1 = x2 /\ s y1 y2)	link to proof	relation-well-founded-thm
WF_LEX_DEPENDENT	!r s. WF r /\ (!a. WF (s a)) ==> WF (\(x1,y1) (x2,y2). r x1 x2 \/ x1 = x2 /\ s x1 y1 y2)	link to proof	relation-well-founded-thm
WF_MEASURE	!m. WF (MEASURE m)	link to proof	relation-natural-thm
WF_MEASURE_GEN	!r m. WF r ==> WF (\x y. r (m x) (m y))	link to proof	relation-well-founded-thm
WF_POINTWISE	!r s. WF r /\ WF s ==> WF (\(x1,y1) (x2,y2). r x1 x2 /\ s y1 y2)	link to proof	relation-well-founded-thm
WF_REC	!r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?f. !x. f x = h f x))	link to proof	relation-natural-thm
WF_REC_INVARIANT	!r. WF r ==> (!h s. (!f g x. (!z. r z x ==> f z = g z /\ s z (f z)) ==> h f x = h g x /\ s x (h f x)) ==> (?f. !x. f x = h f x))	link to proof	relation-natural-thm
WF_REC_TAIL	!p g h. ?f. !x. f x = (if p x then f (g x) else h x)	link to proof	relation-natural-thm
WF_REC_WF	!r. (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (?f. !x. f x = h f x)) ==> WF r	link to proof	relation-natural-thm
WF_UREC	!r. WF r ==> (!h. (!f g x. (!z. r z x ==> f z = g z) ==> h f x = h g x) ==> (!f g. (!x. f x = h f x) /\ (!x. g x = h g x) ==> f = g))	link to proof	relation-natural-thm
WF_UREC_WF	!r. (!h. (!f g x. (!z. r z x ==> (f z <=> g z)) ==> (h f x <=> h g x)) ==> (!f g. (!x. f x <=> h f x) /\ (!x. g x <=> h g x) ==> f = g)) ==> WF r	link to proof	relation-natural-thm
WF_num	WF (<)	link to proof	relation-natural-thm
WLOG_RELATION	!r p. (!x y. p x y ==> p y x) /\ (!x y. r x y \/ r y x) /\ (!x y. r x y ==> p x y) ==> (!x y. p x y)	link to proof	bool-int
W_DEF	W = (\f x. f x x)	link to proof	function-def
W_THM	!f x. W f x = f x x	link to proof	function-thm
ZERO_ADD	!n. 0 + n = n	link to proof	natural-add-def
ZERO_MULT	!n. 0 * n = 0	link to proof	natural-mult-def
all_nth	!p l. ALL p l <=> (!i. i < LENGTH l ==> p (nth l i))	link to proof	list-nth-thm
big_interr	!s x y. big_interr s x y <=> (!r. r IN s ==> r x y)	link to proof	relation-thm
big_interr_def	!s. big_interr s = set_to_relation (INTERS (IMAGE relation_to_set s))	link to proof	relation-def
big_unionr	!s x y. big_unionr s x y <=> (?r. r IN s /\ r x y)	link to proof	relation-thm
big_unionr_def	!s. big_unionr s = set_to_relation (UNIONS (IMAGE relation_to_set s))	link to proof	relation-def
bool_INDUCT	!p. p F /\ p T ==> (!x. p x)	link to proof	bool-class
bool_RECURSION	!a b. ?f. f F = a /\ f T = b	link to proof	bool-class
case_list_cons	!b f h t. case_list b f (CONS h t) = f h t	link to proof	list-dest-def
case_list_id	!l. case_list [] CONS l = l	link to proof	list-dest-thm
case_list_nil	!b f. case_list b f [] = b	link to proof	list-dest-def
case_option_id	!x. case_option NONE SOME x = x	link to proof	option-dest-thm
case_option_none	!b f. case_option b f NONE = b	link to proof	option-dest-def
case_option_some	!b f a. case_option b f (SOME a) = f a	link to proof	option-dest-def
case_sum_id	!x. case_sum INL INR x = x	link to proof	sum-thm
case_sum_left	!f g a. case_sum f g (INL a) = f a	link to proof	sum-def
case_sum_right	!f g b. case_sum f g (INR b) = g b	link to proof	sum-def
concat_cons	!h t. concat (CONS h t) = APPEND h (concat t)	link to proof	list-append-def
concat_nil	concat [] = []	link to proof	list-append-def
dist	!m n. dist m n = (if m <= n then n - m else m - n)	link to proof	natural-distance-def
div_induction	!k p. 1 < k /\ p 0 /\ (!n. ~(n = 0) /\ p (n DIV k) ==> p n) ==> (!n. p n)	link to proof	natural-div-thm
drop_add	!m n l. m + n <= LENGTH l ==> drop (m + n) l = drop m (drop n l)	link to proof	list-take-drop-thm
drop_append	!l1 l2. drop (LENGTH l1) (APPEND l1 l2) = l2	link to proof	list-take-drop-thm
drop_length	!l. drop (LENGTH l) l = []	link to proof	list-take-drop-thm
drop_replicate	!m n x. m <= n ==> drop m (REPLICATE x n) = REPLICATE x (n - m)	link to proof	list-take-drop-thm
drop_suc	!n h t. n <= LENGTH t ==> drop (SUC n) (CONS h t) = drop n t	link to proof	list-take-drop-def
drop_zero	!l. drop 0 l = l	link to proof	list-take-drop-def
emptyr	!x y. ~emptyr x y	link to proof	relation-thm
emptyr_def	emptyr = set_to_relation {}	link to proof	relation-def
ex_nth	!p l. EX p l <=> (?i. i < LENGTH l /\ p (nth l i))	link to proof	list-nth-thm
exp_log_le	!k n. 1 < k /\ ~(n = 0) ==> k EXP log k n <= n	link to proof	natural-exp-log-thm
foldl_append	!f b l1 l2. foldl f b (APPEND l1 l2) = foldl f (foldl f b l1) l2	link to proof	list-fold-thm
foldl_append_assoc	!g f b l1 l2. (!s. g s b = s) /\ (!s1 s2 x. g s1 (f s2 x) = f (g s1 s2) x) ==> foldl f b (APPEND l1 l2) = g (foldl f b l1) (foldl f b l2)	link to proof	list-fold-thm
foldl_cons	!f b h t. foldl f b (CONS h t) = foldl f (f b h) t	link to proof	list-fold-thm
foldl_def	!f b l. foldl f b l = foldr (C f) b (REVERSE l)	link to proof	list-fold-def
foldl_nil	!f b. foldl f b [] = b	link to proof	list-fold-thm
foldl_reverse	!f b l. foldl f b (REVERSE l) = foldr (C f) b l	link to proof	list-fold-thm
foldl_suc	!l k. foldl (\n x. SUC n) k l = LENGTH l + k	link to proof	list-fold-thm
foldl_with_cons	!l1 l2. foldl (C CONS) l2 l1 = APPEND (REVERSE l1) l2	link to proof	list-fold-thm
foldl_with_cons_nil	!l. foldl (C CONS) [] l = REVERSE l	link to proof	list-fold-thm
foldr_append	!f b l1 l2. foldr f b (APPEND l1 l2) = foldr f (foldr f b l2) l1	link to proof	list-fold-thm
foldr_append_assoc	!g f b l1 l2. (!s. g b s = s) /\ (!x s1 s2. g (f x s1) s2 = f x (g s1 s2)) ==> foldr f b (APPEND l1 l2) = g (foldr f b l1) (foldr f b l2)	link to proof	list-fold-thm
foldr_cons	!f b h t. foldr f b (CONS h t) = f h (foldr f b t)	link to proof	list-fold-def
foldr_nil	!f b. foldr f b [] = b	link to proof	list-fold-def
foldr_reverse	!f b l. foldr f b (REVERSE l) = foldl (C f) b l	link to proof	list-fold-thm
foldr_suc	!l k. foldr (\x n. SUC n) k l = LENGTH l + k	link to proof	list-fold-thm
foldr_with_cons	!l1 l2. foldr CONS l2 l1 = APPEND l1 l2	link to proof	list-fold-thm
foldr_with_cons_nil	!l. foldr CONS [] l = l	link to proof	list-fold-thm
funpow_I	!n. funpow I n = I	link to proof	natural-funpow-thm
funpow_add	!f m n. funpow f (m + n) = funpow f m o funpow f n	link to proof	natural-funpow-thm
funpow_mult	!f m n. funpow f (m * n) = funpow (funpow f m) n	link to proof	natural-funpow-thm
funpow_one	!f. funpow f 1 = f	link to proof	natural-funpow-thm
funpow_suc	!f n. funpow f (SUC n) = f o funpow f n	link to proof	natural-funpow-def
funpow_suc'	!f n. funpow f (SUC n) = funpow f n o f	link to proof	natural-funpow-thm
funpow_suc_x	!f n x. funpow f (SUC n) x = f (funpow f n x)	link to proof	natural-funpow-thm
funpow_suc_x'	!f n x. funpow f (SUC n) x = funpow f n (f x)	link to proof	natural-funpow-thm
funpow_zero	!f. funpow f 0 = I	link to proof	natural-funpow-def
inl_inj	!a b. INL a = INL b <=> a = b	link to proof	sum-thm
inr_inj	!a b. INR a = INR b <=> a = b	link to proof	sum-thm
interr	!r s x y. interr r s x y <=> r x y /\ s x y	link to proof	relation-thm
interr_def	!r s. interr r s = set_to_relation (relation_to_set r INTER relation_to_set s)	link to proof	relation-def
interval_suc	!m n. interval m (SUC n) = CONS m (interval (SUC m) n)	link to proof	list-interval-def
interval_zero	!m. interval m 0 = []	link to proof	list-interval-def
irreflexive	!r x. irreflexive r ==> ~r x x	link to proof	relation-thm
irreflexive_def	!r. irreflexive r <=> (!x. ~r x x)	link to proof	relation-def
irreflexive_emptyr	irreflexive emptyr	link to proof	relation-thm
irreflexive_successor	irreflexive successor	link to proof	relation-natural-thm
is_none_none	is_none NONE	link to proof	option-dest-def
is_none_some	!a. ~is_none (SOME a)	link to proof	option-dest-def
is_some_none	~is_some NONE	link to proof	option-dest-def
is_some_some	!a. is_some (SOME a)	link to proof	option-dest-def
large_exp	!k n. 1 < k ==> (?m. n <= k EXP m)	link to proof	natural-exp-thm
last_nth	!l. ~NULL l ==> nth l (LENGTH l - 1) = LAST l	link to proof	list-nth-thm
length_drop	!n l. n <= LENGTH l ==> LENGTH (drop n l) = LENGTH l - n	link to proof	list-take-drop-thm
length_drop_add	!n l. n <= LENGTH l ==> n + LENGTH (drop n l) = LENGTH l	link to proof	list-take-drop-thm
length_interval	!m n. LENGTH (interval m n) = n	link to proof	list-interval-thm
length_nub	!l. LENGTH (nub l) <= LENGTH l	link to proof	list-nub-thm
length_setify	!l. LENGTH (setify l) <= LENGTH l	link to proof	list-nub-thm
length_take	!n l. n <= LENGTH l ==> LENGTH (take n l) = n	link to proof	list-take-drop-thm
length_zip	!l1 l2 n. LENGTH l1 = n /\ LENGTH l2 = n ==> LENGTH (zip l1 l2) = n	link to proof	list-zip-thm
length_zipwith	!f l1 l2 n. LENGTH l1 = n /\ LENGTH l2 = n ==> LENGTH (zipwith f l1 l2) = n	link to proof	list-zip-thm
list_INDUCT	!p. p [] /\ (!h t. p t ==> p (CONS h t)) ==> (!l. p l)	link to proof	list-def
list_RECURSION	!b f. ?fn. fn [] = b /\ (!h t. fn (CONS h t) = f h t (fn t))	link to proof	list-def
list_cases	!l. l = [] \/ (?h t. l = CONS h t)	link to proof	list-thm
log_def	!k n m. k EXP m <= n /\ n < k EXP (m + 1) ==> log k n = m	link to proof	natural-exp-log-def
log_eq	!k n m. 1 < k /\ ~(n = 0) ==> (log k n = m <=> k EXP m <= n /\ n < k EXP (m + 1))	link to proof	natural-exp-log-thm
log_eq_zero	!k n. 1 < k /\ ~(n = 0) ==> (log k n = 0 <=> n < k)	link to proof	natural-exp-log-thm
log_eq_zero_imp	!k n. 1 < k /\ ~(n = 0) /\ n < k ==> log k n = 0	link to proof	natural-exp-log-thm
log_lower_bound	!k m n. 1 < k /\ k EXP m <= n ==> m <= log k n	link to proof	natural-exp-log-thm
log_max	!k m. 1 < k ==> log k (k EXP (m + 1) - 1) = m	link to proof	natural-exp-log-thm
log_min	!k m. 1 < k ==> log k (k EXP m) = m	link to proof	natural-exp-log-thm
log_mono	!k n1 n2. 1 < k /\ ~(n1 = 0) /\ n1 <= n2 ==> log k n1 <= log k n2	link to proof	natural-exp-log-thm
log_mult_upper_bound	!k n1 n2. 1 < k /\ ~(n1 = 0) /\ ~(n2 = 0) ==> log k (n1 * n2) <= log k n1 + log k n2 + 1	link to proof	natural-exp-log-thm
log_one	!k. 1 < k ==> log k 1 = 0	link to proof	natural-exp-log-thm
log_recursion	!k n. 1 < k /\ ~(n = 0) ==> log k n = (if n < k then 0 else log k (n DIV k) + 1)	link to proof	natural-exp-log-thm
log_upper_bound	!k m n. 1 < k /\ ~(n = 0) /\ n < k EXP m ==> log k n < m	link to proof	natural-exp-log-thm
lt_exp_log	!k n. 1 < k /\ ~(n = 0) ==> n < k EXP (log k n + 1)	link to proof	natural-exp-log-thm
map_option_id	map_option I = I	link to proof	option-map-thm
map_option_none	!f. map_option f NONE = NONE	link to proof	option-map-def
map_option_o	!f g x. map_option (f o g) x = map_option f (map_option g x)	link to proof	option-map-thm
map_option_o'	!f g. map_option f o map_option g = map_option (f o g)	link to proof	option-map-thm
map_option_some	!f a. map_option f (SOME a) = SOME (f a)	link to proof	option-map-def
map_suc_interval	!m n. MAP SUC (interval m n) = interval (SUC m) n	link to proof	list-interval-thm
mem_nth	!l x. MEM x l <=> (?i. i < LENGTH l /\ x = nth l i)	link to proof	list-nth-thm
mem_nub	!l x. MEM x (nub l) <=> MEM x l	link to proof	list-nub-thm
mem_setify	!l x. MEM x (setify l) <=> MEM x l	link to proof	list-nub-thm
nth_append	!l1 l2 k. k < LENGTH l1 + LENGTH l2 ==> nth (APPEND l1 l2) k = (if k < LENGTH l1 then nth l1 k else nth l2 (k - LENGTH l1))	link to proof	list-nth-thm
nth_drop	!n l i. n + i < LENGTH l ==> nth (drop n l) i = nth l (n + i)	link to proof	list-take-drop-thm
nth_eq	!l1 l2. LENGTH l1 = LENGTH l2 /\ (!i. i < LENGTH l1 ==> nth l1 i = nth l2 i) ==> l1 = l2	link to proof	list-nth-thm
nth_interval	!m n i. i < n ==> nth (interval m n) i = m + i	link to proof	list-interval-thm
nth_map	!f l i. i < LENGTH l ==> nth (MAP f l) i = f (nth l i)	link to proof	list-nth-thm
nth_replicate	!x n i. i < n ==> nth (REPLICATE x n) i = x	link to proof	list-replicate-thm
nth_suc	!h t n. n < LENGTH t ==> nth (CONS h t) (SUC n) = nth t n	link to proof	list-nth-def
nth_take	!n l i. n <= LENGTH l /\ i < n ==> nth (take n l) i = nth l i	link to proof	list-take-drop-thm
nth_take_drop	!n l i. n <= LENGTH l /\ i < LENGTH l ==> nth l i = (if i < n then nth (take n l) i else nth (drop n l) (i - n))	link to proof	list-take-drop-thm
nth_zero	!h t. nth (CONS h t) 0 = h	link to proof	list-nth-def
nth_zip	!l1 l2 n i. LENGTH l1 = n /\ LENGTH l2 = n /\ i < n ==> nth (zip l1 l2) i = nth l1 i,nth l2 i	link to proof	list-zip-thm
nth_zipwith	!f l1 l2 n i. LENGTH l1 = n /\ LENGTH l2 = n /\ i < n ==> nth (zipwith f l1 l2) i = f (nth l1 i) (nth l2 i)	link to proof	list-zip-thm
nub_def	!l. nub l = REVERSE (setify (REVERSE l))	link to proof	list-nub-def
nub_idempotent	!l. nub (nub l) = nub l	link to proof	list-nub-thm
null_concat	!l. NULL (concat l) <=> ALL NULL l	link to proof	list-append-thm
num_CASES	!m. m = 0 \/ (?n. m = SUC n)	link to proof	natural-thm
num_FINITE	!s. FINITE s <=> (?a. !x. x IN s ==> x <= a)	link to proof	set-finite-thm
num_FINITE_AVOID	!s. FINITE s ==> (?a. ~(a IN s))	link to proof	set-finite-thm
num_INFINITE	INFINITE UNIV	link to proof	set-finite-thm
num_MAX	!p. (?n. p n) /\ (?m. !n. p n ==> n <= m) <=> (?m. p m /\ (!n. p n ==> n <= m))	link to proof	natural-order-thm
num_WF	!p. (!n. (!m. m < n ==> p m) ==> p n) ==> (!n. p n)	link to proof	natural-order-thm
num_WOP	!p. (?n. p n) <=> (?n. p n /\ (!m. m < n ==> ~p m))	link to proof	natural-order-thm
o_ASSOC	!f g h. f o g o h = (f o g) o h	link to proof	function-thm
o_ASSOC'	!f g h. (f o g) o h = f o g o h	link to proof	function-thm
o_PRIM_DEF	(o) = (\f g x. f (g x))	link to proof	function-def
o_THM	!f g x. (f o g) x = f (g x)	link to proof	function-thm
one	!v. v = one	link to proof	unit-def
one_Axiom	!e. ?!fn. fn one = e	link to proof	unit-thm
one_INDUCT	!p. p one ==> (!x. p x)	link to proof	unit-thm
one_RECURSION	!e. ?fn. fn one = e	link to proof	unit-thm
one_axiom	!f g. f = g	link to proof	unit-thm
option_INDUCT	!p. p NONE /\ (!a. p (SOME a)) ==> (!x. p x)	link to proof	option-def
option_RECURSION	!b f. ?fn. fn NONE = b /\ (!a. fn (SOME a) = f a)	link to proof	option-def
option_cases	!x. x = NONE \/ (?a. x = SOME a)	link to proof	option-thm
option_distinct	!a. ~(SOME a = NONE)	link to proof	option-thm
option_inj	!a b. SOME a = SOME b <=> a = b	link to proof	option-thm
pair_INDUCT	!p. (!a b. p (a,b)) ==> (!x. p x)	link to proof	pair-thm
pair_RECURSION	!f. ?fn. !a b. fn (a,b) = f a b	link to proof	pair-thm
real_abs	!x. abs x = (if &0 <= x then x else --x)	link to proof	real-def
real_div	!x y. ~(y = &0) ==> x / y = x * inv y	link to proof	real-def
real_ge	!x y. x >= y <=> y <= x	link to proof	real-def
real_gt	!x y. x > y <=> y < x	link to proof	real-def
real_lt	!x y. x < y <=> ~(y <= x)	link to proof	real-def
real_max	!m n. max m n = (if m <= n then n else m)	link to proof	real-def
real_min	!m n. min m n = (if m <= n then m else n)	link to proof	real-def
real_pow_suc	!x n. x pow SUC n = x * x pow n	link to proof	real-def
real_pow_zero	!x. x pow 0 = &1	link to proof	real-def
real_sub	!x y. x - y = x + --y	link to proof	real-def
reflexive	!r x. reflexive r ==> r x x	link to proof	relation-thm
reflexive_def	!r. reflexive r <=> (!x. r x x)	link to proof	relation-def
reflexive_univr	reflexive univr	link to proof	relation-thm
relation_extension_imp	!r s. (!x y. r x y <=> s x y) ==> r = s	link to proof	relation-thm
relation_to_set	!r x y. x,y IN relation_to_set r <=> r x y	link to proof	relation-thm
relation_to_set_def	!r. relation_to_set r = {x,y | r x y}	link to proof	relation-def
relation_to_set_inj	!r s. relation_to_set r = relation_to_set s ==> r = s	link to proof	relation-thm
relation_to_set_to_relation	!r. set_to_relation (relation_to_set r) = r	link to proof	relation-thm
set_of_list_cons	!h t. set_of_list (CONS h t) = h INSERT set_of_list t	link to proof	list-set-def
set_of_list_nil	set_of_list [] = {}	link to proof	list-set-def
set_of_list_nth	!l. set_of_list l = IMAGE (nth l) {i | i < LENGTH l}	link to proof	list-nth-thm
set_of_list_nub	!l. set_of_list (nub l) = set_of_list l	link to proof	list-nub-thm
set_of_list_setify	!l. set_of_list (setify l) = set_of_list l	link to proof	list-nub-thm
set_to_relation_def	!s x y. set_to_relation s x y <=> x,y IN s	link to proof	relation-def
set_to_relation_to_set	!s. relation_to_set (set_to_relation s) = s	link to proof	relation-thm
setify_cons	!h t. setify (CONS h t) = (if MEM h t then setify t else CONS h (setify t))	link to proof	list-nub-def
setify_idempotent	!l. setify (setify l) = setify l	link to proof	list-nub-thm
setify_nil	setify [] = []	link to proof	list-nub-def
subrelation	!r s. subrelation r s <=> (!x y. r x y ==> s x y)	link to proof	relation-thm
subrelation_antisym	!r s. subrelation r s /\ subrelation s r ==> r = s	link to proof	relation-thm
subrelation_big_interr	!r s. subrelation r (big_interr s) <=> (!t. t IN s ==> subrelation r t)	link to proof	relation-thm
subrelation_def	!r s. subrelation r s <=> relation_to_set r SUBSET relation_to_set s	link to proof	relation-def
subrelation_refl	!r. subrelation r r	link to proof	relation-thm
subrelation_successor_lt	subrelation successor (<)	link to proof	relation-natural-thm
subrelation_trans	!r s t. subrelation r s /\ subrelation s t ==> subrelation r t	link to proof	relation-thm
successor_def	!m n. successor m n <=> SUC m = n	link to proof	relation-natural-def
sum_CASES	!x. (?a. x = INL a) \/ (?b. x = INR b)	link to proof	sum-thm
sum_INDUCT	!p. (!a. p (INL a)) /\ (!b. p (INR b)) ==> (!x. p x)	link to proof	sum-def
sum_RECURSION	!f g. ?fn. (!a. fn (INL a) = f a) /\ (!b. fn (INR b) = g b)	link to proof	sum-def
sum_distinct	!a b. ~(INL a = INR b)	link to proof	sum-thm
take_add	!m n l. m + n <= LENGTH l ==> take (m + n) l = APPEND (take m l) (take n (drop m l))	link to proof	list-take-drop-thm
take_append	!l1 l2. take (LENGTH l1) (APPEND l1 l2) = l1	link to proof	list-take-drop-thm
take_drop	!n l. n <= LENGTH l ==> APPEND (take n l) (drop n l) = l	link to proof	list-take-drop-thm
take_length	!l. take (LENGTH l) l = l	link to proof	list-take-drop-thm
take_one	!h t. take 1 (CONS h t) = [h]	link to proof	list-take-drop-thm
take_replicate	!m n x. m <= n ==> take m (REPLICATE x n) = REPLICATE x m	link to proof	list-take-drop-thm
take_suc	!n h t. n <= LENGTH t ==> take (SUC n) (CONS h t) = CONS h (take n t)	link to proof	list-take-drop-def
take_zero	!l. take 0 l = []	link to proof	list-take-drop-def
transitive_closure_def	!r. transitive_closure r = big_interr {s | subrelation r s /\ transitive s}	link to proof	relation-def
transitive_closure_smallest	!r s. subrelation r s /\ transitive s ==> subrelation (transitive_closure r) s	link to proof	relation-thm
transitive_closure_subrelation	!r. subrelation r (transitive_closure r)	link to proof	relation-thm
transitive_closure_successor_lt	transitive_closure successor = (<)	link to proof	relation-natural-thm
transitive_closure_transitive	!r. transitive (transitive_closure r)	link to proof	relation-thm
transitive_def	!r. transitive r <=> (!x y z. r x y /\ r y z ==> r x z)	link to proof	relation-def
transitive_emptyr	transitive emptyr	link to proof	relation-thm
transitive_lt	transitive (<)	link to proof	relation-natural-thm
transitive_successor_lt	!r. subrelation successor r /\ transitive r ==> subrelation (<) r	link to proof	relation-natural-thm
transitive_univr	transitive univr	link to proof	relation-thm
unionr	!r s x y. unionr r s x y <=> r x y \/ s x y	link to proof	relation-thm
unionr_def	!r s. unionr r s = set_to_relation (relation_to_set r UNION relation_to_set s)	link to proof	relation-def
univr	!x y. univr x y	link to proof	relation-thm
univr_def	univr = set_to_relation UNIV	link to proof	relation-def
unzip_cons	!h x y t xs ys. unzip (CONS h t) = CONS x xs,CONS y ys <=> h = x,y /\ unzip t = xs,ys	link to proof	list-zip-thm
unzip_def	unzip = foldr (\(x,y) (xs,ys). CONS x xs,CONS y ys) ([],[])	link to proof	list-zip-def
unzip_eq_nil1	!l ys. unzip l = [],ys <=> l = [] /\ ys = []	link to proof	list-zip-thm
unzip_eq_nil2	!l xs. unzip l = xs,[] <=> l = [] /\ xs = []	link to proof	list-zip-thm
unzip_nil	unzip [] = [],[]	link to proof	list-zip-thm
wellfounded_emptyr	WF emptyr	link to proof	relation-well-founded-thm
wellfounded_irreflexive	!r. WF r ==> irreflexive r	link to proof	relation-well-founded-thm
wellfounded_subrelation	!r s. subrelation r s /\ WF s ==> WF r	link to proof	relation-well-founded-thm
wellfounded_successor	WF successor	link to proof	relation-natural-thm
zip_append	!x1 x2 y1 y2. LENGTH x1 = LENGTH y1 /\ LENGTH x2 = LENGTH y2 ==> zip (APPEND x1 x2) (APPEND y1 y2) = APPEND (zip x1 y1) (zip x2 y2)	link to proof	list-zip-thm
zip_cons	!x y xs ys. LENGTH xs = LENGTH ys ==> zip (CONS x xs) (CONS y ys) = CONS (x,y) (zip xs ys)	link to proof	list-zip-thm
zip_def	!l1 l2. zip l1 l2 = zipwith (,) l1 l2	link to proof	list-zip-def
zip_nil	zip [] [] = []	link to proof	list-zip-thm
zip_sing	!x y. zip [x] [y] = [x,y]	link to proof	list-zip-thm
zip_unzip	!l xs ys. unzip l = xs,ys <=> LENGTH xs = LENGTH ys /\ l = zip xs ys	link to proof	list-zip-thm
zipwith_append	!f x1 x2 y1 y2. LENGTH x1 = LENGTH y1 /\ LENGTH x2 = LENGTH y2 ==> zipwith f (APPEND x1 x2) (APPEND y1 y2) = APPEND (zipwith f x1 y1) (zipwith f x2 y2)	link to proof	list-zip-thm
zipwith_cons	!f h1 h2 t1 t2. LENGTH t1 = LENGTH t2 ==> zipwith f (CONS h1 t1) (CONS h2 t2) = CONS (f h1 h2) (zipwith f t1 t2)	link to proof	list-zip-def
zipwith_nil	!f. zipwith f [] [] = []	link to proof	list-zip-def
zipwith_sing	!f x y. zipwith f [x] [y] = [f x y]	link to proof	list-zip-thm

Back to ProofCloud main page