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

about the size of a set

Hi, all

I am a new user to PVS system. Now I am using PVS to
prove some properties of a system. I am involving a
question maybe someone can help me.

I am trying to evaluate a conjecture that a set only
contain either 0 or 1 element. It looks that in the
prelude of PVS, no size is defined in set. Can anyone
give the suggestions on this?


Sheng Yang

University of texas at Dallas

Do you Yahoo!?
Protect your identity with Yahoo! Mail AddressGuard