Entry	Value
Package Name	list-filter-thm
Count	7
Theorems	ALL_FILTER : !p q l. ALL p (FILTER q l) <=> ALL (\x. q x ==> p x) l EX_FILTER : !p q l. EX p (FILTER q l) <=> EX (\x. q x /\ p x) l FILTER_APPEND : !p l1 l2. FILTER p (APPEND l1 l2) = APPEND (FILTER p l1) (FILTER p l2) FILTER_MAP : !p f l. FILTER p (MAP f l) = MAP f (FILTER (p o f) l) LENGTH_FILTER : !p l. LENGTH (FILTER p l) <= LENGTH l MEM_FILTER : !p l x. MEM x (FILTER p l) <=> MEM x l /\ p x SET_OF_LIST_FILTER : !p l. set_of_list (FILTER p l) = set_of_list l DIFF {x | ~p x}

Back to main package page