L:V List, i:V, s:Traversal. (j:V. (inr(j) 
s) 
(inl(j) s) j-the_graph- > *i) L-- > *i dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inr(i) / s])l:T List, a,x:T. (x [a / l]) 
x = a 
(x l)| Rank | Theorem | Name |
| 2 | Thm* For any graph
L:V List, i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) L-- > *i dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inr(i) / s]) | [dfl-traversal-consr] |
| cites | ||
| 1 | Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |