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

*To*: pvs-help@csl.sri.com*Subject*: Question on operator*From*: Raphael Couturier <Raphael.Couturier@loria.fr>*Date*: Fri, 10 Apr 1998 17:35:32 +0200*Sender*: Raphael.Couturier@loria.fr

Hello, My problem is the following: If I have the sequent A => B C ------- D To prove it, PVS gives 2 subgoals C -- A D and B C -- D I would like to know if another operator exists or if it is possible to define a new operator having the following behavior. I call op the operator. if we want to prove the sequent A op B C --- D I should prove the sequents -- A and B C -- D Thanks in advance for your help Raphael Couturier

- Prev by Date:
**Re: TYPE functions** - Next by Date:
**Re: Question on operator** - Prev by thread:
**Re: PVS on NT?** - Next by thread:
**Re: Question on operator** - Index(es):