Re: [PVS-Help] Cardinality over strict subsets

[Sam Owre <owre@xxxxxxxxxxx>]

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
> http://loganjerry.googlepages.com/

I already added it and card_strict_subset.
Let me know if you think of others.

Sam