# Re: problem with finite types

```Borzoo Bonakdarpour wrote:
> 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
>

Hi,

The assumption is_finite_type[StatePred] specifies
that there are only finitely many functions of
type PRED[state]. That's sufficient to prove
that ms!1 is finite, but in an indirect way.

What you probably need to assume is that
there are finitely many states, that is,
"is_finite_type[state]".

Bruno
--
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

```