Nuprl - Proof: dfs-properties 2

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

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)

By: Subst (s2 = s') 0

Generated subgoals:

1 s2 = s' 2 steps

2 s2@0:traversal(the_graph). s' = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph) 1 step

About:

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

1	`s2 = s'`	2 steps

2	`s2@0:traversal(the_graph). s' = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph)`	1 step