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

[Eddy Seager <seagere5@xxxxxxxxxxxxxxxxxxx>]

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