is mentioned by

Thm* t:AdjList. t.out t.size(t.size List)	[adjl_out_wf]
Def adjl-vertex-accum(A;s',x.f(s';x);s) == primrec(A.size;s;x,s'. f(s';x))	[adjl-vertex-accum]
Def adjl-graph(G) == < vertices = G.size, edges = x:G.size||G.out(x)||, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > >	[adjl-graph]

Try larger context: Graphs