Re: [PVS-Help] R_pred

[Jerome <jerome@xxxxxxxxxxxxxx>]

I think my problem comes from a misunderstanding as to what R_pred
actually is. One of the parameters of my theory is 'R', which is a
numeric type:

  R: TYPE FROM nnreal

Within the theory, distance and W are functions from some type to R:

  distance: [D -> R]
  W: [D, D -> R]

Thus, to discharge [1] do I need to show that the addition of two
non-negative real numbers is still a non-negative real number? My
original question stems more from surprise (and lazyness) that this
wasn't taken care of by some prelude magic :)

Is this what [1] wants me to show? And, in general, how do I interpret
the _pred convention? Thanks

jerome

On Fri, Nov 07, 2008 at 08:52:34AM -0500, Cesar Munoz wrote:
>Why should it work ? What is the definition of R?  For an arbitrary R,
>the fact that R(x) and R(y) hold doesn't imply that R(x+y) holds. Take
>R=odd? for example.
>
>
>Jerome wrote:
>> I have the following:
>> 
>>    [-1]  W(root, j!1) >= 0
>>    [-2]  R_pred(W(root, j!1))
>>    [-3]  distance(s!1)(root) >= 0
>>    [-4]  R_pred(distance(s!1)(root))
>>      |-------
>>    [1]   R_pred(distance(s!1)(root) + W(root, j!1))
>> 
>> Why is "assert" not an adequate means of discharging? What am I
>> missing? Thanks
>> 
>> jerome
>> 
>> 
>
>-- 
>Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
>National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
>100 Exploration Way  Room 214       http://research.nianet.org/~munoz
>Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
>GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4
>