| Rank | Theorem | Name |
| 14 | Thm* For any graph
 the_obj:GraphObject(the_graph), s:Traversal, i:V.  s':Traversal. ((inr(i)  s)  (inl(i) s)   s' = nil) & ( (inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & 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-properties] |
| cites |
| 13 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & dfs(the_obj;s;i) = (s' @ s) | [dfs-cases] |
| 12 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s) | [dfs-connect] |
| 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] |
| 2 | Thm* x,y,z:T List. (x @ z) = (y @ z)  x = y | [equal_append_front] |
| 1 | Thm* x1,z,x2,x3:T List. ||x1|| = ||z||  (x1 @ x2) = (z @ x3) x1 = z & x2 = x3 | [equal_appends_eq] |
| 0 | Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |