|
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! |