| Rank | Theorem | Name |
| 13 | Thm* For any graph
 the_obj:GraphObject(the_graph), P:((V List)  TraversalProp). P(nil,nil)   (L:V List, s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & P(L,dfsl(the_obj;L))) | [dfsl-induction2] |
| cites |
| 2 | Thm* l1,l2:T List. no_repeats(T;l1 @ l2)  l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) | [no_repeats_append_iff] |
| 1 | Thm* s',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s') | [append_paren] |
| 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* For any graph
the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. P(L,dfsl(the_obj;L))) | [dfsl-induction1] |