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

[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