i,j. (
k
out(i).k=
j))
l:AdjList. adjl_to_adjm(l) AdjMatrix
size
(size List) Typesizesize
Type| Some definitions of interest. | |
| adjl_to_adjm | Def adjl_to_adjm(l) == Case(l) Case mk_adjlist(n; out ) = > mk_adjmatrix(n, i,j. (kout(i).k=j)) |
| Thm* l:AdjList. adjl_to_adjm(l) AdjMatrix | |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| adjmatrix | Def AdjMatrix == size:sizesize |
| Thm* AdjMatrix Type |
About:
 |  |  |  |  |  |
 |  |  |  |  |