Re: [PVS-Help] begginer's question

[Cesar Munoz <munoz@xxxxxxxxxx>]

You should try (grind) instead of (ground):

{-1}  x!1 < 2 * y!1
{-2}  y!1 < 3 * v!1
  |-------
{1}   3 * x!1 < 18 * v!1

Rule? (grind)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.

Cesar

jane huffam wrote:
> Hi,
> I'm studying pvs through "A Tutorial Introduction to PVS" by  Crow, Owre,
> Rushby, Shankar and Srivas.  They gave an example I can't prove. It is
> "decisions", section 4.3. I'm stuck in arith. What do I do after "(then
> (skolem!)(ground))" ?
> Thanks for any tip!
> 

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4