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

RE: [PVS-Help] fullset type properties

All of the properties of "fullest" are available via "expand".  The
heart of issue is the definition of "Index".  You will probably have to
go to the first principles of "is_finite" and provide an injective
function from
(Index) -> below[N] or use "is_finite_surj" and provide a surjective
function from below[N] -> (Index).


> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of Jerome
> Sent: Saturday, June 28, 2008 11:44 PM
> To: pvs-help@xxxxxxxxxxx
> Subject: [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