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

*To*: pvs-help@csl.sri.com*Subject*: How to prove this*From*: Jie Dai <jiedai@cs.uidaho.edu>*Date*: Sat, 18 Mar 2000 15:27:07 -0800*Delivery-Date*: Sat Mar 18 15:26:57 2000*Sender*: jiedai@io.csds.uidaho.edu

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?

- Prev by Date:
**Re: Typecheck question** - Next by Date:
**Re: How to prove this** - Prev by thread:
**Re: Don't understand this TCC** - Next by thread:
**Re: How to prove this** - Index(es):