| Theorem | Name |
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] |
| cites |
Thm* L:T List.  L = nil 0 < ||L|| | [non_nil_length] |
Thm* L:T List. 0 < ||L|| ( x:T, L':T List. L = (L' @ [x])) | [list_decomp_reverse] |
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   | [length_append] |
| Thm* l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2) | [list_accum_append] |