Nuprl - Proof: dfs-df-traversal 2 2 2 1 2 1 1

(44steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s1: traversal(the_graph)
4. s2: traversal(the_graph)
5. i1: Vertices(the_graph)
6. (inr(i1) s1)
7. (inl(i1) s1)
8. paren(Vertices(the_graph);s2)
9. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
10. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
11. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
12. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) (inl(j) s1) (inr(j) s1)
13. df-traversal(the_graph;s1)
14. j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i1
15. df-traversal(the_graph;s2 @ [inr(i1) / s1])
16. j:Vertices(the_graph). i1-the_graph- > *j non-trivial-loop(the_graph;j)
17. j: Vertices(the_graph)
18. i1-the_graph- > *j

(inr(j) s2 @ [inr(i1) / s1])

By: RWO Thm* For any graph (x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y)) -1 THEN SplitOrHyps

Generated subgoals:

1 19. x: Vertices(the_graph)
20. y: Vertices(the_graph)
Dec(x = y) 1 step

2 18. i1 = j
(inr(j) s2 @ [inr(i1) / s1]) 1 step

3 18. z:Vertices(the_graph). z = i1 & i1-the_graph- > z & z-the_graph- > *j
(inr(j) s2 @ [inr(i1) / s1]) 17 steps

About:

(44steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

1	19. `x:` `Vertices(the_graph)` 20. `y:` `Vertices(the_graph)` `Dec(x = y)`	1 step

2	18. `i1 = j` `(inr(j) s2 @ [inr(i1) / s1])`	1 step

3	18. `z:Vertices(the_graph). z = i1 & i1-the_graph- > z & z-the_graph- > *j` `(inr(j) s2 @ [inr(i1) / s1])`	17 steps