| Rank | Theorem | Name |
| 13 | Thm* For any graph
 the_obj:GraphObject(the_graph), l:V List, s:Traversal.  s':Traversal. (i:V. (i  l)   (inl(i) s')  (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s) | [dfs_accum_member] |
| cites |
| 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* l:T List, a,x:T. (x [a / l])  x = a (x l) | [cons_member] |
| 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. (inr(i) s') (inl(i) s')) | [paren_balance2] |
| 3 | Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c) | [l_disjoint_append] |
| 3 | Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b) | [l_disjoint_append2] |
| 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] |
| 0 | Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) | [append_assoc] |