is mentioned by

Thm* t:AdjList. t.size	[adjl_size_wf]
Thm* t:AdjMatrix. t.size	[adjm_size_wf]
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]
Def AdjList == size:size(size List)	[adjlist]
Def AdjMatrix == size:sizesize	[adjmatrix]

In prior sections: int 1 bool 1 sqequal 1 int 2 list 1 mb nat mb list 1 num thy 1 mb list 2 graph 1 1 graph 1 2 prog 1

Try larger context: Graphs