is mentioned by

Thm* DivGraph_2 Graph	[divides-graph2_wf]
Thm* EquivRel G,H:Graph. G H	[graph-isomorphic-equiv]
Thm* G,H:Graph. G H H G	[graph-isomorphic_inversion]
Thm* G,H,K:Graph. G H H K G K	[graph-isomorphic_transitivity]
Thm* G,H:Graph. G = H G H	[graph-isomorphic_weakening]
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 dfsl-traversal(the_graph;nil;nil)	[dfsl-traversal-nil]
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 df-traversal(the_graph;nil)	[df-traversal-nil]
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. t.o Top	[gr_o_wf]
Thm* t:Graph. Incidence(t) Edges(t)Vertices(t)Vertices(t)	[gr_f_wf]
Thm* t:Graph. Edges(t) Type	[gr_e_wf]
Thm* t:Graph. Vertices(t) Type	[gr_v_wf]

Try larger context: Graphs