[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Cardinality over strict subsets
Jerry James <loganjerry@xxxxxxxxx> wrote:
> On Wed, Aug 13, 2008 at 6:10 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> > Actually, Jerry, when you worked on that doubleton theory with me earlier in
> > the year, one of the lemmas you came up with was:
> > singleton_singleton: LEMMA
> > FORALL S: singleton?(S) IMPLIES (EXISTS t: S = singleton(t))
> > One of the comments you made in the code was that you "wish this was in the
> > prelude" :)
> > jerome
> Oh, right, I'd forgotten about that one. What do you think, Sam?
> Jerry James
I already added it and card_strict_subset.
Let me know if you think of others.