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

[PVS-Help] Flatten VS Split



Hello,
I have a very simple questions. Given the following subgoal:

{-1}  (p AND r)
  |-------
[1]   q
[2]   r

Trivially, you could use "& out" on line {-1} which should result in the
following:

{-1}  p
{-2}  r
  |-------
[1]   q
[2]   r

I belive this require issuing the (split -1) conjunctive command.  However
that doesn't work. On the other hand, Flatten works fine. Why is that?
Thank you,
Ahmed