is mentioned by

Thm* For any graph A,B,C:V List. A-- > *B @ C A-- > *B & A-- > *C	[list-list-connect-append]
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* n,k:, c:(nk). p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)	[finite-partition]
Def G H == vmap:(Vertices(G)Vertices(H)), emap:(Edges(G)Edges(H)). Bij(Vertices(G); Vertices(H); vmap) & Bij(Edges(G); Edges(H); emap) & (vmap,vmap) o Incidence(G) = Incidence(H) o emap	[graph-isomorphic]
Def topsortedl(the_graph;L;s) == (i,j:Vertices(the_graph). j = i i-the_graph- > *j i before j s) & (i,j,k:Vertices(the_graph). k-the_graph- > *j k-the_graph- > *i (k':Vertices(the_graph). k' before k L k'-the_graph- > *i) i before j s)	[topsortedl]
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]
Def dfl-traversal(the_graph;L;s) == (i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)) & (j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j) & (i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i)	[dfl-traversal]
Def df-traversal(G;s) == (i:Vertices(G), s1,s2:traversal(G). s = (s1 @ [inr(i)] @ s2) traversal(G) (j:Vertices(G). (inr(j) s2) (inl(j) s2) j-G- > *i)) & (i:Vertices(G), s1,s2:traversal(G). (j:Vertices(G). i-G- > *j non-trivial-loop(G;j)) s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2)))	[df-traversal]
Def non-trivial-loop(G;i) == j:Vertices(G). j = i & i-G- > *j & j-G- > *i	[non-trivial-loop]
Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y	[connect]
Def path(the_graph;p) == 0 < ||p|| & (i:(||p||-1). p[i]-the_graph- > p[(i+1)])	[path]
Def paren(T;s) == s = nil (T+T) List (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. ||s'|| < ||s|| & ||s''|| < ||s|| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive)	[paren]
Def r- > L^k == n:. rn (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))	[arrows]

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

Try larger context: Graphs