Re: [PVS-Help] What's the next step to prove it?

["Jerry James" <loganjerry@xxxxxxxxx>]

On Thu, Apr 17, 2008 at 9:04 AM, lingzhao <maolzh@xxxxxxxxx> wrote:
> I am newer to pvs, when I try to prove some tccs,but I get stuck. The
>  problem is as follows. So how can I prove it? thanks.
>
>  {-1}  x < N
>   |-------
>  {1}   -1 - N * floor((x - 1) / N) + x < N
>  rule?

The "ml3" lemma in the prelude's "mod" theory is probably what you need.
-- 
Jerry James
http://loganjerry.googlepages.com/