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

*To*: pvs-help@csl.sri.com*Subject*: another TCC question*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Sun, 3 Oct 1999 12:42:36 -0400 (EDT)

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

- Prev by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by Date:
**Rewriting** - Prev by thread:
**Rewriting** - Next by thread:
**Moving existential quantifiers out over universal quantifiers** - Index(es):