[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: about the size of a set

Hi Sheng,

> I am trying to evaluate a conjecture that a set only
> contain either 0 or 1 element. It looks that in the
> prelude of PVS, no size is defined in set. Can anyone
> give the suggestions on this?

The prelude defines "card", the cardinality (size) of
finite sets. There are also a number of useful lemmas
that talk about sets of size 0 and 1.