[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Cotuple mutually exclusive component types
- To: pvs-help@csl.sri.com
- Subject: [PVS-Help] Cotuple mutually exclusive component types
- From: Jerry James <james@ittc.ku.edu>
- Date: Fri, 02 Jan 2004 22:40:14 -0600
- 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>
- Original-Received: from quarter.csl.sri.com (mx0.csl.sri.com [130.107.1.30])by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id i034ecm0022044for <pvs-help@postal.csl.sri.com>; Fri, 2 Jan 2004 20:40:39 -0800 (PST)(envelope-from james@eecs.ku.edu)
- Original-Received: from mailgate.sri.com (mailgate.SRI.COM [128.18.243.11])by quarter.csl.sri.com (8.12.9/8.12.10) with SMTP id i034ecKc015444for <pvs-help@csl.sri.com>; Fri, 2 Jan 2004 20:40:38 -0800
- Original-Received: (qmail 10851 invoked from network);3 Jan 2004 04:40:22 -0000
- Original-Received: from localhost (HELO mailgate.SRI.COM) (127.0.0.1)by mailgate.sri.com with SMTP; 3 Jan 2004 04:40:22 -0000
- Original-Received: from stephens.ittc.ku.edu ([129.237.125.220])by mailgate.SRI.COM (SAVSMTP 3.1.0.29) with SMTP idM2004010220402220725for <pvs-help@csl.sri.com>; Fri, 02 Jan 2004 20:40:22 -0800
- Original-Received: from diannao.ittc.ku.edu (diannao.ittc.ku.edu[129.237.126.112])by stephens.ittc.ku.edu (8.12.10/8.12.10/ITTC-ANTISPAM-ANTIVIRUS-3.0)with ESMTP id i034eE54007255for <pvs-help@csl.sri.com>; Fri, 2 Jan 2004 22:40:14 -0600
- Original-Received: from diannao.ittc.ku.edu by diannao.ittc.ku.edu(8.12.8/KU-4.0-client)id i034eE99003007; Fri, 2 Jan 2004 22:40:14 -0600
- Original-Received: (from james@localhost)by diannao.ittc.ku.edu (8.12.8/8.12.8/Submit) id i034eEFJ003005;Fri, 2 Jan 2004 22:40:14 -0600
- Sender: pvs-help-bounces+archive=csl.sri.com@csl.sri.com
- User-Agent: Gnus/5.1002 (Gnus v5.10.2) XEmacs/21.5 (celeriac, linux)
I have been working with cotuples. I'm hitting a problem I don't know
how to solve. The problem boils down to proving the following lemma:
cotuples: THEORY
BEGIN
new_type: TYPE = [nat + set[nat]]
mutually_exclusive_types: LEMMA
FORALL (obj: new_type): IN?_1(obj) /= IN?_2(obj)
END cotuples
If I try (grind), it eliminates everything:
mutually_exclusive_types :
|-------
{1} FORALL (obj: new_type): IN?_1(obj) /= IN?_2(obj)
Rule? (grind)
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
mutually_exclusive_types :
|-------
Other rules give me both IN?_1(obj) and IN?_2(obj) on one side or the
other, but then I can't get anywhere with (smash), (assert), or any
other rule that seems likely to help. How would one prove this?
--
Jerry James
http://www.ittc.ku.edu/~james/