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

Re: Inequations in long proof

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?
or (ASSERT :fnums (-6 -9 1)).

Bruno Dutertre