problem with finite types

[Borzoo Bonakdarpour <borzoo@cse.msu.edu>]

Hi,

I am writing a specification to calculate the finite set of states, which
have a path to a particular state.  The spec looks like:

reachable[state : TYPE]: THEORY

  BEGIN

 ASSUMING

  IMPORTING state[state]

  SP_is_finite : ASSUMPTION is_finite_type[StatePred]
  AC_is_finite : ASSUMPTION is_finite_type[Action]

 ENDASSUMING

  s0, s1 : VAR state

  reverse_reachable_states(x : StatePred,  f : Action) : StatePred =
	(LAMBDA s0 : member(s0, x) AND (EXISTS (s1 : state) : member((s0, s1), f) AND member(s1, x)))

 fpcal (ms: StatePred, f: Action) : RECURSIVE StatePred =

     IF nonempty?(reverse_reachable_states(ms, f)) THEN
        fpcal (union(reverse_reachable_states(ms, f), ms), f)
	ELSE ms
	ENDIF

  MEASURE card(ms)

  END reachable

where StatePred : TYPE = PRED[state] and Action : TYPE = PRED[[state, state]]

I got a TCC:

% Subtype TCC generated (at line 26, column 15) for  ms
    % expected type  S: finite_set[state]
  % unfinished
fpcal_TCC1: OBLIGATION FORALL (ms: StatePred[state]):
is_finite[state](ms);

and I have reached this point in proof:

{-1}  is_finite_type[StatePred]
  |-------
[1]   is_finite[state](ms!1)

which looks very simple, but seems there is no way to prove it.  There
must be something wrong somewhere else.  Does anybody have any idea?

Thanks,
Borzoo


------------------------------------------------------------------------
Borzoo Bonakdarpour
Graduate Research Assistant
Department of Computer Science & Engineering
Michigan State University
E-mail: borzoo@cse.msu.edu
URL: http://www.cse.msu.edu/~borzoo