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

Re: seeking proof of a trivial fact



> b41 : lemma forall (x, y: real): x >=0 and y <= 1
>   => x * y  <= x
>
> Why this lemma is not trivial in PVS ?

If you install the NASA manip and field strategy packages (available at 
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS2-library/pvslib.html),
the lemma b41 can be proved as follows:

(SKOSIMP) (CANCEL-BY 1 "x!1")

Cesar
--
Cesar A. Munoz H.       | munoz@icase.edu, C.A.Munoz@larc.nasa.gov
Staff Scientist         | http://www.icase.edu/~munoz
ICASE                   | Phone +1 757 864-8018  Fax +1 757 864-6134
NASA LaRC, Mail Stop 132C, 3 West Reid Street, Hampton, VA 23681-2199,
USA.