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

Bruno Dutertre