[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