[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Question on operator
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