is mentioned by

Thm* R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y))	[rel-graph_functionality]
Thm* For any graph A,B,C:V List. A-- > *B @ C A-- > *B & A-- > *C	[list-list-connect-append]
Thm* For any graph A:V List, x:V. A-- > *[x] A-- > *x	[list-list-connect-singleton]
Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i	[list-connect-append]
Thm* For any graph i,j:V. [i]-- > *j i-the_graph- > *j	[list-connect-singleton]
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* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) s))	[assert-member-left-paren]
Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s))	[assert-member-right-paren]
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))	[assert-member-paren]
Thm* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)	[trivial-arrows]
Thm* x:, n:. (n | x) (x mod n) = 0	[elim_divides]
Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ L2) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j)))))	[dfsl-traversal]

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

Try larger context: Graphs