# Re: [PVS-Help] Termination TCC

On Tue, Apr 22, 2008 at 6:24 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
All,
I have the following recursive definition:

example: THEORY BEGIN
index:   TYPE  = posnat
value:   TYPE  = real
indices: TYPE+ = 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

When I go to typecheck it, one of the TCC's it gives me is the
following:

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

Why isn't this proved with the "card_remove" theorem from the prelude?
I've tried to prove the obligation by hand, and bring in card_remove
manually, but PVS doesn't seem to know about it:

Rule? (lemma "card_remove")
Found 0 resolutions for card_remove relative to the substitution.

You need to supply the type parameter to the theory.  Try

(lemma "card_remove[index]")

[Also, if anyone knows of a better way to apply a binary function over
a set of values please speak up. For example, given the set {a, b, c,
d}, I'd like to return min(a, min(b, min(c, d))).]

Look at the finite_sets library.  In particular, finite_sets_sum seems to be pretty close to what you are looking for.
--
Jerry James