Nuprl - Proof: dfs-connect

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

For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)

By: Auto THEN Inst Thm* dfs_induction2 [the_graph;the_obj;i,s1,s2. j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j;s;i]

Generated subgoals:

1 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s1: traversal(the_graph)
6. i1: Vertices(the_graph)
7. (inl(i1) s1) (inr(i1) s1)
8. j: Vertices(the_graph)
9. (inr(j) nil)
i1-the_graph- > *j 1 step

2 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s1: traversal(the_graph)
6. s2: traversal(the_graph)
7. s3: traversal(the_graph)
8. i1: Vertices(the_graph)
9. j: Vertices(the_graph)
10. i1-the_graph- > j
11. paren(Vertices(the_graph);s2)
12. paren(Vertices(the_graph);s3)
13. j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > *j@0
14. j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > *j
15. j1: Vertices(the_graph)
16. (inr(j1) s3 @ s2)
i1-the_graph- > *j1 2 steps

3 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s1: traversal(the_graph)
6. s2: traversal(the_graph)
7. i1: Vertices(the_graph)
8. (inl(i1) s1)
9. (inr(i1) s1)
10. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
11. j: Vertices(the_graph)
12. (inr(j) [inl(i1) / (s2 @ [inr(i1)])])
i1-the_graph- > *j 6 steps

4 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s':traversal(the_graph). (j:Vertices(the_graph). (inr(j) s') i-the_graph- > *j) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & dfs(the_obj;s;i) = (s' @ s)
s':traversal(the_graph). (j:Vertices(the_graph). (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s) 1 step

About:

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

1	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s1:` `traversal(the_graph)` 6. `i1:` `Vertices(the_graph)` 7. `(inl(i1) s1) (inr(i1) s1)` 8. `j:` `Vertices(the_graph)` 9. `(inr(j) nil)` `i1-the_graph- > *j`	1 step

2	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s1:` `traversal(the_graph)` 6. `s2:` `traversal(the_graph)` 7. `s3:` `traversal(the_graph)` 8. `i1:` `Vertices(the_graph)` 9. `j:` `Vertices(the_graph)` 10. `i1-the_graph- > j` 11. `paren(Vertices(the_graph);s2)` 12. `paren(Vertices(the_graph);s3)` 13. `j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > j@0` 14. `j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > j` 15. `j1:` `Vertices(the_graph)` 16. `(inr(j1) s3 @ s2)` `i1-the_graph- > *j1`	2 steps

3	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s1:` `traversal(the_graph)` 6. `s2:` `traversal(the_graph)` 7. `i1:` `Vertices(the_graph)` 8. `(inl(i1) s1)` 9. `(inr(i1) s1)` 10. `j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > j` 11. `j:` `Vertices(the_graph)` 12. `(inr(j) [inl(i1) / (s2 @ [inr(i1)])])` `i1-the_graph- > j`	6 steps

4	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s':traversal(the_graph). (j:Vertices(the_graph). (inr(j) s') i-the_graph- > j) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & dfs(the_obj;s;i) = (s' @ s)` `s':traversal(the_graph). (j:Vertices(the_graph). (inr(j) s') i-the_graph- > j) & dfs(the_obj;s;i) = (s' @ s)`	1 step