| Rank | Theorem | Name |
| 14 | Thm* For any graph
 the_obj:GraphObject(the_graph), L:V List. (i L.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) | [dfsl_member] |
| cites |
| 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] |
| 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] |
| 0 | Thm* a,x:T. (x [a])  x = a | [member_singleton] |
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s')) | [paren_balance1] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) | [paren_balance2] |