Re: [PVS-Help] Expected type TCC

[Jerome <jerome@xxxxxxxxxxxxxx>]

I have a similar recursive definition presented in my earlier email:

>example: THEORY BEGIN
>  index:   TYPE  = posnat
>  value:   TYPE  = real
>  indices: TYPE  = non_empty_finite_set[index]
>  myset:   TYPE  = [index -> value]
>  fun:     TYPE  = FUNCTION[value, value -> value]
>
>  curry(f: fun, m: myset, I: indices): RECURSIVE value =
>    LET i: index = choose(I) IN
>      IF singleton?(I) THEN m(i)
>      ELSE f(m(i), curry(f, m, remove(i, I)))
>      ENDIF
>  MEASURE card(I)
>END example

My question, again, is in regards to the TCC's generated. In my last
email, I asked about TCC2; this time I could use some help with TCC1:

curry_TCC1: OBLIGATION
  FORALL (I: indices, i: index):
    NOT singleton?(I) AND i = choose(I) IMPLIES
     NOT empty?[index](remove[index](i, I));

Using finite_sets_sum as an example (as Jerry had mentioned), a
similar TCC is discharge using '(SUBTYPE-TCC)'. Unfortunately,
applying the same rule to my curry_TCC1 isn't as successful.

What exactly does SUBTYPE-TCC do (that it's so successful in the
finite_sets_sum case)? Is there a similar method I can use in my case?
Thanks again.

jerome