For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x))

1

1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) 4. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y 5. T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 6. T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) no_repeats(Vertices(the_graph);vertex-subset(the_obj;x.P(x))) & (x:Vertices(the_graph). (x vertex-subset(the_obj;x.P(x))) P(x))

3 steps

About: