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

thanks.

Sheng Yang

University of texas at Dallas


__________________________________
Do you Yahoo!?
Protect your identity with Yahoo! Mail AddressGuard
http://antispam.yahoo.com/whatsnewfree