RE: [PVS-Help] proved-incomplete because of finite-sets

["Butler, Ricky W. (LARC-D320)" <r.w.butler@xxxxxxxx>]

Go to the PVS install directory.  Then go to the lib/finite_sets
directory and start up PVS4.1.   Go to top.pvs and issue m-x pri.
Then exit after all proofs done.

Rick

> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@csl.sri.com
[mailto:pvs-
> help-bounces+r.w.butler=larc.nasa.gov@csl.sri.com] On Behalf Of Eddy
> Seager
> Sent: Wednesday, February 20, 2008 8:22 AM
> To: pvs-help@csl.sri.com
> Subject: [PVS-Help] proved-incomplete because of finite-sets
> 
> Hello,
> 
> I'm suffering proved-incomplete status because of the finite-sets
library.
> Running M-x spc i get the following:-
> -----------------------------------------------------------
> derivative_log.log_deriv has been PROVED.
> 
>   The proof chain for log_deriv is INCOMPLETE.
>   It depends on the following unproved conjectures:
>     finite_sets_inductions.finite_set_induction_rest
>     finite_sets_minmax.lt_antisymmetric
>     finite_sets_minmax.lt_reflexive
>     finite_sets_minmax.lt_total
>     finite_sets_minmax.lt_transitive
>     finite_sets_minmax.max_TCC1
>     finite_sets_minmax.max_lem
>     finite_sets_minmax.min_TCC1
>     finite_sets_minmax.min_lem
>     finite_sets_minmax.minrec_TCC1
>     finite_sets_below.card_below_fullset
>     finite_sets_below.card_below_fullset_TCC1
>     finite_sets_below.finite_below
>     func_composition.composition_injective
>     func_composition.composition_surjective
>     finite_sets_card_eq.card_injection
>     finite_sets_card_eq.card_surjection
>     finite_sets_card_eq.injection_and_cardinal
>     finite_sets_card_eq.surjection_and_cardinal
> -------------------------------------------------------
> 
> I've just done a fresh install of PVS as well. What's the best way to
> resolve this?
> 
> Regards,
> 
> Eddy Seager
> University of Manchester Undergrad