L1,L2:V List, s:Traversal. L1-- > *L2 
dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)l:T List. (l @ nil) ~ lA,B:V List, i:V. A @ B-- > *i 
A-- > *i 
B-- > *iA,B,C:V List. A-- > *B B-- > *C A-- > *C| Rank | Theorem | Name |
| 4 | Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s) | [dfsl-traversal-append] |
| cites | ||
| 0 | Thm* l:T List. (l @ nil) ~ l | [append_nil_sq] |
| 3 | Thm* For any graph
A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i | [list-connect-append] |
| 0 | Thm* For any graph
A,B,C:V List. A-- > *B B-- > *C A-- > *C | [list-list-connect_transitivity] |