# Re: [PVS-Help] inequalities in PVS

```Alexander,

This problem and many like it can be solved using strategy packages that
we've developed at NASA Langley and NIA.  If you are a user of the NASA
Langley libraries found at

http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

If not, you can retrieve the libraries or just the strategies from the
web site.

A proof of your conjecture is easy to obtain using these strategies,
which were designed to help with cases requiring detailed manipulation
such as yours.  Learning to use them requires some investment of your
time, of course, but if you expect to do a lot of proving, you would
realize a benefit from the effort.

So here is how it goes:

{-1}  x!1 < 1000
{-2}  x!1 > 1
{-3}  x!1 * x!1 > 1
{-4}  x!1 * x!1 < 1000
|-------
{1}   1000 - x!1 * x!1 < 1000 - x!1

Rerunning step: (field 1)
both_sides_minus_lt2 rewrites 1000 - x!1 * x!1 < 1000 - x!1
to x!1 < x!1 * x!1

Simplifying formula 1 with FIELD,
this simplifies to:
m1 :

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
|-------
{1}   x!1 < x!1 * x!1

Rerunning step: (op-ident 1 l)

Applying identity operation to rewrite selected expression,
this simplifies to:
m1 :

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
|-------
{1}   (x!1 * 1 < x!1 * x!1)

Rerunning step: (cancel 1)

Canceling terms from both sides of selected formulas,
this simplifies to:
m1 :

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
|-------
{1}   1 < x!1

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,
Q.E.D.

---------

The strategy "field" performs many reductions automatically, although it
mostly helps when divisions are present.  In this case it rearranges the
conclusion the way we would like it.  Next we want to cancel an "x" from
both sides, but first we need to create a more symmetric formula to set
up the cancellation.  The strategy "op-ident" is the helper and "cancel"
does what we need to eliminate the "x".  The rest is handled by assert.

Regards,

Ben Di Vito

1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234
b.divito@nasa.gov
http://shemesh.larc.nasa.gov/people/bld

---------

A Serebrenik wrote:
> Dear all,
>
> I wonder what proof command should I use for simple manipulation of
> inequalities? I would like, e.g. to prove the following sequent:
> {-1}  integer_pred(x!1)
> {-2}  x!1 < 1000
> {-3}  x!1 > 1
> {-4}  x!1 * x!1 > 1
> {-5}  x!1 * x!1 < 1000
>   |-------
> {1}   1000 - x!1 * x!1 < 1000 - x!1
>
> Using (both-sides - 1000) and (assert) I can reduce the succedent to
> {1'}  -1 * (x!1 * x!1) < -1 * x!1 but this is as far as I get:
> (both-sides * -1) results in an unexpected:
> {1''}  -1 * (x!1 * x!1) * -1 < -1 * x!1 * -1
>
> Best regards,
> Alexander Serebrenik
>
>

```