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

Re: [PVS-Help] question about the list adt

Robert Goldman <rpgoldman@sift.info> wrote:
> 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.

Here's a proof:

 (skolem + ("a" "_"))
 (induct "s")
 (("1" (assert)) ("2" (skosimp) (assert) (decompose-equality -))))

Jerry James, Assistant Professor        Jerry.James@usu.edu
Computer Science Department             http://www.cs.usu.edu/~jerry/
Utah State University