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

Re: [PVS-Help] Cardinality over strict subsets

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

Jerry James wrote:
On Wed, Aug 13, 2008 at 5:11 PM, Sam Owre <owre@xxxxxxxxxxx> wrote: 
I'm happy to add this to the prelude for the next release.
Are there others like this that you know of belong in the
prelude (or, if more specialized, in the finite_sets
library)?


I can't think of any off-hand, but I'll let you know if I come up with
something.  Thanks!