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

proving a property over finite_sets




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