Nuprl - Proof: dfs-cases 2 1

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

At: dfs-cases 2 1

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
6. 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)
7. 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)
8. ((inl(i) s) (inr(i) s))

L:Vertices(the_graph) List, s:traversal(the_graph). s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;L) = (s2 @ s)

By: InductionOnList THEN Reduce 0

Generated subgoals:

1 9. L: Vertices(the_graph) List
10. s1: traversal(the_graph)
s2:traversal(the_graph). s1 = (s2 @ s1) traversal(the_graph) 1 step

2 9. L: Vertices(the_graph) List
10. u: Vertices(the_graph)
11. v: Vertices(the_graph) List
12. s:traversal(the_graph). s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;v) = (s2 @ s)
13. s1: traversal(the_graph)
s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s1;u);v) = (s2 @ s1) 2 steps

About:

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

1	9. `L:` `Vertices(the_graph) List` 10. `s1:` `traversal(the_graph)` `s2:traversal(the_graph). s1 = (s2 @ s1) traversal(the_graph)`	1 step

2	9. `L:` `Vertices(the_graph) List` 10. `u:` `Vertices(the_graph)` 11. `v:` `Vertices(the_graph) List` 12. `s:traversal(the_graph). s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;v) = (s2 @ s)` 13. `s1:` `traversal(the_graph)` `s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s1;u);v) = (s2 @ s1)`	2 steps