Nuprl - Proof: dfs-properties

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

For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)

By: Auto THEN Inst Thm* dfs_member [the_graph;the_obj;s;i] THEN Inst Thm* 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) [the_graph;the_obj;s;i] THEN Inst Thm* dfs-cases [the_graph;the_obj;s;i] THEN ExRepD THEN InstConcl [s2]

Generated subgoals:

1 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s2: traversal(the_graph)
6. (inl(i) s2) (inl(i) s) (inr(i) s)
7. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)
8. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
9. paren(Vertices(the_graph);s2)
10. dfs(the_obj;s;i) = (s2 @ s)
11. s1: traversal(the_graph)
12. j:Vertices(the_graph). (inr(j) s1) i-the_graph- > *j
13. dfs(the_obj;s;i) = (s1 @ s)
14. s': traversal(the_graph)
15. (inr(i) s) (inl(i) s) s' = nil
16. (inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
17. dfs(the_obj;s;i) = (s' @ s)
18. (inr(i) s) (inl(i) s)
s2 = nil 4 steps

2 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s2: traversal(the_graph)
6. (inl(i) s2) (inl(i) s) (inr(i) s)
7. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)
8. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
9. paren(Vertices(the_graph);s2)
10. dfs(the_obj;s;i) = (s2 @ s)
11. s1: traversal(the_graph)
12. j:Vertices(the_graph). (inr(j) s1) i-the_graph- > *j
13. dfs(the_obj;s;i) = (s1 @ s)
14. s': traversal(the_graph)
15. (inr(i) s) (inl(i) s) s' = nil
16. (inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
17. dfs(the_obj;s;i) = (s' @ s)
18. (inr(i) s)
19. (inl(i) s)
s2@0:traversal(the_graph). s2 = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph) 4 steps

3 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s2: traversal(the_graph)
6. (inl(i) s2) (inl(i) s) (inr(i) s)
7. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)
8. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
9. paren(Vertices(the_graph);s2)
10. dfs(the_obj;s;i) = (s2 @ s)
11. s1: traversal(the_graph)
12. j:Vertices(the_graph). (inr(j) s1) i-the_graph- > *j
13. dfs(the_obj;s;i) = (s1 @ s)
14. s': traversal(the_graph)
15. (inr(i) s) (inl(i) s) s' = nil
16. (inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
17. dfs(the_obj;s;i) = (s' @ s)
18. j: Vertices(the_graph)
19. (inr(j) s2)
i-the_graph- > *j 5 steps

About:

(14steps 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. `s2:` `traversal(the_graph)` 6. `(inl(i) s2) (inl(i) s) (inr(i) s)` 7. `l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)` 8. `no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)` 9. `paren(Vertices(the_graph);s2)` 10. `dfs(the_obj;s;i) = (s2 @ s)` 11. `s1:` `traversal(the_graph)` 12. `j:Vertices(the_graph). (inr(j) s1) i-the_graph- > *j` 13. `dfs(the_obj;s;i) = (s1 @ s)` 14. `s':` `traversal(the_graph)` 15. `(inr(i) s) (inl(i) s) s' = nil` 16. `(inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))` 17. `dfs(the_obj;s;i) = (s' @ s)` 18. `(inr(i) s) (inl(i) s)` `s2 = nil`	4 steps

2	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s2:` `traversal(the_graph)` 6. `(inl(i) s2) (inl(i) s) (inr(i) s)` 7. `l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)` 8. `no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)` 9. `paren(Vertices(the_graph);s2)` 10. `dfs(the_obj;s;i) = (s2 @ s)` 11. `s1:` `traversal(the_graph)` 12. `j:Vertices(the_graph). (inr(j) s1) i-the_graph- > *j` 13. `dfs(the_obj;s;i) = (s1 @ s)` 14. `s':` `traversal(the_graph)` 15. `(inr(i) s) (inl(i) s) s' = nil` 16. `(inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))` 17. `dfs(the_obj;s;i) = (s' @ s)` 18. `(inr(i) s)` 19. `(inl(i) s)` `s2@0:traversal(the_graph). s2 = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph)`	4 steps

3	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `s:` `traversal(the_graph)` 4. `i:` `Vertices(the_graph)` 5. `s2:` `traversal(the_graph)` 6. `(inl(i) s2) (inl(i) s) (inr(i) s)` 7. `l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)` 8. `no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)` 9. `paren(Vertices(the_graph);s2)` 10. `dfs(the_obj;s;i) = (s2 @ s)` 11. `s1:` `traversal(the_graph)` 12. `j:Vertices(the_graph). (inr(j) s1) i-the_graph- > j` 13. `dfs(the_obj;s;i) = (s1 @ s)` 14. `s':` `traversal(the_graph)` 15. `(inr(i) s) (inl(i) s) s' = nil` 16. `(inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))` 17. `dfs(the_obj;s;i) = (s' @ s)` 18. `j:` `Vertices(the_graph)` 19. `(inr(j) s2)` `i-the_graph- > j`	5 steps