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

[PVS-Help] prop simplification of COND



Hi,

In the sequent of my proof the cond construction is one of the
antecedents:

COND c1 -> e1,
     c2 -> e2,
     ...
     cn -> en
ENDCOND

I want to split the sequent by splitting this formula into exactly n
branches corresponding to c1, c2, ..., that is, I don't want to do any
further prop simplification of e1, e2, en, because in that case there
would be more than n branches and some subgoals would share the same
proof. 

How do I do that?

Thanks.

Vera