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

At: dfl-traversal-consl 1 1

1. the_graph: Graph
2. L: Vertices(the_graph) List
3. i: Vertices(the_graph)
4. s: traversal(the_graph)
5. (inr(i) s)
6. dfl-traversal(the_graph;L;s)
7. i@0: Vertices(the_graph)
8. s2: traversal(the_graph)
9. j: Vertices(the_graph)
10. (inr(j) s2)
11. (inl(j) s2)
12. inl(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)
13. s = s2
j-the_graph- > *i@0

By: ObviousContradiction [-2]

Generated subgoals:

None

About:
listunioninlinrequal

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