t:AdjList. t.out 
t.size
(t.size List)t:AdjList. t.size 
size(size List) Type == {i:
| 0
i } Type| Some definitions of interest. | |
| adjl_out | Def t.out == 2of(t) |
| Thm* t:AdjList. t.out t.size(t.size List) | |
| adjl_size | Def t.size == 1of(t) |
| Thm* t:AdjList. t.size | |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| nat | Def == {i:| 0i } |
| Thm* Type |
About:
 |  |  |  |  |
 |  |  |  |  |