[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] fullset type properties
I'd like to use the type properties of 'fullset' to finish off a
proof. Unfortunately, I'm not sure how to do that:
|-------
[1] is_finite[index[N, value]](fullset[index[N, value]]) AND
NOT empty?[index[N, value]](fullset[index[N, value]])
Rule? (typepred "fullset")
No change on: (TYPEPRED "fullset")
(I've also tried (typepred "fullset[index[N, value]]") with the same
result.) What is it that I'm not understanding about fullset? Is what
I'm trying to do even possible? Thanks
jerome