[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