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

*To*: Raphael.Couturier@loria.fr*Subject*: Re: Inequations in long proof*From*: "Ricky W. Butler" <rwb@air16.larc.nasa.gov>*Date*: Wed, 23 Jul 1997 06:42:43 -0400*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <33D5D157.61B2@loria.fr>*References*: <33D5D157.61B2@loria.fr>

Raphael Couturier (Raphael.Couturier@loria.fr) writes: > Hello > > My problem is the following. I want to prove a long proof in which I > need to prove that : > y<=-1-j+i+low and i-j+low<=low-1+nbp implies y<=low-2+nbp > > If I try to prove that in a lemma, PVS proves this formula in less than > 1 second with the command ASSERT, whereas if I try to prove it in my > long proof, after 20 minutes, ASSERT gives me no result. > Have you tried hiding all of the irrelevant formulas using the HIDE command before issuing the ASSERT? Rick

**References**:**Inequations in long proof***From:*Raphael Couturier <Raphael.Couturier@loria.fr>

- Prev by Date:
**Inequations in long proof** - Next by Date:
**Re: Inequations in long proof** - Prev by thread:
**Inequations in long proof** - Next by thread:
**Re: Inequations in long proof** - Index(es):