is mentioned by

Thm* A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. no_repeats(Vertices(adjl-graph(A));L) & (y:Vertices(adjl-graph(A)). (y L)) & adjl-vertex-accum(A;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjl-vertex-accum-properties]
Thm* A:AdjList, T:Type, s:T, x:Vertices(adjl-graph(A)), f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. (y:Vertices(adjl-graph(A)). x-adjl-graph(A)- > y (y L)) & adjl-edge-accum(A;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)	[adjl-edge-accum-properties]
Thm* M:AdjMatrix, T:Type, s:T, x:Vertices(adjm-graph(M)), f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. (y:Vertices(adjm-graph(M)). x-adjm-graph(M)- > y (y L)) & adjm-edge-accum(M;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)	[adjm-edge-accum-properties]
Thm* M:AdjMatrix, T:Type, s:T, f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. no_repeats(Vertices(adjm-graph(M));L) & (y:Vertices(adjm-graph(M)). (y L)) & adjm-vertex-accum(M;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjm-vertex-accum-properties]
Thm* For any graph the_obj:GraphObject(the_graph), l:V List, s:Traversal. s':Traversal. (i:V. (i l) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s)	[dfs_accum_member]
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.vaccw (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & t.vacc(f,s) = list_accum(s',x'.f(s',x');s;L))	[gro_vaccw_wf]
Thm* For any graph t:GraphObject(the_graph). t.eaccw (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & t.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))	[gro_eaccw_wf]
Def adjl-edge-accum(A;s',x'.f(s';x');s;x) == list_accum(s',x'.f(s';x');s;A.out(x))	[adjl-edge-accum]
Def dfsl(G;L) == list_accum(s,i.dfs(G;s;i);nil;L)	[dfsl]
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: graph 1 1

Try larger context: Graphs