(13steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: dfsl-traversal-nil 3 4
1. the_graph: Graph
2. j: Vertices(the_graph)
3. nil-the_graph- > *j
(inl(j) nil)
By:
Analyze -1
THEN
Analyze -1
Generated subgoal:

13. y: Vertices(the_graph)
4. (y nil)
5. y-the_graph- > *j
(inl(j) nil)		1 step

About:
nilunioninl

(13steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc