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 = ![]() ![]() ![]() ![]() ![]() |
adjlist | Def AdjList == size:![]() ![]() ![]() ![]() ![]() ![]() |
Thm* AdjList ![]() | |
gr_v | Def Vertices(t) == 1of(t) |
Thm* ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() |
![]() |