[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
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,