Entry	Value
Package Name	list-set-thm
Count	24
Theorems	ALL_F : !l. ALL (\x. F) l <=> NULL l ALL_IMP : !p q l. (!x. MEM x l /\ p x ==> q x) /\ ALL p l ==> ALL q l ALL_MEM : !p l. (!x. MEM x l ==> p x) <=> ALL p l ALL_MP : !p q l. ALL (\x. p x ==> q x) l /\ ALL p l ==> ALL q l ALL_SET_OF_LIST : !p l. ALL p l <=> (!x. x IN set_of_list l ==> p x) ALL_T : !l. ALL (\x. T) l AND_ALL : !p q l. ALL (\x. p x /\ q x) l <=> ALL p l /\ ALL q l CARD_SET_OF_LIST_LE : !l. CARD (set_of_list l) <= LENGTH l EXISTS_EX : !p l. (?x. EX (p x) l) <=> EX (\y. ?x. p x y) l EX_IMP : !p q l. (!x. MEM x l /\ p x ==> q x) /\ EX p l ==> EX q l EX_MEM : !p l. (?x. MEM x l /\ p x) <=> EX p l EX_SET_OF_LIST : !p l. EX p l <=> (?x. x IN set_of_list l /\ p x) FINITE_SET_OF_LIST : !l. FINITE (set_of_list l) FORALL_ALL : !p l. (!x. ALL (p x) l) <=> ALL (\y. !x. p x y) l LENGTH_LIST_OF_SET : !s. FINITE s ==> LENGTH (list_of_set s) = CARD s MEM_LIST_OF_SET : !s. FINITE s ==> (!x. MEM x (list_of_set s) <=> x IN s) MEM_SET_OF_LIST : !l x. MEM x l <=> x IN set_of_list l NOT_ALL : !p l. ~ALL p l <=> EX (\x. ~p x) l NOT_ALL_NOT : !p l. ~ALL (\x. ~p x) l <=> EX p l NOT_EX : !p l. ~EX p l <=> ALL (\x. ~p x) l NOT_EX_NOT : !p l. ~EX (\x. ~p x) l <=> ALL p l NULL_SET_OF_LIST : !l. set_of_list l = {} <=> NULL l SET_OF_LIST_EQ_EMPTY : !l. set_of_list l = {} <=> l = [] SET_OF_LIST_OF_SET : !s. FINITE s ==> set_of_list (list_of_set s) = s

Back to main package page