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

Re: [PVS-Help] prop simplification of COND



Vera,

Try something like 

(repeat (branch (split fnum)((skip)(flatten))))

where fnum is the formula number where the cond construction appears.

Cesar


On Wed, 2005-07-20 at 00:06, Vera Pantelic wrote:
> 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
>      
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988