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

Re: [PVS-Help] Help for a recursion TCC

Title: Re: [PVS-Help] Help for a recursion TCC

My suspicion is that (skosimp*)(rewrite “card_remove[Entity]”)(assert) should work.


On 10/31/07 9:12 PM, "K McElroy" <k_k_m@hotmail.com> wrote:

I am having difficulty proving the below TCC:
FORALL (v: finite_set[Entity]):
NOT empty?(v) IMPLIES
(FORALL (a: (v)):
a = choose(v) IMPLIES
card[Entity](remove[Entity](a, v)) < card[Entity](v));
My PVS code looks like:
%initializes all nodes
set_Node(c: L_Graph, v: finite_set[Entity], n: n_db): recursive L_Graph =
if empty?(v)then c
else let a = choose(v) in set_Node(c, remove(a,v), Node_ops(c`Node,c,a, outgoing_edges(a, c`g)))
endif measure card(v)
As far as I can tell my recursion function should work, so maybe I'm just not using the right proving commands.
Any help would be greatly appreciated

Peek-a-boo FREE Tricks  Treats for You! Get 'em! <http://www.reallivemoms.com?ocid=TXT_TAGHM&loc=us>