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

[PVS-Help] question about the list adt



I was playing around with the list adt in something I was doing, and 
expected to be able to prove the following lemma:

   putative3_1 : LEMMA ( cons(a, s) /= s )

... but was unable to do so.

Question: have I just failed to be able to prove something because of my 
lack of ability with PVS, or is this not a valid consequence of the list 
theory?

I believe that this should be a consequence of the theory, since 
length(s) = n implies length(cons(a, s) = n + 1.

But I don't see where the list_adt theory makes it impossible that the 
cons operator should have an identity.

Thank you for any guidance,
Best,
Robert