Nuprl - Proof: topsort-properties 1 1

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. paren(Vertices(the_graph);depthfirst(the_obj))
4. no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj))
5. df-traversal(the_graph;depthfirst(the_obj))
6. depthfirst-traversal(the_graph;depthfirst(the_obj))
7. i:Vertices(the_graph). (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))
8. non-trivial-loop-free(the_graph)
9. i: Vertices(the_graph)
10. j: Vertices(the_graph)
11. i-the_graph- > *j
12. i = j

i before j topsort(the_obj)

By: Assert inl(i) before inl(j) depthfirst(the_obj)

Generated subgoals:

1 inl(i) before inl(j) depthfirst(the_obj) 5 steps

2 13. inl(i) before inl(j) depthfirst(the_obj)
i before j topsort(the_obj) 1 step

About:

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

1	`inl(i) before inl(j) depthfirst(the_obj)`	5 steps

2	13. `inl(i) before inl(j) depthfirst(the_obj)` `i before j topsort(the_obj)`	1 step