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

*To*: PVS Help <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] R_pred*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Fri, 7 Nov 2008 12:55:25 -0800*In-reply-to*: <49144822.5010608@nianet.org>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20081106233402.GA16079@cs.caltech.edu> <49144822.5010608@nianet.org>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.5.9i

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 >

- Prev by Date:
**Re: [PVS-Help] R_pred** - Next by Date:
**Re: [PVS-Help] R_pred** - Prev by thread:
**Re: [PVS-Help] R_pred** - Next by thread:
**Re: [PVS-Help] R_pred** - Index(es):