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

Re: [PVS-Help] Cardinality over strict subsets

To: Jerome <jerome@xxxxxxxxxxxxxx>
Subject: Re: [PVS-Help] Cardinality over strict subsets
From: "Jerry James" <loganjerry@xxxxxxxxx>
Date: Thu, 14 Aug 2008 10:31:42 -0600
Cc: PVS Help <pvs-help@xxxxxxxxxxx>
Dkim-signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:cc:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references; bh=oahF56mvxe5Q32acQBnyOaLDwOrHVlNDdt1wI94qVDQ=; b=cSsFuhxzeUOphjhhvPcogBCSPT2MQgtLyXcoGPyzLSP87gseflobuqAgjFIMrhZbtW /ImFxGVUYIs3YwtB7KROIBAOga41vbTjhc68zvMbE7B23286J3LNJthJcD47IVXTml1u IhpC4Y9tHMgWqS64PZ2rU1sCmKbIURgrnqPzs=
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=ELttMrRR39NevKMF0kffi0OW/XghICKPCg62rQzZC3MLrER7C8MmDz/MNGrmxR40Xr 1fK9H+88xJInh9b9YEQE1+4c0w4SxGAiZnWmCcdUwd8tRvh5ImYOsjmjcacSdccIVM6n ovXs70372CgiVPaI57whrwC2wQ+5uC58nKagQ=
In-reply-to: <48A37804.5020702@cs.caltech.edu>
List-help: <mailto:pvs-help-request@csl.sri.com?subject=help>
List-id: PVS-Help <pvs-help.csl.sri.com>
List-post: <mailto:pvs-help@csl.sri.com>
List-subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>
List-unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>
References: <20080813214647.GA10440@cs.caltech.edu> <870180fe0808131539t4cd42c16h6359b05f20957846@mail.gmail.com> <26507.1218669074@photon.csl.sri.com> <870180fe0808131622w4a6fe4f4he02244e9f70ac439@mail.gmail.com> <48A37804.5020702@cs.caltech.edu>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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/

Prev by Date: Re: [PVS-Help] Cardinality over strict subsets
Next by Date: Re: [PVS-Help] Cardinality over strict subsets
Prev by thread: Re: [PVS-Help] Cardinality over strict subsets
Next by thread: Re: [PVS-Help] Cardinality over strict subsets
Index(es):
- Date
- Thread