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

s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)

s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)

s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)

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

s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])

traversal(the_graph)

i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)

i:Vertices(the_graph), s:traversal(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s)

d1:. d1 < d (s:traversal(the_graph), i:Vertices(the_graph). M(s)d1 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)))

M(s)d

member-paren(x,y.the_obj.eq(x,y);i;s)

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)

L:Vertices(the_graph) List. (y:Vertices(the_graph). (y L) i-the_graph- > y) (s2:traversal(the_graph). M(s2) < d member-paren(x,y.the_obj.eq(x,y);i;s2) (s':traversal(the_graph). M(s' @ s2)M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');s2;L) = (s' @ s2)))

y:Vertices(the_graph). i-the_graph- > y (y L)

the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L)

M(s' @ [inr(i) / s])M([inr(i) / s])

j = i

(j L)

i@0:Vertices(the_graph). (i@0 L) (inl(i@0) s1) (inl(i@0) [inr(i) / s]) (inr(i@0) [inr(i) / s])

(inl(j) s1)

(inl(j) s')

Inst Thm* x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w [Vertices(the_graph)+Vertices(the_graph);s1;s';[inr(i) / s];[inr(i) / s]]

1	||s1|| = ||s'|| ||[inr(i) / s]|| = ||[inr(i) / s]||	1 step
2	(s1 @ [inr(i) / s]) = (s' @ [inr(i) / s]) (Vertices(the_graph)+Vertices(the_graph)) List	1 step
3	40. s1 = s' (Vertices(the_graph)+Vertices(the_graph)) List 41. [inr(i) / s] = [inr(i) / s] (Vertices(the_graph)+Vertices(the_graph)) List (inl(j) s')	1 step

About: