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

Re: [PVS-Help] cotuple proof




  Bingo!

Thanks,
Dave

"Jerry James" <loganjerry@xxxxxxxxx> wrote on 04/21/2008 01:55:15 PM:

> 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/