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

[PVS-Help] cotuple proof

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?

  I looked at an equivalent DATATYPE theory
and I don't  see how to do the equivalent proof
there, either.