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

Proofing problem



Dear PVS-experts!

Sorry to bother you with a maybe trivial question.
My problem is, PVS wants me to proof:


{-1}  interval > 0
{-2}  interval <= max_interval
[-3]  number_intervals > 0
[-4]  p!1 >= 0
[-5]  p!1 < number_intervals
  |-------
[1]   interval * number_intervals > p!1 * interval - interval


where interval and number_intervals are of type nat.
The (grind) command wont work, so my question is, do I have problems
whith my specification, or is it that I just don't know the right proofing
command.

Thanks a lot for your attention, maybe you can help a rookie.

Best Regards,
wilfried steiner