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

At: dfs induction4
For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) (k:V. (inr(k) s2) j-the_graph- > *k) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inr(i) s1) (inl(i) s1) paren(V;s2) l_disjoint(V+V;s2;s1) no_repeats(V+V;s2) (j:V. (inr(j) s2) i-the_graph- > *j) (j:V. i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s))
By:
Auto
THEN
Inst Thm* dfs_induction3 [the_graph;the_obj;i,s1,s2. P(i,s1,s2) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j);s;i]
THEN
EasyHyp
Generated subgoals:

11. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. i1: Vertices(the_graph)
11. member-paren(x,y.the_obj.eq(x,y);i1;s1)
P(i1,s1,nil)		1 step
 
21. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. i1: Vertices(the_graph)
11. member-paren(x,y.the_obj.eq(x,y);i1;s1)
l_disjoint(Vertices(the_graph)+Vertices(the_graph);nil;s1)		1 step
 
31. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. i1: Vertices(the_graph)
11. member-paren(x,y.the_obj.eq(x,y);i1;s1)
no_repeats(Vertices(the_graph)+Vertices(the_graph);nil)		1 step
 
41. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. i1: Vertices(the_graph)
11. member-paren(x,y.the_obj.eq(x,y);i1;s1)
paren(Vertices(the_graph);nil)		1 step
 
51. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. i1: Vertices(the_graph)
11. member-paren(x,y.the_obj.eq(x,y);i1;s1)
12. j: Vertices(the_graph)
13. (inr(j) nil)
i1-the_graph- > *j		1 step
 
61. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. s3: traversal(the_graph)
12. i1: Vertices(the_graph)
13. j: Vertices(the_graph)
14. i1-the_graph- > j
15. P(j,s1,s2)
16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
18. paren(Vertices(the_graph);s2)
19. j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > *j@0
20. P(i1,s2 @ s1,s3)
21. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1)
22. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3)
23. paren(Vertices(the_graph);s3)
24. j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > *j
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3 @ s2;s1)		1 step
 
71. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. s3: traversal(the_graph)
12. i1: Vertices(the_graph)
13. j: Vertices(the_graph)
14. i1-the_graph- > j
15. P(j,s1,s2)
16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
18. paren(Vertices(the_graph);s2)
19. j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > *j@0
20. P(i1,s2 @ s1,s3)
21. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1)
22. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3)
23. paren(Vertices(the_graph);s3)
24. j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > *j
no_repeats(Vertices(the_graph)+Vertices(the_graph);s3 @ s2)		1 step
 
81. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. s3: traversal(the_graph)
12. i1: Vertices(the_graph)
13. j: Vertices(the_graph)
14. i1-the_graph- > j
15. P(j,s1,s2)
16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
18. paren(Vertices(the_graph);s2)
19. j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > *j@0
20. P(i1,s2 @ s1,s3)
21. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1)
22. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3)
23. paren(Vertices(the_graph);s3)
24. j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > *j
paren(Vertices(the_graph);s3 @ s2)		1 step
 
91. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. s3: traversal(the_graph)
12. i1: Vertices(the_graph)
13. j: Vertices(the_graph)
14. i1-the_graph- > j
15. P(j,s1,s2)
16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
18. paren(Vertices(the_graph);s2)
19. j@0:Vertices(the_graph). (inr(j@0) s2) j-the_graph- > *j@0
20. P(i1,s2 @ s1,s3)
21. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1)
22. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3)
23. paren(Vertices(the_graph);s3)
24. j:Vertices(the_graph). (inr(j) s3) i1-the_graph- > *j
25. j1: Vertices(the_graph)
26. (inr(j1) s3 @ s2)
i1-the_graph- > *j1		3 steps
 
101. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. i1: Vertices(the_graph)
12. member-paren(x,y.the_obj.eq(x,y);i1;s1)
13. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
14. P(i1,[inr(i1) / s1],s2)
15. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1])
16. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
17. paren(Vertices(the_graph);s2)
18. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
P(i1,s1,[inl(i1) / (s2 @ [inr(i1)])])		7 steps
 
111. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. i1: Vertices(the_graph)
12. member-paren(x,y.the_obj.eq(x,y);i1;s1)
13. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
14. P(i1,[inr(i1) / s1],s2)
15. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1])
16. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
17. paren(Vertices(the_graph);s2)
18. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
l_disjoint(Vertices(the_graph)+Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])];s1)		6 steps
 
121. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. i1: Vertices(the_graph)
12. member-paren(x,y.the_obj.eq(x,y);i1;s1)
13. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
14. P(i1,[inr(i1) / s1],s2)
15. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1])
16. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
17. paren(Vertices(the_graph);s2)
18. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
no_repeats(Vertices(the_graph)+Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])])		7 steps
 
131. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. i1: Vertices(the_graph)
12. member-paren(x,y.the_obj.eq(x,y);i1;s1)
13. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
14. P(i1,[inr(i1) / s1],s2)
15. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1])
16. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
17. paren(Vertices(the_graph);s2)
18. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
paren(Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])])		1 step
 
141. 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) (k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k) 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). (inr(i) s1) (inl(i) s1) paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) (j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. s1: traversal(the_graph)
10. s2: traversal(the_graph)
11. i1: Vertices(the_graph)
12. member-paren(x,y.the_obj.eq(x,y);i1;s1)
13. j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
14. P(i1,[inr(i1) / s1],s2)
15. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1])
16. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
17. paren(Vertices(the_graph);s2)
18. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
19. j: Vertices(the_graph)
20. (inr(j) [inl(i1) / (s2 @ [inr(i1)])])
i1-the_graph- > *j		6 steps

About:
consconsnilassertunioninlinrapplyfunction
equalpropimpliesandorallexists

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