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

*To*: Robert Goldman <rpgoldman@xxxxxxxxx>*Subject*: Re: [work] [PVS-Help] question about the list adt*From*: "Cesar A. Munoz" <munoz@xxxxxxxxxx>*Date*: Thu, 12 Apr 2007 16:58:16 -0400*Cc*: "Cesar A. Munoz" <munoz@xxxxxxxxxx>, PVS help list <pvs-help@xxxxxxxxxxx>*In-Reply-To*: <461E9171.5010904@sift.info>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Organization*: NIA*References*: <461E9171.5010904@sift.info>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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

**References**:**[PVS-Help] question about the list adt***From:*Robert Goldman

- Prev by Date:
**[PVS-Help] question about the list adt** - Next by Date:
**Re: [PVS-Help] question about the list adt** - Prev by thread:
**[PVS-Help] question about the list adt** - Next by thread:
**Re: [PVS-Help] question about the list adt** - Index(es):