Re: [PVS-Help] cotuple proof

[dagreve@xxxxxxxxxxxxxxxxxxx]

  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/