Nuprl - Proof: dfs accum member 2 1 2 1

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

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. l: Vertices(the_graph) List
4. u: Vertices(the_graph)
5. v: Vertices(the_graph) List
6. s:traversal(the_graph). s':traversal(the_graph). (i:Vertices(the_graph). (i v) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & list_accum(s',j.dfs(the_obj;s';j);s;v) = (s' @ s)
7. s: traversal(the_graph)
8. s1: traversal(the_graph)
9. (inl(u) s1) (inl(u) s) (inr(u) s)
10. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s1;s)
11. no_repeats(Vertices(the_graph)+Vertices(the_graph);s1)
12. paren(Vertices(the_graph);s1)
13. dfs(the_obj;s;u) = (s1 @ s)
14. s': traversal(the_graph)
15. i:Vertices(the_graph). (i v) (inl(i) s') (inl(i) dfs(the_obj;s;u)) (inr(i) dfs(the_obj;s;u))
16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';dfs(the_obj;s;u))
17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s')
18. paren(Vertices(the_graph);s')
19. list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s;u);v) = (s' @ dfs(the_obj;s;u))
20. i: Vertices(the_graph)
21. (i v)
22. (inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s1) (inr(i) s)

(inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s)

By: AssertBY ((inr(i) s1) (inl(i) s1)) (Auto THEN (Inst Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) [Vertices(the_graph);s1;i]))

Generated subgoal:

1 23. (inr(i) s1) (inl(i) s1)
(inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s) 1 step

About:

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