Re: [PVS-Help] Set clarification

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

Jerome: The set {p: real | p <= m AND p <= n} corresponds to the return
type so that the return value is an element of this set.

-Shankar

Jerome White <jerome@cs.caltech.edu> wrote:

Jerome White <jerome@cs.caltech.edu> wrote:

> The definition of min (from the prelude) is as follows:
> 
>   min(m, n): {p: real | p <= m AND p <= n}
>     = IF m > n THEN n ELSE m ENDIF
> 
> where m and n are real numbers. My confusion is with respect to the
> return type: it appears to me that min returns a set of real
> numbers. Am I reading this correctly? If so, how is it that when used,
> PVS knows the return type is a single value? For example
> 
>   min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c)
> 
> Thanks
> 
> jerome