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

[PVS-Help] Using THEOREM in proof


I am trying to use the THEOREMs defined in the finite_sets theory
associated with the cardinalities.

Unfortunately I am unable to find how to use these THEOREMs. I am trying
to prove LEMMATA like this simplified test example:

card(S) = 0 => empty(S)

This is a lot like the empty_card THEOREM.and card_empty? THEOREM. Can
someone help me to complete this example proof?

Kind regards