Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop

s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s) P(i,s,nil)

s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph). i-the_graph- > j paren(Vertices(the_graph);s2) paren(Vertices(the_graph);s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)

s1,s2:traversal(the_graph), i:Vertices(the_graph). (inl(i) s1) (inr(i) s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])

x,y:Vertices(the_graph). the_obj.eq(x,y) x = y

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)

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) (inr(i1) s1))

RWO Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) 0
THEN
Try (RWO Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) 0)
THEN
Try (RWO Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) 0)
THEN
Try (RWO Thm* a,x:T. (x [a]) x = a 0)

1	l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1)])	1 step
2	no_repeats(Vertices(the_graph)+Vertices(the_graph);[inr(i1)])	1 step
3	((inl(i1) s2) inl(i1) = inr(i1) Vertices(the_graph)+Vertices(the_graph))	3 steps

About: