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

*To*: pvs-help@csl.sri.com*Subject*: help on finite sequences*From*: Venkatesh Phadnavis <vphadnav@eecs.ku.edu>*Date*: Sat, 11 Oct 2003 15:19:56 -0500 (CDT)*Sender*: pvs-help-owner@csl.sri.com

Hello, I am trying to prove a property about a finite_sequence that I build recursively: filter(fs: finite_sequence[T], k: below[fs`length], p: pred[T]): RECURSIVE finite_sequence = IF k = fs`length - 1 THEN IF p(fs`seq(k)) THEN (# length := 1, seq := LAMBDA(n: below[1]): fs`seq(k) #) ELSE empty_seq[T] ENDIF ELSE IF p(fs`seq(k)) THEN o((# length := 1, seq := LAMBDA(n: below[1]): fs`seq(k) #), filter(fs, k+1, p) ELSE filter(fs, k+1, p) ENDIF ENDIF MEASURE fs`length - k; every_filter: LEMMA FORALL (fs: finite_sequence[T], p: pred[T]): LET filtered_sequence = filter(fs, 0, p) IN FORALL (i: below[filtered_sequence`length]): p(filtered_sequence`seq(i)); Essentially I am trying to say that every element of the sequence that is built using filter(...) with predicate p satisfies the predicate p. This looks really easy to prove except that I am unable to extract the ith element of the filter(...) sequence, or the seq function that is being built up. Ignoring the TCCS for the moment, does anyone have any ideas about how to go about this proof? Thanks for your help, Venkatesh.

- Prev by Date:
**PVS/Cygwin** - Next by Date:
**Re: help on finite sequences** - Prev by thread:
**Re: Problem importing theories** - Next by thread:
**Re: help on finite sequences** - Index(es):