RE: [PVS-Help] R_pred

["Butler, Ricky W. (LARC-D320)" <R.W.Butler@xxxxxxxx>]

Not enough info -- it is equivalent to

   [-1]  W >= 0
   [-2]  P(W)
   [-3]  d >= 0
   [-4]  P(d)
     |-------
   [1]   P(d + W)

Knowing that a proposition is true at W and d is not
sufficient to prove it true at d+W

Rick

-----Original Message-----
From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
[mailto:pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf
Of Jerome
Sent: Thursday, November 06, 2008 6:34 PM
To: PVS Help
Subject: [PVS-Help] R_pred

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