[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] cotuple proof
"Jerry James" <loganjerry@xxxxxxxxx>
wrote on 04/21/2008 01:55:15 PM:
> On Mon, Apr 21, 2008 at 10:51 AM, <dagreve@xxxxxxxxxxxxxxxxxxx>
> > 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