# Re: How to prove this

```Jie Dai wrote:
>
> Hi pvs users,
>
> I am a new user of PVS. Is there anyone know why the last
> GRIND can not simplify (y!1 - rem(n)(y!1))/n) to 0/n  too??
> What should I do to complete the proof.
>

> Rerunning step: (LEMMA "rem_mod2")
> Applying rem_mod2
> this simplifies to:
> test :
>
> {-1}  FORALL (b: posnat, x: int): 0 <= x AND x < b IMPLIES rem(b)(x) = x
>
> [-2]  (expt(2, r - 1) = n)
> [-3]  x!1 < n
> [-4]  y!1 < n
>   |-------
> [1]   (x!1 - rem(n)(x!1)) / n = (y!1 - rem(n)(y!1)) / n
>
> Rerunning step: (GRIND)
> Trying repeated skolemization, instantiation, and if-lifting,
> this simplifies to:
> test :
>
> {-1}  rem(n)(x!1) = x!1
> [-2]  (expt(2, r - 1) = n)
> [-3]  x!1 < n
> [-4]  y!1 < n
>   |-------
> {1}   0 / n = (y!1 - rem(n)(y!1)) / n
>
> Rule?
>
> Why the GRIND here can not simplify (y!1 - rem(n)(y!1))/n) to 0/n  too?

That's because the heuristic (GRIND) uses for instantiating quantifiers
tries to find one instantiation only.  In your case, (GRIND)
instantiates
formula -1 with b=n and x=x!1, and does not look for another match.
To get (GRIND) to look for all possible matches, you can use
(GRIND :IF-MATCH ALL), but even that does not always work.

It is better to use "rem_mod2" as a rewrite rule: instead of
doing (LEMMA "rem_mod2"), you can try something like
(AUTO-REWRITE "rem_mod2")(ASSERT).

Bruno
--
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

```