[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?