p:V List. 1 < ||p|| 
path(the_graph;p) path(the_graph;tl(p))as:A List, n:
(||as||-1). tl(as)[n] = as[(n+1)]l:A List. ||l||
1 ||tl(l)|| = ||l||-1 
| Rank | Theorem | Name |
| 2 | Thm* For any graph
p:V List. 1 < ||p|| path(the_graph;p) path(the_graph;tl(p)) | [path-tl] |
| cites | ||
| 1 | Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] | [select_tl] |
| 0 | Thm* l:A List. ||l||1 ||tl(l)|| = ||l||-1 | [length_tl] |