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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Termination TCC*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Tue, 22 Apr 2008 17:24:24 -0700*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

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. Any insight would be appreciated. jerome [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))).]

- Prev by Date:
**Re: [PVS-Help] What's the next step to prove it?** - Next by Date:
**Re: [PVS-Help] Termination TCC** - Prev by thread:
**Re: [PVS-Help] Expected type TCC** - Next by thread:
**Re: [PVS-Help] Termination TCC** - Index(es):