| Rank | Theorem | Name |
| 17 | Thm* For any graph
 the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj)) | [depthfirst-df-traversal] |
| cites |
| 2 | Thm* For any graph
the_obj:GraphObject(the_graph), P:(Traversal  Prop). P(nil)   (s:Traversal, i:V. P(s) P(dfs(the_obj;s;i))) P(depthfirst(the_obj)) | [depthfirst_induction] |
| 0 | Thm* For any graph
df-traversal(the_graph;nil) | [df-traversal-nil] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i)  s') (inl(i) s')) | [paren_balance2] |
| 16 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V. df-traversal(the_graph;s) (j:V. (inr(j) s)  (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;dfs(the_obj;s;i)) | [dfs-df-traversal] |
| 12 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V.  s':Traversal. (inl(i) s')  (inl(i) s) (inr(i) s) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & dfs(the_obj;s;i) = (s' @ s) | [dfs_member] |
| 1 | Thm* s',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s') | [append_paren] |