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

How to prove this



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.

Thanks for your help.

Jie

  |-------
{1}   (FORALL (x, y: processorID): pg(x, r) = pg(y, r))

Rerunning step: (GRIND)
pg rewrites pg(x, r)
  to (x - rem(expt(2, r - 1))(x)) / expt(2, r - 1)
pg rewrites pg(y, r)
  to (y - rem(expt(2, r - 1))(y)) / expt(2, r - 1)
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
test :

{-1}  x!1 < n
{-2}  y!1 < n
  |-------
{1}   (x!1 - rem(expt(2, r - 1))(x!1)) / expt(2, r - 1) =
       (y!1 - rem(expt(2, r - 1))(y!1)) / expt(2, r - 1)

Rerunning step: (LEMMA "round_ax")
Applying round_ax
this simplifies to:
test :

{-1}  (expt(2, r - 1) = n)
[-2]  x!1 < n
[-3]  y!1 < n
  |-------
[1]   (x!1 - rem(expt(2, r - 1))(x!1)) / expt(2, r - 1) =
       (y!1 - rem(expt(2, r - 1))(y!1)) / expt(2, r - 1)

Rerunning step: (REPLACE*)
Repeatedly applying the replace rule,
this simplifies to:
test :

[-1]  (expt(2, r - 1) = n)
[-2]  x!1 < n
[-3]  y!1 < n
  |-------
{1}   (x!1 - rem(n)(x!1)) / n = (y!1 - rem(n)(y!1)) / n

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?