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

At: dfs accum member 2
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)
s':traversal(the_graph). (i:Vertices(the_graph). (i [u / 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);dfs(the_obj;s;u);v) = (s' @ s)
By:
Inst Thm* dfs_member [the_graph;the_obj;s;u]
THEN
InstHyp [dfs(the_obj;s;u)] -3
THEN
ExRepD
THEN
HypSubst -1 0
THEN
HypSubst -7 0
THEN
InstConcl [s' @ s1]
Generated subgoals:

18. 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 [u / v])
(inl(i) s' @ s1) (inl(i) s) (inr(i) s)		5 steps
 
28. 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))
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s' @ s1;s)		1 step
 
38. 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))
no_repeats(Vertices(the_graph)+Vertices(the_graph);s' @ s1)		1 step
 
48. 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))
paren(Vertices(the_graph);s' @ s1)		1 step
 
58. 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))
(s' @ s1 @ s) = ((s' @ s1) @ s) traversal(the_graph)		1 step

About:
listconsunioninlinrequal
impliesandorallexists

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