# problem with finite types

```
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