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

*To*: pvs-help@csl.sri.com*Subject*: Inequations in long proof*From*: Raphael Couturier <Raphael.Couturier@loria.fr>*Date*: Wed, 23 Jul 1997 11:39:35 +0200*Sender*: Raphael.Couturier@loria.fr

Hello My problem is the following. I want to prove a long proof in which I need to prove that : y<=-1-j+i+low and i-j+low<=low-1+nbp implies y<=low-2+nbp If I try to prove that in a lemma, PVS proves this formula in less than 1 second with the command ASSERT, whereas if I try to prove it in my long proof, after 20 minutes, ASSERT gives me no result. Here is my long proof. BIT_1.1.1.1.1.2 : [-1] y!1 + d!1 > low!1 + nbp!1 [-2] ny!1 = y!1 + d!1 [-3] x!1 + d!1 > low!1 + nbp!1 [-4] nx!1 = x!1 + d!1 [-5] x!1 >= low!1 [-6] y!1 <= -1 - j!1 + i!1 + low!1 [-7] x!1 <= y!1 [-8] i!1 - j!1 + low!1 > low!1 [-9] i!1 - j!1 + low!1 <= low!1 - 1 + nbp!1 [-10] i!1 <= j!1 + nbp!1 [-11] i!1 >= j!1 [-12] hi!1 > low!1 [-13] low!1 > 0 [-14] nbp!1 = nb!1 / 2 [-15] nb!1 = 1 - low!1 + hi!1 [-16] nbp!1 >= 1 [-17] i!1 > low!1 [-18] i!1 <= hi!1 [-19] FORALL (x: nat), (y: nat): x >= low!1 AND y <= i!1 - 1 AND x <= y => A!1(x) <= A!1(y) [-20] FORALL (x: nat), (y: nat): x >= i!1 AND y <= hi!1 AND x <= y => A!1(x) >= A!1(y) [-21] j!1 > low!1 [-22] j!1 <= low!1 - 1 + nbp!1 [-23] A!1(j!1 - 1) <= A!1(j!1 - 1 + nbp!1) [-24] A!1(j!1) >= A!1(j!1 + nbp!1) [-25] (FORALL (x: nat): x >= low!1 AND x <= j!1 - 1 => A!1(x) <= A!1(x + nbp!1)) [-26] (FORALL (x: nat): x >= j!1 AND x <= low!1 - 1 + nbp!1 => A!1(x) >= A!1(x + nbp!1)) [-27] (FORALL (x: nat): x >= low!1 AND x <= j!1 - 1 => A!1(x) <= A!1(j!1 - 1)) [-28] (FORALL (x: nat): x >= j!1 AND x <= i!1 - 1 => A!1(x) >= A!1(j!1)) [-29] (FORALL (x: nat): x >= i!1 AND x <= j!1 - 1 + nbp!1 => A!1(x) >= A!1(j!1 - 1 + nbp!1)) [-30] (FORALL (x: nat): x >= j!1 + nbp!1 AND x <= hi!1 => A!1(x) <= A!1(j!1 + nbp!1)) [-31] d!1 = -1 - low!1 + j!1 [-32] FORALL (x: nat): x >= low!1 AND x < low!1 + nbp!1 => Ap!1(x + nbp!1) = max(A!1(x), A!1(x + nbp!1)) [-33] Prop1(low!1, d!1, nbp!1) |------- [1] y!1 <= low!1 - 2 + nbp!1 Of course, I can prove the small proof and use it in a lemma, but in my long proof, I have to use several simple inequations that PVS cannot prove fastly. So I want to know if there is another way to solve my problem. Thanks, Raphaël Couturier

- Prev by Date:
**Proving properties of finite sets** - Next by Date:
**Re: Inequations in long proof** - Prev by thread:
**lemma,inst? and replace** - Next by thread:
**Re: Inequations in long proof** - Index(es):