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

[PVS-Help] Help proving two-dimensional inequality

I have the following lemma I wish to prove:
 oddly_specific_1a: LEMMA
   FORALL(x : {i : real | i >= 0 AND i < 4}, y : {i : real | i >= 2 AND i < 3}):
     -21.1636 + 4.12282 * x + 17.23232 * y - 1.87144 * x * y > 0
Using (model-check) and (grind) get me no further than a (skolem-typepred) would do.

In looking at some other inequality questions asked here, I tried (grind-reals) and (grind :theories real_props) but both of those didn't lead to what looked like useful transformations. I also tried a hail Mary of adding "IMPORTING reals@top" to the top of my theory without luck.

I've plotted this in Grapher (Mac plotter program) and verified that it is indeed true, but I suspect part of the problem might be that I wouldn't know how to rigorously prove this using plain old paper-and-pencil.

Any help in proving this via PVS would be appreciated.