| Rank | Theorem | Name |
| 18 | Thm* For any graph
 the_obj:GraphObject(the_graph), L:V List. (i:V. (i  L))   (non-trivial-loop-free(the_graph) topsortedl(the_graph;L;topsortl(the_obj;L))) & (i:V. (i topsortl(the_obj;L))) & no_repeats(V;topsortl(the_obj;L)) | [topsortl-properties] |
| cites |
| 17 | Thm* For any graph
the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) | [dfsl-properties] |
| 4 | Thm* s:(A+B) List, x:A. (x mapoutl(s))  (inl(x) s) | [mapoutl_member] |
| 5 | Thm* G:Graph. (x,y:Vertices(G). Dec(x = y)) (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s)) | [paren-df-traversal] |
| 1 | Thm* L:(A+B) List, a:A. mapoutl(L) = [a] ( L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil) | [mapoutl_is_singleton] |
| 1 | Thm* L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2) | [mapoutl_is_append] |
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1)  (x l2) | [member_append] |
| 0 | Thm* L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2)) | [mapoutl_append] |
| 6 | Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B)) | [l_before_decomp] |
| 0 | Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) | [append_assoc_sq] |
| 3 | Thm* For any graph
i,j:V. [i]-- > *j i-the_graph- > *j | [list-connect-singleton] |
| 3 | Thm* For any graph
A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i | [list-connect-append] |
| 1 | Thm* x,y:T, L:T List. (x L) (y L) x = y x before y L y before x L | [l_tricotomy] |
| 1 | Thm* For any graph
the_obj:GraphObject(the_graph), x,y:V. Dec(x = y) | [decidable__equal_gr_v] |
| 3 | Thm* l:T List, x,y,z:T. no_repeats(T;l) x before y l y before z l x before z l | [l_before_transitivity] |
| 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] |