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

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

At: dfs-df-traversal 2 2 2 1 2 1 1 3 1 2

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. z: Vertices(the_graph)
19. z = i1
20. i1-the_graph- > z
21. z-the_graph- > *j
22. (inl(z) s1) (inr(z) s1)

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

By: Inst Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) [Vertices(the_graph);s1;z] THEN Analyze -1

Generated subgoals:

1 23. x: Vertices(the_graph)
24. y: Vertices(the_graph)
Dec(x = y) 1 step

2 23. (inl(z) s1)
(inr(j) s2 @ [inr(i1) / s1]) 6 steps

3 23. (inl(z) s1)
(inr(j) s2 @ [inr(i1) / s1]) 1 step

About:

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

1	23. `x:` `Vertices(the_graph)` 24. `y:` `Vertices(the_graph)` `Dec(x = y)`	1 step

2	23. `(inl(z) s1)` `(inr(j) s2 @ [inr(i1) / s1])`	6 steps

3	23. `(inl(z) s1)` `(inr(j) s2 @ [inr(i1) / s1])`	1 step