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

["Miner, Paul S." <paul.s.miner@xxxxxxxx>]

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

Kelly,

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

Paul


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

I am having difficulty proving the below TCC:
 
 
set_Node_TCC2: OBLIGATION
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
 
Thanks
Kelly
 
 

---

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