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

Re: Inequations in long proof



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