Nuprl - Proof: dfs induction2 6

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

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop
4. s: traversal(the_graph)
5. i: Vertices(the_graph)
6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s) P(i,s,nil)
7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph). i-the_graph- > j paren(Vertices(the_graph);s2) paren(Vertices(the_graph);s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)
8. s1,s2:traversal(the_graph), i:Vertices(the_graph). (inl(i) s1) (inr(i) s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
10. T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
11. T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
12. s1: traversal(the_graph)
13. s2: traversal(the_graph)
14. s3: traversal(the_graph)
15. i1: Vertices(the_graph)
16. j: Vertices(the_graph)
17. i1-the_graph- > j
18. P(j,s1,s2)
19. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
20. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
21. paren(Vertices(the_graph);s2)
22. P(i1,s2 @ s1,s3)
23. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1)
24. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3)
25. paren(Vertices(the_graph);s3)