[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Inequations in long proof
Raphael Couturier (Raphael.Couturier@loria.fr) writes:
> 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?