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

[PVS-Help] equivalence class number



Hello everyone
could you tell me how to express the number of equivalence class is finite?

i have try the following method, but failed:

.....
RE_Eq: JUDGEMENT ~ HAS_TYPE equivalence[T]
EqC_finite: formula is_finite(EquivClass(~))
......

when i prove this formula,
it was converted to
is_finite(singleton[T -> set[T]](EquivClass(~)))

why "singleton" occurs?

thanks in advance!

Q.G. XU