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

*To*: <pvs-help@csl.sri.com>*Subject*: proving a property over finite_sets*From*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*Date*: Mon, 11 Aug 2003 16:20:08 -0400 (EDT)*Sender*: pvs-help-owner@csl.sri.com

Hi, I have been struggling to prove an easy-looking property of the following specification: state: TYPE f: finite_set[[state, state]] s0, s1: VAR state X: finite_set[state] set1(rs: finite_set[state]): finite_set[state] = {s0 | EXISTS (s1): (member(s1, rs) AND member((s0, s1), f))} func (fpSet: finite_set[state]) : RECURSIVE finite_set[state] = LET rs = set1(fpSet) IN IF nonempty?(rs) THEN func (union(rs, fpSet)) ELSE fpSet ENDIF MEASURE card(complement(fpSet)) prop: LEMMA FORALL(s0, s1): (member((s0, s1), f) AND member(s1, func(X))) IMPLIES member(s0, func(X)) I tried induction schemes on finite_Sets and mucalculs without any success. I appreciate if your share your thoughts on how to prove this with me. Thanks, Borzoo ------------------------------------------------------------------------ Borzoo Bonakdarpour Graduate Research Assistant 3115 Engineering Building Department of Computer Science & Engineering Michigan State University E-mail: borzoo@cse.msu.edu URL: http://www.cse.msu.edu/~borzoo

- Prev by Date:
**Re: "assertion itheory failed" error** - Next by Date:
**Re: proving a property over finite_sets** - Prev by thread:
**[pvs startup] Unable to locate enough free space...** - Next by thread:
**Re: proving a property over finite_sets** - Index(es):