is mentioned by

Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)	[dfsl-traversal-append]
Thm* For any graph L:V List, i:V, s:Traversal. (inr(i) s) dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inl(i) / s])	[dfl-traversal-consl]
Thm* For any graph L:V List, i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) L-- > *i dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inr(i) / s])	[dfl-traversal-consr]
Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s)	[dfl-traversal-connect]
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 i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;s) df-traversal(the_graph;[inr(i) / s])	[df-traversal-cons2]
Thm* For any graph A,B,C:V List. A-- > *C B-- > *C A @ B-- > *C	[list-list-connect-append2]
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,B:V List. A = B A-- > *B	[list-list-connect_weakening]
Thm* For any graph A,B:V List. B A A-- > *B	[list-list-connect-iseg]
Thm* For any graph A:V List, x:V. A-- > *[x] A-- > *x	[list-list-connect-singleton]
Thm* For any graph A,B,C:V List. A-- > *B B-- > *C A-- > *C	[list-list-connect_transitivity]
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* For any graph p:V List. 1 < ||p|| path(the_graph;p) path(the_graph;tl(p))	[path-tl]
Thm* For any graph x,y:V. x-the_graph- > y x-the_graph- > *y	[edge-connect]
Thm* For any graph x,y:V. x = y x-the_graph- > *y	[connect_weakening]
Thm* For any graph x,y,z:V. x-the_graph- > *y y-the_graph- > *z x-the_graph- > *z	[connect_transitivity]
Thm* For any graph x,y:V. x-the_graph- > *y Prop	[connect_wf]
Thm* t:Graph. Incidence(t) Edges(t)Vertices(t)Vertices(t)	[gr_f_wf]
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 topsorted(the_graph;s) == i,j:Vertices(the_graph). i-the_graph- > *j i = j i before j s	[topsorted]
Def depthfirst-traversal(the_graph;s) == 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) (j:Vertices(the_graph). j = i i-the_graph- > *j (inl(j) s2))	[depthfirst-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 traversal(G) == (Vertices(G)+Vertices(G)) List	[traversal]
Def non-trivial-loop-free(G) == i:Vertices(G). non-trivial-loop(G;i)	[non-trivial-loop-free]
Def non-trivial-loop(G;i) == j:Vertices(G). j = i & i-G- > *j & j-G- > *i	[non-trivial-loop]
Def L1-G- > *L2 == (xL2.L1-G- > *x)	[list-list-connect]
Def L-G- > *x == (yL.y-G- > *x)	[list-connect]
Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y	[connect]
Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y >	[edge]

Try larger context: Graphs