Re: Inequations in long proof

[Bruno Dutertre <bruno@dcs.qmw.ac.uk>]

Raphael Couturier wrote:
> 
> 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.
> 

You can try (ASSERT :flush? t) or (ASSERT :flush? t :type-constraints?
nil)
or (ASSERT :fnums (-6 -9 1)).

Bruno Dutertre

---

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

• Prev by Date: Re: Inequations in long proof
• Next by Date: lemma,inst? and replace
• Prev by thread: Re: Inequations in long proof
• Next by thread: Proving properties of finite sets
• Index(es):
  • Date
  • Thread