Inequations in long proof

[Raphael Couturier <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):
  • Date
  • Thread