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

Re: [PVS-Help] cotuple proof



On Mon, Apr 21, 2008 at 10:51 AM,  <dagreve@xxxxxxxxxxxxxxxxxxx> wrote:
>
> I have defined a cotuple:
>
> co: TYPE = [ int + bool ]
>
> I would like to prove the following:
>
> proof: LEMMA
>   FORALL (x,y: int):
>     IN_1(x) = IN_1(y) IMPLIES (x = y)
>
> But I don't see how.  Is this possible?

Try (decompose-equality).
-- 
Jerry James
http://loganjerry.googlepages.com/