Nuprl - Proof: df-traversal-cons2

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

For any graph i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;s) df-traversal(the_graph;[inr(i) / s])

By: Unfold `df-traversal` 0

Generated subgoals:

1 1. the_graph: Graph
2. i: Vertices(the_graph)
3. s: traversal(the_graph)
4. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
5. 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)
6. 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) (j:Vertices(the_graph). i-the_graph- > *j (inr(j) s2))
7. i@0: Vertices(the_graph)
8. s1: traversal(the_graph)
9. s2: traversal(the_graph)
10. [inr(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 6 steps

2 1. the_graph: Graph
2. i: Vertices(the_graph)
3. s: traversal(the_graph)
4. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *i
5. 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)
6. 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) (j:Vertices(the_graph). i-the_graph- > *j (inr(j) s2))
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. [inr(i) / s] = (s1 @ [inl(i@0)] @ s2) traversal(the_graph)
12. j: Vertices(the_graph)
13. i@0-the_graph- > *j
(inr(j) s2) 3 steps

About:

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

1	1. `the_graph:` `Graph` 2. `i:` `Vertices(the_graph)` 3. `s:` `traversal(the_graph)` 4. `j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > i` 5. `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)` 6. `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) (j:Vertices(the_graph). i-the_graph- > j (inr(j) s2))` 7. `i@0:` `Vertices(the_graph)` 8. `s1:` `traversal(the_graph)` 9. `s2:` `traversal(the_graph)` 10. `[inr(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`	6 steps

2	1. `the_graph:` `Graph` 2. `i:` `Vertices(the_graph)` 3. `s:` `traversal(the_graph)` 4. `j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > i` 5. `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)` 6. `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) (j:Vertices(the_graph). i-the_graph- > j (inr(j) s2))` 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. `[inr(i) / s] = (s1 @ [inl(i@0)] @ s2) traversal(the_graph)` 12. `j:` `Vertices(the_graph)` 13. `i@0-the_graph- > j` `(inr(j) s2)`	3 steps