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

Re: [PVS-Help] Cardinality over strict subsets



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/