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

[PVS-Help] Help for a recursion TCC

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!