Nuprl - Proof: dfs induction 1 1 1 2 2 1 1

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

At: dfs induction 1 1 1 2 2 1 1

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop
4. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
5. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
6. s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)
7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph). i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)
8. s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. M: traversal(the_graph)
10. i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)
11. i:Vertices(the_graph), s:traversal(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s)
12. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
13. 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)
14. 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)
15. d:
16. d1:. d1 < d (s:traversal(the_graph), i:Vertices(the_graph). M(s)d1 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)))
17. s: traversal(the_graph)
18. i: Vertices(the_graph)
19. M(s)d
20. member-paren(x,y.the_obj.eq(x,y);i;s)
21. L: Vertices(the_graph) List
22. u: Vertices(the_graph)
23. v: Vertices(the_graph) List
24. y:Vertices(the_graph). (y [u / v]) i-the_graph- > y
25. s2:traversal(the_graph). M(s2) < d member-paren(x,y.the_obj.eq(x,y);i;s2) (s':traversal(the_graph). M(s' @ s2)M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');s2;v) = (s' @ s2))
26. s2: traversal(the_graph)
27. M(s2) < d
28. member-paren(x,y.the_obj.eq(x,y);i;s2)
29. s':traversal(the_graph). M(s' @ s2)M(s2) & P(u,s2,s') & dfs(the_obj;s2;u) = (s' @ s2)

s':traversal(the_graph). M(s' @ s2)M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');dfs(the_obj;s2;u);v) = (s' @ s2)

By: ExRepD THEN HypSubst -1 0 THEN InstHyp [s' @ s2] -8

Generated subgoals:

1 29. s': traversal(the_graph)
30. M(s' @ s2)M(s2)
31. P(u,s2,s')
32. dfs(the_obj;s2;u) = (s' @ s2)
member-paren(x,y.the_obj.eq(x,y);i;s' @ s2) 2 steps

2 29. s': traversal(the_graph)
30. M(s' @ s2)M(s2)
31. P(u,s2,s')
32. dfs(the_obj;s2;u) = (s' @ s2)
33. s'@0:traversal(the_graph). M(s'@0 @ s' @ s2)M(s' @ s2) & P(i,s' @ s2,s'@0) & list_accum(s',x'.dfs(the_obj;s';x');s' @ s2;v) = (s'@0 @ s' @ s2)
s'@0:traversal(the_graph). M(s'@0 @ s2)M(s2) & P(i,s2,s'@0) & list_accum(s',x'.dfs(the_obj;s';x');s' @ s2;v) = (s'@0 @ s2) 4 steps

About:

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

1	29. `s':` `traversal(the_graph)` 30. `M(s' @ s2)M(s2)` 31. `P(u,s2,s')` 32. `dfs(the_obj;s2;u) = (s' @ s2)` `member-paren(x,y.the_obj.eq(x,y);i;s' @ s2)`	2 steps

2	29. `s':` `traversal(the_graph)` 30. `M(s' @ s2)M(s2)` 31. `P(u,s2,s')` 32. `dfs(the_obj;s2;u) = (s' @ s2)` 33. `s'@0:traversal(the_graph). M(s'@0 @ s' @ s2)M(s' @ s2) & P(i,s' @ s2,s'@0) & list_accum(s',x'.dfs(the_obj;s';x');s' @ s2;v) = (s'@0 @ s' @ s2)` `s'@0:traversal(the_graph). M(s'@0 @ s2)M(s2) & P(i,s2,s'@0) & list_accum(s',x'.dfs(the_obj;s';x');s' @ s2;v) = (s'@0 @ s2)`	4 steps