| Rank | Theorem | Name |
| 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] |
| cites |
| 0 | Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) | [append_assoc_sq] |
| 15 | Thm* For any graph
the_obj:GraphObject(the_graph), P:(V  TraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s)  (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) (k:V. (inr(k) s2) j-the_graph- > *k) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inr(i) s1) (inl(i) s1) paren(V;s2) l_disjoint(V+V;s2;s1) no_repeats(V+V;s2) (j:V. (inr(j) s2) i-the_graph- > *j) (j:V. i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) ( s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)) | [dfs_induction4] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) | [paren_balance2] |
| 0 | Thm* For any graph
i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;s) df-traversal(the_graph;[inr(i) / s]) | [df-traversal-cons2] |
| 3 | Thm* For any graph
(x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y  x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y)) | [connect-iff] |
| 3 | Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) | [decidable__l_member_paren] |
| 0 | Thm* For any graph
the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y) x = y) & (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)) | [graphobj-properties] |
| 2 | Thm* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2])) | [l_member_decomp] |
| 0 | Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) | [append_assoc] |
| 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] |