is mentioned by

Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b))	[fun-graph-rel-graph]
Thm* G:Graph. (x,y:Vertices(G). Dec(x = y)) (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s))	[paren-df-traversal]
Thm* For any graph (x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y))	[connect-iff]
Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s)))	[decidable__l_member_paren]

In prior sections: core int 1 bool 1 int 2 rel 1 num thy 1 mb basic mb nat mb list 1 mb list 2 graph 1 1

Try larger context: Graphs