is mentioned by

Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y x = y	[assert_eq_adjl]
Thm* M:AdjMatrix, x,y:Vertices(adjm-graph(M)). x =M= y x = y	[assert_eq_adjm]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2) l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s1) (j:V. i-the_graph- > j j = i (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction3]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2) l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction]
Thm* For any graph the_obj:GraphObject(the_graph). M:(Traversal). (i:V, s:Traversal. M([inl(i) / s])M(s)) & (i:V, s:Traversal. member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s))	[dfs-measure]
Thm* For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) (x:V. P(x) & Q(x)) vertex-count(the_obj;x.P(x)) < vertex-count(the_obj;x.Q(x))	[vertex-count-less]
Thm* For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) vertex-count(the_obj;x.P(x))vertex-count(the_obj;x.Q(x))	[vertex-count-le]
Thm* For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x))	[vertex-subset-properties]
Thm* For any graph the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y) x = y) & (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L))	[graphobj-properties]
Thm* For any graph eq:(VV), eqw:(x,y:V. eq(x,y) x = y), eacc:(T:Type. (TVT)TVT), eaccw:(T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)), vacc:(T:Type. (TVT)TT), vaccw:(T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L)), other:Top. mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other) GraphObject(the_graph)	[mkgraphobj_wf]
Thm* For any graph t:GraphObject(the_graph). t.eqw (x,y:V. t.eq(x,y) x = y)	[gro_eqw_wf]
Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e >	[adjm-graph]
Def GraphObject(the_graph) == eq:Vertices(the_graph)Vertices(the_graph)(x,y:Vertices(the_graph). (eq(x,y)) x = y)(eacc:(T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top))	[graphobj]

In prior sections: bool 1 list 1 union mb basic mb nat mb list 1 mb list 2 graph 1 1 graph 1 2 rel 1

Try larger context: Graphs