Entry	Value
Package Name	list-set-def
Count	9
Theorems	ALL_CONS : !p h t. ALL p (CONS h t) <=> p h /\ ALL p t ALL_NIL : !p. ALL p [] EX_CONS : !p h t. EX p (CONS h t) <=> p h \/ EX p t EX_NIL : !p. ~EX p [] LIST_OF_SET_PROPERTIES : !s. FINITE s ==> set_of_list (list_of_set s) = s /\ LENGTH (list_of_set s) = CARD s MEM_CONS : !x h t. MEM x (CONS h t) <=> x = h \/ MEM x t MEM_NIL : !x. ~MEM x [] set_of_list_cons : !h t. set_of_list (CONS h t) = h INSERT set_of_list t set_of_list_nil : set_of_list [] = {}

Back to main package page