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

Re: [PVS-HELP] Choose Function

To: pvs-help@xxxxxxxxxxx
Subject: Re: [PVS-HELP] Choose Function
From: schoppekloppe <schoppekloppe@xxxxxxxx>
Date: Mon, 20 Apr 2009 17:29:29 +0200
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.de;h=Received:X-Yahoo-Newman-Property:Message-ID:Date:From:User-Agent:MIME-Version:To:Subject:References:In-Reply-To:Content-Type:Content-Transfer-Encoding;b=2G0NZY/jJv4OB6WtQrqBmn6zx4+wuKsiVYjEPPdSI3+f+sUqjAu00JzkcI0voQ6j3OpFbjVhCKi28SZy/a8p8zNtvieAqjIHJkfINW/sgEwzm+N9qgG0pNhPhq+hNBA5uz+lqJRZ4EGCpzjhb3cxdM7PffXOlh6Q1OjWe9UWO2U=;
In-Reply-To: <440214338.32641@eyou.net>
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: <440214338.32641@eyou.net>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx
User-Agent: Thunderbird 2.0.0.21 (X11/20090318)

SongFu schrieb:
> I want know how to proof the following:
>
> choose({x: nat| x=1}) =1

Use the lemma "choose_singleton[nat]" and then expand "singleton".
-- 
Christian Henkel

References:
- [PVS-HELP] Choose Function
  - From: SongFu

Prev by Date: Re: [PVS-Help] Installation problem: cmulisp-local-source-directorynotset
Next by Date: Re: [PVS-HELP] Choose Function
Prev by thread: [PVS-HELP] Choose Function
Next by thread: Re: [PVS-HELP] Choose Function
Index(es):
- Date
- Thread