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

*To*: pvs-help@csl.sri.com*Subject*: Re: forall clause within a set-comprehension*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Tue, 11 May 1999 09:36:17 -0700*CC*: pvs-help@csl.sri.com*References*: <3737EC2F.B7CDFC0B@sbox.tu-graz.ac.at>*Sender*: bruno@csl.sri.com

Gernot Lepuschitz wrote: > > Is it possible to prove this lemma: > > empty_dict: LEMMA {w: Word | > FORALL (l: Letter > | member(l, ), > (w1: Word | member(w1, retrDictd(empty))): > w = cons(l, w1)} > =emptyset[Word] > > I tried to do a (expand "emptyset"),(apply-extensionality) which leads > me to this state: > > {-1} FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter): empty))), > (w1: Word | member(w1, retrDictd(empty))): > x!1 = cons(l, w1) > |------- > [1] (({w: Word | > FORALL (l: Letter | member(l, dom(LAMBDA (l: Letter): > empty))), > (w1: Word | member(w1, retrDictd(empty))): > w = cons(l, w1)}) > = ({x: Word | FALSE})) > How can I deal with the FORALL clause within the set comprehension ?? > (apply-extensionality) already delt with it by introducing antecedent {-1}. Now you have to prove that formula -1 is false. Formula [1] is simply kept from the previous goal but it's probably not useful anymore. It's usually better to use (apply-extensionality :hide? t) rather than (apply-extensionality). In your case, this would get rid of [1]. Without knowing the definition of retrDictd(empty) and dom(...) it's hard to be sure but it is not clear whether {-1} is false. You have to find a letter l and a Word w1 such that x!1 /= cons(l, w1) member(l, dom(LAMBDA (l: Letter): empty)) member(w1, retrDictd(empty)). If one of retrDictd(empty) or dom(LAMBDA (l: letter): empty) is empty, then you can't find such l and w1. In this case, formula -1 is true and lemma empty_dict is false. -- Bruno Dutertre | bruno@csl.sri.com CSL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

**References**:**forall clause within a set-comprehension***From:*Gernot Lepuschitz <gernot@sbox.tu-graz.ac.at>

- Prev by Date:
**forall clause within a set-comprehension** - Next by Date:
**A question** - Prev by thread:
**forall clause within a set-comprehension** - Next by thread:
**errors** - Index(es):