[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

another TCC question

I have a theory in which I introduce a few types, and one operation; here
are the relevant types:

VERTEX_PAIR : TYPE+ = {x: finite_set[nat]| 0 < card(x) and card(x) < 3}

EDGE : TYPE = [# pair: VERTEX_PAIR, wt: nat #]

GRAPH : TYPE = finite_set[EDGE]

I then define the following operation:

g, g_result: VAR GRAPH
v1, v2, w: VAR nat

GotByIncluding(v1, v2, w, g, g_result): bool =
    (g_result = union(g, singleton((# pair := {v: nat| v=v1 or v=v2},
                                      wt := old_w
                                    #))
                      ))

When I typecheck the theory, this definition generates an unprovable TCC,
namely:

Insert_TCC1: OBLIGATION
  (FORALL (x: [# pair: [nat -> bool], wt: nat #]): TRUE) AND
   (FORALL (x: [nat -> bool]):
      is_finite[nat](x) AND 0 < card[nat](x) AND card[nat](x) < 3);

Why is the second universal in this conjunctive TCC getting generated? I'm
being asked to show that any predicate on the naturals is finite and
between 0 and 3 in size???  There's probably some obvious point I'm
missing, but I'm not seeing it.

Anyone to the rescue?

Mark Aronszajn
WVU-RSRG