graph
1
2
Sections
Graphs
Doc
Theorem
Name
Thm*
For any graph dfsl-traversal(the_graph;nil;nil)
[dfsl-traversal-nil]
cites
Thm*
l1,l2:T List. (l1 @ l2) = nil
l1 = nil & l2 = nil
[append_is_nil]
graph
1
2
Sections
Graphs
Doc
l1,l2:T List. (l1 @ l2) = nil 
l1 = nil & l2 = nill1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil