Definitions graph 1 3 Sections Graphs Doc

Some definitions of interest.
adjl-edge-accum Def adjl-edge-accum(A;s',x'.f(s';x');s;x) == list_accum(s',x'.f(s';x');s;A.out(x))
adjl-graph Def adjl-graph(G) == < vertices = G.size, edges = x:G.size||G.out(x)||, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > >
adjlist Def AdjList == size:size(size List)
Thm* AdjList Type
gr_v Def Vertices(t) == 1of(t)
Thm* t:Graph. Vertices(t) Type

About:
pairproductlistitnatural_numberlambda
applyfunctionuniversememberall
!abstraction

Definitions graph 1 3 Sections Graphs Doc