Nuprl - Proof: df-traversal-cons2 1 1

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

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. s2: traversal(the_graph)
9. [inr(i) / s] = [inr(i@0) / s2]
10. j: Vertices(the_graph)
11. (inr(j) s2)
12. (inl(j) s2)

j-the_graph- > *i@0

By: SplitCons -4 THEN Subst (i@0 = i) 0

Generated subgoals:

1 9. j: Vertices(the_graph)
10. (inr(j) s2)
11. (inl(j) s2)
12. inr(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)
13. s = s2
i@0 = i 1 step

2 9. j: Vertices(the_graph)
10. (inr(j) s2)
11. (inl(j) s2)
12. inr(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)
13. s = s2
j-the_graph- > *i 1 step

About:

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

1	9. `j:` `Vertices(the_graph)` 10. `(inr(j) s2)` 11. `(inl(j) s2)` 12. `inr(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)` 13. `s = s2` `i@0 = i`	1 step

2	9. `j:` `Vertices(the_graph)` 10. `(inr(j) s2)` 11. `(inl(j) s2)` 12. `inr(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)` 13. `s = s2` `j-the_graph- > *i`	1 step