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

*To*: Laurent FERIER <lfe@info.fundp.ac.be>*Subject*: Re: Quantifiers*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Mon, 22 Feb 1999 09:47:22 -0800*CC*: pvs-help@csl.sri.com, lfe@leibniz.info.fundp.ac.be*References*: <36D170F0.72F9@info.fundp.ac.be>*Sender*: bruno@csl.sri.com

Laurent FERIER wrote: > > Hello! > > I (unsucessfully) tried to prove something in the following form: > > [-1] (FORALL (t: Time): P(t) > [-2] (FORALL (t: FiniteTime): NOT P(t) > |-------- > > This is trivially true, but I've know no mean to prove it. > Furthermore, I do not understand the extensionality proof > commands. Can someone help me? > Presumably, FiniteTime is a subtype of Time. For the sequent to be true, you need FiniteTime to be nonempty. In this case, the proof is simply to instantiate formula -1 and -2 with the same constant of type FiniteTime. For example, if "0" is of type FiniteTime, just do (inst - "0")(inst - "0"). You can also do something like (inst - "epsilon! (x: FiniteTime): true") (inst - "epsilon! (x: FiniteTime): true"). -- 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**:**Quantifiers***From:*Laurent FERIER <lfe@info.fundp.ac.be>

- Prev by Date:
**Quantifiers** - Next by Date:
**PVS dump files** - Prev by thread:
**Quantifiers** - Next by thread:
**PVS Grammar** - Index(es):