| Rank | Theorem | Name |
| 18 | Thm* For any graph
 the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & df-traversal(the_graph;depthfirst(the_obj)) & depthfirst-traversal(the_graph;depthfirst(the_obj)) & (i:V. (inr(i)  depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))) | [depthfirst-properties] |
| cites |
| 5 | Thm* G:Graph. (x,y:Vertices(G). Dec(x = y))   (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s)) | [paren-df-traversal] |
| 17 | Thm* For any graph
the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj)) | [depthfirst-df-traversal] |
| 15 | Thm* For any graph
the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) | [depthfirst_paren] |
| 15 | Thm* For any graph
the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)) | [depthfirst_member] |
| 1 | Thm* For any graph
the_obj:GraphObject(the_graph), x,y:V. Dec(x = y) | [decidable__equal_gr_v] |