Nuprl - graph_1_3 Citations of topsorted

graph 1 3 Sections Graphs Doc

Def topsorted(the_graph;s) ==

i,j:Vertices(the_graph). i-the_graph- > *j

i = j

i before j

is mentioned by

Thm* For any graph the_obj:GraphObject(the_graph). L:V List. (non-trivial-loop-free(the_graph) topsorted(the_graph;L)) & (i:V. (i L)) & no_repeats(V;L) [topsort-exists]

Thm* For any graph the_obj:GraphObject(the_graph). (non-trivial-loop-free(the_graph) topsorted(the_graph;topsort(the_obj))) & (i:V. (i topsort(the_obj))) & no_repeats(V;topsort(the_obj)) [topsort-properties]

Try larger context: Graphs

graph 1 3 Sections Graphs Doc

`Thm* For any graph the_obj:GraphObject(the_graph). L:V List. (non-trivial-loop-free(the_graph) topsorted(the_graph;L)) & (i:V. (i L)) & no_repeats(V;L)`	[topsort-exists]
`Thm* For any graph the_obj:GraphObject(the_graph). (non-trivial-loop-free(the_graph) topsorted(the_graph;topsort(the_obj))) & (i:V. (i topsort(the_obj))) & no_repeats(V;topsort(the_obj))`	[topsort-properties]