| Rank | Theorem | Name |
| 19 | Thm* For any graph
 the_obj:GraphObject(the_graph). (non-trivial-loop-free(the_graph)   topsorted(the_graph;topsort(the_obj))) & (i:V. (i  topsort(the_obj))) & no_repeats(V;topsort(the_obj)) | [topsort-properties] |
| cites |
| 18 | Thm* For any graph
the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & df-traversal(the_graph;depthfirst(the_obj)) & depthfirst-traversal(the_graph;depthfirst(the_obj)) & (i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))) | [depthfirst-properties] |
| 3 | Thm* L:T List, x,y:T. x before y L  ( L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3)) | [l_before-iff] |
| 4 | Thm* P:(T   ), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L) | [mapfilter_before] |
| 3 | Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) | [member_mapoutl] |
| 4 | Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s)) | [no_repeats_mapoutl] |