Re: [PVS-Help] Set clarification

[Jerome White <jerome@xxxxxxxxxxxxxx>]

I see, so the fact that min returns a single real value is implicit?

On Sat, Jun 13, 2009 at 10:46:40AM -0700, Natarajan Shankar wrote:
>
>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
>