Nuprl - Proof: dfl-traversal-consr

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

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])

By: Unfold `dfl-traversal` 0

Generated subgoals:

1 1. the_graph: Graph
2. L: Vertices(the_graph) List
3. i: Vertices(the_graph)
4. s: traversal(the_graph)
5. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
6. L-the_graph- > *i
7. i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)
8. j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j
9. i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i
10. i@0: Vertices(the_graph)
11. s1: traversal(the_graph)
12. s2: traversal(the_graph)
13. [inr(i) / s] = (s1 @ [inr(i@0)] @ s2) traversal(the_graph)
14. j: Vertices(the_graph)
15. (inr(j) s2)
16. (inl(j) s2)
j-the_graph- > *i@0 5 steps

2 1. the_graph: Graph
2. L: Vertices(the_graph) List
3. i: Vertices(the_graph)
4. s: traversal(the_graph)
5. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
6. L-the_graph- > *i
7. i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)
8. j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j
9. i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i
10. j: Vertices(the_graph)
11. (inr(j) [inr(i) / s])
L-the_graph- > *j 2 steps

3 1. the_graph: Graph
2. L: Vertices(the_graph) List
3. i: Vertices(the_graph)
4. s: traversal(the_graph)
5. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
6. L-the_graph- > *i
7. i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)
8. j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j
9. i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i
10. i@0: Vertices(the_graph)
11. s1: traversal(the_graph)
12. s2: traversal(the_graph)
13. j:Vertices(the_graph). i@0-the_graph- > *j non-trivial-loop(the_graph;j)
14. [inr(i) / s] = (s1 @ [inl(i@0)] @ s2) traversal(the_graph)
L-the_graph- > *i@0 3 steps

About:

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

1	1. `the_graph:` `Graph` 2. `L:` `Vertices(the_graph) List` 3. `i:` `Vertices(the_graph)` 4. `s:` `traversal(the_graph)` 5. `j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > i` 6. `L-the_graph- > i` 7. `i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > i)` 8. `j:Vertices(the_graph). (inr(j) s) L-the_graph- > j` 9. `i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > i` 10. `i@0:` `Vertices(the_graph)` 11. `s1:` `traversal(the_graph)` 12. `s2:` `traversal(the_graph)` 13. `[inr(i) / s] = (s1 @ [inr(i@0)] @ s2) traversal(the_graph)` 14. `j:` `Vertices(the_graph)` 15. `(inr(j) s2)` 16. `(inl(j) s2)` `j-the_graph- > *i@0`	5 steps

2	1. `the_graph:` `Graph` 2. `L:` `Vertices(the_graph) List` 3. `i:` `Vertices(the_graph)` 4. `s:` `traversal(the_graph)` 5. `j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > i` 6. `L-the_graph- > i` 7. `i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > i)` 8. `j:Vertices(the_graph). (inr(j) s) L-the_graph- > j` 9. `i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > i` 10. `j:` `Vertices(the_graph)` 11. `(inr(j) [inr(i) / s])` `L-the_graph- > *j`	2 steps

3	1. `the_graph:` `Graph` 2. `L:` `Vertices(the_graph) List` 3. `i:` `Vertices(the_graph)` 4. `s:` `traversal(the_graph)` 5. `j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > i` 6. `L-the_graph- > i` 7. `i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > i)` 8. `j:Vertices(the_graph). (inr(j) s) L-the_graph- > j` 9. `i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > i` 10. `i@0:` `Vertices(the_graph)` 11. `s1:` `traversal(the_graph)` 12. `s2:` `traversal(the_graph)` 13. `j:Vertices(the_graph). i@0-the_graph- > j non-trivial-loop(the_graph;j)` 14. `[inr(i) / s] = (s1 @ [inl(i@0)] @ s2) traversal(the_graph)` `L-the_graph- > i@0`	3 steps