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

At: dfl-traversal-consl
For any graph L:V List, i:V, s:Traversal. (inr(i) s) dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inl(i) / s])
By:
Auto
THEN
Unfold `dfl-traversal` 0
Generated subgoals:

11. 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. s1: traversal(the_graph)
9. s2: traversal(the_graph)
10. [inl(i) / s] = (s1 @ [inr(i@0)] @ s2) traversal(the_graph)
11. j: Vertices(the_graph)
12. (inr(j) s2)
13. (inl(j) s2)
j-the_graph- > *i@0		3 steps
 
21. 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. j: Vertices(the_graph)
8. (inr(j) [inl(i) / s])
L-the_graph- > *j		3 steps
 
31. 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. s1: traversal(the_graph)
9. s2: traversal(the_graph)
10. j:Vertices(the_graph). i@0-the_graph- > *j non-trivial-loop(the_graph;j)
11. [inl(i) / s] = (s1 @ [inl(i@0)] @ s2) traversal(the_graph)
L-the_graph- > *i@0		3 steps

About:
listconsunioninlinrimpliesall

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