```Hi Robert,

The following is a proof script (in ProofLite format) that discharges
this lemma using the length function.

%|- putative3_1 : PROOF
%|- (then (skosimp)
%|-  (spread (case "length(cons(a!1, s!1)) = length(s!1)")
%|-   ((grind) (assert))))
%|- QED

There are many ways to prove this lemma. Note, for example, that << is
well_founded order and that s << cons(x,s), therefore s /= cons(x,s).

Hope that this helps,
Cesar

On Thu, 2007-04-12 at 16:07, Robert Goldman 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.
>
> 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
--
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4

```