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

At: dfs induction4 11
1. 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)
By:
Inst Thm* graphobj-properties [the_graph;the_obj]
THEN
RWO Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s)) -8
THEN
RWO Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a) -5
THEN
RWO Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b) 0
THEN
RWO Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c) 0
THEN
RWO Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b) 0
Generated subgoals:

112. ((inl(i1) s1) (inr(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. (inr(i1) 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:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
20. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
21. 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)
22. 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)
(inl(i1) s1)		2 steps
 
212. ((inl(i1) s1) (inr(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. (inr(i1) 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:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
20. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
21. 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)
22. 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)
(inr(i1) s1)		2 steps
 
312. ((inl(i1) s1) (inr(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. (inr(i1) 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:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
20. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
21. 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)
22. 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)
l_disjoint(Vertices(the_graph)+Vertices(the_graph);nil;s1)		1 step

About:
listconsconsnilboolassertunioninlinrapply
functionuniverseequalpropimpliesandorall
exists

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